Understanding the unsoundness of Rust type compile time eq / neq

Question

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 ?

Answer 1

But type equality is also a compile time only thing

Is it?

trait IsEq<T> {
    fn explode(&mut self, value: T);
}

// Imaginary syntax.
impl<T, U> IsEq<U> for T where T != U {
    fn explode(&mut self, value: T) {
        // Do nothing.
    }
}

impl<T> IsEq<T> for T {
    fn explode(&mut self, value: T) {
        // Allowed, since `Self == T`.
        *self = value;
    }
}

If there is some way to implement the above trait for both T != U and T == U separately, then there must be a way to make the above code compile. But then explode() can trivially cause UB because monomorphization doesn't consider lifetimes:

let mut long: &String = ...;
{
    let short: String = ...;
    IsEq::explode(&mut long, &short);
}
// `long` refers `short` after it is dead, a use-after-free!

The reason this code will pass is that during codegen, when we decide which method to call, lifetimes are already erased and treated uniformly. So codegen see &'erased String for both types, which seems equal. We cannot make codegen lifetime-dependent, since this will mean an explosion of the monomorphizations we need to make - for every impl TypeWithLifetime, we will need to copy the code for every lifetime used.