fn foo<T>(_: T) where for<'a> T: 'a {}
fn main() {
let a = 1;
let b = &a;
foo(b);
}
The (expected) error message contains the following caveat:
note: due to current limitations in the borrow checker, this implies a `'static` lifetime
--> src/main.rs:3:34
|
3 | fn foo<T>(_: T) where for<'a> T: 'a {}
| ^^
I thought I knew what this message meant, but I'm not sure anymore. In the GATs stabilization announcement, there's an example with a where Self: 'a bound should be implied, but isn't, due to a borrow checker limitation.
However, there are no implied bounds in the above code, so the obvious interpretation of for<'a> T: 'a is that T satisfies 'a for any lifetime 'a, which includes 'static. Is this a "current limitation in the borrow checker" which is anticipated to change? Or is the message misleading?
For what I hope is an absurd example, should I expect the following code to stop compiling in a future edition?
fn foo<T>(x: T) where for<'a> T: 'a { bar(x) }
fn bar<T>(_: T) where T: 'static {}
What it's telling you is that today, fn foo<T>(_:T) where for<'a> T: 'a is the same as fn foo<T>(_:T) where T: 'static. This is the borrow checker limitation the error message references; ideally, for<'a> T: 'a should be more general than T: 'static, as it should accept any value of type T regardless of the lifetime parameter.
However, the borrow checker can't handle this right now - so to get useful features out to everyone, the compiler understands for<'a> T: 'a as a weird way to write T: 'static - and when the borrow checker is improved, it will permit code that doesn't compile today to compile.
I don't see how the version with the for bound is more general in this case. For 'a='static, T: 'static. Also, for every 'a, 'static: 'a. Doesn't that mean that T: 'static, and nothing more?
But you can’t relax a universal quantification ∀ like that. Because 'static is a valid lifetime, T:'static is one of the infinite bounds implied by for<'a> T:'a. Similarly, T:'static implies T:'a for every other possible lifetime 'a. So, unless the meaning of for<'a> starts to mean something other than ∀a over the domain of lifetimes the two statements will continue to be equivalent— Each necessarily implies the other.
Shouldn't it reject T = &'short U because there are lifetimes 'long1, 'long2, ... , 'static that represent regions the type &'short U isn't allowed to exist in?
There are cases, like GATs, where we don't really want universal ∀a, but rather "all 'a that T outlives." We can already write T: 'static when that's really wanted, so for<'a> T: 'a could be interpreted to mean for<'a where T: 'a>. Or perhaps we'll add a new syntax like that...
fn foo<T>(_:T) where for<'a> T: 'a does not restrict the choices you can make for T. It restricts what foo can assume about T.
In the case of fn foo<T>(_:T) where T: 'static, you restrict the choices that you can make for T to ones that meet the lifetime constraint 'static. As Rust checks the body of foo, it's aware that T: 'static, and will permit foo to act on this assumption.
In the case of fn foo<'a, T>(_:T) where T: 'a, you're telling Rust that there exists a single lifetime 'a that's at least as long as the longest lifetime in T, and that foo can assume that it will be called with a T that meets that lifetime. This is usually good enough, because Rust can find that lifetime for you and type-check this function.
A higher-ranked trait bound like in fn foo<T>(_:T) where for<'a> T: 'a is a special case - you're telling Rust that it doesn't matter what lifetime bound is chosen for T, it's still an acceptable bound as far as foo is concerned (as long as the lifetime region is at least the body of foo).
Using fn bar below as a caller, it's possible to tease out the difference between T: 'static and T' for<'a> T: 'a:
fn bar() {
let stat: &'static str = "hello";
let a: String = "world".to_string();
let ref_a = &a;
foo(stat);
foo(ref_a);
}
If foo has a T: 'static bound, the call to foo(ref_a) will fail to compile - we know that ref_ will not live for 'static, since it takes a reference to data that's dropped at the end of bar.
If foo has a for<'a> T: 'a bound, however, the call to foo(ref_a) should compile, but doesn't right now. This is because foo is constrained to taking a T whose lifetime is in the set for<'a>, and that infinite set includes the definite value that it has in bar.
An alternative way to look at this is to read the constraints as setting out the sets of things that contain the parameterised item. T: 'static says that T must be in the set of things that meet the lifetime 'static. T: Display + Debug says that T must be in the set of things that implement the traits Display and Debug. In this interpretation, for<'a> T: 'a is saying that for each call to foo, T must have a lifetime that's found in the set for<'a>.
I don’t quite follow. for<‘a> isn’t a set; it’s a quantifier that describes the relationship between ’a, the listed proposition (bound), and the set of all lifetimes longer than the function body¹. Here, it sounds like you’re describing the existential quantifier ∃a instead of the universal ∀a.
Shouldn’t that get a different syntax, like exist<‘a>? If not, how can I tell when for<‘a> is behaving existentially and when it’s behaving universally?
¹ Or maybe some other well-defined set of lifetimes, per @cuviper
I don't think that's right -- we want all 'a that T outlives, that are at most the lifetime of T itself.
For something like a GAT LendingIterator, this is so we can have a reborrowed lifetime in fn next(&mut self) -> Self::Item<'_>, where we want lifetimes that are shorter than Self. This does work until you write that in a constraint, e.g. where for<'a> <I as LendingIterator>::Item<'a>: Debug, then that for<'a> gets maximized to include 'static.
This isn't my understanding of higher ranked trait bounds.
Higher rank trait bounds introduce an unbound lifetime which can be substituted for any lifetime. for<'a> T: 'a therefore means that T outlives all 'a, up to and including 'static, and therefore for<'a> T: 'a should have the same meaning as T: 'static.
The problem in the GATs example is that you want to constrain the variable 'a introduced in for<'a> to be limited to lifetimes 'a for which T::Foo<'a> is valid, in other words you want to express something like for<'a where T::Foo<'a>: 'a> T::Foo<'a>: Debug - now the bound is not abstract over any lifetime, its only for lifetimes for which that inner where clause holds true. This is psuedosyntax; I think the lang team may plan to do this all through some implied bounds rules but I'm not up to date on their plans.
If this functionality is introduced and the implied bounds rules also apply to this case, then for<'a> T: 'a would be a tautology - equivalent to for<'a where T:'a> T: 'a - "for every lifetime that T outlives, T outlives that lifetime." I'm not sure the plan includes implied bounds for this case, but that's what the error message suggests.
So whether or not the error message is wrong depends on the plans for implied bounds in relation to higher rank trait bounds.
Like with impl Trait, ∃ and ∀ are two sides of the same abstraction. To the person who gets to decide the concrete type behind the impl Trait, it's an ∃; to the person who has to accept any possibility, it's an ∀.
where bounds spell out requirements that the caller must abide by. This means that where for<'a> T: 'a would mean that the caller must supply a T such that the implementation can substitute whichever 'a they want in.
So I can't actually think of a case where for<'a> would create an existential chosen by the caller. I think it would be the difference between a parameter of for<'a> impl Trait and impl for<'a> Trait, but I can't quite justify the former being exists<'a> impl Trait.
There's actually a difference between types and lifetimes to potentially explain why the ∃/∀ duality makes more sense for types than lifetimes -- for types, the code gets monomorphized, turning the ∀ into the required "∃ instantiations". For lifetimes, though, a ∀ bound actually results in a single instantiation which handles each lifetime in a strictly uniform manner.
It's a combination of several pieces of syntax (for<'a> ... and T: 'a) that are independently useful, but might not represent anything particularly interesting when combined. A similar example is &'a mut T<'a> which is almost always useless, but is part of the language because its component parts are useful in other contexts.
For what it’s worth, I would love to see the addition of for<where…> syntax, even if it can be elided in some places. It would help clarify some complicated HRTBs where the implicit bound might not be obvious, such as:
where for<'a> &'a T: IntoIterator<Item=impl 'a + AsRef<U>>
I would go further than that, and request that implicit bounds not be added in cases like this thread's OP, where the signature without the implicit bound already "makes sense." (I think "well-formed" the term to describe this?) Higher-ranked lifetime bounds are hard enough on their own; making people second-guess whether the compiler added extra invisible where clauses they didn't want or need seems like a recipe for disaster.
for<'a> T: 'a is perhaps an unfortunate example because at least according to one interpretation, it's not just a superset of T: 'static but exactly equivalent to T: 'static. Let's take a different example,
trait Quux<'a> {}
fn foo<T>(x: T) where for<'a> T: Quux<'a> { bar(x) }
fn bar<T>(_: T) where T: Quux<'static> {}
Now, I think we would all agree that for<'a> T: Quux<'a> and T: Quux<'static> are different constraints. But the above code nevertheless compiles, which means that the compiler is treating for<'a> T: Quux<'a> as universal and implying T: Quux<'static>. The error message when I try to pass this foo something that doesn't implement Quux<'static> says so explicitly:
error: implementation of `Quux` is not general enough
--> src/main.rs:11:5
|
11 | foo(b);
| ^^^^^^ implementation of `Quux` is not general enough
|
= note: `Quux<'0>` would have to be implemented for the type `&()`, for any lifetime `'0`...
= note: ...but `Quux<'1>` is actually implemented for the type `&'1 ()`, for some specific lifetime `'1`
Where it makes me scratch my head is that it still says due to current limitations in the borrow checker (in another part of the error message).
Note that if I actually implement Quux<'_> universally it compiles even with a non-'static reference. So the error message's this implies a `'static` lifetime clearly does not mean that foo requires T: 'static; it only requires T: Quux<'static>. So the borrow checker is not inferring a T: 'static bound here, which makes total sense, because it has no reason to.
The GATs example is different because I::Item<'a>: is only well-formed when I: 'a, and meaningless otherwise (the point of writing where Self: 'a in the trait). So although for<'a> I::Item<'a>: Debug is currently interpreted as
for any lifetime 'a, I::Item<'a> is well-formed, and implements Debug
(which is consistent with bounds outside of HRTBs), it could in the future be changed to mean
for any lifetime 'a, ifI::Item<'a> is well-formed, then it implements Debug
(which is not consistent with bounds outside of HRTBs), but this change would (I believe?) have no effect on any code that does not have an implicit well-formedness condition, including the example in the OP and the one above with Quux.