I would like some clarification on NLL (Non-Lexical Lifetimes) as defined in RFC 2094.
Specifically, I would like to examine the following example from the document, albeit slightly modified:
struct Metadata {
f1: i32,
}
fn main() {
{
/* 1 */ let mut _mfoo = Metadata { f1: 22 };
/* 2 */ let mut _mbar = Metadata { f1: 55 };
/* 3 */ let mut _r_a = &_mfoo;
/* 4 */ let _r_b = &_r_a; // 'a : 'b
/* 5 */ let _r_c = &**_r_b; // Supporting Prefixes: SP = {**_r_c}; ==> 'a : 'c
/* 6 */ // What is considered borrowed here?
/* 7 */ let _tmp = (*_r_c).f1; // Last use of _r_c !!!!!!
}
}
As indicated by the text, there are the following two constraints on the lifetimes involved:
'a : 'b
'a : 'c
I am trying to definitively understand these lifetimes and would like to present my interpretation based on the mental model I am building, but first, I would like to share my reasoning on a modified version of the previous code that does not involve _r_a being mutable:
struct Metadata {
f1: i32,
}
fn main() {
{
/* 1 */ let mut _mfoo = Metadata { f1: 22 };
/* 2 */ let mut _mbar = Metadata { f1: 55 };
/* 3 */ let _r_a = &_mfoo;
/* 4 */ let _r_b = &_r_a; // 'a : 'b
/* 5 */ let _r_c = &**_r_b; // Supporting Prefixes: SP = {**_r_c}; ==> 'a : 'c
/* 6 */ // What is considered borrowed here?
/* 7 */ let _tmp = (*_r_c).f1; // Last use of _r_c !!!!!!
}
}
In this case, the two constraints 'a : 'b and 'a: 'c do not surprise me:
-
_r_c borrows what _r_a has already borrowed (i.e., the variable _mfoo) and maintains that borrow, sharing it with _r_a, until it is LIVE (until the end of the instruction let _tmp = (*_r_c).f1;).
-
Once _r_c becomes DEAD, the variable _mfoo continues to be borrowed/pointed to by _r_a alone ('a : 'c), which therefore must remain LIVE.
And why must it remain live?
Since it must point to the same variable pointed to by _r_c (as they are defined, it could not be otherwise), what would it mean for _r_a to no longer be live? It would mean that the variable _mfoo has been destroyed, but then _r_c would be a dangling reference.
Now let's return to the initial example, which instead involves _r_a being mutable.
/* 1 */ let mut _mfoo = Metadata { f1: 22 };
/* 2 */ let mut _mbar = Metadata { f1: 55 };
/* 3 */ let mut _r_a = &_mfoo;
/* 4 */ let _r_b = &_r_a; // 'a : 'b
/* 5 */ let _r_c = &**_r_b; // Supporting Prefixes: SP = {**_r_c}; ==> 'a : 'c
/* 6 */ // What is considered borrowed here?
/* 7 */ let _tmp = (*_r_c).f1; // Last use of _r_c !!!!!!
After reborrowing, I can make _r_a borrow another variable, for example, _mbar via _r_a = &_mbar, BUT the constraints remain unchanged, continuing to impose 'a : 'c.
In reality, it would make sense (from my perspective) to also be able to do something like this:
/* 4 */ let _r_b = &_r_a; // 'a : 'b
/* 5 */ let _r_c = &**_r_b; // Supporting Prefixes: SP = {**_r_c}; ==> 'a : 'c
/* 6.1 */ _r_a = &_mbar;
/* 6.2 */ drop(_mbar); // Since `_r_a` and `_r_c` now borrow 2 different variables
/* 6 */ let _tmp = (*_r_c).f1; // Last use of _r_c !!!!!!
But obviously, this violates the constraint 'a : 'c.
Why is this the case?
Is it a conservative choice in the development of the Rust compiler and its borrow checker, or is there something else I am missing?