chalkify: Implement lowering rule Implied-Bound-From-Trait

[tmandry]

For #49177.

TODO:

• Implement where clauses besides trait and projection predicates
• Is the output of the lower_trait_higher_rank test correct?
• Remove Self::Trait from the query tcx.predicates_of(<trait_id>).predicates
• Consider moving tests to compile-fail to make them more manageable

[tmandry]

r? @nikomatsakis

[scalexm]

What does this comment refer to actually?

[tmandry]

Nothing, I added it by accident!

[scalexm]

So actually the rule we want is FromEnv(WC) :- FromEnv(Self: Trait<P1..Pn>). But there is a slight subtlety: the FromEnv in the left hand side is not exactly a real FromEnv predicate, it's rather some notation (maybe not very appropriate, I agree):

• if WC == TraitRef, then indeed it means FromEnv(TraitRef)
• if WC == ProjectionPredicate, then again it means FromEnv(ProjectionPredicate)
• in any other case, WC is left unchanged, e.g. in the above FromEnv(T: 'a) just means T: 'a
  see this section in the book.

As an example, given this trait:

trait Foo<'a, T> where T: Copy, T: 'a, T: Iterator<Item = i32> { }

we would like the following clauses:

forall<'a, Self, T> {
    FromEnv(T: Copy) :- FromEnv(Self: Foo<'a, T>).
    FromEnv(T: Iterator<Item = i32>) :- FromEnv(Self: Foo<'a, T>).
    (T: 'a) :- FromEnv(Self: Foo<'a, T>).
}

[tmandry]

Oops, I really don't know how I mixed that up >.>

Doing the rest in a match clause really ought to be a matter of using Lower IMO, but right now it eagerly lowers straight to a Goal when DomainGoal is needed. I want to play around with this when I get some time.

[scalexm]

Yeah, I think I'm going to issue a fix for the eager lowering soon, it should benefit the ergonomics of your PR

[scalexm]

As an aside, to avoid writing again code about binders, I'd rather see something like:

impl<'tcx> DomainGoal<'tcx> {
    fn into_from_env_goal(self) -> DomainGoal<'tcx> {
        match self {
            DomainGoal::Holds(wca) => DomainGoal::FromEnv(wca),
            other => other // unchanged
        }
    }
}

then the same thing recursively for Goal:

impl<'tcx> Goal<'tcx> {
    fn into_from_env_goal(self) -> Goal<'tcx> {
        match self {
            Goal::DomainGoal(dg) => Goal::DomainGoal(dg.into_from_env_goal()),
            Goal::Quantified(q, g) => Goal::Quantified(q, g.into_from_env_goal()),
            /* ... */
        }
    }
}

and then you can just do something like:

let predicates = tcx.predicates_of(def_id).predicates.lower();

/* do appropriate things to remove the `Self: Trait` predicate */

let predicates = predicates.into_iter().map(|p| p.into_from_env_goal());

[scalexm]

Actually I was mistaken this would not quite work since we only can have DomainGoal as a consequence. Ok so do as you want 😀

[scalexm]

You might want to keep this comment just above your code which generates the clauses just below.

[scalexm]

The output looks good, just need to change to FromEnv(...) :- FromEnv(Self: Foo<F>) instead of FromEnv(...) :- Implemented(Self: Foo<F>) 😃

[tmandry]

Rebased on #49497 and it definitely makes things nicer! 🏂

Note that the test output for HRTBs changed.

[nikomatsakis]

Blocked on #49497

[scalexm]

I’d like to review one more time once #49497 lands.

[nikomatsakis]

Few nits -- seems roughly right? I've been doing reviews all day though so my "attention to detail" is starting to flag. I'll try and take another look tomorrow.

[nikomatsakis]

I don't understand this comment actually

[tmandry]

Neither do I, honestly. I was tired when I wrote this.

[nikomatsakis]

Can we make where_clause implement LowerFromEnv? So we can just do where_clause.lower_from_env()?

[scalexm]

I was going to suggest, instead of the LowerFromEnv machinery:

trait IntoFromEnvGoal {
    fn into_from_env_goal(self) -> Self;
}

impl<'tcx> IntoFromEnvGoal for DomainGoal<'tcx> {
    fn into_from_env_goal(self) -> DomainGoal<'tcx> { /* ... */ }
}

and then a straightforward:

ProgramClause::ForAll(
    // we might map a dummy binder here, ok for now
    where_clause.lower().map_bound(|goal| ProgramClause {
        goal: goal.into_from_env_goal(),
        hypotheses
    })
)

[tmandry]

Yep, IntoFromEnvGoal turns out to be much simpler. Thanks!

[tmandry]

Changed implementation to use IntoFromEnvGoal as suggested by @scalexm, rebased, and squashed. Also, added some Outlives predicates to the test.

This should be ready, modulo the predicates_of query, which I can do as part of this PR or separately. I'll be working on that this afternoon.

[nikomatsakis]

@bors r+

[bors]

📌 Commit 7ac35ea has been approved by nikomatsakis

[bors]

⌛ Testing commit 7ac35ea with merge a8a8d6b...

[bors]

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