About Non-Lexical Lifetimes

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?

Let's see what NLL says in the failing example.

I think you understand this so I'll fold it.

Using your notation, 'c has to be alive at 7:

    /* 7 */ let _tmp = (*_r_c).f1;   //  Last use of _r_c

And this means 'a must also be alive, because 'a: 'c.

Then back at 6, we have:

    /* 6.1 */ _r_a = &_mbar;
    /* 6.2 */ drop(_mbar);

mbar must be borrowed for 'a (since r_a is a &'a _), which includes everything from 6.1 to 7. So mbar is borrowed at 6.2.

But being borrowed is incompatible with being moved, so you get a borrow check error.

I guess what you're asking is, why can't the borrow of _mfoo to be somehow disassociated from _r_a on reassignment. That's certainly a reasonable question for the example; the only thing making mbar get borrowed for 'a is the type system (the fact that _r_a's type includes the lifetime parameter, and that imposes a lifetime bound when assigned to).

I think the tricky part would be making a formal ruleset for this that is sound in every case.

Note that NLL does go to some lengths to accommodate reassignable references, just not in a way that helps this example.


The rest of this comment consists of potential corrections/clarifications which are, I think, tangential to your actual question.

The differences between &_ and &mut _ is very relevant to NLL/borrow checking generally.

But whether a binding is mut or not (let _r_a versus let mut _r_a) does not matter, provided both compile. That is, adding unnecessary mut bindings changes borrow checking not-at-all. So how NLL works in your second code block is exactly the same as in the first code block.

It's only in your last code block, where you have _r_a = &_mbar; drop(_mbar), things have changed -- because these are new uses of values, not because you (were required to) declare a mut binding per se.

NLL doesn't really reason about things this way. Indeed, borrow checking isn't allowed to change the liveness of variables. Instead, the things which make a variable dead (like being moved or going out of scope) are uses which may conflict with being borrowed. Borrow checking analyzes where and how things[1] are borrowed, and checks all uses for conflicts with the borrows.

The literal answer is that _mfoo and **_r_b are borrowed (have "loans" in NLL) at that point.

The error in the non-compiling version is because _mbar is borrowed when dropped.


  1. places, including variables ↩︎

2 Likes

Thank you for your reply.

I still have several questions about this topic, but first, I would like to get a clarification that is indispensable for me, even though it may seem trivial, if not useless and perhaps borderline ridiculous, to those who are well-versed in the subject. This is a very controversial point for me:

In the document in question, the following two definitions (among others) are given:

DEF_1) "... Intuitively, in the new proposal, the lifetime of a reference lasts only for those portions of the function in which the reference may later be used (where the reference is live, in compiler speak). ... If a lifetime contains the point P, that implies that references with that lifetime are valid on entry to P"

DEF_2) "... we will consider lifetimes as a set of points in the control-flow graph"

Of course, there is more said, but in the end, I always have this question:

QUESTION(S): What exactly are these "points" being discussed?

  • Where are they located?
  • What exactly does it mean:
    "If a lifetime contains the point P, that implies that references with that lifetime are valid on entry to P"?

This is something I am not fully grasping, and I would like to describe - in very crude terms - my current mental model of the issue using some personal terminology:

A program is a sequence of instructions that is statically analyzed by the compiler/borrow checker, which determines the "states of the program" at the end of each instruction through a combination of Forward & Backward Analysis that, from an implementation perspective, I imagine is the depth-first search referred to in the document. In my mental model, these "points" I am questioning identify these states.

But what do I mean by "state of the program"?
I mean the "state of the variables and/or the memory allocated to them" that the program uses, and this state is determined by answering similar questions (I am very crude and incomplete, I know):
Is the variable x alive?
Can the memory of variable x be freed?

In summary, referring to a generic variable x of reference type present in the code:

A) The points in the CFG in question, including those referenced in DEF_2, do not correspond to the instructions.
B) The effects of the instructions (preceding and succeeding) are felt in them, and the variable x is "measured" (is it alive?).
C) The code portions mentioned in DEF_1 are composed of those instructions that follow and precede (in order!) two points (as described above) of a CFG execution path.

