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
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.0could 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
when generalizing a projection we have to be careful. We're using
?ident.universefor 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.
?xsub<() as Trait<?y>>::Assocmust not generalize
?xto<() as Trait<?y>>::Assocas?xmay get inferred to a subtype of the normalized projection. Otherwise this would be incomplete. Should emitAliasRelatein this case instead. example2.
?xeq<?x as Trait>::Assoc:heavy_check_mark:this must not result in a universe error as the alias may be normalized to
?x. https://github.com/rust-lang/rust/issues/1057873.
?xeq<<T as Id<?x>>::Id as Unnormalizable>::AssocThis may hold, as
?xcan be constrained to<T as Unnormalizable>::Assoc: example. We cannot simply emit aNormalizesTogoal if equating fails the occurs check, as we could also normalize a nested projection instead.4.
?x.0eq<() as Trait<?y.1>>::AssocThis must not generalize
?x.0to<() as Trait<?z.1>>::Assocbecause that should result in a universe error but it must also not relate it to<() as Trait<?z.0>>::Assocbecause the projection may not actually normalize to a type mentioningzso if we then equate the substs inAliasRelatewe end up pulling down the universe of?yto0as well which would be incomplete. Should instead emitAliasRelate(?x.0, <() as Trait<?y.1>>::Assoc, Equate).5.
<?x.1 as Trait>::Assoceq?y.0Roughly the same setup as the previous issue but with a different potential unsoundness.
If we generalize
?y.0to<?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: Traitand no other candidates for provingTraitas we would consider ourselves unable to normalize<?z.0 as Trait>::Assocas?z.0 eq !T.1would give a universe error and we would returnNoSolution. This is wrong if the assoc type does not actually mention the placeholder as we would be able to instantiate?y.0with the assoc type's normalized form.This could likely only occur with
non_lifetime_bindersthat support where clauses and it would also likely have to be slighltly more complex of a reproduction to workaround the fact that?0: Traitare always ambiguous.6.
for<'a> fn(<<?x as OtherTrait>::Assoc as Trait<'a>>::Assoc)eq?xTODO: explain why this is an issue
7.
for<'a> fn(<?0.0 as Trait<'a, ?2.1>>::Assoc)eq?1.0<?0.0 as Trait<'a, ?2.1>>::Assocmay 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.?1.0tofor<'a> fn(<?0.0 as Trait<'a, ?3.0>>::Assoc)?1.0tofn(?3.0)with an obligation to provealias-relate(<?0.0 as Trait<'^0_0, ?2.1>>::Assoc, eq, ?3.0).?1.0tofn(?4.0)and enter the binder and emit analias-relate(<?0.0 as Trait<!3.2, ?2.1>>::Assoc, eq, ?4.0).?4.0could not be instantiated with something containing the!3.2placeholder even though we would like to end up with?1.0potentially being able to be resolved to something likefor<'a> fn(&'a u32)?4.0could somehow be instantiated with something containing!3.2we would have no way of converting that placeholder back into a bound var for the originalfn(?4.0)Solutions:
for<'a> fn(<?0.0 as Trait<'a>>::Assoc)to?2.0and emitting arelate(for<'a> fn(<?0.0 as Trait<'a>>::Assoc, eq, ?2.0)obligation and instantiating?1.0with?2.0.for<'a> fn(?0.0 as Trait<'a>>::Assoc)tofor<'a> fn(?2.0<'a>)and instantiate?1.0with that, while emitting an obligationfor<'a> alias-relate(<?0.0 as Trait<'a>>::Assoc, eq, ?2.0<'a>).NoSolutionduring coherence as it does not matter if we are incomplete during hir typeck.AliasKind::Ambiguousin coherence, which will result in ambiguity when attempting to prove goals involving itThere have been various large comments on PRs about soundness of generalization: one, two