projection normalizes-to mismatch

previous doc: https://hackmd.io/noGGefTfQ0eCARFb3D0tJw

fn next<T: Iterator<Item = U>, U>(t: &mut T) -> Option<U> {
    t.next()
}

fn foo<T: Iterator>(t: &mut T) {
    let _: Option<T::Item> = next(t);
    // `next` here uses `T::Item` for `U` so
    // `normalizes-to` doesn't work.
}

Projection in the environment is treated solely as normalizes-to. We use Projection bounds to normalize without checking whether the term is equal to the associated type. As a goal, Projection can be fulfilled using alias-eq. This means that Projection as an assumption is stronger than what we need to prove when it's used as a requirement.

possible solutions

I believe the only way to solve this in a reasonable timeframe is by actually splitting Projection goals and NormalizesTo.

The question is: how do we prove Projection goals in this case:

Projection tries normalizes-to and uses eq if it fails

This is the behavior of the old solver. It's a bit of a mess for multiple reasons:

• if normalizes-to is ambiguous, we have to detect whether the inference var is still unconstrained or not. If the inference var is still unconstrained, we must not bubble up any inference constraints as we may later want to fall back to eq.
• unclear how to implement eq. Calling eq would just end up at alias-relate. At this point the next alternative may be better

Projection directly equates the types

well, this causes a fun issue

// compile-flags: -Ztrait-solver=next
// check-pass

fn foo(i: isize) -> isize { i + 1 }

fn apply<A, F>(f: F, v: A) -> A where F: FnOnce(A) -> A { f(v) }

pub fn main() {
    let f = |i| foo(i);
    assert_eq!(apply(f, 2), 3);
}

a minimized version:

trait Trait {
    type Assoc;
}

impl<T> Trait for T {
    type Assoc = T;
}

fn impls_trait<T: Trait<Assoc = T>>() -> T {
    todo!()
}

fn main() {
    let _: u32 = impls_trait::<_>();
    //~^ ERROR type mismatch resolving `<_ as Trait>::Assoc == _`
    //~^ NOTE cyclic type of infinite size
}

impls_trait<?0> requires proving Projection(<?0 as Trait>::Assoc, ?0), equating the projection and the inference variable results in an occurs check failure. This requires some changes to generalization.

Another issue which is more frequent due to Projection now simply equating types:

trait Trait<'a> {
    type Assoc;
}
fn foo<'a, T: Trait<'a, Assoc = U>, U>() {}
fn main() {
    foo::<_, _>();
}

This test now triggers the "unstable query result" warning. We start with Projection(<?0 as Trait<&'1>::Assoc, ?2), this returns YES: ?1 = <?0 as Trait<&'1>::Assoc, reproving Projection(<?0 as Trait<&'1>::Assoc, <?0 as Trait<&'1>::Assoc) requires Projection(<?0 as Trait<&'1>::Assoc, <?0 as Trait<&'2>::Assoc) due to uniquification, which is ambiguous.

generalization uwu

Generalization is generally broken when dealing with aliases and higher ranked types^[1].

The issues with with generalizating aliases can mostly be summarized as: generalizing an inference variable to an alias is pretty much always wrong as it does not consider the option to first normalize the alias instead. It is also broken if the projection contains bound variables, which we should delay until later.

A minimal fix

Inside of the generalizer, stop generalizing projections, replace them with inference variables. When relating an inference variable with a projection directly, generalize, if there is an occurs check failure, emit a NormalizesTo goal instead.

This is not a great fix:

• the occurs check failure may be in a nested projection ?x == Alias<<?x as ToUnit>::Assoc. We would be able to constrain ?x to Alias<()> here.
• it means that subtyping for projections is still incorrect

notes from 2023-10-23

Adding to this issue

for<'a> fn(<<?x as OtherTrait>::Assoc as Trait<'a>>::Assoc) eq ?x

?x could be set to for<'a> fn(<T as Trait<'a>>::Assoc) which would then
pass the occurs check and equate successfully.

We must not replace <<?x as OtherTrait>::Assoc as Trait<'a>>::Assoc with an inference variable as that variable is unable to name 'a.

how Niko expects the "theoretically perfect" rules to look is that you can normalize at any point, kind of like this…

?X does not occur in Y
----------------------
Env |- ?X = Y : C[?X := Y]

Y normalizes-to Y'
Env |- ?X = Y' : C
----------------------
Env |- ?X = Y : C

----------------------
Env |- T normalizes-to T


impl { type Alias = T }
----------------------
Env |- Alias[P*] normalizes-to T


Env |- Pi normalizes-to Qi
----------------------
Env |- Ty[P0..Pn] normalizes-to Ty[P0...Qi...Pn]

In cases where normalization fails, we could make the solver return "P = Q if P = Q", which effectively means "ambiguous normalization". When proving a binder, if the returned goals include 'a, then we can return that the binder must be equal.

Ideally we show that the "best" path through those rules above is to always normalize as much as we can (sound/complete)