Rfcs: Type inequality constraints in `where` clauses

[spinda]

The idea of a != constraint form in where clauses has come up multiple times, in discussions of the where clause itself, in https://github.com/rust-lang/rust/issues/20041 as a counterpart to the == constraint form, and in various proposals for negative trait reasoning (!Trait). I'd like to extract this idea into its own RFC.

Say we want to write a From instance for ! reflecting its ability to implicitly cast to any type.

#![feature(never_type)]

trait From<T> {
    fn from(T) -> Self;
}

impl<T> From<T> for T {
    fn from(t: T) -> Self { t }
}

impl<T> From<!> for T {
    fn from(t: !) -> Self { t }
}

This produces an overlapping error because both impls cover !: From<!>. Specialization can't help here, as the first impl does not fully contain the second. What's necessary is a way to limit the scope of the second impl to exclude T == !, avoiding the overlap altogether. I'd like to propose the following syntax:

#![feature(inequality_constraints)]
#![feature(never_type)]

trait From<T> {
    fn from(T) -> Self;
}

impl<T> From<T> for T {
    fn from(t: T) -> Self { t }
}

impl<T> From<!> for T where T != ! {
    fn from(t: !) -> Self { t }
}

Negative reasoning for traits has been held up in the past due to concerns over implementing a trait for a new type becoming a breaking change. The == constraint has been held up due to an expectation that it would affect normalization (see https://github.com/rust-lang/rust/pull/22074#issuecomment-73678356). The != constraint doesn't suffer from either of these issues and can be very useful on its own, so I think it makes sense to split it off.

[joshtriplett]

This seems plausible. I can imagine that in the future, if we have full specialization support (allowing overlapping instances with rules for selecting more specific instances over more general instances), the use case of manually excluding conflicting types would disappear. However, in the meantime, this would work.

In the interests of not making the perfect the enemy of the good, it'd be nice to know whether we expect to have specialization support quickly enough to make this unnecessary, or if the ecosystem would benefit significantly from an intermediate step.

[withoutboats]

Negative reasoning tends to be a source of issues, this is definitely a non-trivial feature. We have to work through the implications of it to make sure it doesn't break any guarantees we want coherence to uphold. I would say specialization will definitely be stabilized before this feature could be.

We should maybe have a tag for negative reasoning proposals so we can keep track of all of them.

[joshtriplett]

@withoutboats

I would say specialization will definitely be stabilized before this feature could be.

In that case, it seems like the most critical question on this proposal is whether it has use cases that specialization would not address. If it does, I'd like to see some examples of them. If it doesn't, and we think specialization will get implemented first before this feature would, then I don't think we'd want to accept it.

[withoutboats]

You could impl<T> Foo for T where T != SomeType without implementing Foo for SomeType. Specialization doesn't enable this. I'm not sure this is a good idea since this gets us away from the uniformity that trait-based polymorphism encourages.

[joshtriplett]

@withoutboats You could do that, but I wondered if any specific use case might motivate that. None come to mind, but I wondered if the proposer might have one, or if anyone else might.

[Ericson2314]

There's the blanket From for everything. I think this would be overkill there, as I rather somehow exploit the fact that the overlapping implementations are identical.

[withoutboats]

@Ericson2314 is there a blanket From<!> for everything? How is that coherent with the blanket From<Self>?

[glaebhoerl]

I suspect the point was intended to be that there isn't, because it wouldn't be, and that this could be a way to solve it (but not the best one).

[withoutboats]

Oh I see I misread "There's the blanket From impl" as "There is a blanket From impl"

[spinda]

@Ericson2314

There's the blanket From for everything. I think this would be overkill there, as I rather somehow exploit the fact that the overlapping implementations are identical.

Do you mean rustc would be doing some sort of code equivalence checking? That seems like it would be hard/fiddly to me.

[spiveeworks]

use case:
making a generic union based on a type-level cons list, and a downcast trait,

trait TypeInfo {}
trait Downcast<_T: TypeInfo> {}


union Cons<A, B>
    where A: Copy + TypeInfo,
          B: Copy,
{
    head: A,
    tail: B,
}

impl<A, B> Downcast<A> for Cons<A, B>
    where A: Copy + TypeInfo,
          B: Copy,
{}

impl<E, A, B> Downcast<E> for Cons<A, B>
    where A: Copy + TypeInfo,
          B: Copy + Downcast<E>,
{}

This gives an error for conflicting implementations, which could be fixed by constraining the second impl to A != E

Specialization itself doesn't solve this, although if I recall correctly, Niko has mentioned that specialization could be loosened further eventually, but I don't understand well enough to tell if this would be allowed.

[mjbshaw]

Another use case is relaxing the object safety escape hatch for traits (discussion here). RFC 255 introduces the concept of object safety for traits. For example, consider the following trait T:

trait T {
  fn foo();
  fn bar<T>(&self);
}

foo and bar make T no longer object safe. Currently, the only escape hatch is adding a where Self: Sized constraint. That's a rather unfortunate escape hatch, though, as Sized is overly broad and prevents unsized types (like extern types) from meeting these requirements.

Type inequality constraints could solve this. The escape hatch could be where T != dyn T, which should be sufficient for object safety (assuming I haven't overlooked something) and would allow unsized types (that aren't trait objects) to have these trait methods.

[bb010g]

Is anything in the compiler blocking this, or has there been a lack of interest in implementation so far?

[Kixunil]

Another benefit of this would be less boilerplate.

With lattice specialization:

impl<T> From<T> for T {
    fn from(this: T) -> Self  {
        this
    }
}

impl<T> From<!> for T {
    fn from(this: !) -> Self {
        this
    }
}

impl From<!> for ! {
    fn from(this: !) -> Self {
        this
    }
}

With inequality:

impl<T> From<T> for T where T != ! {
    fn from(this: T) -> Self  {
        this
    }
}

impl<T> From<!> for T {
    fn from(this: !) -> Self {
        this
    }
}