` for<'a> &'a T ` seems to require ` T: 'static `

help
5

Really, &'a T come with an “implied bound” of T: 'a. In a normal where bound or the like, this would mean extra requirement… but if the lifetime is introduced in higher-order bounds, i.e. some for<'a> …-style HRTBs[1], the intended meaning is instead that the for<'a> … quantifier is meant to only range over all such lifetimes that fulfill T: 'a.

The “current limitation of the type system” that this compiler error mentions is that the type system doesn’t actually properly support such restricted ranges for for<'a> … trait bounds, but kind-of rather just behaves as-if these were to truly range over all possible lifetimes, just that whenever you’re going to use that same bound, you’ll have to sort-of mention the very same &'a T type again and now if that’ll be in a context about some concrete (not higher-rank) lifetime parameter, that gives rise to the same implied bound once-again and now you gotta actually fulfill it.

So all is fine.

Except when it isn’t. :collision:

Yeah, anyway, in most practical cases this works as intended though, but as linked above there is some unsoundness on one hand, and as noted in this thread / by that compilation error, there are some remaining restrictions on the other hand.

“Proper support” would mean that something like for<'a> &'a Generator: GenerateName would more literally desugar to something like

for <'a> ( if <Generator: 'a> /* then */ ( &'a Generator: GenerateName ) )

(there is no actual official syntax for this … yet … I believe … so take it as pseudo-code)

One difficulty of proper support, as far as I remember, is that it would imply the type system needs to handle bounds like

impl<'a, 'b, 'i> …
where
    'a: 'i,
    'b: 'i,
    for<'l> ( if<'a: 'l, 'b: 'l> ( 'i: 'l )),
{ … }

and

impl<'a, 'b, 'u> …
where
    'u: 'a,
    'u: 'b,
    for<'l> ( if<'l: 'a, 'l: 'b> ( 'l: 'u )),
{ … }

which can be used to nail down 'i or 'u, effectively to be equal, to the “intersection”, or the “union” of two lifetimes 'a and 'b, respectively;[2] and I think may have read somewhere that at least one of the two [not sure off the top of my head which one it was, “intersection” or “union”] is somehow more fundamentally beyond the capabilities of what the current type system could handle.

  1. "higher-rank trait bounds" ↩︎

  2. equivalently you can think of thes as something like of binary supremum and infimum if you consider the : an order relation ↩︎

2 Likes