I’ve been messing a lot with Rust type system, and I’ve always hit the same barrier, the fact that we can’t tell if two types are the same at compile time. More precisely, the fact that two types are different.

It is easy to write type equality trait bounds:

trait IsSame<T> {}
impl<T> IsSame<T> for T {}
[...] where U: IsSame<T>

But I’ve been struggling for type inequality, and precisely to write something like:

trait Boolean {} // type level boolean
struct True;
impl Boolean for True {}
struct False;
impl Boolean for False {}

// the trait I want to implement
trait IsEq<T> {
    // for <T as IsEq<T>> this is `True`, otherwise this is `False`
    type Eq: Boolean;
}

Most of the answer I’ve read is that this would not be possible, as it is unsound, but I’m failing to understand why. How could one break something with such a trait ?

The major argument I’ve seen is when lifetimes comes into play, things breaks down. I would be naively thinking that type equality also applies to lifetimes, meaning that &'a () == &'b () implies that 'a == 'b, and we can have lifetime equality as 'a == 'b <=> 'a: 'b && 'b: 'a.

I understand that TypeId can only exists for 'static types, as it can be be built at runtime where lifetimes don’t exists. But type equality is also a compile time only thing, so how could it break Rust’s soundness ?