Do not emit alias-eq when instantiating a type var from a canonical response in the new solver by compiler-errors · Pull Request #109037 · rust-lang/rust (original) (raw)

I think the approach this PR takes is not correct. This ended up kind of a huge comment, sorry for giant wall of TEXT :<

I think generalizer right now is wrong for projections. The case of ?0 <: <?1 as Trait>::Assoc will result in generalizing the projection to <?1 as Trait>::Assoc (assuming universes are OK) and then instantiate ?0 to <?1 as Trait>::Assoc and relate <?1 as Trait>::Assoc <: <?1 as Trait>::Assoc which will trivially succeed.

If we imagine ?1 getting inferred to Foo<?2> and an impl such as:
impl<T> Trait for Foo<T> { type Assoc = T; }
Then ideally what would happen here is that post-normalization we end up with Foo<?2> <: Foo<?3> instead of Foo<?1> <: Foo<?1>. With lazy norm this probably will likely get worse and introduce backwards compatibility problems where we will end up having projections instead of their normalized form.

Fixing this will be incompatible with the way that this PR currently has sub/sup relate the substs of projections. I suspect that in the future we will want to change AliasEq to AliasRelate that stores a variance (for whether to do eq/sub/sup). Generalization would then turn projections into infer vars and then emit AliasRelate so that the previous case of:
?0 <: <?1 as Trait>::Assoc will result in us generalizing <?1 as Trait>::Assoc to ?2, instantiating ?0 to ?2 and then emitting AliasRelate(?2, sub, <?1 as Trait>::Assoc). (Although the exact way that we solve this problem may not be this but I think its almost guaranteed that relating substs like this PR does, will be incompatible with a solution)

This could probably be fixed by just Not setting eager_relate_projections_via_substs for sub/sup and only doing it for eq.

Instantiation relating the substs of projections when doing eq is less obviously incorrect but still wrong I think.

Generalizer has a special case to avoid creating new infer vars for invariant positions except for the situation where the var being instantiated is in a lower universe than the variable being generalized. So we can actually end up in a situation where generalizing a projection results in a type that is not == to the version before generalizing:

If we were to relate the substs of these two projections ?1.1 would get inferred to have the universe of ?2.0 as it is lower. This could then go on to cause universe errors when relating ?1.1 with a placeholder in universe 0 as the infer var has now been resolved to ?2.0 which cannot name the placeholder.

This is likely unsound during coherence as it would cause NoSolution when the aliases being equal could have held through other means that the substs being equal. For example it's possible that ?2.0 and ?1.1 would each get inferred to completely different types allowing normalization to succeed with the normalized types ending up equal.

I suspect that you could get the same issue with sub/sup however since those are not used for coherence it would probably be "fine" for those to be incorrect.

This could probably be fixed by only setting eager_relate_projections_via_substs when we are not in intercrate mode. Right now new solver's behaviour for alias equality does not change between coherence and type checking and I think that is desirable to maintain unless completely necessary to give up (which I do not think this issue requires)

I am not entirely sure what lcnr's plan for the FIXME in unify_query_var_values is. Eventually we do need to handle it some way for occurs check on projections so that ?0 eq <?0 as Trait>::Assoc does not give us NoSolution instead of ambiguity during coherence (afaik the current plan is to emit PredicateKind::Ambig when this occurs). Handling this would only require downgrading the QueryResult to ambiguous if there are any goals.

If we wanted to handle AliasEq here though we would have to actually evaluate the nested goals afaict because under lazy norm we may end up with these AliasEq goals actually being able to succeed via normalized tys being equal.

I haven't talked about the somewhat more subjective complaints about this PR (generally the solution having a "hacky" vibe that is probably a soundness footgun as relating substs is generally Very Wrong) since I think the more objective problems (this PR being unsound as is) are more important.