Variance and Subtyping

help
1

In regard to subtypes in Rust, I learned that if a composite type U<V> is invariant in V, then the compiler does not perform any subtyping on U with respect to V. However, after I did some experiments to check how the compiler performs subtyping, I found a result that could be inconsistent with the above assertion, so I would like to share it here.

Here is my code:

fn main() {
    let x = 1;

    // Case1: Works fine.
    {
        let y = &mut &&x;
        let z = &mut &**y;
        g(z);
        let _extend_lifetime_of_y_up_to_here = y;
    }

    // Case 2: Does not compile.
    {
        let y = &mut &mut &x;
        let z = &mut &mut **y;
        f(z);
        let _extend_lifetime_of_y_up_to_here = y;
    }
}

fn f<'a>(_x: &'a mut &'a mut &'a u8) {}
fn g<'a>(_x: &'a mut &'a &'a u8) {}

and its result:

error[E0505]: cannot move out of `y` because it is borrowed
  --> main.rs:17:48
   |
14 |         let y = &mut &mut &x;
   |             - binding `y` declared here
15 |         let z = &mut &mut **y;
   |                      -------- borrow of `**y` occurs here
16 |         f(z);
17 |         let _extend_lifetime_of_y_up_to_here = y;
   |                                                ^
   |                                                |
   |                                                move out of `y` occurs here
   |                                                borrow later used here
   |

It is understandable that case 2 did not compile. First of all, if I explicitly denote the types of y and z, they should take the forms of &'1 mut &'2 mut &'3 u8 and &'4 mut &'5 mut &'3 u8 , respectively, because the third lifetime '3 must be inherited exactly considering the fact that both types are invariant in that lifetime while the first and second lifetimes need not to coincide across y and z due to the reborrows. Therefore, if I pass z to the function f, it effectively freezes any objects with the lifetime '3. More precisely, in compiler's point of view, when it sees y, it must assume that z and _x, which is the argument of f generated inside the function, are also alive as they share the same lifetime '3.
However, this logic should be applicable to case 1 as well since the above logic relies only on the fact that &mut &mut &'3 u8 is invariant in '3 which is true for &mut &&'3 u8. Neverthless, the compiler did not compilain about case 1.

What is the logic behind this? Could the compiler possibly perform subtyping on &mut &&'3 u8 with respect to '3?

2 
let z = &mut &mut &***y;

works fine.

I think but not sure it has something to do with the hidden variables. (and only & being copy.)

    // Case 2: Does not compile.
    {
        let mut y1 = &x;
        let mut y0 = &mut y1;
        let y = &mut y0;
        
        let mut z0 = &mut **y;
        let z = &mut z0;
        f(z);

        let _extend_lifetime_of_____up_to_here = y1;
    }
1 Like
3

That's mostly true, but not entirely true. With mutable references there are process called “reborrow” that splits one mutable references into sequence of many mutable references.

Without such ability you wouldn't be able to even create x: &mut i32; and then pass it into a function as &mut i32… but it's pretty underdocumented varince type.

1 Like
4

Let’s dissect the assignment to z in both cases:

let y = &mut &mut &x;

We take y – as you did – as a variable of some type &'1 mut &'2 mut &'3 u8, we look at the second line now.

let z = &mut &mut **y;

This compound expression &mut &mut **y consists of 5 things:

  • outer &mut _ expression
  • inner &mut _ expression
  • an outer deref *_ expression inside of that
  • an innermost deref *_ expression inside of that
  • the local-variable expression y

A &mut _ expression is a value expression, and inside of it, it expects a place (thus creating a place expression context). A *_ expression is a place expression, and inside of it, you might naively expect a value (the pointer/reference being de-referenced)… the reference calls it a place expression context though, so I guess it’s more complicated in some cases. This question isn’t even about place expressions vs. value expressions… a good simplified view of the situation is thus: place expressions are more “magical” and do get considered by the compiler in context; the exact meaning of a value expression containing place-expressions as constituents is often easier to intuitively reasoned about as a whole. So we’ll decompose the expression along those more course boundaries into:

  • outer &mut _ expression
  • inner &mut **y expression

considering something like &mut **y as a single operation as a whole.

We haven’t fully eliminated the story of “places” yet… the outer &mut _ expression does expect a place, but gets the &mut **y value; which would usually result in a temporary variable for the duration of evaluating this whole thing, kind-of desugaring to:

let z = {
    let mut temporary = &mut **y;
    &mut temporary
};

but that desugaring wouldn’t work, as temporary is dropped while still borrowed (at least if we use z at all). In this case, “temporary lifetime extension” also applies, as a consequence, the more correct desugaring is

// now `temporary` lives at the same level as `z`
let mut temporary = &mut **y;
let z = &mut temporary

In fact, it’s probably beneficial to re-write the whole test code by eliminating implicit temporaries

#[allow(unused_mut)]
fn main() {
    let x = 1;

    // Case1: Works fine.
    {
        let mut temporary1 = &x;
        let mut temporary2 = &temporary1;
        let y = &mut temporary2;
        let mut temporary3 = &**y;
        let z = &mut temporary3;
        g(z);
        let _extend_lifetime_of_y_up_to_here = y;
    }

    // Case 2: Does not compile.
    {
        let mut temporary1 = &x;
        let mut temporary2 = &mut temporary1;
        let y = &mut temporary2;
        let mut temporary3 = &mut **y;
        let z = &mut temporary3;
        f(z);
        let _extend_lifetime_of_y_up_to_here = y;
    }
}

fn f<'a>(_x: &'a mut &'a mut &'a u8) {}
fn g<'a>(_x: &'a mut &'a &'a u8) {}

