Implement Chalk lowering rule Normalize-From-Impl

[fanzier]

This extends the Chalk lowering pass with the "Normalize-From-Impl" rule for generating program clauses from a trait definition as part of #49177.

r? @nikomatsakis

[fanzier]

Note that this is my first real rustc contribution. So if I'm doing things wrong, let me know!

Also I wasn't sure how to test where clauses for associated types (WC1 in the rule). It seems like this (and GATs in general) are not fully implemented yet?

[nikomatsakis]

@fanzier

Note that this is my first real rustc contribution. So if I'm doing things wrong, let me know!

Welcome! Sorry for me being slow! Still catching up from Rust All Hands.

[nikomatsakis]

@fanzier

Also I wasn't sure how to test where clauses for associated types (WC1 in the rule). It seems like this (and GATs in general) are not fully implemented yet?

Yep. Still a WIP.

[nikomatsakis]

Looks good! One nit.

[nikomatsakis]

Nit: can we make this for_associated_type_value or impl_item, something like that?

[fanzier]

Good point, changed it to type_value.

[TimNN]

Your PR failed on Travis. Through arcane magic we have determined that the following fragments from the build log may contain information about the problem.

Click to expand the log.

Resolving deltas: 100% (611592/611592), completed with 4857 local objects.
---
[00:00:55] configure: rust.quiet-tests := True
---
$ find $HOME/Library/Logs/DiagnosticReports -type f -name '*.crash' -not -name '*.stage2-*.crash' -not -name 'com.apple.CoreSimulator.CoreSimulatorService-*.crash' -exec printf travis_fold":start:crashlog\n\033[31;1m%s\033[0m\n" {} \; -exec head -750 {} \; -exec echo travis_fold":"end:crashlog \; || true
find: `/home/travis/Library/Logs/DiagnosticReports': No such file or directory
travis_time:end:046c5333:start=1523061092073389157,finish=1523061092080636946,duration=7247789
travis_fold:end:after_failure.3
travis_fold:start:after_failure.4
travis_time:start:22b74af9
$ dmesg | grep -i kill
[ 10.964306] init: failsafe main process (1092) killed by TERM signal

I'm a bot! I can only do what humans tell me to, so if this was not helpful or you have suggestions for improvements, please ping or otherwise contact @TimNN.

[fanzier]

The Travis failure seems to be spurious.

[nikomatsakis]

@bors r+

[bors]

📌 Commit 2a18fdc has been approved by nikomatsakis

[kennytm]

@bors r-

The log bot is still being tested, so don't rely entirely on it yet. The Travis failure is legit.

[00:23:22] Compiling rustc_traits v0.0.0 (file:///checkout/src/librustc_traits)
[00:23:23] error[E0061]: this function takes 1 parameter but 2 parameters were supplied
[00:23:23] --> librustc_traits/lowering.rs:226:18
[00:23:23] |
[00:23:23] 226 | let clause = Clause::Implies(where_clauses, normalize_goal);
[00:23:23] | ^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^ expected 1 parameter
[00:23:23] [00:23:23] error: aborting due to previous error
[00:23:23] [00:23:23] error: Could not compile `rustc_traits`.

[scalexm]

Apart from the travis failure, seems mostly good, but there are some things which I think are not necessary, like adding the where clauses of the impl in the right hand side of Normalize(...) :- .... Anyway the PR introduces the Normalize domain goal, which was missing, so this is cool.

As for other rules related to associated types, I'd prefer to start by implementing all of them in chalk (not done yet, but they are fully described here ), and we'll probably revisit the rules in rustc one this has been done and proof tested in chalk.

[fanzier]

@kennytm Good to know. I rebased and updated the code.

@scalexm I implemented the rule from the rustc guide (https://rust-lang-nursery.github.io/rustc-guide/traits-lowering-rules.html#lowering-impl-items). If I'm understanding you correctly, you're saying that the WC part of WC && WC1 is unnecessary. But if WC is not satisfied then the associated type doesn't exist because the trait is not implemented. What am I missing here?

[scalexm]

@fanzier the rustc guide is not entirely up to date when it comes to associated types (especially because the rules have not been fully implemented and tested in chalk yet). I’m not sure yet if we want to assert that the trait is implemented in the Normalize predicate or somewhere else (especially because these where clauses have already been proved when typechecking the whole impl block). Anyway, let’s assume that we we would want this assertion in the Normalize predicate: then in that case, it would be better to have:

Normalize(<T as Trait>::AssocType -> U) :- Implemented(T: Foo) && WC1

rather than rewriting all the where clauses denoted by WC, i.e. we would juste « factorize » the where clauses into Implemented(T: Foo). I hope this makes sense :)

[fanzier]

@scalexm Thanks for the explanation, that makes sense. I'll change it as you suggested.

[nikomatsakis]

@bors delegate=scalexm

[bors]

✌️ @scalexm can now approve this pull request

[kennytm]

@bors retry rollup

[kennytm]

@bors r- rollup-

Unfortunately #49800 has changed some types and caused this PR to fail. See #49939 (comment) for error log.

[fanzier]

Can someone please approve this again? I only rebased and made it compile.

[scalexm]

@bors r+

[bors]

📌 Commit b7c4a57 has been approved by scalexm

[bors]

⌛ Testing commit b7c4a57 with merge d703622...

[bors]

☀️ Test successful - status-appveyor, status-travis
Approved by: scalexm
Pushing d703622 to master...