change equate for binders to not rely on subtyping

[spastorino]

summary by @spastorino and @lcnr

Context

The following code:

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. This happens because TypeId::of::<One>() is not the same as TypeId::of::<Two>() despite them being considered the same types by the type checker.

Currently the type checker considers binders to be equal if subtyping succeeds in both directions: for<'a> T<'a> eq for<'b> U<'b> holds if for<'a> exists<'b> T<'b> <: T'<a> AND for<'b> exists<'a> T<'a> <: T<'b> holds. This results in for<'a> fn(&'a (), &'a ()) and for<'a, 'b> fn(&'a (), &'b ()) being equal in the type system.

TypeId is computed by looking at the structure of a type. Even though these types are semantically equal, they have a different structure resulting in them having different TypeId. This can break invariants of unsafe code at runtime and is unsound when happening at compile time, e.g. when using const generics.

So as seen in main, we can assign a value of type Foo::<One> to a binding of type Foo<Two> given those are considered the same type but then when we call deref, it calls downcast_ref that relies on TypeId and we would hit the None arm as these have different TypeIds.

As stated in #97156 (comment), this causes the API of existing crates to be unsound.

What should we do about this

The same type resulting in different TypeIds is a significant footgun, breaking a very reasonable assumptions by authors of unsafe code. It will also be unsound by itself once they are usable in generic contexts with const generics.

There are two options going forward here:

• change how the structure of a type is computed before relying on it. i.e. continue considering for<'a> fn(&'a (), &'a ()) and for<'a, 'b> fn(&'a (), &'b ()) to be equal, but normalize them to a common representation so that their TypeId are also the same.
• change how the semantic equality of binders to match the way we compute the structure of types. i.e. for<'a> fn(&'a (), &'a ()) and for<'a, 'b> fn(&'a (), &'b ()) still have different TypeIds but are now also considered to not be semantically equal.

---

Advantages of the first approach:

• with the second approach some higher ranked types stop being equal, even though they are subtypes of each other

General thoughts:

• changing the approach in the future will be breaking
  • going from first to second may break ordinary type checking, as types which were previously equal are now distinct
  • going from second to first may break coherence, because previously disjoint impls overlap as the used types are now equal
  • both of these are quite unlikely. This PR did not result in any crater failures, so this should not matter too much

Advantages of the second approach:

• the soundness of the first approach requires more non-local reasoning. We have to make sure that changes to subtyping do not cause the representative computation to diverge from semantic equality
  • e.g. we intend to consider higher ranked implied bounds when subtyping to [fix] Implied bounds on nested references + variance = soundness hole #25860, I don't know how this will interact and don't feel confident making any prediction here.
• computing a representative type is non-trivial and soundness critical, therefore adding complexity to the "core type system"

---

This PR goes with the second approach. A crater run did not result in any regressions. I am personally very hesitant about trying the first approach due to the above reasons. It feels like there are more unknowns when going that route.

Changing the way we equate binders

Relating bound variables from different depths already results in a universe error in equate. We therefore only need to make sure that there is 1-to-1 correspondence between bound variables when relating binders. This results in concrete types being structurally equal after anonymizing their bound variables.

We implement this by instantiating one of the binder with placeholders and the other with inference variables and then equating the instantiated types. We do so in both directions.

More formally, we change the typing rules as follows:

for<'r0, .., 'rn> exists<'l0, .., 'ln> LHS<'l0, .., 'ln> <: RHS<'r0, .., 'rn>
for<'l0, .., 'ln> exists<'r0, .., 'rn> RHS<'r0, .., 'rn> <: LHS<'l0, .., 'ln>
--------------------------------------------------------------------------
for<'l0, .., 'ln> LHS<'l0, .., 'ln> eq for<'r0, .., 'rn> RHS<'r0, .., 'rn>

to

for<'r0, .., 'rn> exists<'l0, .., 'ln> LHS<'l0, .., 'ln> eq RHS<'r0, .., 'rn>
for<'l0, .., 'ln> exists<'r0, .., 'rn> RHS<'r0, .., 'rn> eq LHS<'l0, .., 'ln>
--------------------------------------------------------------------------
for<'l0, .., 'ln> LHS<'l0, .., 'ln> eq for<'r0, .., 'rn> RHS<'r0, .., 'rn>

---

Fixes #97156

r? @lcnr

[spastorino]

Firing a crater run as failing tests are related to nightly features and are going to be fixed as soon as PRs like #118118 land.

@bors try

[bors]

⌛ Trying commit 3679fde with merge 5698a58...

[bors]

☀️ Try build successful - checks-actions
Build commit: 5698a58 (5698a58b0ad644406b5e61434ba7c63af6e05169)

[spastorino]

@craterbot check

[craterbot]

👌 Experiment pr-118247 created and queued.
🤖 Automatically detected try build 5698a58
🔍 You can check out the queue and this experiment's details.

ℹ️ Crater is a tool to run experiments across parts of the Rust ecosystem. Learn more

[spastorino]

@bors try

[bors]

⌛ Trying commit d3841fb with merge ab2dc84...

[craterbot]

🚧 Experiment pr-118247 is now running

ℹ️ Crater is a tool to run experiments across parts of the Rust ecosystem. Learn more

[bors]

☀️ Try build successful - checks-actions
Build commit: ab2dc84 (ab2dc84cfc2c30bb279a7cd2bfef172c30260142)

[spastorino]

@craterbot cancel

[craterbot]

🗑️ Experiment pr-118247 deleted!

ℹ️ Crater is a tool to run experiments across parts of the Rust ecosystem. Learn more

[spastorino]

@craterbot check

[craterbot]

👌 Experiment pr-118247 created and queued.
🤖 Automatically detected try build ab2dc84
🔍 You can check out the queue and this experiment's details.

ℹ️ Crater is a tool to run experiments across parts of the Rust ecosystem. Learn more

[lcnr]

r=me after final nits

[spastorino]

@bors r=lcnr rollup=never

[bors]

📌 Commit 4a2e3bc has been approved by lcnr

It is now in the queue for this repository.

[bors]

⌛ Testing commit 4a2e3bc with merge 878c8a2...

[bors]

☀️ Test successful - checks-actions
Approved by: lcnr
Pushing 878c8a2 to master...

[rust-timer]

Finished benchmarking commit (878c8a2): comparison URL.

Overall result: ❌ regressions - no action needed

@rustbot label: -perf-regression

Instruction count

This is a highly reliable metric that was used to determine the overall result at the top of this comment.

	mean	range	count
Regressions ❌ (primary)	-	-	0
Regressions ❌ (secondary)	0.5%	[0.4%, 1.0%]	7
Improvements ✅ (primary)	-	-	0
Improvements ✅ (secondary)	-	-	0
All ❌✅ (primary)	-	-	0

Max RSS (memory usage)

This benchmark run did not return any relevant results for this metric.

Cycles

This benchmark run did not return any relevant results for this metric.

Binary size

This benchmark run did not return any relevant results for this metric.

Bootstrap: 650.957s -> 651.156s (0.03%)
Artifact size: 311.09 MiB -> 311.50 MiB (0.13%)