Description
Equating aliases whose normalization is ambiguous is sus™ as there are conflicting requirements.
Equate should be complete
We do not want the equating of two types to result in unnecessary inference or region constraints. Both because it is not nice™ and also because it is unsound when done during coherence (rust-lang/rust#102048). This means that for an ambiguous alias like <T as WithAssoc<'lt>>::Assoc
in the below example, we must not simply equate the generic arguments of the alias.
trait Trait<T> {}
trait WithAssoc<'a> {
type Assoc;
}
impl<T: for<'a> WithAssoc<'a>> Trait<T> for for<'a> fn(<T as WithAssoc<'a>>::Assoc) {}
impl<'a, T: WithAssoc<'a>> Trait<T> for fn(<T as WithAssoc<'a>>::Assoc) {}
Type relations should be idempotent
Relating a type with itself should always succeed. Because of MIR typeck we have an even stronger invariant: relating a type with itself (modulo regions) should always succed (potentially emitting region constraints).
This is necessary as we erase regions after HIR typeck and replace them with unique region inference variables during MIR typeck. The below example currently fails because we try to eagerly normalize <T as Trait<'a>>::Assoc
somewhere, avoiding this issue.
struct Invariant<T>(*mut T);
trait Trait<'a> {
type Assoc;
}
fn foo<'a, T>(
x: Invariant<<T as Trait<'a>>::Assoc>,
) -> Invariant<<T as Trait<'a>>::Assoc>
where
T: for<'b> Trait<'b, Assoc = <T as Trait<'b>>::Assoc>,
{
let y = x;
y
}
We currently uniquify lifetimes when canonicalizing solver inputs to avoid any dependencies on the exact lifetimes. Not doing so ended up causing ICEs during MIR typeck: #27. This means we need to handle types which are structurally equal up to regions everywhere, causing issues for non-defining uses of opaque types in their defining scope (#74)
Relating aliases whose normalization is ambiguous cannot be both complete and idempotent (ignoring regions) at the same time
@lcnr would like to "fix" this by requiring aliases to be either normalizable or rigid, causing aliases with ambiguous normalization to not be well-formed. This means we don't have to worry if their behavior is inconsistent.