generalization is incomplete for aliases

[lcnr]

when generalizing a projection we have to be careful. We're using ?ident.universe for inference variables in a given universe.

given that this is already an issue in on stable we could add a test for this and stabilize even with this incompleteness.

1. ?x sub <() as Trait<?y>>::Assoc

must not generalize ?x to <() as Trait<?y>>::Assoc as ?x may get inferred to a subtype of the normalized projection. Otherwise this would be incomplete. Should emit AliasRelate in this case instead. example

2. ?x eq <?x as Trait>::Assoc ✔️

this must not result in a universe error as the alias may be normalized to ?x. rust-lang/rust#105787

3. ?x eq <<T as Id<?x>>::Id as Unnormalizable>::Assoc

This may hold, as ?x can be constrained to <T as Unnormalizable>::Assoc: example. We cannot simply emit a NormalizesTo goal if equating fails the occurs check, as we could also normalize a nested projection instead.

4. ?x.0 eq <() as Trait<?y.1>>::Assoc

This must not generalize ?x.0 to <() as Trait<?z.1>>::Assoc because that should result in a universe error but it must also not relate it to <() as Trait<?z.0>>::Assoc because the projection may not actually normalize to a type mentioning z so if we then equate the substs in AliasRelate we end up pulling down the universe of ?y to 0 as well which would be incomplete. Should instead emit AliasRelate(?x.0, <() as Trait<?y.1>>::Assoc, Equate).

5. <?x.1 as Trait>::Assoc eq ?y.0

Roughly the same setup as the previous issue but with a different potential unsoundness.

If we generalize ?y.0 to <?z.0 as Trait<'a>>::Assoc (the self ty ending up in a lower universe than ?x.1) this is potentially incomplete if we have a param env candidate such as !T.1: Trait and no other candidates for proving Trait as we would consider ourselves unable to normalize <?z.0 as Trait>::Assoc as ?z.0 eq !T.1 would give a universe error and we would return NoSolution. This is wrong if the assoc type does not actually mention the placeholder as we would be able to instantiate ?y.0 with the assoc type's normalized form.

This could likely only occur with non_lifetime_binders that support where clauses and it would also likely have to be slighltly more complex of a reproduction to workaround the fact that ?0: Trait are always ambiguous.

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

TODO: explain why this is an issue

7. for<'a> fn(<?0.0 as Trait<'a, ?2.1>>::Assoc) eq ?1.0

• We cannot just return a universe error here as <?0.0 as Trait<'a, ?2.1>>::Assoc may normalize to something that does not name the placeholder in a higher universe than ?1.0. This would then be unsound in coherence as we are erroring when there is nothing actually wrong.
• For reasons listed in previous headers we cannot generalize ?1.0 to for<'a> fn(<?0.0 as Trait<'a, ?3.0>>::Assoc)
• We can't generalize ?1.0 to fn(?3.0) with an obligation to prove alias-relate(<?0.0 as Trait<'^0_0, ?2.1>>::Assoc, eq, ?3.0).
  • Escaping bound vars bad actually
• We can't generalize ?1.0 to fn(?4.0) and enter the binder and emit an alias-relate(<?0.0 as Trait<!3.2, ?2.1>>::Assoc, eq, ?4.0).
  • ?4.0 could not be instantiated with something containing the !3.2 placeholder even though we would like to end up with ?1.0 potentially being able to be resolved to something like for<'a> fn(&'a u32)
  • Even if ?4.0 could somehow be instantiated with something containing !3.2 we would have no way of converting that placeholder back into a bound var for the original fn(?4.0)

Solutions:

• We could generalize entire type with the binder to an infer var, instead of just the projection, this would result in generalizing for<'a> fn(<?0.0 as Trait<'a>>::Assoc) to ?2.0 and emitting a relate(for<'a> fn(<?0.0 as Trait<'a>>::Assoc, eq, ?2.0) obligation and instantiating ?1.0 with ?2.0.
  • This has the potential to block type inference in undesirable ways that may be too backwards incompatible to justify.
• Another another potential solution may be to implement HKT(?) so that we can generalize for<'a> fn(?0.0 as Trait<'a>>::Assoc) to for<'a> fn(?2.0<'a>) and instantiate ?1.0 with that, while emitting an obligation for<'a> alias-relate(<?0.0 as Trait<'a>>::Assoc, eq, ?2.0<'a>).
  • This is probably a lot of work and annoying to do just to solve some (probably?) niche unsoundness
• Make universe errors downgrade to ambiguity instead of NoSolution during coherence as it does not matter if we are incomplete during hir typeck.
  • This will result in coherence not being able to use universe errors as a way of telling that impls do not overlap. This is currently a future compat lint but it triggers on code patterns we would ideally like to accept.
• Generalize the alias to an AliasKind::Ambiguous in coherence, which will result in ambiguity when attempting to prove goals involving it

---

There have been various large comments on PRs about soundness of generalization: one, two