A modest proposal around negative reasoning and auto traits

I've been thinking about negative trait bounds a fair amount lately. I think I'm starting to get a picture of how I see them fitting into our system. This description is very similar to RFC 1148, but it differs in a few particulars. It also incorporates some description of auto traits.

First, as in RFC 1148, the idea would be to embrace "intuitionistic" over classical logic. What this means is that proving T: Trait and proving T: !Trait are basically the same process: one can prove T: Trait by finding a suitable impl of Trait, and likewise one can prove T: !Trait by finding a suitable impl of !Trait. It is however entirely possible that one cannot prove either T: Trait or T: !Trait, so this means that !(T: Trait) does not imply T: !Trait nor vice-versa. In fact, in a sense, Trait and !Trait are almost completely independent predicates -- but as we'll see, coherence does ensure that T: Trait xor T: !Trait, which have an important semantic implications (but doesn't affect what rustc does in particular).

In this RFC, I will adopt the RFC 1148 notation of writing T: ?Trait to mean that neither T: Trait nor T: !Trait are provable. Unlike RFC 1148, I don't anticipate making this something that users can actually type (though one could imagine allowing impl ?Trait declarations for auto traits in particular).

Second, we would adapt coherence to be based primarily on explicit negative impls. I put forward an initial proposal that is fully backwards compatible, but I suspect this is an area where we could get away with some changes. In particular, I would like to at minimum remove #[fundamental]. See the section on "Negative reasoning in coherence" for details.

Negative impls

In terms of impls, users would now have the ability to explicitly implement a "negative impl". This can be understood as a commitment that the type will never implement the given trait:

impl<...> !Trait<...> for Type { }

These impls don't have any particular restrictions. As today, their body is always empty (maybe we should just write a ;).

Most parts of the system would treat !Trait basically as if it were a completely distinct trait from Trait. So if you want to that T: !Trait, you would search for negative impls that cover that case. If you want to prove that T: Trait, you would search for positive impls that cover that case.

Put another way, if you ignore coherence, you could consider:

trait Trait { ... }
impl Trait for T { ... }
impl !Trait for U { }

as being equivalent to introducing a marker trait NotTrait like so:

trait Trait { ... }
trait NotTrait { /* empty */ }
impl Trait for T { ... }
impl NotTrait for U { }

Negative bounds

We can also permit negative bounds of the form T: !Trait. As described in the previous section, T: !Trait only holds if we can find a suitable negative impl. (However, we could also drop support for these bounds, at least for now, which simplifies some aspect of this proposal; see the list of "unknowns and variants" at the end.)

Coherence of `Trait` and `!Trait`

The only bit of the system that really acts differently is coherence. We use the term "polarity" to refer to whether an impl is for Trait (positive polarity) or !Trait (negative polarity).

The coherence rules would ensure that every pair of positive impls is disjoint. They also ensure that every positive impl is disjoint with every negative impl.

Note that the coherence rules do not need to ensure that every negative impl is disjoint with every negative impl. This is basically analogous to RFC 1268, the RFC we adopted which relaxes the coherence rules for marker traits. Unfortunately, it carries the same implementation complications -- if we cannot solve those, then we should simply have coherence ensure that negative impls are disjoint.

Negative reasoning in coherence (and backwards compatibility)

In general I would like to try to integrate !Trait bounds into coherence better. This is where things get a bit tricky. Let's first describe my ideal world. Ideally, to my mind, the coherence overlap algorithm would rely only on explicit negative impls.

That is, the algorithm for judging overlap might look something like this (this is an adapted version of what we have today):

Replace all type and lifetime variables with inference variables.
Unify the trait references (if not possible, the impls are disjoint).
Let P be the union of the where clauses on both impls.
Let Q be a set containing the "flat map" of the inverse of the where clauses in P, as follows:
- T: Trait<..> becomes Some(T: !Trait<..>)
- T: !Trait<..> becomes Some(T: Trait<..>)
- all other where clauses (e.g., T: 'a, 'a: 'b) become None
  - iow, they have no inverse and cannot be used to prove disjointedness
If we can successfully evaluate any of the where clauses in Q, then the impls are disjoint.
Otherwise, they may overlap.

However, this procedure has two limitations:

It doesn't understand mutually inconsistent sets of bounds.
It would probably break far too many existing crates to be feasible. In particular, it doesn't permit any of implied negative logic that RFC 1023 specified.

Let's look at those two things in detail.

Mutually inconsistent sets of bounds

The other problem with the procedure above is that it will not be able to handle pairs of impls like the following:

impl<T:Foo> Bar for T { }
impl<T:!Foo> Bar for T { }

These two impls really ought to be considered disjoint, because we know that T: Foo xor T: !Foo. Unfortunately, the procedure above will fail, because it will try to prove that T: Foo (and fail) and then try to prove that T: !Foo (and fail). In particular, we need a "directional" overlap check, where we consider the preconditions of one impl, and use those to check for contradictions with the other impl. This is quite similar to what specialization does. Alternatively, we could try to adapt the approach specified in RFC 586 of detecting "mutually inconsistent" bounds in a set of bounds, but that feels a bit trickier to me (for example, we would need to ensure that neither impl is inconsistent on its own, as well).

Since this doesn't seem that tricky, I'm just going to assume we solve this for now. :)

Backwards compatibility

For reference, the rules there was that coherence could use implicit negative reasoning about a trait reference T: Trait<U..> if that trait reference met the following critera:

the types [T, ...U] in the trait reference meet the orphan rules; or,
the trait Trait is declared #[fundamental].

There are two ways we could incorporate this kind of reasoning into the scheme described thus far:

You could extend the notion of T: !Trait<..> to say:
- if the types meet the orphan rules, you can deduce that !Trait holds simply by the absence of a positive impl
Or you could keep !Trait as requiring an explicit impl, but just allow coherence to use a slightly extended form of negative reasoning.

I favor the second approach. In particular, I would extend the algorithm I gave before with another step (step 6 is new):

