# 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 :sparkles:

// 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](https://github.com/rust-lang/trait-system-refactor-initiative/issues/8) 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

[^1]: &nbsp; `for<'a> fn(&'a ()) <: ?0` sets `?0` to `for<'a> fn(&'a ())` even though it could also be `fn(&'whatever ())`.

### notes from 2023-10-23

Adding to [this issue](https://github.com/rust-lang/trait-system-refactor-initiative/issues/8)

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)