and the resulting compilation error (and non-error) remains the same.

So let’s get back to the question of lifetimes. As I (and you) said, we do have y of type &'1 mut &'2 mut &'3 u8 in case 2.

Next step is thus

let mut temporary3 = &mut **y;

Now &mut ** is producing some value of some type &'4 mut &'5 u8 of course. It does so by mutably borrowing the target of the target of y. That target’s type is &'3 u8, so we produce a value of type &'4 mut &'3 u8 actually ('5 == '3). The lifetime '4 on the other hand comes from this mutable borrow. Naively, this should mean '4 is as long as the variable y is considered mutably borrowed. More precisely, the compiler understands re-borrowing (borrowing the target of a reference) a bit more precisely, and for this case, it will be allowed for '4 to be even longer than y exists, as long as y isn’t touched anymore and as long as the lifetime '4 is still at most as long as the lifetime '1, the outer lifetime of the mutable reference (of type &'1 mut &'2 mut &'3 u8) that we re-borrowed. We do use y again, so this side-note was kind-of irrelevant, and the lifetime '4 must end before y is used again (the borrow was mutable, i.e. exclusive).

We could also imagine the lifetime '4 can perhaps still be further shortened at this time (when assigning this reference to the temporary) but that wouldn’t really help with anything down the line, so let’s ignore that idea.

Finally, we create z by mutably borrowing temporary, creating a value of type &'6 mut &'4 mut &'3 u8. This is more straightforward; just '6 is the lifetime of this mutable borrow.

How can we now create a value with 3 equal lifetimes &'a mut &'a mut &'a u8 that f expects? Variance won’t help with anything. It would allow us to make the lifetime in '6 shorter, but it’s already the shortest lifetime of the three. (A type &'6 mut &'4 mut &'3 u8 always comes with implied bounds '4: '6 and '3: '6; more generally &'a T requires T: 'a which in turn desugars to a list of 'l: 'a bounds, for every lifetime 'l mentioned in the type T). If it’s already the shortest, and we can only shorten further, this won’t make the two be any closer together.

Fortunately, between types without destructors, many different borrows can all actually be considered to end simultaneously. This is basically why the code compiles if _extend_lifetime_of_y_up_to_here = y is removed. If it isn’t removed, then that lines however creates a problem:

At that point of _extend_lifetime_of_y_up_to_here = y, the mutable re-borrow of y must have ended, so we can access y at all. But since we have access to y, and thus to the &'3 u8 all the way inside, the lifetime '3 must still be completely alive. So we know that '3 then is truly longer than '4, and they couldn’t have been equal.

Now for case 1:

The reson starts similarly, however we now have &**y, an immutable “re-borrow” of some value of (the target of the target of) y, which had type &'1 mut &'2 &'3 u8; and we produce some &'4 &'5 u8-typed value, to be assigned to temporary3.

As mentioned, the exact meaning of a value expression containing place-expressions as constituents is often easier to intuitively reasond about as a whole; the compiler understands this concept of immutably borrowing behind 2 layers of indirection with built-in reference types, and it will not impose the more straightforward bound that '4 is exactly as long as y is considered to be borrowed. Instead, it understands that immutably borrowing the target’s target of a &'1 mut &'2 &'3 u8 reference can be implemented by merely copying the &'2 &'3 u8 reference, so '4 can be as long as '2. In fact, it may be the easiest to think of temporary3 simply as being assigned a copy of this &'2 &'3 u8 value. However… you can also consider that the actual value of temporary3 can be the result of coercing this value to some subtype, and this time it could matter. This is because of the covariance of &'2 &'3 u8 in both '2 and '3, so by covariance we could make the resulting '4 and '5 lifetimes of temporary3: &'4 &'5 u8 to be any 2 lifetimes such that '2: '4, '3: '5 (and '3: '2 and '5: '4 are always implied bounds), but '4 and '5 could even be closer together.

I’m not 100% sure that this coercion is the most relevant part of the resoning[1]; the notable part instead is probably just that the re-borrow here is not completely detatched from the variable y; i.e. y itself is not considered borrowed at all after the re-borrow &**y has been created. (The only connection is between the lifetimes of the types of y and its re-borrow; but y itself isn’t kept borrowed).

So anyways, finally we mutably borrow temporary3 and get some &'6 mut &'4 &'5 u8 and '6 is how long temporary3 is considered borrowed. And this can be of type &'6 mut &'2 &'3 u8, if you’d like to ignore the potential additional complexity discussed previously, or you could say any lifetime '4 and '5 as long as '2: '4, '3: '5 is fulfilled, as discussed above. Anyways… passing this to g means that temporary3 will now be borrowed for as long as '2 and '3 (or '4 and '5) which are unrelated to whether or not y is accessed [i.e. none of these lifetimes need to end to allow an access to y!]

One thing that also becomes obvious with these discussions is the fact that lifetimes are only concerned about when borrows end, not when they begin: What I mean is: the lifetimes '2 and '3 in the case1-discussion above (and even the lifetime '4 and '5) do already “exist” long before temporary3 is first borrowed; yet when passing the result to g, it’s ultimately fine to consider these lifetimes all equal to the lifetime '6, even though they started earlier. But only the end of lifetimes matters, so as the point where we’re promising to g that the lifetimes are all the same, we kind of say “well… now these are all live, so they’re the same now, since you can’t time-travel back into the past and thus only the question of ‘when do they end?’ still matters”.

  1. I’m also curious now if an example can be crafted where this exact detail would be more significant; because I don’t actually know if the compiler considers this kind of coercion possible or not ↩︎

2 Likes