Perhaps a very simple example can help understand my view to potentially correct and/or refine it.

I deliberately avoid copies of references, references to references, and reborrow (I believe I will have to return to similar situations in the near future).

struct Metadata {
    f1: i32,
}

fn main() {
    {
        let mut result = 0;
        let mut _mfoo = Metadata { f1: 22 };
        let mut _mbar = Metadata { f1: 55 };
         
        let mut ref_v = &_mfoo;
        // Point A
         
        if true {
            let _tmp = 0;      
            // Point B
            
            let _tmp = ref_v.f1;
            // Point C

            _mfoo.f1 += 1;
            // Point D

            _mfoo.f1 += 1;
            // Point E
        } else {
            let _tmp = 0;
            // Point F

            result = ref_v.f1 + 1;
            // Point G

            let _tmp = 0;
            // Point H

            ref_v = &_mbar;
            // Point I
            
            let _tmp = 0;
            // Point L
            
            result = ref_v.f1 + 1;
            // Point M
            
            let _tmp = 0;
            // Point N
        }
    }
}

Basically, it consists of two execution paths, of which I intend to examine the following (I would analyze the other in absolutely the same way):

// PATH_ELSE
{
    let mut ref_v = &_mfoo;
    // Point A

    let _tmp = 0;
    // Point F

    result = ref_v.f1 + 1;
    // Point G

    let _tmp = 0;
    // Point H

    ref_v = &_mbar;
    // Point I
    
    let _tmp = 0;
    // Point L
    
    result = ref_v.f1 + 1;
    // Point M
    
    let _tmp = 0;
    // Point N
}

Note: "let _tmp = 0;" is a placeholder for any instruction or block of instructions that does not use the reference ref_v;

The analysis of the 1st instruction raises the question of whether ref_v is ALIVE after it (at point A). This cannot be decided because at this point the following instructions have not yet been examined, so it is not yet known whether the borrowed value will be used (by the reference, i.e., by the alias of _mfoo).

The same applies after examining the next 2nd instruction (point F).

The analysis of the 3rd instruction sees that the variable borrowed by ref_v is used through this alias, and thus it can be determined that the reference ref_v is alive in F and A (Backward Analysis?), while nothing can be said about point G (same reasoning as before: the following instructions are not yet known).

The analysis of the 4th instruction (point I) still cannot determine whether ref_v is alive.

The analysis of the 5th instruction reveals that ref_v borrows another variable (_mbar), which implies that ref_v is DEAD in points H and G, while nothing can yet be said about whether ref_v is alive or dead at point I.

The analysis of the 6th instruction leaves in doubt whether ref_v is alive at point L.

The analysis of the 7th instruction sees a use of the pointed value, and thus it can be determined that ref_v is alive at points L and I, while nothing can be said about point M.

The analysis of the 8th and final instruction - which does not use the value pointed by ref_v - finally establishes that ref_v is DEAD at points N and M.

Thus, given 'a the lifetime of ref_v, it results that 'a = {A,F,I,L} limiting the analysis to the execution path of the else branch.

What do you think of this reconstruction?

(Not read compiler code as not compiler dev) I only think there is one way analysis*. (see bottom)

The only thing to be considered is can _mfoo be borrowed. (then keep track of it.) Too much analysis of future is way too complicated.

    let mut _mfoo = Metadata { f1: 22 };
    let mut _mbar = Metadata { f1: 55 };
     
    let mut ref_v = &_mfoo;

    if true {
        _mbar.f1 += 1; // NLL means can print below and change here without error (despite else branch referencing _mbar)
    } else {
        ref_v = &_mbar; // NLL. No longer track borrow of _mfoo
        _mfoo.f1 +=1; // NLL means can print below and change here without error
    }
    //_mfoo.f1 +=1; // still no changing outside branch before the print
    //_mbar.f1 +=1;
    println!("{}", ref_v.f1);

Each branch tracks separately. Then at end a combined tracker is formed for what ref_v will require be borrowed if later used.

