ITADN

Distinctness II: Recursion is also applicable to Rust

#21Openlcnr 创建于 2023-06-06
L
lcnrcommented
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. 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`.
0 条评论