search

rust-lang / a-mir-formality

a model of MIR and the Rust type/trait system
Apache License 2.0
285 stars 33 forks source link

prevent Copy and Drop impls for same type #14

Open nikomatsakis opened 2 years ago

nikomatsakis commented 2 years ago

According to https://doc.rust-lang.org/reference/special-types-and-traits.html#copy one also has to check that Drop is not implemented for a type that implements Copy. As far as I can tell this can't be stated currently as there is no logical negation nor a predicate that asserts that a trait is not implemented.

Originally posted by @ltentrup in https://github.com/nikomatsakis/a-mir-formality/issues/10#issuecomment-1107448775

nikomatsakis commented 2 years ago

We probably want to add a (not-provable Goal) goal into the solver so that we can express this -- but I wouldn't want that exposed as a where-clause.

digama0 commented 2 years ago

This seems closely related to coherence checks: coherence means something like Implemented T -> Implemented U -> T = U while copy/drop has the form Implemented T -> Implemented U -> False so I imagine that the same techniques can be used in both cases (two trait implementations in negative position)