*Now see the analysis the other (way when removing comment)

error[E0506]: cannot assign to `_mfoo.f1` because it is borrowed
  --> src/main.rs:18:5
   |
9  |     let mut ref_v = &_mfoo;
   |                     ------ `_mfoo.f1` is borrowed here
...
18 |     _mfoo.f1 +=1;
   |     ^^^^^^^^^^^^ `_mfoo.f1` is assigned to here but it was already borrowed
19 |     //_mbar.f1 +=1;
20 |     println!("{}", ref_v.f1);
   |                    -------- borrow later used here

The error message could very well complain about the use on print line being the problem. My thought is the developers chose to reverse after detecting the error.

Statements in the control-flow graph.

Assuming a compiling program, it means if some reference &'a _ exists, and 'a contains P, when the program reaches P the reference is still valid.

If you're talking about this, that's for expanding lifetimes based on 'a: 'b constraints, it's not the liveness analysis.

The NLL RFC doesn't given an algorithm for liveness, it just defines lifetime liveness in terms of variable liveness, which (like CFGs and basic blocks) is a general compiler technique.

I think the exact mechanics are an implementation detail. The compiler could work in passes, where for example all variable liveness is determined, and then after that lifetime liveness is determined and the rest of the NLL algorithm runs. Or the compiler could work by defining program flow logically, recording the facts of the CFG, and then just query the resulting database/logic program when it needs to know if a variable (or lifetime, etc) is alive.

I'm rewriting my last message because it was completely wrong due to copy & paste operations.

I agree, but the example I provided was very simple as it was mainly aimed at understanding what these points in the CFG that define lifetimes are and where they are located.
However, even in such a case, to be precise, constraints due to subtyping should be specified:

// PATH_ELSE
{
    let mut ref_v = &_mfoo;
    
    if true                      // Point A                      ('_mfoo : 'ref_v)@ A          subtyping constraint
                                 //                             ('ref_v :{A})@A               liveness constraint

    let _tmp = 0;                // Point F                      ('ref_v :{F})@F               liveness constraint
    

    result = ref_v.f1 + 1;       // Point G                      ('ref_v :{G})@G               liveness constraint                       

    let _tmp = 0;                // Point H                      "ref_v DEAD"
    
 
    ref_v = &_mbar;             
        
    let _tmp = 0;                // Point I                      ('_mbar : 'ref_v)@ I          subtyping constraint
                                 //                             ('ref_v :{I})@I               liveness constraint
    
    
    result = ref_v.f1 + 1;       // Point L                      ('ref_v :{L})@L               liveness constraint
    
    
    let _tmp = 0;                // Point M                      "ref_v DEAD"
}

Certainly, it is said that the inference algorithm solves the constraints to establish the lifetimes in play (and not only determines the liveness of a variable), but to provide its result, it must have all the constraints and should be the one to establish them (preliminarily deciding the liveness of the variables involved).

So, it seems to me that the algorithm first establishes these constraints (including where a variable is alive) and only then applies the inference part.

Do you agree?

I hope I have explained what I mean and that I can make myself understood in the following (forgive me, but I already have doubts about the topic, and moreover, English is not my native language).

Now, however, in order to internalize these damned lifetimes, I would like to dissect a few more things:

Question nr 1:

The document states:
"a lifetime L is live at a point P if there is some variable p which is live at P, and L appears in the type of p."

The word that disturbs me is "appears."

I will start with a first example in which I specify the constraints but especially for convenience, I explicitly specify the lifetimes in the type:

{
    let foo: i32 = 11;                           // Point 1
    let ref_foo: &'a i32 = &'a foo;              // Point 2     
	
    let ref_ref_foo: &'b &'a i32 = &'b ref_foo;  // Point 3		('foo : 'a) @ 3					subtyping constraint
												 //				('a :{3}) @ 3    				liveness constraint ---------+	
                                                                                                                             |
    let tmp: i32 = 0;                            // Point 4		('a : 'b) @ 4					subtyping constraint ---+    |
	                                             //				('a :{4}) @ 4					liveness constraint     |    |
												 //				('b :{4}) @ 4		  			liveness constraint     'b   |
                                                                                                                        |   'a
    let tmp: i32 = **ref_ref_foo;                // Point 5		('b :{5}) @ 5					liveness constraint  ---+    |
												  //			('a :{5}) @ 5												 |
	                                                                                                                         |
	let tmp = *ref_foo;							 // Point 6		('a :{6}) @ 6					liveness constraint  --------+
												 //				ref_ref_foo is NOT LIVE

    let tmp: i32 = 0;                            // Point 7		ref_foo is NOT LIVE
}

