-
Notifications
You must be signed in to change notification settings - Fork 12.9k
New issue
Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.
By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.
Already on GitHub? Sign in to your account
unsoundness relating to WF requirements on trait object types #44454
Comments
Actually, thinking about this more, the problem is maybe not quite how I was thinking of it. That is, it seems like the problem lies in the definition of object safety. That is, if you imagine that you had to write the impl for impl<X> Animal<X> for Animal<X> { ... } and this would fail the well-formedness checks because The goal of the object safety rules are to ensure such an impl could be written. Maybe the rules of object safety have to be more conditional -- i.e., |
Here is an actual unsoundness, using |
This looks similar to #27675 - in both cases we have a trait object that is not WF. I think a reasonable way to solve this would be to have a trait object predicate depend on a 'λ₀...'λₙ lifetimes
τ₀...τₙ types
Trait object-safe
~~WF(for<...> Trait<'λ₀...'λₙ, τ₀...τₙ>) - this part is new~~
WF(for<...> Trait<'λ₀...'λₙ, τ₀...τₙ>: Trait<'λ₀...'λₙ, τ₀...τₙ>) - this part is new
----------------
for<...> Trait<'λ₀...'λₙ, τ₀...τₙ>: for<...> Trait<'λ₀...'λₙ, τ₀...τₙ> |
The "this part is new" part is actually more subtle than I realized. Object types (aka
And the idea is that if the trait is object-safe, we can write a "compiler impl" impl<'λ₀...'λₙ, τ₀...τₙ> Traitl<'λ₀...'λₙ, τ₀...τₙ> for dyn Trait<'λ₀...'λₙ, τ₀...τₙ> {
// ...
} If we want to write such an impl, we need the where-clauses on the trait (both associated types and others) to hold. For supertraits, this follows by obvious induction. For other constraints, this is something that won't hold by itself. Therefore, we probably need to add these other predicates as conditions on the impl, and have impl<'λ₀...'λₙ, τ₀...τₙ> Trait<'λ₀...'λₙ, τ₀...τₙ> for dyn Trait<'λ₀...'λₙ, τ₀...τₙ>
where WF(Trait<'λ₀...'λₙ, τ₀...τₙ>: dyn Trait<'λ₀...'λₙ, τ₀...τₙ>)
{
// ...
} |
I agree that it is the same as #27675. As we said on IRC, I think that the current fix is roughly as I described here -- in particular, when we check that |
Shall we close this as a dupe, then? |
ping @arielb1 -- whatever happened with your branch here? I remember we had some discussions about cycles and don't recall how (if at all) they were resolved. |
Marking P-medium. While there's overlap with #27675, this issue has more in-depth information. We plan to keep them both open until fixed. |
We agreed that this issue and #27675 shared a similar root cause, but my weaponized example still compiles on both stable and nightly and is still unsound. I did not know about #73905 until now, but it seems to only have fixed the case of Conversely, it’s less obvious why there should be a problem with The reason being that lifetime requirements are syntactic and if you allow rust-lang/chalk#203 describes a formal solution under the full implied bounds setting (it would need to be slightly adapted for RFC 2027 ). I think an easy fix with the current limited form of implied bounds would just be to collect all lifetimes appearing in |
another repro for the same issue (i think) trait Trait<ARG: 'static>: 'static {
type Assoc: AsRef<str>;
}
fn hr<T: ?Sized, ARG>(x: T::Assoc) -> Box<dyn AsRef<str> + 'static>
where
T: Trait<ARG>
{
Box::new(x)
}
fn extend_lt<'a>(x: &'a str) -> Box<dyn AsRef<str> + 'static> {
type DynTrait = dyn for<'a> Trait<&'a str, Assoc = &'a str>;
hr::<DynTrait, _>(x)
}
fn main() {
let extended = extend_lt(&String::from("hello"));
println!("{}", extended.as_ref().as_ref());
} |
@rustbot claim |
We looked at this in the types meeting -- none of the the existing reproductions compile anymore -- but we're not sure if this is truly fixed or not. It's not clear what made them stop compile. A good first step would be bisecting to see what PR fixed this example: |
searched nightlies: from nightly-2020-01-01 to nightly-2022-11-30 bisected with cargo-bisect-rustc v0.6.4Host triple: x86_64-unknown-linux-gnu cargo bisect-rustc --access github --regress error so it was fixed by #99217 |
it looks like the original unsoundness was fixed before #99217, it seems like that stopped compiling in 1.61. @Nilstrieb can I get you to bisect this one as well? use std::any::Any;
trait Animal<X>: 'static { }
trait Projector {
type Foo;
}
impl<X> Projector for dyn Animal<X> {
type Foo = X;
}
fn make_static<'a, T>(t: &'a T) -> &'static T {
let x: <dyn Animal<&'a T> as Projector>::Foo = t;
let any = generic::<dyn Animal<&'a T>, &'a T>(x);
any.downcast_ref::<&'static T>().unwrap()
}
fn generic<T: Projector + Animal<U> + ?Sized, U>(x: <T as Projector>::Foo)
-> Box<dyn Any>
{
make_static_any(x)
}
fn make_static_any<U: 'static>(u: U) -> Box<dyn Any> {
Box::new(u)
}
fn main() {
let a = make_static(&"salut".to_string());
println!("{}", *a);
} |
I got
Unfortunately, there is no CI builds anymore for this range, and I do not have the power to bisect those commit myself now. Reproduce with |
I'm guessing it was @compiler-errors' #92285 |
that's cool, looks like we only need the add ui tests and can then close this issue 🎉 |
Signed-off-by: Yuki Okushi <[email protected]>
…errors Add some regression tests for rust-lang#44454 Closes rust-lang#44454 r? `@compiler-errors` Signed-off-by: Yuki Okushi <[email protected]>
…iaskrgr Rollup of 6 pull requests Successful merges: - rust-lang#105411 (Introduce `with_forced_trimmed_paths`) - rust-lang#105532 (Document behaviour of `--remap-path-prefix` with several matches) - rust-lang#105537 (compiler: remove unnecessary imports and qualified paths) - rust-lang#105539 (rustdoc: Only hide lines starting with `#` in rust code blocks ) - rust-lang#105546 (Add some regression tests for rust-lang#44454) - rust-lang#105547 (Add regression test for rust-lang#104582) Failed merges: r? `@ghost` `@rustbot` modify labels: rollup
So @scalexm pointed me at this curious example:
There's a lot going on here, but the key point is that, in the call to
foo::<Animal<&'a i32>, &'a i32>
, we assume thatAnimal<&'a i32>: Animal<&'a i32>
. This is reasonable, since it's a trait object type -- however, it is a malformed trait object type, and hence one where no impl could ever exist (i.e., we could never make an instance of this type). Interestingly, we are not smart enough to extend this to the case where the'static
bound is applied directly (hence the commented out call tobaz::<Animal<&'a i32>>
.At the very least, this is inconsistent behavior, but I feel like there is an unsoundness lurking here. What makes me nervous is that we say that a projection type
<P0 as Trait<P1...Pn>>::Foo
outlives'a
ifPi: 'a
for alli
. I am worried that you could use an impl like this:to prove then that
<Animal<&'a i32> as Projector>::Foo
outlives'static
(say). I have not yet quite managed to weaponize this, but I got pretty close -- that's a gist in which we invoke a functionis_static<U: 'static>(u: U)
whereU
will be of type&'a i32
when monomophized. If rustc were as smart as chalk, I suspect we could easily craft a transmute of some kind to&'static i32
. There may be a way to do it within current rustc too.I'm not sure what's the best fix here. I suspect we should require that trait object types meet the WF requirements declared on the trait; and yet, I think the reason we did not is because we don't know the
Self
type, which means we can't fully validate that. =) This also feels a mite inconsistent with implied bounds. (Perhaps most likely is that we could tweak the WF rules for trait objects to specifically target lifetime bounds, but I have to think about that, feels .. hacky?)We could tweak the notion of what type parameters are constrained -- or at least which may appear in a projection. e.g., we could disallow that impl of
Projector
forAnimal<X>
, becauseX
would not be considered "sufficiently" constrained to appear intype Foo = ...
. Backwards incompatible, obviously, and feels unfortunate.This causes actual unsoundness, as discovered by @scalexm in #44454 (comment);
cc @arielb1 @aturon
The text was updated successfully, but these errors were encountered: