stedolan / counterexamples

Counterexamples in Type Systems
http://counterexamples.org
372 stars 23 forks source link

Distinctness II: Recursion is also applicable to Rust #21

Open lcnr opened 1 year ago

lcnr commented 1 year ago

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 https://github.com/rust-lang/rust/issues/105787#issuecomment-1579512541. 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.