Following the approach of the lifetime inference algorithm, I get that:
'a = {3,4,5,6} and 'b = {4,5}
and the definition in question:
"a lifetime L is live at a point P if there is some variable p which is live at P, and L appears in the type of p"
confirms that at points 4 and 5 L = 'a is alive because the variable ref_ref_foo is alive and its type (which is &'b &'a) APPEARS 'a.

But if we consider this second example:

{
    let foo: i32 = 11;                            // Point 1
    let ref_foo: &'a i32 = &'a foo;               // Point 2
	
    let copy_ref_foo: &'b i32 = ref_foo;          // Point 3	('foo : 'a) @ 3					subtyping constraint --------+
												  //			('a :{3}) @ 3			                                     |
												                                                                             |
    let tmp: i32 = 0;                             // Point 4	('a : 'b) @ 4					subtyping constraint ---+    |
												  //			('a :{4}) @ 4												 |
												  //			('b :{4}) @ 4					liveness constraint     |    |
												  //			                                          				'b   |
												                                                                        |   'a
    let tmp: i32 = *copy_ref_foo;                 // Point 5	('b :{5}) @ 5					liveness constraint ----+    |
												  //			('a :{5}) @ 5												 |
																															 |
	let tmp = *ref_foo;							  // Point 6	('a :{6}) @ 6					liveness constraint ---------+
												  //			copy_ref is NOT LIVE
												  
    let tmp: i32 = 0;                             // Point 7	ref_foo is NOT LIVE
}

