-
Notifications
You must be signed in to change notification settings - Fork 13.4k
Implied bounds / well-formedness of references treats contravariant lifetimes the same as covariant #106431
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
Comments
From talking to @BoxyUwU; there's an alternate way to look at this:
This all makes sense and is consistent. The tricky thing is the first line: implied bounds come from well-formedness, and there's not an actual WF reason for contravariant lifetimes to behave that way: In fact, the syntax I think the real issue here is:
We should probably better document implied bounds, and consider relaxing how they work around contravariant lifetimes. (as far as the Yoke issue, I do have a fix I can apply; though I'd rather not have to, I know it's going to take a while for there to be motion on this in any direction) |
FWIW I'm happy to sit down and document WF/implied bounds if someone can tell me where it should go and help me with specifics, like, which things are WFness and which bounds are implied. |
I don't think this is an issue with variance. The real issue here is that all lifetimes that appear on trait objects and fn pointers are treated as "outlives components" of the underlying type. This can occur with invariant and covariant lifetimes as well. Here is an example with invariant lifetime trait Trait<'a> {}
fn test<'a>(_: &'static dyn Trait<'a>) { // implies 'a: 'static !!
None::<&'static &'a ()>; // check 'a: 'static
} This might not be desired and can lead to surprising behavior, like
Universal quantifiers for trait bounds is bounded by the condition that trait input types must be well-formed. For example, the trait bound |
That is in fact what is being referred to here with respect to "variance", as the actual way of expressing this conversation involves wheeling out predicates in a language that is not Rust (logic) because Rust only interprets lifetime bounds in contextual manners... i.e. variance... and thus having an overly consistent behavior in terms of creating outlives requirements here is inconsistent with how the lifetimes in question are read and written. That is a problem whether or not it is a strict "soundness issue" in the compiler, because the underlying thesis of Rust is that the combination of unsafe code with lifetimes can be used to create programs that constrain behavior to what is sound. And that means it needs to, as much as possible, not fall down into a pile of miserable edge-cases when it comes to actually trying to do that. |
I have fixed the tags. The categories are made for humanity, humanity was not made for the categories. Let's not bog down this issue's comment thread with further haggling over whether it is "unsound" or merely "surprising", please. |
I don’t see good ways to change the current behavior here, but feel free to point out where I might not be seeing the way out. The proposition of this issue – or perhaps feature request – is that
If the invariant case where So I guess the invariant case would need to become But then implementing such a closure could become next to impossible in the invariant case: If the closure body did not get to infer As far as I can tell, the proposed argument here might be that we want something like Even if we made sure that every contravariant (in For illustration: For example, if
|
WG-prioritization assigning priority (Zulip discussion). @rustbot label -I-prioritize +P-medium |
Yeah, I agree. I do think this is a niche behavior that needs to be documented somewhere. I might take a crack at it. |
I spent some time trying to create full-blown unsoundness example based on this bug. I. e. to create program, which will print garbage or something similar. I was unable to do so. It seems that described behavior is not a bug. It is simply deliberate design. Currently existence of type Moreover, currently So, So, this "bug" is not really bug, unless you want to redesign But this means that we should very clearly describe meaning of |
I also believe that we should document this behavior somewhere and there isn't anything we can change behavior-wise. I started to write some docs for the reference about implied bounds rust-lang/reference#1261. That documentation is fairly vague at times because implied bounds are an inconsistent mess and unsound, so documenting the status quo there is somewhat :/ What I am unsure about is where an in-depth documentation would be appropriate, the reference, nomicon, or dev-guide? |
@rustbot label +A-docs |
Uh oh!
There was an error while loading. Please reload this page.
Potentially related to #25860 . The issues seem related but the examples are pretty different so I figured I'd file this as separate.
I'm not yet sure if I can craft an actual self-contained soundness bug out of this, but it does cause a soundness bug in
Yoke
which relies onfor<'a>
working correctly: unicode-org/icu4x#2926. I have multiple potential fixes for the yoke issue, but it's worth at least noting.TLDR: Rust currently correctly implies a
'inner: 'outer
bound when you have&'outer &'inner _
. It is also incorrectly implying this for&'outer fn(&'inner _)
The reduced example is as follows:
(playpen)
This should not compile.
F
requires the returned string to be valid for ALL lifetimes'all
, whereas we're returning a string of lifetime's
This code is behaving the same as this code:
where the concrete type of
F
isfor<'all> FnOnce(&'all &'co u8) -> &'all str
, and well-formedness implies that'all
must be shorter than'co
, so you end up getting a'co: 'all
bound, and's: 'co
ends up giving us's: 'all
, so even though there is afor<'all>
, the'all
is actually artificially restricted to being "for all shorter than'co
" and returning data of lifetime's
is valid there.(the
's: 'co
is actually not necessary forco_shorter()
to compile, but it's easier to explain that way)Basically, for
&'outer Foo<'inner>
, the implied bound probably should be:Foo
:'inner: 'outer
Foo
: NothingFoo
:'inner: 'outer
, or nothingBasically the implied bound is safe when things are guaranteed to not be contravariant. It's actually fine to have the implied bound for e.g. the invariant case of
&'outer Cell<'inner _>
, because a cell is logically a tuple of a covariant getter and contravariant setter, and the setter implies no bounds but the getter can imply bounds.This does give me some pause since typically we tend to believe that code that works on invariant types will also work on contravariant types, and here's a situation where it won't; so perhaps it's safer to also opt invariant lifetimes out of this. Idk.
Contravariant types could imply the bound'outer: 'inner
because function parameters can't live for less than the function does, but I'm not sure this implied bound is ever useful. Does lead to a nice symmetry though.The Yoke bug (unicode-org/icu4x#2926) only shows up for contravariance due to how Yoke is structured. It's not clear to me that there's a way to write an unsafe abstraction that relies on
for<'a>
being truly universal where an implied bound coming from an invariant type may cause unsoundness. But I could be wrong.A further exploration can be found in this code (playpen):
Show code
The line
attach(contravariant_cart, |_| &s);
should not compile, nor should the functioncontra_shorter()
.contra_longer()
happens to correctly fail to compile because the same variance trick that savescovariant_cart_shorter
does not apply here.cc @pnkfelix @lcnr
Thanks to @workingjubilee for rubberducking this with me.
The text was updated successfully, but these errors were encountered: