Allow trait bounds to be strict, e.g. in strict context T: Trait1 + Trait2 + ... would means that T implements exactly Trait1 + Trait2 + ....
Motivation
Enable negative reasoning on trait bounds.
Solve the intersecting implementation cases not supported by specialization.
Interaction with specialization
Implementations using strict trait bounds would always be more specific than those which don't.
Interaction with auto traits
Auto traits would be implicitly added to strict trait bounds unless opted out.
Would like to hear some feedback on this very simple idea. At first glance it seems to avoid the pitfalls of negative trait bounds (!Trait) while still enabling negative reasoning.
If you're saying that T implements no other traits, that's not really possible: any downstream crate can always declare a new trait and implement it for the type(s) in question.
Plus, it would make adding a trait impl a breaking change, which is not true today, and undesirable.
There are plans to allow explicit negative trait impls to promise "this type will never impl this trait", which then will eventually also allow negative reasoning about those traits in the type system.
Indeed but this is true for any negative reasoning feature unless you restrict it at crate level or something.
Also, fixing any strict impl you break that way is straightforward since you just have to make a new one with the extra traits. If we consider the same scenario with negative trait bounds the fix is not obvious because you are breaking the intended behavior, while here it's more like extra specialization.
It makes sense to delegate the strict impl to any downstream crate which chose to add new traits. If you want to build on top of the existing functionality you could always use a newtype pattern.
From the upstream crate point of view you could also prevent that scenario altogether with a feature like sealed types. Or as said earlier restrict negative reasoning at crate level.
No. Typically negative reasoning is always explicit about which traits it applies to, and only traits that already exist can explicitly be mentioned. This means that traits that are newly created downstream would not be considered and cause problems in an upstream negative reasoning.
I think that you misunderstood the question and that @Aaron1011 was referring to the fact that a strict bound not including Foo could never be satisfied when Foo has a blanket impl for all types.
Sure, my bad. And then the orphan rules make it is impossible to break such upstream negative reasoning. But then, why don't we have !Trait on stable Rust already ? Compiler limitations ?
No deep, technical reason that I'm aware of. I think it's just a huge design space with lots of very subtle questions that's kind of pointless to dig into (more than we already have) until much higher-priority trait system features like GATs, impl Trait/async in traits and basic specialization get somewhere close to stabilization. Especially since, as you said yourself, there's a huge overlap between negative impls and specialization, so until the ecosystem gets its hands on specialization it's impossible to tell if there's any significant demand for the specific things that only negative impls can do.
IMO, the interesting question for this thread is: Would you ever want to use a strict trait bound as opposed to a negative impl or specialization? Offhand I don't know of any cases where you clearly would.
It's my understanding that there is great interest in supporting negative trait bounds for all traits. I don't know of any use case of strict trait bounds that couldn't be solved more elegantly with negative trait bounds.