NLL inference doesn't work when it probably should

[arielb1]

NLL inference does not work with this code, where it probably should:

#![allow(warnings)]

use std::cell::Cell;

struct S1<'c, 'a: 'c, 'x: 'a>(&'c Cell<&'a u32>, &'x ());
struct S2<'c, 'b: 'c + 'x, 'x>(&'c Cell<&'b u32>, &'x ());

fn assert_sig<'a, 'b, 'c, F>(a: &'c Cell<&'a u32>, b: &'c Cell<&'b u32>,
                             f: F) -> Box<for<'x> Fn(&'a &'x (), &'x &'b ())+'c>
                             where 'a: 'c,
                                   'b: 'c,
     F: for<'x> Fn(S1<'c, 'a, 'x>, S2<'c, 'b, 'x>) + 'static
{
    Box::new(move |x, y| f(S1(a, x), S2(b, y)))
}

fn manual_closure<'c, 'a, 'b, 'x>(x1: S1<'c, 'a, 'x>, x2: S2<'c, 'b, 'x>)
{
    x1.0.set(x2.0.get());
}

fn main() {
    let (a, mut b, w0, w1, c_a);
    a = 0;
    b = 0;
    w0 = &();
    w1 = &();
    c_a = Cell::new(&a);
    let c_b = Cell::new(&b);
    
    // weirdly enough, this does *not* force 'a: 'b, because within
    // the closure, we know that 'a: 'x & 'x: 'b and therefore
    // 'a: 'b.
    let assert = assert_sig(&c_a, &c_b, manual_closure);
    
    if true {
        assert(&w0, &w1); // this forces 'a: 'x, 'x: 'b
    } else {
        // but *nothing* is forced here
        b = 1;
        println!("{}", c_a.get());
    }
}

Similar code with a closure: https://gist.github.com/b0ed5e73062f343367fb9a22a2fe9d72

[nikomatsakis]

Investigating.

[nikomatsakis]

The problem is that the type of c_b is Box<Fn>, and that is not known to have a no-op destructor. If we alter the example to insert a drop at the right spot, everything compile successfully:

#![allow(warnings)]

use std::cell::Cell;

struct S1<'c, 'a: 'c, 'x: 'a>(&'c Cell<&'a u32>, &'x ());
struct S2<'c, 'b: 'c + 'x, 'x>(&'c Cell<&'b u32>, &'x ());

fn assert_sig<'a, 'b, 'c, F>(
    a: &'c Cell<&'a u32>,
    b: &'c Cell<&'b u32>,
    f: F,
) -> Box<for<'x> Fn(&'a &'x (), &'x &'b ()) + 'c>
where
    'a: 'c,
    'b: 'c,
    F: for<'x> Fn(S1<'c, 'a, 'x>, S2<'c, 'b, 'x>) + 'static,
{
    Box::new(move |x, y| f(S1(a, x), S2(b, y)))
}

fn manual_closure<'c, 'a, 'b, 'x>(x1: S1<'c, 'a, 'x>, x2: S2<'c, 'b, 'x>) {
    x1.0.set(x2.0.get());
}

fn main() {
    let (a, mut b, w0, w1, c_a);
    a = 0;
    b = 0;
    w0 = &();
    w1 = &();
    c_a = Cell::new(&a);
    let c_b = Cell::new(&b);

    // weirdly enough, this does *not* force 'a: 'b, because within
    // the closure, we know that 'a: 'x & 'x: 'b and therefore
    // 'a: 'b.
    let assert = assert_sig(&c_a, &c_b, manual_closure);

    if true {
        assert(&w0, &w1); // this forces 'a: 'x, 'x: 'b
    } else {
        // but *nothing* is forced here
        drop(assert); // <-- added this
        b = 1;
        println!("{}", c_a.get());
    }
}

[nikomatsakis]

Interestingly, the work towards three-point error messages in borrowck (#45988) made this quite clear. Running the compiler with "cause-dumping" enabled gives this output:

lunch-box. rustc --stage1 ~/tmp/arielb3.rs -Znll -Zborrowck=mir -Znll-dump-cause -Zdump-mir=nll
error[E0506]: cannot assign to `b` because it is borrowed
  --> /home/nmatsakis/tmp/arielb3.rs:43:9
   |
32 |     let c_b = Cell::new(&b);
   |                         -- borrow of `b` occurs here
...
43 |         b = 1;
   |         ^^^^^ assignment to borrowed `b` occurs here
   |
   = note: because of a outlives relation created at `bb2[6]`
           because of a outlives relation created at `bb2[6]`
           because of a outlives relation created at `bb3[0]`
           because of a outlives relation created at `bb3[9]`
           because of a outlives relation created at `bb3[10]`
           because of a outlives relation created at `bb3[10]`
           because of a outlives relation created at `bb4[0]`
           because `_12` is dropped at bb6[0]

"cause dumping" tells us what led compiler to think that borrow should include this point. In this case, _12 is c_b.

[nikomatsakis]

Closing this for now.