How can let y; and let y: _; be different to the borrow checker?

[steffahn]

@rustbot label A-borrow-checker, C-discussion

I’ve tested across this code example when trying to understand corner-cases of borrow checker behavior:

fn test() {
    let x = Box::new(1);
    let y = &(&*x, 123);
    let r = &y.1;
    drop(x);
    println!("{r}");
}

The fact that this does work in the first place is slightly cool; given that the type of y, &'a (&'b i32, i32) would usually come with an 'b: 'a bound, but the rest of the code make it so that the re-borrow in r (which could have lifetime &'a i32) lives longer than the Box that the inner &'b i32 comes from.

But then I noticed – slightly disappointed – that

fn test() {
    let x = Box::new(1);
    let y: _ = &(&*x, 123);
    let r = &y.1;
    drop(x);
    println!("{r}");
}

no longer works! Now, I first thought… such type annotations can sometimes reasonably have significant effects on the meaning of the code, in particular some let y: &_ = …; usually starts allowing y to be created through a reborrow … at least for &mut T that’s sometimes very relevant.

But here, I’m not actually providing any concrete type in the first place. So why would the added : _ still make any difference?

For a slight variation with the same effect, these two have the same distinction:

fn test() {
    let x = Box::new(1);
    let y_target = (&*x, 123);
    let y;
    y = &y_target;
    let r = &y.1;
    drop(x);
    println!("{r}");
}

behavior:
compiles successfully

---

vs

fn test() {
    let x = Box::new(1);
    let y_target = (&*x, 123);
    let y: _;
    y = &y_target;
    let r = &y.1;
    drop(x);
    println!("{r}");
}

behavior:

error[E0505]: cannot move out of `x` because it is borrowed
 --> src/lib.rs:7:10
  |
2 |     let x = Box::new(1);
  |         - binding `x` declared here
3 |     let y_target = (&*x, 123);
  |                     --- borrow of `*x` occurs here
...
7 |     drop(x);
  |          ^ move out of `x` occurs here
8 |     println!("{r}");
  |               --- borrow later used here
  |
help: consider cloning the value if the performance cost is acceptable
  |
3 -     let y_target = (&*x, 123);
3 +     let y_target = (&x.clone(), 123);
  |

(playground)

It seems surprising that let y; and let y: _; aren’t fully equivalent; in my mind, they should simply both leave the type of y to-be-inferred for later. [Still, I’d also suspect that “implementation details of type inference” + “interaction of type information with the borrow checker” somehow forms the answer to this.]

I’m leaving this with just C-discussion for now; I haven’t found this reported elsewhere here on the rust-lang/rust issue tracker (as far as the search bar & labels could tell me). If someone else deems this to be a bug and/or well-fixable, we can turn it into C-bug as well 😇

[theemathas]

Related to rust-lang/reference#788

[jieyouxu]

cc @lqd in case you know about this edge case.

[lqd]

Ascribing types usually makes a constraint hold at every point in the CFG, so I wonder if it’s related. In any case, to find more about these examples, I’d look for differences in the NLL MIR, -Zdump-mir=nll -Zverbose-internals, and the graphviz visualizations accompanying it.

[steffahn]

Okay, in those files (working with the first, i.e. the temporary-lifetime-extension-powered variant of the example), the top section of the mir changes like

        debug x => _1;                   // in scope 1 at src/main.rs:5:9: 5:10
-       let _2: &'?24 (&'?25 i32, i32) ; // in scope 1 at src/main.rs:6:9: 6:10
+       let _2: &'?24 (&'?25 i32, i32) as UserTypeProjection { base: UserType(1), projs: [] }; // in scope 1 at src/main.rs:6:9: 6:10
        scope 2 {
            debug y => _2;               // in scope 2 at src/main.rs:6:9: 6:10
            let _5: &'?28 i32;           // in scope 2 at src/main.rs:7:9: 7:10
            scope 3 {
                debug r => _5;           // in scope 3 at src/main.rs:7:9: 7:10
                let mut _20: &'?45 [&'?46 str; ValTree(Leaf(0x0000000000000002): usize)]; // in scope 3 at src/main.rs:9:14: 9:19
            }
        }
    }

