Lifetimes, quantification, and subtypes

1

I'm trying to wrap my head around issue 25860 and the discussion there. Are references truly covariant? The function f roughly has the type

forall 'a . forall 'b &'a &'b () -> &'b T -> &'a T

(please forgive this notation). This type makes sense for all 'a and 'b because we can only construct an instance of &'a &'b () if 'b : 'a. But then the transformation going from foo2 to foo3 in the companion blog post seems fishy. To prove that the transformation is legal my understanding is that we would have to instantiate for an arbitrary 'out lifetime and show the transformation always holds. So we need to choose an arbitrary 'out and then convert &'out &'static () to &'out &'short (). But we can only do that if 'short : 'out.

More generally, it seems like if S is a subtype of T we can only obtain a function &'x S -> &'x T if T : 'x. So are references really covariant? When are we allowed to substitute a longer-lived reference for a shorter-lived one?

2

Note that we abuse the terminology of "types" to apply to lifetimes as well, even though lifetimes on their own are not types. Putting that aside, we have

'long: 'short => 'long <: 'short
// If 'long outlives 'short, 'long is a subtype of 'short

And we say that &'a T is covariant in 'a (and T), meaning

'long <: 'short => &'long T <: &'short T

And as a result, we can coerce a &long T into its supertype &'short T.

More generally, if a type constructor Z(P) is covariant in its parameter P, we have

P <: Q => Z(P) <: Z(Q)

That's covariance -- this relationship between the subtyping of the parameters and the subtyping of the type constructor.

However, we have fn(U) as being contra-variant in U; that means, fn(&'a T) is contravariant in 'a as well, thus:

'long <: 'short => fn(&'short T) <: fn(&'long T)
// General contravariance:  P <: Q => Z(Q) <: Z(P)

From which we can coerce a fn(&'short T) into a fn(&'long T).

Are we lengthening any borrow in order to do so? No, fn(U) is not itself a (type of a) borrow.

After this coercion (in isolation), can we lengthen any borrows by passing them in? No, it just means I can pass in longer-lived borrows to a function that is expecting shorter-lived borrows. The same result could be achieved by shortening the parameter's lifetime. I can no longer pass shorter-lived borrows into the coerced function, because it now demands a longer borrow.

Does this mean references are not always covariant? No, being covariant defines how the subtypes of parameters of a type constructor relate to the subtypes of the outputs of the type constructor. Just because &'a T being covariant in 'a can be interpreted as "The 'a of a &'a T can only coerce to something shorter" does not mean you can conclude "The 'a of a fn(&'a T) can only coerce to something shorter", even though there's a &'a T in there. Those are two different type constructors. The entire composed type constructor must be taken into account.

What might happen if you could coerce fn(&'static T) to fn(&'short T)? Then you could store a reference to a local variable in a global resource by passing it into the previously-&'static T-expecting function, for example. That is say, it would be unsound.

The transformation is problematic because it breaks the relationship between the two parameters. In foo2, two of the borrows had to have the same lifetime, and there was an implied bound due to the first parameter:

  • 'short: 'out

And that implied bound is required to make the original foo -- which returns the second parameter -- sound. I.e. the relationship between the two parameters is crucial here.

The coercion to foo3 breaks that relationship -- the two borrows longer have to have the same lifetime. Moreover, the implied bound is now (the trivial):

  • 'static: 'out

And any choice of 'x for 'out where 'x strictly outlives 'short is UB as it will "lifetime transmute" 'short to something longer. (foo4 is a concrete example of such a choice, 'static.)

If you replace both 'short with 'static, there is no problem [1].

Another section of the article examines how the breaking of these relationships is problematic even when there is no contravariance at play.

  1. with soundness; you can no longer pass in x ↩︎

1 Like
3

I'm not asking about contravariance; I understand that. I'm trying to understand why the coercion is illegal and why rustc erroneously allows it. The constructor I'm interested in is &'a. If S <: T, then it seems like &'a S <: &'a T isn't always true; you need to require T : 'a. That's the covariance issue that concerns me, and that rule is being broken in the coercion.

1 Like
4

Ah, perhaps I understand now. Apologies in advance if the rest of this is still missing the mark though.

I'm not sure how much your aware of, so first let me refer you to the well-formed (WF) types section of RFC 1214. In short, in the face of WF, &'a S implies a S: 'a bound, and &'a T implies a T: 'a bound. Both have to be true for the coercion to happen (i.e. you coerce between WF types).

But the fact that these bounds are implicit is indeed part of the problem: You can lose an implied bound during coercion that is needed for soundness.

A couple notes about RFC1214:

  • See also RFC 2093 which removed the discussed annotation requirements on type declarations
  • The RFC sites the issue and says it's a contravariance issue, but as the article shows, it is not
    • And the follow-up RFC has not come to be

The second piece which is important to note is that for<...> is "limited" by any implied bounds that are present! That is, these two can be considered the same due to WF:

  for<'out> fn(&'out &'short (), &'short) -> &'out ()
  // Made up syntax I will refer to as `for<where>`
  for<'out where 'short: 'out> fn(&'out &'short (), &'short) -> &'out ()

And the problem is that rustc considers it okay to perform

  for<'out where 'short: 'out> fn(&'out &'short (), &'short) -> &'out ()
  <:
  for<'out> fn(&'out &'static (), &'short) -> &'out ()

Because it was only implied, the for<where> bound is lost after the coercion, but 'short is still present in the type and the bound is required for soundness. Adding these where binders to the compiler (or explicitly) as discussed in the article is one way to keep bounds which are no longer implied.

Another upside of some explicit form for these bounds is that they would have additional applications. See for example how scoped threads are being implemented using implied bounds to emulate for<where>.

With the binders, Rust could still soundly allow:

  // for<'out> fn(&'out &'short (), &'short) -> &'out 
  // AKA:
  for<'out where 'short: 'out> fn(&'out &'short (), &'short) -> &'out
  <:
  for<'out where 'short: 'out> fn(&'out &'static (), &'short) -> &'out
  // Cannot be made less explicit as the clause is not implied elsewhere

But disallow

  // for<'out> fn(&'out &'short (), &'short) -> &'out 
  // AKA:
  for<'out where 'short: 'out> fn(&'out &'short (), &'short) -> &'out
  <:
  for<'out> fn(&'out &'static (), &'short) -> &'out
  // Invalid!

I believe that only allowing replacement of all instances of a given parameter when coercing [1] also avoids the problem without where<> binders or for<...where...>[2], but am curious if anyone else can show otherwise.

  1. that is, you cannot coerce only one of the two 'short to 'static, you must coerce both or neither ↩︎

  2. as after coercion, there is nothing left that would interact with the dropped bound ↩︎

5

Thank you; this is very helpful.

6

This topic was automatically closed 90 days after the last reply. New replies are no longer allowed.