Normalization doesn't take into account which impl actually applied

[flodiebold]

Split off from #234:

#[test]
fn normalize_into_iterator() {
    test! {
        program {
            trait IntoIterator { type Item; }
            trait Iterator { type Item; }
            struct Vec<T> { }
            struct u32 { }
            impl<T> IntoIterator for Vec<T> {
                type Item = T;
            }
            impl<T> IntoIterator for T where T: Iterator {
                type Item = <T as Iterator>::Item;
            }
        }

        goal {
            forall<T> {
                exists<U> {
                    Normalize(<Vec<T> as IntoIterator>::Item -> U)
                }
            }
        } yields {
            "Unique"
        }
    }
}

I'd expect this test to pass because the second IntoIterator impl should not have any effect at all here, but the result is instead ambiguous, because apparently the Normalize rule from the second impl applies too, because it just checks that the type implements IntoIterator, and not that it does so with that impl. That seems really wrong.

Niko:

We wind up with these two program clauses:

for<type> Normalize(<Vec<^0> as IntoIterator>::Item -> ^0) :- 
    Implemented(Vec<^0>: IntoIterator)

for<type> Normalize(<^0 as IntoIterator>::Item -> <^0 as Iterator>::Item) :- 
    Implemented(^0: IntoIterator)

I think what I'd expect is something like

for<type> Normalize(<Vec<^0> as IntoIterator>::Item -> ^0)

for<type> Normalize(<^0 as IntoIterator>::Item -> <^0 as Iterator>::Item) :- 
    Implemented(^0: Iterator)

In particular, inlining the where-clauses and conditions of the impl into the rule. @scalexm -- do you recall why we set things up the way we did?

scalexm:

I don’t think there’s any good reason why the where clauses are not inlined.
I probably thought it was equivalent because there would be a « perfect match » with the impl, but of course two impls can have a non-empty intersection with respect to their receiver type.