Replace all type and lifetime variables with inference variables.
Unify the trait references (if not possible, the impls are disjoint).
Let P be the union of the where clauses on both impls.
Let Q be a set containing the "flat map" of the inverse of the where clauses in P, as follows:
- T: Trait<..> becomes Some(T: !Trait<..>)
- T: !Trait<..> becomes Some(T: Trait<..>)
- all other where clauses (e.g., T: 'a, 'a: 'b) become None
  - iow, they have no inverse and cannot be used to prove disjointedness
If we can successfully evaluate any of the where clauses in Q, then the impls are disjoint.
Let R be the set of trait references in P that meet the criteria from RFC 1023.
- Check whether any of those cannot be proven, using today's classical logic.
- If so, the impls are disjoint.
- However, we issue a deprecation warning suggesting the use of an explicit negative impl.
Otherwise, the impls may overlap.

Note that we continue to permit the same impls as ever, but we issue a deprecation warning. That is, we are going to try and actively migrate people to use explicit negative logic (but we are not going to take the implicit logic away).

There are several reasons that I favor the approach of deprecating implicit negative logic and containing the damage to coherence rather than infecting T: !Trait<..> altogether:

Implicit negative logic is easy to do by accident. I suspect we are accidentally making assumptions about types that we are not aware we are making. I know I found some cases like that in the standard library from time to time. Moreover, by adding a deprecation warning, we may eventually get ourselves into a position where we can remove the implicit logic altogether (either as part of a Rust 2.0, or just if we are able to determine that the logic is not widely used).
Implicit negative logic is dangerous. If we make !Trait use the implicit logic of specialization, it means that one cannot understand T: !Trait as being equivalent to T: NotTrait, but rather one must think of it as a different thing altogether, obeying much more complex rules. This means that the interactions with the existing system, and in particular lifetime erasure, become much less clear; it also means that we must think very carefully about how it will interact with new features like specialization.
- I don't yet have a smoking gun problem, but it seems clear that, at minimum, specialization would have to consider T: !Trait<..> very carefully in any kind of "lifetime-parametric" analysis.
- Also, most prolog and logic systems have shied away from classical logic, because it cannot be implemented in a complete fashion. I'm not sure of the details here, but it seems to me we would be wise to stay away too. (And implicit negative logic is a kind of classical logic, since we assume that !(T: Trait) implies T: !Trait.
Implicit negative logic is challenging to implement. At minimum, implicit negative logic would make the implementation of region inference and lifetime erasure much more complex. Today, all of our region bounds devolve into 'a: 'b relations, which are reflexive (that is, 'a: 'a). (Equality can be understood as 'a: 'b and 'b: 'a.). This means that we can implement region inference using fixed-point iteration (well, mostly), and that we can implement lifetime erasure by just replacing all lifetimes with 'static. If we allowed implicit negative logic, though, you could construct irreflexive lifetime relations:
```
trait Foo<'a, 'b> { }
  
struct LocalType;
impl Foo<'a, 'b> for LocalType where 'a: 'b { }
```
Now LocalType: !Foo<'x, 'y> is true if 'x: 'y does NOT hold, which means that 'x must be strictly smaller than y. This would break a lot of assumptions in the compiler.

Removing fundamental

So far, I haven't proposed anything backwards incompatible. However, one of the things that makes explicit !Trait impls appealing to me is that they offer a better alternative to #[fundamental]. I suspect we could get away with removing #[fundamental] altogether and just keeping the implicit negative logic around local types. (Ideally, we'd get rid of that too, but I think that could break a lot of code. We'll have to test.)

The reason that I think we can remove #[fundamental] is that we were very parsimonius about applying it. Currently, it is only applied to three traits in the standard library:

the Sized trait; and,
the closure traits Fn...FnOnce.

Clearly, the special logic around Sized would have to stay: but that's ok with me. Sized is a very special trait. It does not permit ANY user-defined impls, and it is always evaluated by the compiler to a boolean value, essentially (though false might mean "not known to be Sized).

The special logic around closure traits we could probably remove. The reason this was added was to support the string patterns API, which wants to be able to accept either a closure or a constant string without a problem. So removing #[fundamental] would require us to add explicit negative impls of FnMut to (at least) the following implementors of Pattern:

impl<'a, C> Pattern<'a> for CharEqPattern<C> where C: CharEq
impl<'a> Pattern<'a> for char
impl<'a, 'b> Pattern<'a> for &'b [char]
impl<'a, 'b> Pattern<'a> for &'b &'b str
impl<'a, 'b> Pattern<'a> for &'b str
impl<'a, 'b> Pattern<'a> for &'b String

What I don't know is what other traits out there in the wild might be affected. That is, anybody can write a trait like Pattern -- unfortunately, RFC 1210 did not require an unstable feature gate to employ the #[fundamental] attribute. I regret that now, but luckily we were very parsimonious in applying it, which may be good enough. The only way to know is to implement it and try it out (well, actually, some targeted acks through the crates.io sources might be helpful too).

Interaction with specialization

If/when we add specialization, I don't think it adds any particular complications. This is precisely because of the fact that !Trait can be thought of as equivalent to a marker trait NotTrait (but with added coherence support). If however we were to incorporat RFC 1023 like logic into !Trait, things get more complicated -- then we'd probably have to consider !Trait, when applied to a fundamental trait or local types, as being lifetime-non-parametric. That would be unfortunate.

Refining the auto trait specification

The auto trait RFC differs in several particulars from the actual implementation, which causes confusion. The most important one is that it specifies a kind of "fallback" semantics, where we first look for positive impls, then negative impls, then finally a default impl. This is basically the "implicit negative logic" I decried above. What is actually implemented is actually much more aligned with what you see in this document, but it still contains some worrisome bugs, such as #23072.

In general, I think auto traits should be considered a kind of "defaulting" mechanism. That is, if for some given type T, you do not supply any impls, then we will automatically supply one for you. This impl will ensure that T: Trait is implemented only if all the types of all data reachable from T implement Trait. We never generate an automatic T: !Trait impl.

The categories of types where a default impl will be generated if no applicable impl is found are:

Scalar types like i32 etc -- these are just implemented by default.
Tuples for each arity, like (_,), (_, _), etc -- these are implemented by default if their component types are implemented.
Reference types &_ and &mut _ as well as pointer types *const _ and *mut _ -- these are implemented if their referent is implemented.
Slice types [_] and array types [_; N] for every possible length -- these are implemented by default if their component types are implemented.
User-declared struct and enum types S<..> -- these are implemented by default if their field types are implemented (see the algorithm below).

Let me give some examples to try and clarify this.

Synthesizing impls: some examples on structs and enums

Let's start with some examples involving user-defined struct and enum types. I'll use the Send trait as my example of an auto trait trait (Send happens to be an unsafe trait, so you'll see the unsafe keyword below, but that is basically orthogonal to the main point).

As we will see in these examples, the basic intution is that if the user declares anything about a given struct or enum, then auto trait traits behave normally for that type, like any other trait. It's only in the case where the user declares nothing that the auto trait acts differently.

Here is the most basic example: if we just declare a new struct type, and nothing else, then we will synthesize an impl for that struct. (In fact, the precise process by which this impl is synthesized is fairly subtle, but let's ignore that for now.)

struct StructA<T> {
    vec: Vec<T>
}

// There are no explicit of impls of any polarity for `StructA`,
// and hence this implies the creation of an impl roughly like this:
//
// unsafe impl<T> Send for StructA<T>
//    where T: Send { }

Note that this implies that we can never prove StructA<T>: !Send because we do not synthesize a !Send impls (though we may of course fail to prove StructA<T>: Send, if we cannot prove T: Send).

However, if there are any explicit impls for a struct (of any polarity, and with any type parameters), then no impl is synthesized at all:

struct StructB<T> { .. }
unsafe impl Send for StructB<i32> { }

// Issue #23072
struct StructC<T> { .. }
impl<T:Default> !Send for StructC<T> { }

// Issue #27554
struct StructD<T> { .. }
unsafe impl<T:Default> Send for StructD<T> { }

// No synthetic impls created for `Struct{B,C,D}`.

Let's look at StructB first. There is one explicit impl, so that means we can prove StructB<i32>: Send but we can't prove StructB<T>: Send for any type T != i32. This also implies that the current behavior for issues #23072 and #27554 is in fact roughly correct. Consider StructC above -- because of the explicit negative impl, we can prove that StructC<Foo>: !Send, but only if Foo: Default. However, since there are now no positive impls at all, we can never prove StructC<T>: Send for any T (and in particular it doesn't matter whether T: Default or not). Similarly, for StructD, we can only prove that StructD<T>: Send if T: Default.

Synthetic impls for things other than structs or enums

When you declare an auto trait, you can also declare impls for the builtin type constructors (that is, types other than structs or enums). Those too act to suppress or enable synthetic impls, and the intution is roughly the same: if you say nothing about some builtin type cosntructor, then it will follow the default rules, but if you say anything at all, it acts like any other trait.

The set of builtin type constructors is in fact infinite, and it is roughly as follows. I will use _ to indicate types; I am intentionally not giving the types a name since the type constructor applies regardless of what the type is.

scalars: i32, u32, etc
pointers: *const _, *mut _
references: &_, &mut _ (for any lifetime)
tuples: (_,), (_, _), (_, _, _), ...
slices: [_]
arrays: [_; 0], [_; 1], [_; 2], ...

Let's see some examples to see how this works. For all the examples to come, I'll assume the impls are declared alongside a simple auto trait trait MyOibitTrait, declared like so:

trait MyOibitTrait { }
impl MyOibitTrait for .. { }

OK, let's start with scalars. If I say nothing about i32, say, then it is assumed i32: MyOibitTrait. But I can also pick and choose for specific scalar types:

impl MyOibitTrait for i32 { }
impl !MyOibitTrait for f32 { }

then we find that while i32: MyOibitTrait still holds, f32: MyOibitTrait does not. Moreover, f32: !MyOibitTrait does hold.

Let's move on to pointers. By default, *const T: MyOibitTrait holds if T: MyOibitTrait holds. But I might want to override that, as in the Send trait:

impl<T:!Send> !MyOibitTrait for *const T { }
impl<T:Send> MyOibitTrait for *const T { }

Now there is no synthetic impl for *const T, and hence *const T: MyOibitTrait is only provable if T: Send. Similarly, *const T: !MyOibitTrait is only provable if T: !Send. Otherwise, if T: ?Send, then *const T: ?MyOibitTrait.

Finally, let's talk about tuples, slices, and arrays. We might want to just prohibit implementing auto traits over these kinds of types, because there are an infinite set of them. It's not really clear then how useful it can be to write a specific impl. However, if we did permit it, it might have the following meaning:

// For whatever reason, MyOibitTrait is always
// implemented for two-tuples:
impl<T,U> MyOibitTrait for (T, U) { }

// But we still generate synthetic impls for other arities:
//
// impl<T> MyOibitTrait for (T,) { } // 1-tuple
// impl<T,U,V> MyOibitTrait for (T,U,V) { } // 3-tuple
// impl<T,U,V,W> MyOibitTrait for (T,U,V,W) { } // 4-tuple
// ...

I guess alternatively we might just lump all tuples together, so if you write an impl for a 2-tuple, it prevents any impls from being generated for tuples or other arities (and similarly for array lengths). That would probably be better.

Unknowns and variants

Let me just note down some unknowns and variants in this proposal:

The entire proposal fits together even without adding explicit where clauses of the form T: !Trait. That is, we might just add negative impls (at least to start) and incorporate those into coherence, and leave negative reasoning out elsewhere.
The precise coherence algorithm that incorporates knowledge of T: Trait xor T: !Trait. (I don't think, though, that knowing about this "xor property" is important anywhere outside of coherence.) Seems fairly non-scary. This point is moot if we drop explicit T: !Trait bounds.
The precise algorithm by which synthetic auto trait impls are created. I am coming around to the idea of making auto traits purely inductive but following a kind of "coinductive-like" elaboration procedure: basically building out a tree of things to prove and stopping whenever we get to either a user-provided case or a cycle. This also seems mostly non-scary at this point, but I haven't had time to write it up.
We may want a way to impl ?OibitTrait for Type, see section below for more details.

Auto traits and `?Trait` impls

You'll note that there is no way here to supress the generation of a synthetic impl without also making an affirmative declaration of some kind. That is, I can either impl OibitTrait for MyStruct or I can impl !OibitTrait for MyStruct, but either way I am making a future commitment. Maybe I just want to hold off on that.

In fact, this can be done, but it's kind of hacky. You have to use a dummy private type as a member of the struct:

struct Dummy;
impl !OibitTrait for Dummy { }

pub struct MyStruct {
    dummy: Dummy
}

(For generic types, one can use a similar hack to impl !OibitTrait for MyStruct<Dummy>.)

To make this more of a first-class declaration, we could permit an explicit impl of ?MyOibitTrait:

impl ?OibitTrait for Dummy { }

This would suppress all synthetic impls. However, I am not particulary keen on including this option, for a few reasons:

it suggests that T: ?Trait is a "predicate that can be proven", just like T: Trait and T: !Trait, but in fact T: ?Trait would be quite different (and, in particular, it holds because of the absence of impls, typically).
I'm not sure how often this is necessary; the dummy trick seems not intolerable.

nikomatsakis/a-modest-proposal.md Secret

Negative impls

Negative bounds

Coherence of `Trait` and `!Trait`

Negative reasoning in coherence (and backwards compatibility)

Mutually inconsistent sets of bounds

Backwards compatibility

Removing fundamental

Interaction with specialization

Refining the auto trait specification

Synthesizing impls: some examples on structs and enums

Synthetic impls for things other than structs or enums

Unknowns and variants

Auto traits and `?Trait` impls

withoutboats commented Jan 18, 2016

withoutboats commented Jan 18, 2016

nikomatsakis commented Mar 10, 2016

nikomatsakis commented Mar 10, 2016

arielb1 commented Jul 21, 2016

nikomatsakis/a-modest-proposal.md Secret

Negative impls

Negative bounds

Coherence of Trait and !Trait

Negative reasoning in coherence (and backwards compatibility)

Mutually inconsistent sets of bounds

Backwards compatibility

Removing fundamental

Interaction with specialization

Refining the auto trait specification

Synthesizing impls: some examples on structs and enums

Synthetic impls for things other than structs or enums

Unknowns and variants

Auto traits and ?Trait impls

withoutboats commented Jan 18, 2016

withoutboats commented Jan 18, 2016

nikomatsakis commented Mar 10, 2016

nikomatsakis commented Mar 10, 2016

arielb1 commented Jul 21, 2016

Coherence of `Trait` and `!Trait`

Auto traits and `?Trait` impls