Skip to content
New issue

Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.

By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.

Already on GitHub? Sign in to your account

Distinctness II: Recursion is also applicable to Rust #21

Open
lcnr opened this issue Jun 6, 2023 · 0 comments
Open

Distinctness II: Recursion is also applicable to Rust #21

lcnr opened this issue Jun 6, 2023 · 0 comments

Comments

@lcnr
Copy link

lcnr commented Jun 6, 2023

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.

Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment
Labels
None yet
Projects
None yet
Development

No branches or pull requests

1 participant