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?

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

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

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.

• 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 ↩︎

Thank you; this is very helpful.

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