# Lifetimes, quantification, and subtypes

**URL:** <https://internals.rust-lang.org/t/lifetimes-quantification-and-subtypes/16572>\
**Category:** Uncategorized\
**Created:** [May 3, 2022, 10:02pm UTC](https://internals.rust-lang.org/t/lifetimes-quantification-and-subtypes/16572 "2022-05-03T22:02:35Z")\
**Posts on this page:** 6\
**Page:** 1

<div class="post-metadata">

**Author:** ![user16251](https://sea2.discourse-cdn.com/flex002/user_avatar/internals.rust-lang.org/user16251/32/10186_2.png) [@user16251](https://internals.rust-lang.org/u/user16251)\
**Post date:** [May 3, 2022, 10:02pm UTC](https://internals.rust-lang.org/t/lifetimes-quantification-and-subtypes/16572/1 "2022-05-03T22:02:35Z")

</div>

I'm trying to wrap my head around [issue 25860](https://github.com/rust-lang/rust/issues/25860) and the discussion there. Are references truly covariant? The function `f` roughly has the type

```rust
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](https://lcnr.de/blog/diving-deep-implied-bounds-and-variance/) 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?

---

<div class="post-metadata">

**Author:** ![quinedot](https://sea2.discourse-cdn.com/flex002/user_avatar/internals.rust-lang.org/quinedot/32/7294_2.png) [@quinedot](https://internals.rust-lang.org/u/quinedot)\
**Post date:** [May 4, 2022, 12:28am UTC](https://internals.rust-lang.org/t/lifetimes-quantification-and-subtypes/16572/2 "2022-05-04T00:28:52Z")

</div>

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

```rust
'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

```rust
'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

```rust
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:

```rust
'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.

> [@user16251](#):
>
> But then the transformation going from `foo2` to `foo3` in the [companion blog post](https://lcnr.de/blog/diving-deep-implied-bounds-and-variance/) seems fishy.

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`

---

<div class="post-metadata">

**Author:** ![user16251](https://sea2.discourse-cdn.com/flex002/user_avatar/internals.rust-lang.org/user16251/32/10186_2.png) [@user16251](https://internals.rust-lang.org/u/user16251)\
**Post date:** [May 4, 2022, 1:05am UTC](https://internals.rust-lang.org/t/lifetimes-quantification-and-subtypes/16572/3 "2022-05-04T01:05:44Z")

</div>

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.

---

<div class="post-metadata">

**Author:** ![quinedot](https://sea2.discourse-cdn.com/flex002/user_avatar/internals.rust-lang.org/quinedot/32/7294_2.png) [@quinedot](https://internals.rust-lang.org/u/quinedot)\
**Post date:** [May 4, 2022, 3:13am UTC](https://internals.rust-lang.org/t/lifetimes-quantification-and-subtypes/16572/4 "2022-05-04T03:13:25Z")

</div>

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

> [@user16251](#):
>
> If `S <: T` , then it seems like `&'a S <: &'a T` isn't always true; you need to require `T : 'a` .

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.](https://rust-lang.github.io/rfcs/1214-projections-lifetimes-and-wf.html#well-formed-types) 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](https://rust-lang.github.io/rfcs/2093-infer-outlives.html) 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:

```rust
  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

```rust
  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>`.](https://github.com/rust-lang/rust/issues/93203#issuecomment-1041588991)

With the binders, Rust could still soundly allow:

```rust
  // 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_

```rust
  // 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

---

<div class="post-metadata">

**Author:** ![user16251](https://sea2.discourse-cdn.com/flex002/user_avatar/internals.rust-lang.org/user16251/32/10186_2.png) [@user16251](https://internals.rust-lang.org/u/user16251)\
**Post date:** [May 4, 2022, 11:58am UTC](https://internals.rust-lang.org/t/lifetimes-quantification-and-subtypes/16572/5 "2022-05-04T11:58:48Z")

</div>

Thank you; this is very helpful.

---

<div class="post-metadata">

**Author:** ![system](https://sea2.discourse-cdn.com/flex002/user_avatar/internals.rust-lang.org/system/32/14092_2.png) [@system](https://internals.rust-lang.org/u/system)\
**Post date:** [August 2, 2022, 11:59am UTC](https://internals.rust-lang.org/t/lifetimes-quantification-and-subtypes/16572/6 "2022-08-02T11:59:24Z")

</div>

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