More flexible coherence rules that permit overlap

[nikomatsakis]

There is a need for more flexible coherence rules, and in particular a way to permit overlap in some cases. There are numerous proposals for how to go about achieving that. Here is a summary:

• Specialization
• Negative bounds (e.g., RFC #586)
• Crate-local or scoped impls

Note that a prime concern here is forwards compatibility. See RFC #1023 (and this internals thread) for details.

RFCs and other links:

• #586
• #1148
• A modest proposal around negative reasoning and auto traits

[pnkfelix]

A discussion with niko today revealed that a naive specialization feature could cause the drop check rule (RFC 769) to break.

In particular, if we allow one to:

1. define a function/method m that is defined with input x:T for all types T,
2. call m on self.0 within the Drop implementation for some type D<F>(F) that, under the drop check rule, is not subject to any ordering constraints since it has no lifetime parameters and F has no bounds, and
3. specialize that method m to a particular type T = &'a Stuff, that actually dereferences through the &'a reference.

Then one could end up in a situation where the drop implementation for D ends up accessing data that has expired via m(self.field).

[withoutboats]

Hi.

I think negative bounds as discussed in RFC #586 would be very valuable, with the following modification to avoid the problem of backwards incompatibility: impl<T: !Foo> does not mean that T doesn't impl Foo, but that T impls !Foo (which seems like a plain-text reading of the code when written out like this). A T which does not impl either Foo or !Foo therefore does not meet the bound for either impl<T: Foo> or impl<T: !Foo>. This would require also that negative impls be possible for all traits, not only default traits, so that one could write e.g. impl<T> !Num for Vec<T> {}, indicating a contract that Vec is not a number (without as much semantic overhead of coming up with a whole concept of contracts).

Doing this would limit the usefulness of negative bounds somewhat (because T: Foo and T: !Foo would not cover the whole range of types), but I think would be well worth it to avoid the rather enormous backwards compatibility hazard discussed in the prior RFC.

It might be worth doing, also, that if there exists a trait Foo: !Bar, impl Foo for Quux implies impl !Bar for Quux, but requiring the explicit declaration is probably better.

Types defined in std should negatively implement various traits where a backwards compatible commitment to not implementing that trait exists. This is a backwards compatible change.

Adding negative bounds to traits which should not logically cohere (e.g. Integer and Float or Signed and Unsigned) is also a good decision. This is not a backwards compatible change, but the code it would break seems like it was 'in bad faith' so to speak and if this change were done early enough I don't know how serious of a violation of semver it would be to break backcompat for something like that. More importantly, though I can think of several traits in unstabilized crates that are logically incoherent, I can't think of any traits that are stable in 1.0 that ought logically to have a negative trait bound with any other trait.

Some sort of specification system would be useful in addition to this for a lot of the use cases you've highlighted, but this alone would open up a lot of more straightforward cases, such as enabling new traits to 'piggyback' on standardized or otherwise commonly imported traits without violating coherence rules (e.g. the trait DoshDistimmer could be implemented such: impl<T: Integer> DoshDistimmer for T {} as well as impl<T: Float> DoshDistimmer for T {}, and (since Vec<T> impls !Num) impl<T> DoshDistimmer for Vec<T>).

[withoutboats]

Here's an interesting case:

trait Foo { }

trait Bar {
    type Baz;
}

impl<T> Foo for T where T: Bar<Baz=u32> { }
impl<T> Foo for T where T: Bar<Baz=i32> { }

This is currently incoherent, because the coherence rules do not allow us to infer that the intersection between Bar<Baz=u32> and Bar<Baz=i32> is empty. However, I believe that this would be a sound rule to add to the coherence system:

T ≠ U → Trait<Type=T> ∩ Trait<Type=U> = ∅

In my own use case for this, I want to provide blanket impls for functions that return one of two different types.

[Centril]

cc #2451.