Hidden Details of Rust's Reborrow, Double References, and Lifetimes

Why does the following code:

struct S;

fn foo<'a, 'b>(rb: &'b &'a mut S) -> &'a S {
    let xxx = &**rb;    

    xxx
}

cause a compilation error, with the compiler suggesting changing &'a S to &'b S? After making this modification, the error disappears.

Or, to ask the question differently:

In let xxx: &'x S = &**rb;, should 'x be equal to 'a or 'b?

From the compilation result, xxx is inferred to have the type &'b S, meaning 'x = 'b. However, based on my understanding of Rust's language rules, I find it difficult to explain why this is the case.

Can someone provide an explanation, ideally considering Rust's language rules regarding nested borrows, reborrowing, variance, shared references, and mutable references? Thanks

It must be equal to (or shorter than β€” shorter is always an option[1]) 'b, because if it was not, then it would be possible to write this function:

fn bar(s: &'a mut S) {
    let xxx: &'a mut S = foo<'a, '_>(&s);
    mutate(s);
    println!("{xxx}"); // oops, we used a stale reference
}

The general principle, I believe (I cannot give you a formal answer) is that when you have access to a mutable reference (whether direct or via another reference), if you wish to obtain a reference to its referent, you must do that as a reborrow to ensure the result is valid, and a reborrow of a mutable reference always has a lifetime no longer than the shortest lifetime that got you to it. That is, xxx's type has the lifetime that is the shortest of all involved lifetimes (or shorter, if desired).

Shared references are different β€” if you had rb: &'b &'a S, then when you &**rb, you are allowed to make a copy of &'a S and get another &'a S. Reborrowing a shared reference is the same thing as making a copy of a shared reference.

All of this arises as consequences of maintaining the exclusivity of mutable/exclusive references.


  1. You can consider that a covariant coercion, or you can consider it flexibility of assigning lifetimes to references; either leads to the same answer. β†©οΈŽ

1 Like

The closest thing to a specification on reborrows so far is the NLL RFC.

Prefixes. We say that the prefixes of an lvalue are all the lvalues you get by stripping away fields and derefs. The prefixes of *a.b would be *a.b, a.b, and a.

Note that these dereferences are built-in dereferences; Deref implementation based references are method calls. The perspective is post-desugar, where ever dereference and reborrow, etc, is explicit.

Supporting prefixes. To define the reborrow constraints, we first introduce the idea of supporting prefixes – this definition will be useful in a few places. The supporting prefixes for an lvalue are formed by stripping away fields and derefs, except that we stop when we reach the deref of a shared reference. Inituitively, shared references are different because they are Copy – and hence one could always copy the shared reference into a temporary and get an equivalent path.
[...]
Reborrow constraints. Consider the case where we have a borrow (shared or mutable) of some lvalue lv_b for the lifetime 'b:

lv_l = &'b lv_b      // or:
lv_l = &'b mut lv_b

In that case, we compute the supporting prefixes of lv_b, and find every deref lvalue *lv in the set where lv is a reference with lifetime 'a. We then add a constraint ('a: 'b) @ P, where P is the point following the borrow (that’s the point where the borrow takes effect).

In short, start from the inside and go out. Your reborrow is constrained by the lifetime of the first shared reference, or (if there is none) of the outermost reference. It can be shorter, i.e. it doesn't have to be equal (or reborrows of &mut _ would be useless).

Note also that nested references likes &'b &'a mut _ imply 'a: 'b.

2 Likes

Given this signature:

fn foo<'a, 'b>(rb: &'b &'a mut S) -> &'a S

the compiler suggested adding 'b: 'a, which, as I understand it, would make 'a == 'b.
Can the compiler infer this automatically?

Correct.

Infer what, that they'd be the same? It would be nice if analytics took that into account and suggested the simpler signature.

1 Like