universal-regions table not populated with late bound lifetimes from parent functions

[nikomatsakis]

This example:

#![allow(warnings)]
#![feature(nll)]

trait Bazinga { }

impl<F> Bazinga for F { }

fn produce<'a>(data: &'a u32) -> impl Bazinga + 'a {
    let x = move || {
        let _data: &'a u32 = data;
    };
    x
}

fn main() { }

causes an ICE:

error: internal compiler error: librustc_mir/borrow_check/nll/universal_regions.rs:825: cannot convert `ReFree(DefId(0/0:5 ~ playground[f23d]::produce[0]), BrNamed(crate0:DefIndex(1:10), 'a))` to a region vid

This is split off from #51351 and I think retains the spirit of the original example better.

[nikomatsakis]

Indeed, this is a bit tricky. I'm not actually sure how we should handle this case where we have a late-bound lifetime ('a) from a parent function. It's not part of the closure's generics -- it does appear in the closure's list of upvars, but in fact it may map to many different regions within the closure itself. Ugh.

I suppose we probably have to create a kind of "special treatment" for these things, where we make a dedicated region-vid for each of the (named) late-bound lifetimes in the parent and we include that as part of the ClosureRegionRequirements that we propagate back up to our parent. Then the caller can unify this 'a with its own.

[nikomatsakis]

So, to try and elaborate a bit more on what I was saying in my previous comment:

In the case of a late-bound region from a parent function, it will be not be part of the closure's generics. It may show up in the types of upvars or something like that. So for example if you had:

fn foo<'a>(x: &'a u32, mut y: Vec<&'a u32>) {
  let closure = move || y.push(x);
  ...
}

then the closure would have two upvars (x and y) and of course their types will ultimately reference 'a.

The interesting thing though is that the closure doesn't know that. The way that we check closures is to replace all the free regions that appear in their signatures with fresh names. So, from the closure's point of view, it has two upvars: x: &'0 u32 and y: Vec<&'1 u32>. When we type-check the closure's body, we will find out that '0: '1 must hold, in order for y.push(x) to be allowed. We will propagate this relationship back in the ClosureRegionRequirements struct. Effectively we've inferred the closure to something like struct Closure<'x, 'y> where 'x: 'y.

Our caller meanwhile knows that x and y are instantiated with the parameters, so it will basically replace both '0 and '1 with 'a -- i.e., Closure<'a, 'a> -- and then of course it must prove that 'a: 'a, which is clearly true. The requirement to prove 'a: 'a is created by the apply_requirements method on ClosureRegionRequirements.

So now the problem is: imagine that the user wrote 'a somewhere in the closure body (as in the original example)... the closure itself doesn't know that this is related to the types of x and y etc.

What I think we want to do is this:

• We walk backwards and find all the named late-bound regions that are in scope from the closure's parent (actually the closure base). Let's call this list NLB.
  • Early bound regions appear in the closure's generics, so they don't matter.
• We create an extra universal region for each of those and we add it to the indices map -- so if the user writes 'a, it will get mapped to that.
  • We will then create where clauses as normal.
• Finally, on the caller side, when we invoke apply_requirements, it will take not only the closure def-id and closure substs but also the NLB vector (from the caller's POV). This will permit us to relate things to these named late-bound regions as normal.

So to work through an example, if you had:

fn foo<'a, 'b>(x: &'a u32) {
  let closure = move || {
    let v: &'b u32 = x; // should be an error...
  };
  ...
}

then we will wind up (in the closure body) with an upvar of &'0 u32 and also an entry (from the NLB list) mapping 'b => '1. We will infer a closure region requirement that '0: '1. On the caller side, we will map '0 => 'a and '1 => 'b and then get a requirement that 'a: 'b, which we cannot satisfy (and hence a (probably cryptic) error will result).

[nikomatsakis]

Should be fixed now