Coherence check
Coherence works in two parts. The first is the orphan check, which is unaffected by this RFC: the orphan check is the one that ensures that you only implement foreign traits for types that are local to your crate.
The second part of the coherence check is the overlap check. The principle here is that if you have two impls Impl1
and Impl2
for some trait Trait
, we wish to ensure that Impl1
and Impl2
cannot apply to the same set of inputs P0: Trait<P1...Pn>
.
Negative of a where clause
We define the negative of a where clause Negative(WC)
as a partial function that converts T: Trait
to T: !Trait
:
Negative(P0: Trait<P1...Pn>) = Some(P0: !Trait<P1...Pn>)
Negative(for<'a..'z> P0: Trait<P1...Pn>) = Some(for<'a..'z> P0: !Trait<P1...Pn>)
Negative(WC) = None
, otherwise
New disjointness rules
The coherence check is extended with a new rule for determining when Impl1
and Impl2
are disjoint (the rule is applied twice for any pair (A, B)
of impl, once with A
as Impl1
and once with B
as Impl1
). These rules are alternatives to the existing rule, which means that any program that compiles today continues to compile, but we will also consider new programs as passing the coherence check.
In plain English, the idea is that we can consider Impl1
and Impl2
to be disjoint if whenever Impl1
applies, some where clause in Impl2
cannot hold (i.e., we can prove the negative of it) (and vice versa).
Disjoint(Impl1, Impl2)
holds if, for some substitution S and some where clause WC on Impl2:S(TraitRef(Impl2)) = TraitRef(Impl1)
-- there is some instantiation S of the Impl2 generics such that Impl1 and Impl2 apply to the same typesNegative(S(WC)) is provable, given the environment of Impl1
-- we can prove the negative version of some where clase from Impl2
In operational terms:
Disjoint(Impl1, Impl2)
if...- Instantiate
Impl1
with placeholders - Instantiate
Impl2
with inference variables - Equate all type parameters from
Impl1
andImpl2
- There exists some where clause
WC
onImpl2
wherenegative(WC)
holds.
- Instantiate