Weird bug around projections about chalk

[scalexm]

It seems related to the fact that U is unused when proving <T as Foo>::Item<U>: Bar. For example, the following goal answers Unique as expected:

trait Bar<T> { }
trait Foo { type Item<T>: Bar<T>; }

forall<T, U> {
    if (T: Foo) {
        <T as Foo>::Item<U>: Bar<U>
    }
}

Also, considering these lines:
https://github.com/rust-lang-nursery/chalk/blob/d67e5691557b09cfd725d18895c436b3c5f12dbf/src/ir.rs#L369-L380

if I change the Ty::Projection to the skolemized type, I also get No solution for the goal cited above:

forall<T, U, V> {
    if (T: Foo<Item<U> = V>) {
        V: Bar
    }
}

so it seems to be linked with the skolemized type.

[scalexm]

Ok the funny thing is that this goal:

forall<U, T> {
    if (T: Foo) {
        <T as Foo>::Item<U>: Bar
    }
}

(note that T and U are reversed) answers Unique =)

Basically, in the setting described in my first comment, we are looking for a type ?0 which satisfies:

ProjectionEq(<!1 as Foo>::Item<!2> = (Foo::Item)<?0, !1>)

so ?0 gets to unify with !2 but the problem is that ?0 is in universe U1 so it fails... Hence if the variables are reversed, this works. I don't really know what to think about this.

[nikomatsakis]

OK, let me try to spell out what is happening. I see the problem that @scalexm specified:

• we start out wanting to solve !1: Foo => <?0 as Bar>::Item<?1> = ?2, ?2: Bar
• we go seeking a solution to !1: Foo => ?0: Foo
  • this is u-canonicalized to have ?0 in U1, since U2 is not relevant
  • u_canonicalization puts ?0 into U1, since that is the maximal universe we can see
  • we then unify it with ?0 with the skolemized result; this includes a free existential variable, whch winds up in U1
• when this result is re-instantiated in the, it keeps this universe.

I think this last step is in error. I think when we re-instantiate an answer, we should create its variables in the most recent universe within the caller.

[nikomatsakis]

I have a branch (issue-144) that fixes the test, but I'm not sure it's totally the right fix overall. It instantiates existentials in the context of their caller; this seems fine for the goals, but I'm a bit nervous about it with respect to region constraints. I'll have to see if I can craft a counter example.

[nikomatsakis]

@scalexm and I were talking about the bug that I am afraid in #wg-traits on Discord (GUID b713dffa-1603-43c9-8418-3dc11979487c, that marks the end).

UPDATE: link to Discord

[krk]

This can no longer be reproduced with ef45646:

?- forall<T, U> { if (T: Foo) { <T as Foo>::Item<U>: Bar } }
Unique; substitution [], lifetime constraints []