Following the approach of the lifetime inference algorithm, I get similarly to before that:
'a = {3,4,5,6} and 'b = {4,5}
but this time the definition:
"a lifetime L is live at a point P if there is some variable p which is live at P, and L appears in the type of p"
cannot confirm that "at points 4 and 5 L = 'a is alive because there isn't another variable alive in whose type 'a APPEARS" because the type of copy_ref_foo is "&'b i32" (in which 'a DOES NOT APPEAR).

Maybe my interpretation of the definition is a bit too orthodox, and probably bordering on obtuseness.

However, here is my personal interpretation of the definition:
"a lifetime L is live at a point P if there is some variable p which is live at P, and L EXTENDS or is the same as the lifetime of p."

What do you think?

Now one last point,
Question nr 2:

Consider this example:

{
    let foo = 11;					// Point 1
    let ref_b;						// Point 2
    {								// Point 3								
        let ref_a = &foo;			// Point 4
        ref_b = ref_a;				// Point 5			('foo : 'a) @ 5		subtyping constraint ---------------+
																('a :{5}) @ 5		liveness constraint					|
																														|
    }								// Point 6			('a : 'b) @ 6		subtyping constraint ---+           'a
									//					('b :{6}) @ 6		liveness constraint		|			|
									//					ref_a is NOT LIVE							|	 		|
																											'b			|
																											|	 		|
    let _tmp = *ref_b;				// Point 7			('b :{7}) @ 7		liveness constraint  ---+-----------+
}									// Point 8			ref_b is NOT LIVE

So, if I'm not mistaken:

  • 'a = {5, 6, 7} = lifetime of ref_a
  • 'b = {6, 7} = lifetime of ref_b

which highlights that the lifetime of a reference (ref_a) can extend beyond those portions of code where the reference is alive and can thus be used through dereferencing.

This brings me to an alternative view of the lifetime of a reference:
I would say that the lifetime of a specific reference p (understood as a set of instructions) is actually a constraint on the memory that p has borrowed, and this constraint imposes that - in the portion of code identified - such memory cannot be freed, and this for two reasons:

  1. The reference p is still alive (without ever being dead) and thus still has the memory borrowed.
  2. The reference p is dead, but the borrowing of the memory it had in charge has been transferred to its alias through its copy or through the introduction of a reference that borrows p or even through reborrow.

It seems to me something that goes beyond the (intuitive) definition provided in the document:
"Intuitively, in the new proposal, the lifetime of a reference lasts only for those portions of the function in which the reference may later be used (where the reference is live, in compiler speak)."

What do you think?

I'll try to come back to this topic when I'm better able to reply. Might be a few days.

Preliminaries and whatnot

Based on the RFC, that's how NLL works, but ultimately it's an implementation detail. As mentioned before, another approach -- that of the next generation borrow checker -- would be to record the base facts and rules from which the other information can be derived, and then query for the required information as needed.

In any case, as far as I know, looking at things that way is still an accurate mental model for understanding the borrow checker.


You quote the "rough outline" of the RFC near the end of your last post, which also contains this blurb:

However, in order to successfully type the full range of examples that we would like, we have to go a bit further than just changing lifetimes to a portion of the control-flow graph. We also have to take location into account when doing subtyping checks. This is in contrast to how the compiler works today, where subtyping relations are “absolute”. That is, in the current compiler, the type &'a () is a subtype of the type &'b () whenever 'a outlives 'b ('a: 'b), which means that 'a corresponds to a bigger portion of the function. Under this proposal, subtyping can instead be established at a particular point P. In that case, the lifetime 'a must only outlive those portions of 'b that are reachable from P.

But in the end, that was too expensive for NLL and will be delayed until sometime after the next borrow checker (Polonius) lands.

I ignore any nuance around this in my response, NLL algorithm wise. It doesn't matter for the given examples.[1]


In your examples, you're acting like here...

let ref_foo: &'a i32 = &'foo foo;

...'foo and 'a must always be in the same. In most simple examples, this will be the case (and presenting things that way can be a useful shortcut for cutting down tedium when working out NLL by hand). But note that they don't have to be the same. This part of the RFC mentions them being distinct; ref_foo being alive will initially populate 'a, and solving constraints based on subtyping will later populate 'foo.

Similarly, subtyping can kick in for nested shared reference assignments too.

I'm not going to not take that shortcut below, as lifetime solving is relevant to how some of the examples work. If nothing else, thinking about the simple cases where it doesn't really matter can still act as a warmup.

Example 1

Minding the note above, we get...

    let foo: i32 = 11;                           // Point 1
    let ref_foo: &'a i32 = &'f foo;              // Point 2 ('f: 'a)
    let ref_ref_foo: &'b &'c i32 = &'r ref_foo;  // Point 3 ('r: 'b, 'a: 'c, 'c: 'b)
    let tmp: i32 = 0;                            // Point 4
    let tmp: i32 = **ref_ref_foo;                // Point 5
    let tmp = *ref_foo;							 // Point 6
    let tmp: i32 = 0;                            // Point 7

The liveness of ref_foo does give 'a = { 3, 4, 5, 6 }, and the liveness of ref_ref_foo does give 'b = { 4, 5 } as well as 'c = { 4, 5 }.

Solving the constraints due to subtyping gives 'f = { 3, 4, 5, 6 } and 'r = { 4, 5 }. So in the end we have 'f = 'a and 'b = 'c = 'r.

Example 2

Example 2a:

    let foo: i32 = 11;                            // Point 1
    let ref_foo: &'a i32 = &'f foo;               // Point 2 ('f: 'a)
    let copy_ref_foo: &'b i32 = ref_foo;          // Point 3 ('a: 'b)
    let tmp: i32 = 0;                             // Point 4
    let tmp: i32 = *copy_ref_foo;                 // Point 5
    let tmp = *ref_foo;							  // Point 6
    let tmp: i32 = 0;                             // Point 7

ref_foo is alive at 3, 4, 5, 6 because it is used on line 6 without being overwrote. Note that it doesn't have to be used on lines 4 and 5 to be alive on lines 4 and 5. 'a appears in ref_foo's type, so 'a initially (i.e. due to liveness) consists of { 3, 4, 5, 6 } again. (And nothing later extends this lifetime.)

And also 'b = { 4, 5 } and then subtyping constraints give us 'f = 'a similar to before.

However, perhaps you meant this (call it Example 2b):

    let foo: i32 = 11;                            // Point 1
    let ref_foo: &'a i32 = &'f foo;               // Point 2 ('f: 'a)
    let copy_ref_foo: &'b i32 = ref_foo;          // Point 3 ('a: 'b)
    let tmp: i32 = 0;                             // Point 4
    let tmp = *ref_foo;							  // Point 5
    let tmp: i32 = *copy_ref_foo;                 // Point 6
    let tmp: i32 = 0;                             // Point 7

Here I've swapped lines 5 and 6. So from liveness now we get

  • 'a = { 3, 4, 5 }
  • 'b = { 4, 5, 6 }

In particular, note how 'a doesn't yet contain 6 because ref_foo is no longer alive on line 6.

But solving lifetimes then expands this to

  • 'a = { 3, 4, 5, 6 }
  • (and then 'f = { 3, 4, 5, 6 })

Because all of 4, 5, 6 are reachable from 'a: 'b @ 4, so 6 is added to 'a.

That sounds like the result of lifetime solving based on constraints to me.

In terms of the RFC: A lifetime can contain points outside the liveness constraints of the lifetime, due to subtyping and reborrowing constraints. Your personal interpretation sounds like you want "lifetime liveness" and "lifetime" to be the same thing.

I don't think anyone cares about details on this level unless they're talking about the implementation or the RFC, whatever that's worth. E.g. no one's going to care about the distinction between "lifetime" and "lifetime liveness constraint" in your typical borrow checker topic on this forum. But it may be confusing to redefine things when talking about the RFC.

Example 3

{
    let foo = 11;					    // Point 1
    let ref_b: &'b i32;				    // Point 2
    {								    // Point 3								
        let ref_a: &'a i32 = &'f foo;	// Point 4 ('f: 'a)
        ref_b = ref_a;				    // Point 5 ('a: 'b)
    }								    // Point 6
    let _tmp = *ref_b;				    // Point 7
}									    // Point 8

From liveness: 'a = { 5 }, 'b = { 6, 7 }.[2]

After solving: 'a = { 5, 6, 7 }, 'f = { 5, 6, 7 }.

Correct.

That would be a loan, not a lifetime per se. Loans can be shorter than their associated lifetime to accommodate things like overwriting references (problem case #4). And also carry information about what kind of borrow (shared, exclusive) is active on the associated place.

(Similar to "lifetime liveness", most of the time this distinction doesn't matter for figuring out a typical borrow checker error or whatnot.[3])

All uses of places are checked for borrows, not just freeing memory. Taking a &mut _ to a place requires the same "permissions" as freeing/destructing/moving a value, for example.

I agree that it's an incomplete description, since a lifetime can extend beyond the liveness of the reference. (This was true before NLL too, incidentally, but I'm unfamiliar with how things actually worked at that level of detail back then. Perhaps the assignment results in both types having the same lifetime, but that is just a blind guess.)

Prior to NLL, the lifetime of references that were assigned to variables lasted at least until the variable went out of scope. It was as-if such references had destructors that "examined the lifetime". So one had to introduce artificial blocks like this somewhat often.[4] With NLL, blocks rarely matter for references as far as borrow checking goes.[5] This is presumably what the quoted statement is about.


  1. I believe it means constraint solving ignores the "reachability" aspect and acts in a full sub/superset manner, but haven't done the legwork to prove convince myself of this rigorously. ↩︎

  2. ref_b isn't alive until assigned ↩︎

  3. Rarely it does come up when explaining why something can compile. ↩︎

  4. in certain types of code anyway; I ran into it early and often in my Rust journey ↩︎

  5. You can't have a reference to a reference if the inner reference goes out of scope; that's about it. ↩︎