Distinctness II: Recursion is also applicable to Rust #21
Description
https://counterexamples.org/distinctness-recursion.html
Coherence in Rust is used to check that there are no overlapping trait impls. Failing to prevent overlapping impls can be exploited to get memory unsafety. Coherence works by instantiating each pair of trait implementations with inference variables and trying to unifying the impl headers. If unification fails, the impls don't overlap. During coherence, we therefore rely on distinctness being correct for soundness.
The Rust bug is rust-lang/rust#105787 (comment). Going from overlapping trait impls to actual memory unsafety is difficult and annoying so I didn't bother in this issue.
To simplify: Rust fails to unify <?0 as Trait>::Assoc with ?0 (using ?0 to annotate an inference variable) via the occurs check even though <?0 as Trait>::Assoc could later normalize to just ?0.