How does Region Inference work?


#1

Hi,

I am trying to understand how Rust’s region inference algorithm works. I have went through the docs

My understanding of region inference is that ‘region’ and ‘lifetime’ is equivalent, thus the purpose is to infer the lifetimes of borrows. The inference algorithm collects lifetime constraints over the course of a function, e.g., for:

fn foo<'a: 'b,'b>(a: &'a str, b: &'b str) -> &'a str {
  let c = &123; // 'c
  a
}

There are two types of lifetimes: bounded and free. Bounded lifetimes originate from the function body ('c). Free lifetimes are unbound as they originate from some arbitrary outer scope ('a and 'b).

Regions are inferred somewhat differently from types. Rather than eagerly unifying things, we simply collect constraints as we go, but make (almost) no attempt to solve regions.

First question: How are the constraints collected? I understand that constraints for the free lifetimes are specified in the signature, e.g., 'a: 'b, but I’m not sure about the bounded lifetimes? I suppose one constraint is that 'c does not not outlive the lifetime of 123.

Lexical region resolution is done by initially assigning each region variable to an empty value. We then process each outlives constraint repeatedly, growing region variables until a fixed-point is reached. Region variables can be grown using a least-upper-bound relation on the region lattice in a fairly straightforward fashion.

Second question: How does the inference algorithm work at a high-level? I’m not sure why the region variables are grown here or what the region lattice refers to.

Third question: What is the output of the inference algorithm? Is it a concrete lifetime for each borrow, corresponding to a particular scope?


#2

Just to check, are you interested in what stable Rust does today, or the brand new algorithms that are still under the “NLL” feature? I think the new logic is mostly documented at https://github.com/rust-lang/rfcs/blob/master/text/2094-nll.md, though the details may change again: Blog post: An alias-based formulation of the borrow checker


#3

I would like to gain an understanding of the stable first, but I’ll check out the NLL after


#4

I am trying to visualize it. If I have these constraints, should I get this ordering and this region lattice?

Constraints | Ordering | Region-lattice 
------------|----------|--------------
  'a:'b+'c  | 'a <= 'b |      'd      Join, LUB (Most Specific Supertype)
  'b:'d     | 'a <= 'c |      / \     
  'c:'d     | 'b <= 'd |    'b  'c    
  'd        | 'c <= 'd |      \ /     
            |          |      'a      Meet, GLB (Most Common Subtype)

I’m not sure how this example would look in code though.