NLL lets borrowck observe drop order for `let (a, b);`

[pnkfelix]

NLL is built on MIR-borrowck. MIR-borrowck operates on the control-flow graph encoded in the MIR.

We didn't (and still do not) want to let borrowck depend on details of how we choose to codegen the MIR from a given AST (in particular for match expressions), and so we put some effort into trying to obscure those details from the view of MIR-borrowck.

But there was a case that we (potentially) overlooked: MIR encodes the order in which the variables a and b are dropped in let (a, b);, and now NLL/MIR-borrowck takes advantage of that knowledge when checking code.

• I say "potentially" here because, as @nikomatsakis pointed out to me, the dynamic drop order was of course always observable (unlike say the particular details of the order in which we consider match arms when compiling match). So ths arguably does not fall into the same bucket as the previous motivation for FalseEdges in the MIR.

In particular, in the following example (adapted from ui/dropck-eyepatch.rs):

#![feature(nll)]

// The types in this file follow a pattern, D{t,r}, where:
//
// - D means "I implement Drop"
//
// - t suffix is used when the first generic is a type
//
// - r suffix is used when the first generic is a lifetime.

use std::fmt;

struct Dt<A: fmt::Debug>(&'static str, A);
struct Dr<'a, B:'a+fmt::Debug>(&'static str, &'a B);

impl<A: fmt::Debug> Drop for Dt<A> {
    fn drop(&mut self) { println!("drop {} {:?}", self.0, self.1); }
}
impl<'a, B: fmt::Debug> Drop for Dr<'a, B> {
    fn drop(&mut self) { println!("drop {} {:?}", self.0, self.1); }
}

fn main() {
    use std::cell::Cell;
    let c_long;
    let (c, mut dt, mut dr): (Cell<_>, Dt<_>, Dr<_>);
    c_long = Cell::new(1);
    c = Cell::new(1);

    // No error: sufficiently long-lived state can be referenced in dtors
    dt = Dt("dt", &c_long);
    dr = Dr("dr", &c_long);
    println!("{:?}", (dt.0, dr.0));
    
    // Error: destructor order imprecisely modelled
    dt = Dt("dt", &c);
    //~^ ERROR `c` does not live long enough
    dr = Dr("dr", &c);
    //~^ ERROR `c` does not live long enough
    println!("{:?}", (dt.0, dr.0));
}

Using AST-borrowck (by commenting out the #![feature(nll)] at the top) emits the following errors:

error[E0597]: `c` does not live long enough
  --> src/main.rs:36:20
   |
36 |     dt = Dt("dt", &c);
   |                    ^ borrowed value does not live long enough
...
41 | }
   | - `c` dropped here while still borrowed
   |
   = note: values in a scope are dropped in the opposite order they are created

error[E0597]: `c` does not live long enough
  --> src/main.rs:38:20
   |
38 |     dr = Dr("dr", &c);
   |                    ^ borrowed value does not live long enough
...
41 | }
   | - `c` dropped here while still borrowed
   |
   = note: values in a scope are dropped in the opposite order they are created

Using NLL compiles successfully, because NLL/MIR-borrowck only sees a more precise model of the relative drop order of the variables declared via let (c, dt, dr);, and takes advantage of it.

---

The question is: Are we okay with this side-effect of NLL?

I don't think it was explicitly documented as an intended effect.

However, I think the fact that we used to use an imprecise model for the drop-order in let (c, dt, dr); previously was more due to the weaknesses of AST-borrowck. Under NLL, we can encode the more precise relationships needed to check the borrowing behavior in this program and validate that it is safe to let dt and dr hold references to c here.

[pnkfelix]

This probably needs to be brought to the attention of the lang team (at least...)

(but i'm not nominating it for discussion yet because i want to ruminate on the matter a bit.)

[pnkfelix]

The main argument I can think of in favor of the old static semantics is that some people may prefer developers to be forced to write let a; let b; when the drop order is significant, and allow let (a, b); only when it is not significant (between those two variables).

However, my personal suspicion is that this change to the static semantics will solve more usability problems for our users than it "causes."

[nikomatsakis]

I don't think we are going to fix this. It seems hard and anyway changing the evaluation order here would be...unadvisable imo? I'll nominate for lang time but I'm also going to go ahead and FCP to close.

[nikomatsakis]

@bors fcp close

The old AST based borrow check was not "aware" of the drop order for variables within a single let (they were given the same "scope"). So it considered that in a case like:

let (a, b) = ...

a and b were dropped "simultaneously". Thus is prevented cycles between them. Of course, users could observe the order at runtime.

The new borrow checker seems things after lowering and hence it naturally knows the order in which a and b will be dropped. Therefore, it permits b to have references into a, even if b has a destructor (because it knows a will not yet have been dropped by then). (It would not permit a to have references into b.)

I think this is OK. We are not going to change that ordering anyway -- see also RFC 1857.

[nikomatsakis]

Putting on the Release milestone.