More pieces to the puzzle:
- The error is present even without the
(Decider, u8)
impl.
- The error disappears if you replace each
(Decider, [whatever])
with (Decider, Decider, [whatever])
.
From<T> for Target
is isomorphic to Trait for T
(and AFAIK the orphan rules don't currently give any special treatment to Self
, simply treating it as the zeroth type parameter), so I'm going to simplify things and focus on this example:
A simpler successful scenario:
pub trait Trait {}
impl<T> Trait for Vec<T>
where T: Trait {}
impl<K,V> Trait for Vec<(K, V)>
where K: Trait, V: Trait {}
A simpler broken scenario:
pub trait Trait {}
pub struct Struct;
impl<T> Trait for (Struct, Vec<T>) // <-- changed
where T: Trait {}
impl<K,V> Trait for (Struct, Vec<(K, V)>) // <--- changed
where K: Trait, V: Trait {}
By inspection, in both scenarios, overlap only occurs if there may exist K
, V
such that:
K: Trait,
V: Trait,
(K, V): Trait,
Notice my use of the word "may." Negative reasoning in the trait system is tricky; there's a decent blog post by aturon about it. Basically, it is not good enough merely for us to fail to construct a counterexample from our given impls; that only suffices in the "closed world" modality described in the blog post. We must also consider impls that could be written in downstream crates, or added to upstream crates.
It was at this point that I began writing up an analysis of how I thought the compiler reasoned about this, in particular using the orphan rules to prove that (K, V): Trait
alone is unsatisfiable.
...but, uhhh...then I noticed that this example also fails:
An even simpler broken example:
pub trait Trait {}
pub struct Struct;
impl<T> Trait for Vec<T>
where T: Trait {}
impl<K,V> Trait for Vec<(K, V)>
where K: Trait, V: Trait {}
impl Trait for (Struct, u8) {} // <--- added
Applying simple logic, one can see that (K, V): Trait
implies (K, V) = (Struct, u8)
(due to the orphan rules), and that Struct: !Trait
and u8: !Trait
(again, due to the orphan rules). But the compiler does not reason this far.
tl;dr: The compiler's methods of reasoning are a lot more limited than they may sometimes seem.