and in the basic block around the assignment, we have

    bb1: {
        FakeRead(ForLet(None), _1);      // bb1[0]: scope 0 at src/main.rs:5:9: 5:10
        StorageLive(_2);                 // bb1[1]: scope 1 at src/main.rs:6:9: 6:10
        StorageLive(_3);                 // bb1[2]: scope 1 at src/main.rs:6:17: 6:27
        StorageLive(_4);                 // bb1[3]: scope 1 at src/main.rs:6:18: 6:21
        _4 = &'?9 (*_1);                 // bb1[4]: scope 1 at src/main.rs:6:18: 6:21
        _3 = (move _4, const ConstValue(Scalar(0x0000007b): i32)); // bb1[5]: scope 1 at src/main.rs:6:17: 6:27
        StorageDead(_4);                 // bb1[6]: scope 1 at src/main.rs:6:26: 6:27
        _2 = &'?10 _3;                   // bb1[7]: scope 1 at src/main.rs:6:16: 6:27
        FakeRead(ForLet(None), _2);      // bb1[8]: scope 1 at src/main.rs:6:9: 6:10
+       AscribeUserType(_2, o, UserTypeProjection { base: UserType(2), projs: [] }); // bb1[9]: scope 1 at src/main.rs:6:12: 6:13
        StorageLive(_5);                 // bb1[…]: scope 2 at src/main.rs:7:9: 7:10
        _5 = &'?11 ((*_2).1: i32);       // bb1[…]: scope 2 at src/main.rs:7:13: 7:17
        FakeRead(ForLet(None), _5);      // bb1[…]: scope 2 at src/main.rs:7:9: 7:10
        StorageLive(_6);                 // bb1[…]: scope 3 at src/main.rs:8:5: 8:12
        StorageLive(_7);                 // bb1[…]: scope 3 at src/main.rs:8:10: 8:11
        _7 = move _1;                    // bb1[…]: scope 3 at src/main.rs:8:10: 8:11
        _6 = ConstValue(ZeroSized: fn(Box<i32>) {std::mem::drop::<Box<i32>>})(move _7) -> [return: bb2, unwind: bb7]; // bb1[…]: scope 3 at src/main.rs:8:5: 8:12
                                         // mir::ConstOperand
                                         // + span: src/main.rs:8:5: 8:9
                                         // + const_: Const { ty: fn(Box<i32>) {std::mem::drop::<Box<i32>>}, val: Value(ConstValue(ZeroSized: fn(Box<i32>) {std::mem::drop::<Box<i32>>})) }
    }

i.e. some operation called AscribeUserType appears shortly after the assignment.

---

And then under Inference Constraints in that file, there are apparently really some new constraints from this, reading things like

| '?24: '?47 due to TypeAnnotation(Declaration) at All(src/main.rs:6:12: 6:13) (src/main.rs:6:12: 6:13 (#0)
| '?24: '?49 due to TypeAnnotation(Ascription) at All(src/main.rs:6:12: 6:13) (src/main.rs:6:12: 6:13 (#0)
| '?25: '?48 due to TypeAnnotation(Declaration) at All(src/main.rs:6:12: 6:13) (src/main.rs:6:12: 6:13 (#0)
| '?25: '?50 due to TypeAnnotation(Ascription) at All(src/main.rs:6:12: 6:13) (src/main.rs:6:12: 6:13 (#0)

and

| '?47: '?24 due to TypeAnnotation(Declaration) at All(src/main.rs:6:12: 6:13) (src/main.rs:6:12: 6:13 (#0)
| '?48: '?25 due to TypeAnnotation(Declaration) at All(src/main.rs:6:12: 6:13) (src/main.rs:6:12: 6:13 (#0)
| '?48: '?47 due to BoringNoLocation at All(src/main.rs:6:12: 6:13) (src/main.rs:6:12: 6:13 (#0)
| '?49: '?24 due to TypeAnnotation(Ascription) at All(src/main.rs:6:12: 6:13) (src/main.rs:6:12: 6:13 (#0)
| '?50: '?25 due to TypeAnnotation(Ascription) at All(src/main.rs:6:12: 6:13) (src/main.rs:6:12: 6:13 (#0)
| '?50: '?49 due to BoringNoLocation at All(src/main.rs:6:12: 6:13) (src/main.rs:6:12: 6:13 (#0)