fallback clauses considered harmful / how to handle projection equality

[nikomatsakis]

In working on #73, I encountered a problem with the concept of a "fallback clause", which is currently a key part of how we handle normalization. The idea of a fallback clause is that it is a clause that we use if no other clauses apply. That seems fine but it's actually too weak: we wind up coming up with "unique" solutions that are not in fact unique.

Consider this example:

trait Iterator { type Item; }
struct Foo { }
struct Vec<T> { }
a

and this goal:

forall<T> {
    if (T: Iterator) {
        exists<U> {
            exists<V> {
                U: Iterator<Item = V>
}   }   }   }

Here, there are two values for U and V:

• exists<W> { U = Vec<W>, V = W }
• U = T, V = T::Item

However, our current system will select the first one and be satisfied. This is because the second one is considered a "fallback" option, and hence since the first one is satisfied, it never gets considered. This is not true of the SLG solver, since I never could figure out how to integrate fallback into that solver -- for good reasons, I think.

I have a branch de-fallback that adresses this problem by removing the notion of fallback clauses. Instead, we have a new domain goal, "projection equality", which replaces normalization in a way (though normalization, as we will see, plays a role). When we attempt to unify two types T and U where at least one of those types is a projection, we "rewrite" to projection equality (really, we could rewrite all of unification into clauses, but I chose the more limited path here, since otherwise we'd have to handle higher-ranked types and substitution in the logic code).

Projection equality is defined by two clauses per associated item, which are defined when lowering the trait (well, when lowering the declaration of the associated item found in the trait). The first clause is what we used to call the "fallback" rule, basically covering the "skolemized" case:

forall<T> {
    ProjectionEq(<T as Iterator>::Item = (Iterator::Item)<T>)
}

The second clause uses a revised concept of normalization. Normalization in this setup is limited to applying an impl to rewrite a projection to the type found in the impl (whereas before it included the fallback case):

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

Both of these rules are created when lowering the trait. When lowering the impl, we would make a rule like:

forall<T> {
    Normalizes(<Vec<T> as Iterator>::Item -> T) :-
        (Vec<T>: Iterator).
}

This all seems to work pretty well. Note that ProjectionEq can never "guess" the right hand side unless normalization is impossible: that is exists<X> { ProjectionEq(<Vec<i32> as Iterator>::Item = X) } is still ambiguous. But if you want to force normalize, you can use the Normalizes relation (which would only be defined, in that example, wen X = i32).

However, the tests are currently failing because we are running into problems with the implied bounds elaborations and the limitations of the recursive solver. (The SLG solver handles it fine.) In particular, there is a rule that looks something like this:

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

This is basically saying, if we know (somehow) that T::Item is equal to U, then we know that T must implement Iterator. It's reasonable, but it winds up causing us a problem. This is because, in the recursive solver, when we are doing normalization, we apply the normalization clause cited above, and then must prove that (Vec<T>: Iterator). To do that, we turn to our full set of clauses, which includes a clause from the impl (which is the right one) and the clause above. The reverse elaboration clause always yields ambiguous -- this is because there is no unique answer to ProjectionEq, and U is unconstrained.

I'm not 100% sure how to resolve this problem right now, so I thought I'd open the issue for a bit of discussion.

cc @scalexm @aturon

[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.