Weird bug around projections

[scalexm]

Given the following traits:

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

and the following goal:

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

we give No solution whereas this should be Unique. Note that if we remove the generic parameter from Item, this works fine.

Basically at some point, the projection type <T as Foo>::Item<U> fails to unify with the skolemized type, as we can see in the debug log:

| resolvent_clause(
:     goal=ProjectionEq(<!1 as Foo>::Item<!2> = (Foo::Item)<?0, !1>),
:     clause=ForAll(for<type, type> ProgramClauseImplication { consequence: ProjectionEq(<?1 as Foo>::Item<?0> = (Foo::Item)<?0, ?1>), conditions: [] })) {
: | instantiate(arg=ProgramClauseImplication { consequence: ProjectionEq(<?1 as Foo>::Item<?0> = (Foo::Item)<?0, ?1>), conditions: [] })
: | new_variable: var=?1 ui=U2
: | new_variable: var=?2 ui=U2
: | instantiate: vars=[?1, ?2]
: | consequence = ProjectionEq(<?2 as Foo>::Item<?1> = (Foo::Item)<?1, ?2>)
: | conditions = []
: | unify(a=ProjectionEq(<!1 as Foo>::Item<!2> = (Foo::Item)<?0, !1>),
: :       b=ProjectionEq(<?2 as Foo>::Item<?1> = (Foo::Item)<?1, ?2>)) {
: : | unify_ty_ty(a=!2,
: : :             b=?1) {
: : : | unify_var_ty(var=?1, ty=!2)
: : : | unify_var_ty: var ?1 set to !2
: : | }
: : | unify_ty_ty(a=!1,
: : :             b=?2) {
: : : | unify_var_ty(var=?2, ty=!1)
: : : | unify_var_ty: var ?2 set to !1
: : | }
: : | unify_ty_ty(a=(Foo::Item)<?0, !1>,
: : :             b=(Foo::Item)<?1, ?2>) {
: : : | unify_ty_ty(a=?0,
: : : :             b=!2) {
: : : : | unify_var_ty(var=?0, ty=!2)
: : : | }
: : | }
: | }
| }

Note that the following answers Unique as expected:

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

cc @nikomatsakis

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