Idea: Strict trait bounds

Idea

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.

Well what does that mean?

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.

11 Likes

How would this interact with traits that have blanket impls? E.g.

trait Foo {}
impl<T> Foo for T {}
3 Likes

@CAD97

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.

@Aaron1011

Strict impls would specialize blanket impls.

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.

2 Likes

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 ?

Treat them like auto traits.

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.

(I should probably mention that https://github.com/rust-lang/rust/pull/68004 did happen earlier this year, although if you read all the fine print it's clearly and very intentionally nowhere close to a complete negative impls feature)

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.

2 Likes

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.