forked from rust-lang/rust
-
Notifications
You must be signed in to change notification settings - Fork 0
Commit
This commit does not belong to any branch on this repository, and may belong to a fork outside of the repository.
Auto merge of rust-lang#118247 - spastorino:type-equality-subtyping, …
…r=lcnr change equate for binders to not rely on subtyping *summary by `@spastorino` and `@lcnr*` ### Context The following code: ```rust 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 `TypeId`s. As stated in rust-lang#97156 (comment), this causes the API of existing crates to be unsound. ## What should we do about this The same type resulting in different `TypeId`s 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 `TypeId`s 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] rust-lang#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 rust-lang#97156 r? `@lcnr`
- Loading branch information
Showing
22 changed files
with
319 additions
and
112 deletions.
There are no files selected for viewing
This file contains bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
This file contains bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
This file contains bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
This file contains bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
This file contains bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
This file contains bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
This file contains bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
This file contains bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
10 changes: 6 additions & 4 deletions
10
tests/ui/coherence/coherence-fn-covariant-bound-vs-static.stderr
This file contains bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
Original file line number | Diff line number | Diff line change |
---|---|---|
@@ -1,13 +1,15 @@ | ||
error[E0119]: conflicting implementations of trait `Trait` for type `for<'r> fn(fn(&'r ()))` | ||
--> $DIR/coherence-fn-covariant-bound-vs-static.rs:17:1 | ||
warning: conflicting implementations of trait `Trait` for type `for<'r> fn(fn(&'r ()))` | ||
--> $DIR/coherence-fn-covariant-bound-vs-static.rs:22:1 | ||
| | ||
LL | impl Trait for for<'r> fn(fn(&'r ())) {} | ||
| ------------------------------------- first implementation here | ||
LL | impl<'a> Trait for fn(fn(&'a ())) {} | ||
| ^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^ conflicting implementation for `for<'r> fn(fn(&'r ()))` | ||
| | ||
= warning: the behavior may change in a future release | ||
= note: for more information, see issue #56105 <https://github.com/rust-lang/rust/issues/56105> | ||
= note: this behavior recently changed as a result of a bug fix; see rust-lang/rust#56105 for details | ||
= note: `#[warn(coherence_leak_check)]` on by default | ||
|
||
error: aborting due to 1 previous error | ||
warning: 1 warning emitted | ||
|
||
For more information about this error, try `rustc --explain E0119`. |
This file contains bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
Oops, something went wrong.