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 rust-lang/rust#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 rust-lang/rust#22074 (comment)). 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.