Typesystem soundness hole involving cyclically-defined ATIT, and normalization in trait bounds #135011
Comments
rustbot
added
needs-triage
With LLVM assertions enabled, I get this instead of just a SIGILL: and if I pass I believe the difference you're observing on nightly is #133499 cc @nikic Oh oops, we document that IR is not verified by default, so it's definitely intentional that on nightly we crash somewhat incoherently with invalid IR. |
jieyouxu
removed
the
needs-triage
|
@steffahn Can you (or anyone else having context here) please provide a digestible summary of this issue? What is happening that shouldn't?
By reading this sentence I infer that it's not a simple regression. Would you like the appropriate team to discuss this? Thank you from the triage. |
|
It's not really a regression at all in the conventional sense. |
|
@apiraino I meant to write “this is not a regression” but in the most technical sense of “introduction of GATs make type system unsound” it's perhaps technically a regression; sorry for the confusing wording. [The interpretation of “introduction of GATs make type system unsound” is assuming I don't find a way to rewrite the reproduction without relying on GATs.] |
steffahn
changed the title
|
To help with understanding of the first step involved in this soundness issue, it's a cyclically defined associated type; the pattern is mirroring the following reduced example // take a trait `Impossible` that no type should be allowed/able to implement
// not even implemented by trait objects
trait Impossible: Sized {}
trait MetaImpossible {
type Assoc: Impossible;
}
trait MetaMetaImpossible {
type Assoc: MetaImpossible;
}
impl<T: MetaMetaImpossible> MetaImpossible for T {
type Assoc = <T::Assoc as MetaImpossible>::Assoc;
}
impl MetaMetaImpossible for () {
type Assoc = ();
}
// now `()` implements `MetaImpossible`,
// and thus technically `<() as MetaImpossible>::Assoc` implements `Impossible`
// Making this into a real issue is “just” a question of whether we can make use
// of this illegal implementation, without “mentioning” `<() as MetaImpossible>::Assoc`
// too concretely, in a way that would motivate the compiler to actually try
// to reduce/simplify the type `<() as MetaImpossible>::Assoc` according to the `impls`
// of `MetaMetaImpossible for ()` and `<T: MetaMetaImpossible> MetaImpossible for T`.If the above was already somehow (systematically) forbidden, that could theoretically be way to close this soundness issue. Possible caveats:
|
|
edit: I started writing this before steffahn's update right above mine, and didn't notice it before I sent this out. Looks like my point 1 is the same one they brought up There are two possible locations where this is going wrong:
impl<P: TyEqImpl + DeriveEqFromImpl> TyEq for P {
type ProofDef = <P::Proof as TyEq>::ProofDef;
}The problem with this impl is that it doesn't actually provide a concrete type for As a bit more evidence, specializing the impl for impl<L, R> TyEq for FakeRefl<L, R> {
type ProofDef = <<FakeRefl<L, R> as TyEqImplPrf<()>>::Proof as TyEq>::ProofDef;
}
I don't see anything else that could be going wrong right now, the rest looks fine. |
This mechanism is used twice actually. The other place is between Inside Outside, where |
|
Another place of interest is here struct RewriteReflRight<P>(P);
impl<P> DeriveEqFromImpl for RewriteReflRight<P> {}
impl<P, L, R> TyEqImpl for RewriteReflRight<P>
where
P: TyEq<LHS = L, RHS = R>,
{
type LHS = L;
type RHS = R;
type Proof<_Dummy: RewriteReflRightHelper> = _Dummy::RewriteRight<Refl<L>, R, P::ProofDef>;
type ProofValue = Refl<L>;
type ProofIsProofValue = Refl<Refl<L>>; // <- HERE! #######################################
}[I collapsed the rest of this response, as it has become a bit long&rambly with multiple follow-up comments in edits. This doesn't add too much in describing the issue. But please feel free to read for rough ideas on a possible direction of a fix.]This section has become a bit unstructured / stream-of-consciousness, sorry for that. With the edits below, I explore aspects of the meaning/semantics of trait bounds on associated items, and how this issue might be fixable with the compiler collecting extra obligations for checks based on those semantics, which would then need to the be executed during monomorphization. In this code section (marked ProofIsProofValue: TyEq<LHS = Self::Proof<()>, RHS = Self::ProofValue>is fulfilled. Filling in the definitions, that's Refl<Refl<L>>: TyEq<LHS = <()>::RewriteRight<Refl<L>, R, P::ProofDef>, RHS = Refl<L>>It does this by being to do this with the So the compiler was able to reduce the left sides of the required So that is: reducing <()>::RewriteRight<Refl<L>, R, P::ProofDef>to Refl<L>which involves looking into / applying the type definitions of the generic Notably, it does this reduction happens in a context where Then, for concrete types, we can evaluate e.g. you could even write in let r: <RewriteReflRight<FakeRefl<Vec<u8>, String>> as TyEqImpl>::ProofIsProofValue = Refl(Refl(vec![]));and that works fine. Now, if the intended contract for associated types in traits (in the context of the possibility of cyclical, non-terminating definitions) is something like “if the associated type can be evaluated/normalized (post-monomorphization), then it has the promised trait bound” then we would have a problem at this exact place. Perhaps more accurately even, the contract could be “if the associated type can be evaluated/normalized (post-monomorphization), and all types appearing in the trait bound can be evaluated/normalized; then it has the promised trait bound”. Or something along those lines… Roughly speaking: With such a contract established, the compiler would need to pay attention during normalization/projection in generic contexts, and notice how in particular the type Edit: Actually, to be fair, the trait bound here also involves So another possible place to blame might actually be
It even seems to be able to call a function with that bound explicitly, e.g. fn transmute_inner_1<L, R, P: TyEq<LHS = L, RHS = R>>(x: L) -> R {
transmute_inner_2__::<<P::ProofIsProofValue as TyEq>::ProofDef, L, R, P::ProofValue, P>();
// call::<P::Proof<()>>(); // fails
transmute_inner_2::<<P::ProofIsProofValue as TyEq>::ProofDef, L, R, P::ProofValue, P>(x)
}
fn call<T>() {}
fn transmute_inner_2__<Rw, L, R, Actual, P: TyEq<LHS = L, RHS = R, ProofValue = Actual>>()
where
P::Proof<()>: TyEq<LHS = L, RHS = R>,
{
}however, only once the type Perhaps Edit2: This is interesting. I guess it would make sense if Hence, the usual case of calling a function with a Edit3: Coming back to the situation around
then it seems that associated types are quite distinct in a relevant manner. The trait bound on type ProofIsProofValue: TyEq<LHS = Self::Proof<()>, RHS = Self::ProofValue>;actually only mentions The user in More precisely thus, a concept of “all types appearing in the trait bound can be evaluated/normalized” would probably need to only talk about “types appearing in the trait bound in parameters (not associated types)”. Although to be fair, it's hard to say – perhaps multiple different contracts could actually work, as long as the compiler made sure that all places that remove any of the implicit “evaluation must terminate during monomorphization”-style requirement from a trait bound do instead add the same requirement to the definition/“body” of the associated type and/or function that did so. |
steffahn
changed the title
steffahn
changed the title
|
During the (unfinished) process of trying to get to a more minimal reproducing example eventually, I did come across a version of this that works ever since Rust 1.1. (<- this is not an easier to understand version, but it might be of interest as a test case.) [In Rust 1.1 on compiler-explorer] |
apiraino
removed
the
I-prioritize
|
i've been playing with this to make sure I have a full understanding of how exactly this exploit works (and have a bunch of thoughts on how to fix it), a WIP minimization from first principles: https://rust.godbolt.org/z/WxTfWo3jb // An always applicable impl.
trait ProjectTo {
type Usize;
type This;
type Myself;
}
impl<T> ProjectTo for T {
type Usize = usize;
type This = T;
type Myself = T;
}
// A diverging associated type whose item-bound must not apply
// and differs from an always applicable impl.
trait Diverges {
type Diverge<T: Diverges>: ProjectTo<Usize = &'static str>;
}
impl Diverges for () {
type Diverge<T: Diverges> = T::Diverge<()>;
}
// We need to transfer the item bound to an existing type while only
// using the diverging associated type in a generic context.
//
// The idea is to use an indirection which uses the diverging associated type
// in a where-clause. This then uses its item-bound in the caller and normalizes
// via the applicable impl internally.
//
// `<T as Apply<D::Diverge<()>>::Assoc` for `D: Diverge` has
// an invalid item-bound and can be normalized to a concrete type while
// `D` is still generic.
trait Apply<D> {
type Assoc: ProjectTo<Myself = usize>;
}
impl<T: ProjectTo<Myself = <D as ProjectTo>::Usize>, D> Apply<D> for T {
type Assoc = T;
}
// It's still difficult to actually using this item bound as we must
// avoid `D::Diverge<()>` being mentioned in the MIR. We otherwise
// try to normalize it during codegen and error with overflow instead.
fn transmute<D: Diverges>(x: &usize) -> &&'static str {
// We need to prove the where-bounds here while `D` is still generic
// as they mention `D::Diverge<()>`.
//
// We normalize `<&'static str as Apply<D::Diverge<()>>>::Assoc` to `&'static str`
// here. We therefore need to prove `&'static str: ProjectTo<This = &'static str>`
// and `&'static str: Apply<D::Diverge<()>>`. Proving the second where-clause relies
// on the item bound of `D::Diverge<()>`.
provide_where_bound::<D, _>(x)
}
// `<T as ProjectTo>::This` normalizes to the rigid associated type
// `<T as Apply<D::Diverge<()>>>::Assoc` inside of this function.
fn provide_where_bound<D: Diverges, T>(x: &usize) -> &T
where
T: ProjectTo<This = <T as Apply<D::Diverge<()>>>::Assoc>,
T: Apply<D::Diverge<()>>,
{
// We therefore prove `<T as Apply<D::Diverge<()>>>::Assoc: ProjectTo<Myself = usize>`
// here. This holds thanks to the item-bound.
apply_where_bound::<T>(x)
}
// `<T as ProjectTo>::This` normalizes to `T` inside of this function.
// THis means we've now get the incorret where-bound `T: ProjectTo<Myself = usize>`
// inside of this function. Exploiting this is trivial.
fn apply_where_bound<T>(x: &usize) -> &T
where
<T as ProjectTo>::This: ProjectTo<Myself = usize>,
{
via_impl::<T>(x)
}
fn via_impl<T>(x: &<T as ProjectTo>::Myself) -> &T {
x
}
pub fn main() {
println!("{}", transmute::<()>(&0));
}I recently thought about diverging associated types themselves and expected them to be theoretical unsound, cc rust-lang/trait-system-refactor-initiative#133. I have not been able to craft an actual example back then as I mostly considered their interactions with the occurs check Good job @steffahn. This is a wonderful unsoundness and I am incredibly excited about it :3 |
|
Is this more “minimal”? I don’t know… but it’s certainly more concise… more dense… anyway 😅 trait Tr: Sized {
type Eq<T>;
type EqLPrf<R>: Tr<Eq<Self> = Self::Prf<Self, R>>;
type Prf<L, R>: Tr<Eq<L> = R>;
type Rw<L: Tr<Eq<L> = <<R as Tr>::Prf<R, L> as Tr>::Eq<R>>, R>: Tr<Eq<L> = R>;
fn transmute<R>(self) -> R;
}
impl<L_> Tr for L_ {
type Eq<T> = T;
type EqLPrf<R: Tr> = L_;
type Prf<L: Tr<Eq<L> = L>, R: Tr> = L::Rw<L, R>;
type Rw<L: Tr<Eq<L> = R>, R> = L;
fn transmute<R: Tr>(self) -> <<R::EqLPrf<L_> as Tr>::Eq<R> as Tr>::Eq<R> {
self
}
}
fn main() {
let s: String = vec![65_u8, 66, 67].transmute();
println!("{}", s); // ABC
}Edit: Eliminating/combining some more types… trait Tr: Sized {
type Eq<T>;
type Prf<L, R>: Tr<Eq<L> = R>;
fn transmute<L: Tr, R>(l: L) -> R;
}
impl<__> Tr for __ {
type Eq<T> = T;
type Prf<L: Tr<Eq<<R::Prf<R, L> as Tr>::Eq<R>> = R>, R: Tr> = L;
fn transmute<L, R: Tr>(l: L) -> <R::Prf<R, L> as Tr>::Eq<R> {
l
}
}
fn main() {
let s: String = <()>::transmute(vec![65_u8, 66, 67]);
println!("{}", s); // ABC
} |
|
I'll make this one into a follow-up because it's getting a bit wild; only one (generic) associated type is enough trait Tr: Sized {
type Prf<L, R>: Tr<Prf<L, ()> = R>;
fn transmute<R>(self) -> R;
}
impl<L_> Tr for L_ {
type Prf<L: Tr<Prf<<R::Prf<R, L> as Tr>::Prf<R, ()>, ()> = R>, R: Tr> = L;
fn transmute<R: Tr>(self) -> <R::Prf<R, L_> as Tr>::Prf<R, ()> { self }
}
fn main() {
let s: String = vec![65_u8, 66, 67].transmute();
println!("{}", s); // ABC
}or, with a bit less trait Tr: Sized { type Prf<R>: Tr<Prf<R> = Self>; }
impl<L> Tr for L {
type Prf<R: Tr<Prf<R> = <L::Prf<R> as Tr>::Prf<R>>> = R where L: Tr;
}
fn transmute<L: Tr, R>(r: L) -> <L::Prf<R> as Tr>::Prf<R> { r }
fn main() {
let s: String = transmute::<_, String>(vec![65_u8, 66, 67]);
println!("{}", s); // ABC
}the trait Tr<R>: Sized { type Prf: Tr<R, Prf = Self>; }
impl<L, R> Tr<R> for L {
type Prf = R where L: Tr<R>, R: Tr<R, Prf = <L::Prf as Tr<R>>::Prf>;
}
fn transmute<L: Tr<R>, R>(r: L) -> <L::Prf as Tr<R>>::Prf { r }
fn main() {
let s: String = transmute::<_, String>(vec![65_u8, 66, 67]);
println!("{}", s); // ABC
} |
trait Tr<R>: Sized { type Prf: Tr<R, Prf = Self>; }
impl<L, R> Tr<R> for L {
type Prf = R where L: Tr<R>, R: Tr<R, Prf = <L::Prf as Tr<R>>::Prf>;
}
fn transmute<L: Tr<R>, R>(r: L) -> <L::Prf as Tr<R>>::Prf { r }
fn main() {
let s: String = transmute::<_, String>(vec![65_u8, 66, 67]);
println!("{}", s); // ABC
}that minization is actually a separate unsoundness (or at least what I intend to do to fix the original is insufficient there 💀). That sure is something |
// We only check that GAT where-clauses of the *trait* while normalizing;
// normalizing `<T as Trait<U>>::Proof` to `U` trivially succeeds.
trait Trait<R>: Sized {
type Proof: Trait<R, Proof = Self>;
}
impl<L, R> Trait<R> for L {
// We prove that the impl item is compatible with the trait in the
// env of the trait, which is pretty much empty.
//
// `L: Trait<R>` is trivial
// `R: Trait<R, Proof = <L::Proof as Trait<R>>::Proof>` normalizes to
// `R: Trait<R, Proof = <R as Trait<R>>::Proof>` normalizes to
// `R: Trait<R, Proof = R>` is trivial
//
// Proving the item-bound holds assumes the *impl where-bounds*.
// We normalize the where-bound `R: Trait<R, Proof = <L::Proof as Trait<R>>::Proof>`
// by using the item-bound of `L::Proof`: `R: Trait<R, Proof = L>` 💀¹. Proving the
// item-bound of `<L as Trait<R>>::Proof` is now trivial.
type Proof
= R
where
L: Trait<R>,
R: Trait<R, Proof = <L::Proof as Trait<R>>::Proof>;
}What's happening at ¹ is that proving that the item-bounds of an associated type is able You've found a new way to exploit rust-lang/trait-system-refactor-initiative#62, answering the question posed in rust-lang/trait-system-refactor-initiative#116 😊 |
|
My perspective of the original unsoundness is that we're able to rely on the item-bounds of an associated type while never actually normalizing the associated type, which is unsound in case it diverges. While your new minimization does not actually have any associated type which diverges. We're able to normalize |
Oh… that’s interesting! I didn’t even really pay attention to the fact that it’s no longer containing containing any “cyclically defined ATIT”, at least for certain notions of “cyclically defined”. I got there (to the minimization) in a relatively incremental/step-by-step manner; but that certainly explains why I was having a hard time [i.e. not succeeding in] trying to translate the last version back into one without ATIT- |
|
Alright, have a minimization I am happy with now and feel like I properly understand this bug: // Always applicable impls. Using two separate traits
// for clarity/simplicity.
trait IdA {
type This;
}
impl<T> IdA for T {
type This = T;
}
trait IdB {
type This;
}
impl<T> IdB for T {
type This = T;
}
trait Trivial {
type Usize;
}
impl<T> Trivial for T {
type Usize = usize;
}
// A diverging associated type whose item-bound must not apply
// and differs from an always applicable impl.
trait Diverges<T> {
type Diverge<Recur: Diverges<T>>: Trivial<Usize = T>;
}
impl<T> Diverges<T> for () {
type Diverge<Recur: Diverges<T>> = Recur::Diverge<()>;
}
// An impl with a where-clause which is normalized using the blanket impl when
// checking that its item-bounds hold. We then prove that where-clause via the
// incorrect item-bound from above.
//
// This allows us to transfer the item-bound to a concrete type while only
// using the diverging associated type in a generic context.
//
// Concretely, this is impl is well-formed as `<T as IdA>::This` normalizes to
// `<Recur as Trivial>::Usize` which is then normalized to `usize` by using
// the blanket impl. This means `<T as IdA>::This: IdB<This: Copy>` trivially
// holds.
//
// This means it should only be possible to instantiate it with `usize` itself.
// Instantiating `Recur` with `<D as Diverges<T>>::Diverge<()>` causes it to apply
// for all `T` instead.
trait Apply<D> {
type Assoc: IdB<This: Copy>;
}
impl<T: IdA<This = <Recur as Trivial>::Usize>, Recur> Apply<Recur> for T {
type Assoc = <T as IdA>::This;
}
fn copy_me<T, D: Diverges<T>>(x: T) {
// Need to prove the where-bounds of `provide_where_bound` in a generic context
// as normalizing `D::Diverge<()>` would otherwise overflow.
//
// Using the impl of `Apply` requires `T: IdA<This = <D::Diverge<()> as Trivial>::Usize>`.
// We normalize `<D::Diverge<()> as Trivial>::Usize` to `T` using the item-bound of
// `D::Diverge<()>` at which point the impl trivially applies.
provide_where_bound::<D, T>(x)
}
fn provide_where_bound<D: Diverges<T>, T>(x: T)
where
T: IdA<This = <T as Apply<D::Diverge<()>>>::Assoc>,
T: Apply<D::Diverge<()>>,
{
// Inside of this function `<T as Apply<D::Diverge<()>>>::Assoc` is rigid,
// allowing us to use its incorrect item-bound.
//
// <<T as IdA>::This as IdB>::This: Copy
// ------------------------------------- normalize `<T as IdA>::This` via where-bound
// <<T as Apply<D::Diverge<()>>>::Assoc as IdB>::This: Copy
// -------------------------------------------------------- prove via item-bound
apply_where_bound::<T>(x)
}
fn apply_where_bound<T>(x: T)
where
<<T as IdA>::This as IdB>::This: Copy,
{
// We simply normalize `<<T as IdA>::This as IdB>::This` to `T` inside of this
// function.
dup(x, x)
}
fn dup<T>(_x: T, _y: T) {}
pub fn main() {
copy_me::<String, ()>(String::from("hello there"));
}As mentioned by @nikomatsakis in rust-lang/trait-system-refactor-initiative#133 (comment) we've got a few ways forward here. I expect that the most likely approach will be to make sure we recheck where-clauses of functions during monomorphization to trigger the overflow at this point. Eagerly detecting potentially diverging associated types feels impossible to me without breaking too much existing code. @compiler-errors has implemented this in #135216 for a crater run. Landing this may be blocked on the new solver as it will likely cause new overflow errors due to hitting the recursion limit. These are fatal with the old trait solver. |
|
Small note that may be of interest: this also works: trait Diverges<T> {
type Diverge<Recur: Diverges<T>>: Trivial<Usize = T>;
}
impl<T> Diverges<T> for () {
type Diverge<Recur: Diverges<T>> = Recur::Diverge<Recur>; // `::Diverge<Recur>` instead of `::Diverge<()>`
}In other words, there's no need for a self-recursive trait impl for this. This is in fact the classic exploit for how to construct a non-terminating term in a language that allows for non-positive recursion ( Also tiny simplification: you don't need to involve impl<Recur> Apply<Recur> for () {
type Assoc = <Recur as Trivial>::Usize;
}I made my own version of this to help me understand. |
|
I've tried to minimize a GAT-free version (and no trait Rewrite<R>: Sized {
type Result: Multi<(), Simpl = Self>;
}
impl<L, R, E> Rewrite<R> for L
where
<E as Equal<<L as Equal<R>>::To>>::To: Multi<(), Simpl = L>,
R: Multi<L, Cyclic = E>,
{
type Result = <L as Equal<R>>::To;
}
trait Equal<R>: Sized {
type To: Multi<Self>;
}
impl<L, R> Equal<R> for L {
type To = R;
}
trait Multi<L>: Sized {
type Cyclic: Equal<<L as Equal<Self>>::To, To = L>;
type Simpl: Multi<(), Simpl = <L as Rewrite<Self>>::Result>;
}
impl<L, R> Multi<L> for R
where
L: Equal<R>,
{
type Cyclic = <L::To as Multi<L>>::Cyclic;
type Simpl = L::To;
}
fn transmute<L, R>(x: L) -> R
where
R: Multi<L, Simpl = R>,
{
transmute_inner_1::<L, R>(x)
}
fn transmute_inner_1<L, R>(x: L) -> <R as Multi<L>>::Simpl
where
R: Multi<L>,
L: Rewrite<R>,
{
transmute_inner_2::<<R as Multi<L>>::Simpl>(x)
}
fn transmute_inner_2<R>(x: <<R as Multi<()>>::Simpl as Multi<()>>::Simpl) -> R {
x
}
fn main() {
let s: String = transmute(vec![65_u8, 66, 67]);
println!("{:?}", s); // ABC
}(on 1.49 in compiler-explorer) This is rather minimized for "size" (fewer traits, fewer associated types), not for ease of understanding. Which also means traits and types get dual use and are hard to name; like |
|
Of course, given the 1.1 version exists, that’s not a full soundness regression at that point, but it still seems interesting 1.49 keeps coming up here. So I was curious where exactly the relevant change was lying: Bisection this points to #80246 being relevant… which also explains the remarkably confusing bisection behavior, lol. (I had to go 2 release cycles newer than the anticipated nightly range; but the PR apparently was beta-backported very close before a release). It’s funny that the PR description reads like the change was mainly about becoming more restrictive, but apparently for this code, effectively the compiler became more lenient instead? Edit: There’s a second relevant bisection point. The code between stable versions goes from not compiling due to a (huge) list of overflow and mismatch errors (this is rather lengthy… click to expand)directly to the code working. On nightly, there’s an intermediate step, where it returns a different, shorter error which goes away with the abovementioned #80246. Out of curiosity, I've bisected this earlier point of change now as well, and the relevant PR appears to be #73905 |
This isn't quite trivial, but well… it works.
a “transmute” in safe Rust:
(playground)
Besides this unsoundness, there are also many ICEs. This isn't surprising, since we're not really transmuting, but rather sort-of … convincing the type system that the 2 types were never different in the first place.
Or interesting LLVM-errors
Oh… that one on nightly has… the compiler itself execute a SIGILL? (Is that actual UB in the compiler!? Or UB in LLVM? Or can SIGILL be part of a deliberate crash condition?)
From a background of “this works a bit like Coq”, the relevant parts that make this work is how:
FakeRefl<L, R>is a “proof” thatLandRare the same types, which doesn't terminate (i.e. it is cyclically defined in terms of itself)Rewrite…step which rewritesRefl<L>(a proof ofTyEq<LHS = L, RHS = R>) using thisFakeReflproofFakeReflbefore its (indirectly and cyclically defined)ProofDeftype ever ends up being instantiatedOf course, this is just my intuitive description from a user perspective :-)
I have no idea which part of this code to blame exactly. Perhaps someone else with better knowledge of the theory behind Rust's typesystem and trait system could have a better clue here.
I'm not quite sure ifthis can perhaps be "simplified" to remove the need for GATsUpdate: It can be "simplified" to remove the need for GATs. (playground)
Update2: It's even possible to rework this into working since Rust 1.1
(this section has become somewhat outdated due to this update, click to expand anyway)
I'm not quite sure if this can perhaps be "simplified" to remove the need for GATs; however, I wasn't able to the
Rewrite…stuff to work without this trickwhere the (vacuous)
_Dummy: RewriteReflRightHelperrestriction prevents the compiler from already knowing the concreteRewriteReflRightHelperimpl. (If you worry about the syntactical mismatch ofhere vs
without bounds on
_Dummyin the trait definition: that's actually avoidable (<- see this playground on how the bound can be repeated everywhere and theimpl RewriteReflRightHelper for …can even be for a concrete type only).So for now, I would conjecture that this soundness hole does require GATs.
Edit: I completely forgot about the (generous) usage of GATs inside of
RewriteReflRightHelper~ so, yes, GATs seem fairly integral to this.Edit2: Nevermind, those can all be eliminated leaving only a single GAT.
(end of somewhat outdated section)
This is not a regression. It also isn't influenced by
-Znext-solver.This is a relatively clean typesystem hole, on stable Rust, without many of the other known-problematic features such as HRTBs, lifetimes, variance, trait objects, or implicitly defined trait impls for functions/closures/etc…
@rustbot label I-unsound, I-ICE, I-crash, T-types, A-type-system, A-trait-system, A-associated-items
The text was updated successfully, but these errors were encountered: