Incompleteness via bidirectional normalizes-to

[compiler-errors]

We assemble three candidates for alias-relate goals -- normalizes-to-lhs and normalizes-to-rhs goals (assembling a projection goal for each side of the relation if it's an alias), and a subst-relate goal where we structurally relate aliases if they're both aliases of the same def-id.

Sometimes we get into the case where the choice of normalizes-to branch in alias-relate are both valid, but we cannot make a choice of which one to take because they are different -- either returning equivalent but permuted region constraints, or equivalent opaque type definitions but differing modulo normalization.

a TAIT example

type Tait = impl Iterator<Item = impl Sized>;

fn mk<T>() -> T { todo!() }

fn a() {
    let x: Tait = mk();
    let mut array = mk();
    let mut z = IntoIterator::into_iter(array);
    z = x;
    array = [0i32; 32];
}

Which fails with:

error[E0284]: type annotations needed: cannot satisfy `Tait <: <[i32; 32] as IntoIterator>::IntoIter`
  --> <source>:11:9
   |
11 |     z = x;
   |         ^ cannot satisfy `Tait <: <[i32; 32] as IntoIterator>::IntoIter`

Consider this failing goal: AliasRelate(Tait, <[i32; 32] as IntoIterator>::IntoIter).

As mentioned above, we have three different candidates to satisfy this goal:

1. subst-relate: fails because we can't directly equate the substs of different alias kinds.
2. normalizes-to-rhs: Tait normalizes-to <[i32; 32] as IntoIterator>::IntoIter
   • Ends up infering opaque definition - Tait := <[i32; 32] as IntoIterator>::IntoIter
3. normalizes-to-lhs: <[i32; 32] as IntoIterator>::IntoIter normalizes-to Tait
   • Find impl candidate, substitute the associated type - std::array::IntoIter<i32, 32>
   • Equate std::array::IntoIter<i32, 32> and Tait
     • Ends up infering opaque definition - Tait := std::array::IntoIter<i32, 32>

The problem here is that (2.) and (3.) are equally valid and also essentially equivalent, since we have aliases that normalize on both sides, but due to lazy norm, they end up inferring different opaque type definitions that are only equal after normalizing them further.

an RPIT example

This isn't limited to TAITs, and this can be adapted to RPITs too:

fn test() -> impl Iterator<Item = impl Sized> {
    IntoIterator::into_iter([0i32; 32])
}

Failing similarly with:

error[E0284]: type annotations needed: cannot satisfy `<[i32; 32] as IntoIterator>::IntoIter <: impl Iterator<Item = impl Sized>`
 --> <source>:2:5
  |
2 |     IntoIterator::into_iter([0i32; 32])
  |     ^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^ cannot satisfy `<[i32; 32] as IntoIterator>::IntoIter <: impl Iterator<Item = impl Sized>`

Solution(s)

Fall back to the intersection of both normalizes-to goals

we can make progress by considering a fourth candidate where we compute both normalizes-to branches together and canonicalize that as a response. This is essentially the AND intersection of both normalizes-to branches. In an ideal world, we'd be returning something more like the OR intersection of both branches, but we have no way of representing that either for regions (maybe eventually) or opaques (don't see that happening ever).

An attempt to fix this is open in rust-lang/rust#112076.

Eagerly normalize opaque type responses

Most of the easily constructible examples of this issue happening are due to opaque type responses. We could instead eagerly normalize opaque types in query responses so that try_merge_responses are more likely to succeed due to being identical responses.

Only combine responses if they're equal "modulo opaque types", and combine those

Same as the first proposed solution, but only being applied when responses differ in their opaque types.

Thoughts

This incompleteness seems to be a consequence of lazy norm and the current opaque type inference strategy, but I guess I could see it being weakened to only apply when opaque type inference is involved to avoid its fallout. Since we currently prefer subst-relate candidates in alias-relate ambiguity [todo issue], it's particularly difficult to construct a case where we need this for projections.

[BoxyUwU]

either returning equivalent but permuted region constraints

do you have an example for this?

[compiler-errors]

@BoxyUwU: yes I believe this reproduces the issue

trait Foo {
    type Assoc;
    fn mk(self) -> Self::Assoc;
}

impl Foo for &i32 {
    type Assoc = i32;
    fn mk(self) -> Self::Assoc { 0 }
}

// This impl candidate doesn't matter, we just must not be able to
// eagerly choose a candidate given a self type like `&?0`.
impl Foo for &() {
    type Assoc = ();
    fn mk(self) -> Self::Assoc { }
}

trait Foo2 {
    type Assoc;
    fn mk2(self) -> Self::Assoc;
}

impl Foo2 for &u32 {
    type Assoc = i32;
    fn mk2(self) -> Self::Assoc { 0 }
}

// This impl candidate doesn't matter, we just must not be able to
// eagerly choose a candidate given a self type like `&?0`.
impl Foo2 for &() {
    type Assoc = i32;
    fn mk2(self) -> Self::Assoc { 0 }
}

fn main() {
    let mut i = Default::default();
    let mut x = Foo::mk(&i);
    
    let mut j = Default::default();
    x = Foo2::mk2(&j);
    
    i = 1i32;
    j = 2u32;

    // This sets up a goal like `<&u32 as Foo2>::Assoc <: <&i32 as Foo>::Assoc`
    // Due to eager norm in HIR typeck still existing, we must do it this way,
    // first constructing the alias-relate then filling in the self types later.
}

Evaluating either normalizes-to branch changes the order that we evaluate the impl candidates, which gives us different regions in the response.

Fails with:

error[E0284]: type annotations needed: cannot satisfy `<&u32 as Foo2>::Assoc <: <&i32 as Foo>::Assoc`
  --> /home/gh-compiler-errors/test.rs:40:9
   |
40 |     x = Foo2::mk2(&j);
   |         ^^^^^^^^^^^^^ cannot satisfy `<&u32 as Foo2>::Assoc <: <&i32 as Foo>::Assoc`

[lcnr]

https://github.com/rust-lang/rust/blob/d4ba2b4c7c938cf90c03a265cb31356537f608ad/compiler/rustc_trait_selection/src/solve/alias_relate.rs#L89-L112C1

looking at the impl, this is incomplete if both projections are currently ambiguous to normalize but will end up being rigid. Want to write an test for that at some point, I don't think this is a big issue but I do remember us assuming that this is not an 'actual' incompleteness.

[BoxyUwU]

with rust-lang/rust#117278 landed is this issue now obsolete, afaict there's no matching on solver mode in compute_alias_relate_goal anymore?