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 types
    • Negative(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 and Impl2
    • There exists some where clause WC on Impl2 where negative(WC) holds.