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