Borrow checker is confused by return statements

[Blei]

Unless I'm misunderstanding something, the following code should work (it's a minimized example based on code from cscottnet on irc):

fn insert_and_get_borrow<'r>(arr: &'r mut ~[int], i: int) -> &'r int {
    for arr.each |j| {
        if *j == i { return j; }
    }
    // If not included yet, add it
    arr.push(i);
    &arr[arr.len() - 1]
}

Instead it results in this error:

bar.rs:6:4: 6:7 error: cannot borrow `*arr` as mutable because it is also borrowed as immutable
bar.rs:6     arr.push(i);
             ^~~
bar.rs:2:8: 2:11 note: second borrow of `*arr` occurs here
bar.rs:2     for arr.each |j| {
                 ^~~
error: aborting due to previous error

I don't know about the underlying code, but it looks like the borrow checker is confused by the return statement and assumes that the argument to return (the j) is borrowed for the rest of the function, thus making the new immutable borrow fail.

The following workaround compiles without problems:

fn insert_and_get_borrow_workaround<'r>(arr: &'r mut ~[int], i: int) -> &'r int {
    let mut found_index = None;
    for uint::range(0, arr.len()) |index| {
        if arr[index] == i { found_index = Some(index); }
    }
    match found_index {
        Some(index) => &arr[index],
        None => {
            // If not included yet, add it
            arr.push(i);
            &arr[arr.len() - 1]
        }
    }
}

[cscott]

http://paste.debian.net/5129/ is the original longer example. (But I'm mostly commenting here just to add myself to the cc list.)

[nikomatsakis]

Closing as a dup of #6393. The borrow checker is not in fact confused by return statements, but rather is defending you against a subtle and non-obvious possible error, albeit in its simple minded sort of way.

To demonstrate what I mean, consider this version of your code which works fine:

fn insert_and_get_borrow<'r>(arr: &'r mut ~[int], i: int) -> &'r int {
    let mut j = 0, n = arr.len();
    while j < n {
        if arr[j] == i { return &arr[j]; }
    }
    // If not included yet, add it
    arr.push(i);
    &arr[arr.len() - 1]
}

fn main() { }

Now consider this version, which generates an error:

fn insert_and_get_borrow<'r>(arr: &'r mut ~[int], i: int) -> &'r int {
    let mut j = 0, n = arr.len();
    while j < n {
        let p = &arr[j]; // (*)
        if *p == i { return p; }
    }
    // If not included yet, add it
    arr.push(i);
    &arr[arr.len() - 1]
}

fn main() { }

The reason that an error is generated is because the scope of the pointer p is 'r. This means that when the pointer is created on the line (*), that pointer is valid from that point until the end of the function. Now, to the reader, it's obvious that if we do not return p, then it is out of scope and so the borrow can be ended. However, the borrow checker does not attempt to track aliasing, so it has no way to know that the pointer is not copied and hidden away. Similarly, in your original example, the borrow checker does not know that the each function doesn't keep it's own copy of the pointers it is giving you in some location. If it did so, those pointers would be invalidated by arr.push.

(Note: it is also true that the borrow checker does not know that the each function implements the for protocol correctly, so it's possible that more loop iterations could continue to run even after a return statement, though I think that after the loop a return would always be honored in any case, at least the way that trans works right now)

[ezyang]

Hey @nikomatsakis, there is one thing I don't quite understand about your explanation, which is why the first code fragment you posted does compile. After all, it is performing a borrow with lifetime 'r, just as in the first case, but somehow, borrowck doesn't consider this borrow live for the rest of the function. So what's different about actually assigning a variable?

[nikomatsakis]

It is not assigning to a variable that makes a difference but rather the control flow. In the first fragment, there is a return that unconditionally follows the borrow, so we know that the borrow is never live after the loop.