`TypeId` exposes equality-by-subtyping vs normal-form-syntactic-equality unsoundness.

[lcnr]

EDIT by @BoxyUwU
playground

type One = for<'a> fn(&'a (), &'a ());
type Two = for<'a, 'b> fn(&'a (), &'b ());

mod my_api {
    use std::any::Any;
    use std::marker::PhantomData;

    pub struct Foo<T: 'static> {
        a: &'static dyn Any,
        _p: PhantomData<*mut T>, // invariant, the type of the `dyn Any`
    }
    
    impl<T: 'static> Foo<T> {
        pub fn deref(&self) -> &'static T {
            match self.a.downcast_ref::<T>() {
                None => unsafe { std::hint::unreachable_unchecked() },
                Some(a) => a,
            }
        }
        
        pub fn new(a: T) -> Foo<T> {
           Foo::<T> {
                a: Box::leak(Box::new(a)),
                _p: PhantomData,
            } 
        }
    }
}

use my_api::*;

fn main() {
    let foo = Foo::<One>::new((|_, _| ()) as One);
    foo.deref();
    let foo: Foo<Two> = foo;
    foo.deref();
}

has UB from hitting the unreachable_unchecked because TypeId::of::<One>() is not the same as TypeId::of::<Two>() despite them being considered the same types by the type checker. Originally this was thought to be a nightly-only issue with feature(generic_const_exprs) but actually the weird behaviour of TypeId can be seen on stable and result in crashes or UB in unsafe code.

original description follows below:

---

#![feature(const_type_id, generic_const_exprs)]

use std::any::TypeId;
// `One` and `Two` are currently considered equal types, as both
// `One <: Two` and `One :> Two` holds.
type One = for<'a> fn(&'a (), &'a ());
type Two = for<'a, 'b> fn(&'a (), &'b ());
trait AssocCt {
    const ASSOC: usize;
}
const fn to_usize<T: 'static>() -> usize {
    const WHAT_A_TYPE: TypeId = TypeId::of::<One>();
    match TypeId::of::<T>() {
        WHAT_A_TYPE => 0,
        _ => 1000,
    } 
}
impl<T: 'static> AssocCt for T {
    const ASSOC: usize = to_usize::<T>();
}

trait WithAssoc<U> {
    type Assoc;
}
impl<T: 'static> WithAssoc<()> for T where [(); <T as AssocCt>::ASSOC]: {
    type Assoc = [u8; <T as AssocCt>::ASSOC];
}

fn generic<T: 'static, U>(x: <T as WithAssoc<U>>::Assoc) -> <T as WithAssoc<U>>::Assoc
where
    [(); <T as AssocCt>::ASSOC]:,
    T: WithAssoc<U>,
{
    x
}


fn unsound<T>(x: <One as WithAssoc<T>>::Assoc) -> <Two as WithAssoc<T>>::Assoc
where
    One: WithAssoc<T>,
{
    let x: <Two as WithAssoc<T>>::Assoc = generic::<One, T>(x);
    x
}

fn main() {
    println!("{:?}", unsound::<()>([]));
}

TypeId being different for types which are considered equal types allows us to take change the value of a projection by switching between the equal types in its substs and observing that change by looking at their TypeId. This is possible as switching between equal types is allowed even in invariant positions.

This means that stabilizing const TypeId::of and allowing constants to flow into the type system, e.g. some minimal version of feature(generic_const_exprs), will be currently unsound.

I have no idea on how to fix this. I don't expect that we're able to convert higher ranked types to some canonical representation. Ah well, cc @rust-lang/project-const-generics @nikomatsakis

[lcnr]

I don't expect that we're able to convert higher ranked types to some canonical representation

Ok, I have an idea on how to convert higher ranked types to some canonical representation. I just don't think that idea is very good. I also don't know how I would extend this to implication types in the future

[CAD97]

To clarify, is

One and Two are equal types with different type ids

