fallback clauses considered harmful / how to handle projection equality about chalk

[nikomatsakis]

I am reminded that what I have really wanted to do for some time is to handle projection equality during lowering. Specifically, I'd like to lower an impl like this:

impl<T: Iterator> Foo<T> for <T as Iterator>::Item {
}

to a clause like this:

forall<T, U> {
    (U: Foo<T>) :-
        T: Iterator,
        ProjectionEq(<U as Iterator>::Item = U)
}

right now, we detect this "dynamically" by rewriting equalities between projections as we unify. I'd prefer for unification to be simple. This keeps the solvers simple.

The main reason I've not pursued this transformation is that it will require us to deal with higher-ranked types and their instantiation. For example, how do we deal with for<'a> fn(<Slice<'a, T> as Iterator>::Item) unifying with (say) for<'b> fn(&'b T)? Currently, we will (during unification) perform the substitutions. In Lambda Prolog, it could be coded into rules because substitution is a first-class thing. But so far we've not had this in Chalk.

One side effect though of the current setup is that the SLG solver can't handle unifications of the form <T as Iterator>::Item = <T as Iterator>::Item. What winds up happening is that when we produce an answer, we try to unify the resulting goal with the original goal, which creates a fresh goal, etc. We could maybe sidestep this by not unifying answers with goals (substitution would seem to be more efficient anyway), but it's not completely trivial to do thanks to truncation. Probably still possible. But feels like not the right thing to me.

[nikomatsakis]

OK, I fixed the problem with the SLG solver. Instead of unifying the "pending goal" with the result from a query, we now take the values directly from the answer substitute and substitute them into the pending goal. This is more efficient to boot.

[nikomatsakis]

I also fixed the problem with the recursive solver by changing how we elaborate, which is kind of hacky but then again implied bounds need some care anyhow.