prevent negative impl cycles

[nikomatsakis]

When integrating negative impls into a-mir-formality, I realized a problem with the current check.

The current logic has a check that, at its heart, boils down to this:

• If there are two overlapping impls and one impl requires T: Trait, and we can prove T: !Trait, then this impl can be ignored.

This assumes that the coherence checker is guaranteeing that T: Trait and T: !Trait do not hold for the same T. This is generally true, but there is a trick, because this code is running during coherence. So you can wind up with the coherence check for Trait (which has the job of proving that T: Trait and T: !Trait do not overlap) also relying on that same condition.

In the current trait checker, this leads to a cycle, but in a-mir-formality, which permits cycles, it leads to unsoundness. Given that I plan to propose that we allow cycles for all traits (i.e., coinductive semantics), this is a problem.

Here is an example test:

trait MyTrait { }

struct Foo { }

impl !MyTrait for Foo { }

impl MyTrait for Foo
where
    Foo: MyTrait // in formality, this would work
{ }

What happens in this test:

• We see that the two impls overlap.
• We see that the second impl has Foo: MyTrait and try to prove Foo: !MyTrait, which succeeds (there is a negative impl, after all).
• We conclude that the two impls are disjoint (but that's not true, obviously).

I'll leave discussion on the best way to fix this for issue text.

[nikomatsakis]

@rustbot label +P-low -I-prioritize

I am removing the prioritization label. This is a feature gated, incomplete feature, so the unsoundness here is not relevant to stable Rust.

[nikomatsakis]

One possible fix is to leverage the query system to prevent cycles between traits:

Before we try to prove T: !Trait, we could force a query that checks that Trait and !Trait have been proven disjoint. If we are in the process of checking coherence for Trait, this would then force a cycle.

I'm not sure how I feel about this fix. It may be that the rules we're using for proving positive/negative impls disjoint can be improved in some other way.