the issue here, and the rest is just exploiting this to demonstrate the unsoundness? (At least this seems to break the guarantees I understand TypeId to be providing... it just isn't exploitable without a way to substitute the "equal" types.)

If this holds, then the resolution is to ether give One and Two the same type id or to make One and Two nonequal types.

Giving One and Two the same type id would be disastrous, as it would allow e.g. dynamically casting for<'a> fn(&'a T) -> &'a T to for<'a> fn(&'a T) -> &'static T.

cc also @eddyb #95845, as using the v0 mangling for TypeId would erase the lifetimes from higher ranked types AIUI. The current impl of #95845 still uses the current hash, so wouldn't be problematic, but this is something to keep in mind w.r.t. the information contained in TypeId vs the v0 type mangling.

(The issue OP ccs itself; this is likely a typo?)

[eddyb]

There is a lot of confusion here wrt all the pieces involved.

Both legacy and v0 mangling, and both the TypeId hash and a v0-mangling-based implementation (like #95845), use the same encoding for higher-ranked lifetimes (it's why the v0 mangling mentions lifetimes at all!), though legacy symbols/type hashes only as the input to the hash.

You couldn't not mangle them because otherwise TypeId::of::<One> and TypeId::of::<Two> would clash in their symbol names (and that's actually how I found out that v0 mangling needed to reason about for<'a>, when implementing it, heh).

That all uses "binder anonymization" so the fully normalized types are:

• One: for<'0> fn(&'0 (), &'0 ())
• Two: for<'0, '1> fn(&'0 (), &'1 ())

The issue here is this broken fragment of type unification code:

rust/compiler/rustc_infer/src/infer/equate.rs

Lines 154 to 159 in cd282d7

	if a.skip_binder().has_escaping_bound_vars() || b.skip_binder().has_escaping_bound_vars() {
	self.fields.higher_ranked_sub(a, b, self.a_is_expected)?;
	self.fields.higher_ranked_sub(b, a, self.a_is_expected)
	} else {
	// Fast path for the common case.
	self.relate(a.skip_binder(), b.skip_binder())?;

This treats (T <: U) + (U <: T) as meaning T = U. But that's not sound at all!

Too much of Rust's typesystem depends on T = U matching "identity" (judgmental syntactic equality if you want) with "enough normalization", so a definition equivalent to "subtyping both ways" only works if it's compatible, and in this case it's not.

I don't think there's an "obvious choice" for which of One or Two should be "the normal form" for the other (Two seems more likely but it still feels dubious), so the correct thing to do (at least in the interim) is to stop using subtyping entirely when dealing with strong equality, and only support anonymizing the binders (which is the only thing done for the maximal normalization used by symbol names and TypeId, tho sadly I don't think we always do it, yet).

Even if we normalized one of One or Two to the other, equality should still not use subtyping, and instead normalize to a common type first, to avoid the "unproven assertion" that "both-ways subtyping" implies "equality" (as opposed to the trivial truth in the other direction, which is given by subtyping reflexivity AFAIK).

[eddyb]

Retitled the issue to reflect the situation as I understand it (TypeId only exposes this the same way e.g. symbol names or any other type-equality-sensitive part of rustc might).

[RalfJung]

One and Two are equal types with different type ids.

In which sense are these types "equal"? Two allows references with different lifetimes, One does not, so those look like different types to me.

Going off the issue title, are you saying they each are a subtype of the other? That is different from saying they are "equal" though. Might be good to update the issue description because this confused the heck out of me until I read #97156 (comment).

Cc #97156

You are Cc'ing an issue in itself? probably a typo, not sure which issue you meant though.

[oli-obk]

Two allows references with different lifetimes, One does not, so those look like different types to me.

Well... from a user perspective any function that will be allowed as a function pointer of type One will also be allowed as a function pointer of type Two. Also any caller to One can just also call Two without any visible behaviour (if the function pointers actually point to the same function).

So they are structurally different, but behaviour wise they are the same. If we had sufficiently smart normalization we could normalize One to Two, just gets hard to do that normalization properly in the presence of more complicated variance (mutable references and interior mutability)

[eddyb]

@RalfJung FWIW I changed the issue title, it was something else before.

In which sense are these types "equal"?

Specifically unification in the Equate mode - we seem to have special-cased "each of the two types is a subtype of the other" to imply "equality" without justifying/enforcing it in a way the rest of the compiler - which mostly relies on Ty<'tcx>: Eq (and I assume that sort of "syntactic match" is equivalent to judgmental equality), especially after post-monomorphization normalization.

---

@oli-obk The normalization wouldn't need to be perfectly clever. You would just perform it before checking for equality (without involving subtyping), just like we do with anonymizing the lifetimes bound by the for<...> to avoid their order (or DefIds) affecting any semantics.

That is, we have to remove the unsound equality-via-subtyping logic and try to cover any breakage with a subset of the possible higher-ranked normalization (e.g. if a lifetime only appears in the outermost fn pointer type's input types, and its variance is the default for that position, so not invariant or otherwise flipped, then it can be split into one lifetime per position) - we could maybe even make this be part of anonymize_late_bound_regions, since that has to replace every one of those lifetime positions anyway.

---

EDIT: I regret using the word "judgmental" (or its misspelling, apparently), because I just remembered that type equality judgments can definitely involve subtyping, that distinction is more about "being built-in" vs reified proofs of type equality (or "paths" in HoTT).
("syntactic" should be correct though, I'll switch to that)