projection bounds sus

https://github.com/compiler-errors/next-solver-hir-issues/issues/1

We have to keep accepting this snippet:

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.
}

status quo on stable

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.

fn next<T>(t: &mut T) -> Option<T::Item>
where
    T: Iterator<Item = <T as Iterator>::Item>,
    // This results in solver overflow.
{
    t.next()
}

As a requirement, 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.

is this unsound

We assume something stronger than what we prove. We assume normalizes-to but only prove alias-eq.

However, in both cases the term is proven to be semantically equal to the term, so this should not be unsound.

other issues

This does break down in this example:

trait WithAssoc {
    type Assoc;
}

trait Trait<U> {
    fn foo()
    where
        Self: WithAssoc<Assoc = U>;
}

impl<T: WithAssoc> Trait<T::Assoc> for T {
    fn foo() {}
}

This overflows while normalizing the param_env in compare_predicate_entailment for foo. The param_env contains a T: WithAssoc<Assoc = T::Assoc> bound which we can prove, but cannot use.

how to deal with this

At its core there are 3 possible ways forward.

1 change goals to be closer to normalizes-to

We could introduce the concept of rigid projections, i.e. <T as Trait>::Assoc normalizes to <T as Trait>::Assoc [rigid]. This would allow this example to compile. It may also avoid the normalization cycle present on stable as T::Assoc could already be a [rigid] associated type here.

trait WithAssoc {
    type Assoc;
}

trait Trait<U> {
    fn foo()
    where
        Self: WithAssoc<Assoc = U>;
}

impl<T: WithAssoc> Trait<T::Assoc> for T {
    fn foo() {}
}

It does add a non-trivial additional amount of complexity to the solver refactor however, so I would like to avoid it if possible.

2 changing assumptions to be closer to alias-eq

This is difficult, as now we can't simply use a projection bound to normalize in this case. We'd have to deal with the possibility of not actually making progress. This feels difficult to implement in nicely.

3 accept the difference between goals and assumptions

Change the new solver to also have the behavior of the old one whereProjection clauses are treated differently, depending on whether they are a goal or an assumption. This is annoying as it means that new solver will also be broken for

trait WithAssoc {
    type Assoc;
}

trait Trait<U> {
    fn foo()
    where
        Self: WithAssoc<Assoc = U>;
}

impl<T: WithAssoc> Trait<T::Assoc> for T {
    fn foo() {}
}

It feels concerning that environments can become broken by substituting a valid instantiation. But given that this is not unsound and avoids any breaking changes, this feels like the easiest path forwards.

how to implement this

It would be nice if predicates and clauses were completely different. With this, we could have fn Predicate::from_clause which maps Clause::Projection to Predicate::AliasRelate. I don't expect that to happen soon and it may also badly impact performance.

Without this we could still add Predicate::NormalizesTo and have the new solver prove Predicate::Projection by emitting Predicate::AliasEq. Predicate::NormalizesTo would still look for Clause::Projection in the environment. This is probably somewhat costly wrt to perf but it may be fine?