Confused about standard overconstrained lifetime example

help
1

I know that the following standard example is refused by the borrow checker:

struct X<'a, T>{s: &'a T}
impl<'a, T> X<'a, T> {
    fn foo(&'a mut self) {}
}
fn main() {
    let s = String::new();
    let mut x = X{s: &s};
    x.foo();
    x.foo();
}

The given explanation is: the implementation of 'foo' constrains the lifetime of the mutable borrow of 'self' to equal the lifetime of the held reference. But the held reference, and therefore the mutable borrow created at the first 'foo' call, lives through the second 'foo' call, which tries to create a second mutable reference (QED).

To me, this is a bit glib, and I feel like it's sweeping another possibility (which would compile) under the carpet. Let me explain my thought process.

The way I've been able to make sense of lifetime annotations is just to say that, going into each function call, the compiler has a notion of the types (including lifetimes) of the arguments, and it does the minimal amount of coercion to make them match the function signature. That is why, when you pass values x, y with lifetimes 'x, 'y to a function with signature (x: &'a X, y: &'a Y) the compiler doesn't puke, but just selects 'a to be the intersection of 'x and 'y and coerces x, y to &'a X, &'a Y for the duration of the function call.

In my example, let's say that the reference held by x has lifetime the entire body of main, call it 'main_body. It seems clear that the compiler is inferring a type X<'main_body, String> for x. Then at both 'foo' calls it's using the implementation of 'foo' for X<'main_body, String> which requires a &'main_body mut self, hence the error.

However, you could imagine a different logical flow. The compiler could reason instead that the two mutable borrows should have disjoint lifetimes, e.g. just the single lines that make use of them, 'line_8 and "line_9. You could imagine that the compiler handles the first 'foo' call by coercing x to X<'line_8, String>, which only requires a &'line_8 mut self, and likewise handles the second 'foo' call by coercing x to X<'line_9, String>, which only requires a &'line_9 mut self, and there would be no issue with the borrow checker.

Why doesn't it do this? Note that I'm not saying it should, I'm just genuinely confused about why in the formal model of type inference this isn't what happens.

N.B. I don't think the issue is that the selection of the type of x for the 'foo' call somehow happens before looking at the signature of 'foo'. Indeed, you can produce a functionally identical example using a function rather than a method, like this:

fn foo<'a, T>(x: &'a mut X<'a, T>) {}
...
    foo(&mut x);
    foo(&mut x);
...

When you look at it like that, the logic I'm suggesting seems even more reasonable: ordinarily, due to non-lexical lifetimes, we would see two mutable borrows in a row like that and just assume that the compiler knew to make sure that the first borrow ended before the second began.

TLDR: why do my constraints appear to PROMOTE the lifetime of the mutable borrow rather than DEMOTING the lifetime parameter in the type of x ???

2

If the two foo method calls on lines 8 and 9 were to be allowed, then correct type being used on line 8 would actually need to be &'line_8 mut X<'s, String>, where 's is the duration where x borrows s. Because &mut is invariant, this type cannot be converted into a &'line_8 mut X<'line_8, String>

The reason the conversion is disallowed is because, if the conversion were to be allowed, then, in a more complicated setup, the foo() method might get a reference to part of X itself, and store that reference inside T. The reference would then, in the second foo() call, coexist with a &mut X reference, which is unsound.

1 Like
3

Here's an example of a use-after-free that could occur if the conversion I mentioned was allowed:

struct X<'a>{s: &'a str, other: String}
impl<'a> X<'a> {
    fn foo(&'a mut self) {
        if self.other == "" {
            self.other = String::from("abcd");
        } else {
            self.other = String::new();
        }
        println!("{:?}", self.s);
        self.s = &self.other;
    }
}

fn convert<'a, 'b>(x: &'a mut X<'b>) -> &'a mut X<'a> {
    // lie to the borrow checker
    unsafe { std::mem::transmute(x) }
}

fn main() {
    let s = String::new();
    let mut x = X{s: &s, other: String::new()};
    convert(&mut x).foo();
    x.foo();
}
3 Likes
4
1 Like
5

The technical term you may be looking for is "variance". It doesn't choose the intersection, incidentally, but the equality constraint does mean that any lifetime that works must be within the intersection.

Lifetimes under &mut _ are invariant, meaning they can't be coerced to something shorter (or longer). The reason is that allowing variance would be, generally speaking, unsound -- you could create use-after-free situations and so on.

For example (the scenario @themathas described).

Or like so.

The constraints say that the type of x and the borrow of x used to call x.foo have to have exactly the same lifetime, due to a combination of invariance under &mut _ and equating them by giving them the same generic parameter in foo's signature.

In the body of main, the type and thus the lifetime has to be valid wherever x is used, and the exclusive borrow has to be that long too; once the exclusive borrow which is as long as the validity of the type is created, the value cannot be used ever again, except through that borrow -- because it is exclusive and lasts for as long as the type is valid.

3 Likes
6

Thank you all very much, this makes sense. I can tell I’m going to like it here!

N.B. I actually did know that &mut T is invariant in T, but somehow missed that my proposal broke that. I think the version where ‘foo’ is a function and ‘main’ contains the lines

…
    foo(&mut x);
    foo(&mut x);
…

makes this clearer: at the moment you construct &mut x, you’re still in the frame of ‘main’, so it has to be of type &mut X<‘main_frame>, and now the type of x is locked down when passing to foo’s frame since &mut T is invariant in T.

7

This topic was automatically closed 90 days after the last reply. We invite you to open a new topic if you have further questions or comments.