Why are there overlapping impls?

#![feature(negative_impls)]
trait Ordinal {}
trait Gt<L: Ordinal> {}
impl<O: Ordinal> !Gt<O> for O {}
impl<O: Ordinal> !Gt<Succ<O>> for O {}
struct Zero;
impl Ordinal for Zero {}
struct Succ<O: Ordinal>;
impl<O: Ordinal> Ordinal for Succ<O> {}
impl<L: Ordinal, O: Ordinal> Gt<L> for Succ<O> where O: Gt<L> {}
impl<O: Ordinal> Gt<O> for Succ<O> {}

(Playground)

Errors:

   Compiling playground v0.0.1 (/playground)
error[E0751]: found both positive and negative implementation of trait `Gt<Succ<_>>` for type `Succ<_>`:
 --> src/lib.rs:9:1
  |
4 | impl<O: Ordinal> !Gt<O> for O {}
  | ----------------------------- negative implementation here
...
10 | impl<L: Ordinal, O: Ordinal> Gt<L> for Succ<O> where O: Gt<L> {}
  | ^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^ positive implementation here

For more information about this error, try `rustc --explain E0751`.
error: could not compile `playground` (lib) due to 1 previous error

For there to be a possible implementation of Gt<Succ<O>> for Succ<O> on line 9, it would then be required that O implement Gt<Succ<O>> (since L would be Succ<O>), but that clearly isn't possible due to the negative implementation on line 5

I don't know that negative impls have coherence implications yet. Probably will eventually, but unstable be unstable.

+#![feature(with_negative_coherence)]

(By the way @scottmcm, AFAIK there's no tracking issue for this feature and you just sort of have to know about it. It would be great if it could become more discoverable.)


However, it doesn't help the OP. I think this isn't really a negative coherence thing, so much as a "mutually exclusive where clauses aren't considered" thing, ala not supporting two implementations that have different associated types constraints.

But I could be wrong.

2 Likes

This topic was automatically closed 90 days after the last reply. We invite you to open a new topic if you have further questions or comments.