From my understanding, variation is a type system construct, based on which the compiler could do much of the intended semantics of the whole lifetime idea just from purely a type system level, as illustrated in the example provided in nomicon: the assign function wants a concrete same type T for its two input arguments, while finding it not possible since &mut T is invariant over T. So far so good.
fn assign<T>(input: &mut T, val: T) {
*input = val;
}
fn main() {
let mut hello: &'static str = "hello";
{
let world = String::from("world");
assign(&mut hello, &world);
}
println!("{hello}"); // use after free 😿
}
But how about this snippet?
fn main() {
let mut s = String::from("outer");
let mut v = Vec::new();
v.push(&mut s);
{
let mut s = String::from("inner");
v.push(&mut s);
}
// code compiles iff this line is commented out
// what does variance have to say about this `println!`?
println!("{:?}", v);
}
I understood that by the fact &'a mut T is covariant over 'a, Rust could do type resolution to determine that the vector is indeed something like Vec<&'inner mut String>, i.e. the concrete type of T in Vec<T> is &'inner mut String, making the inner block compiles, but how exactly does the variant system determine that the println! line is inappropriate? In other words, my question is that, to my understanding, variance is for type system to do type resolution, which means it's applicable iff there are several types and we'd like to see if they could be coerced into same type, but println! doesn't have the other type to compare to.
Or, it might be the case that variance just isn't the whole picture, and ultimately we'd rely on some other lifetime semantics to determine if code is valid Rust? To add on that, the whole subtype idea that variance relies on also ultimately stems from lifetime being covered by some other lifetime...
On a side note, what exactly is a memory model, and what does it mean to say that Rust currently doesn't have one?
Lifetimes create constraints. Variance is only part of that. The borrow checker generates a constraints equation, and check if there is a solution.
Variance is one kind of constraint indeed, it tells us if a lifetime can grow or shrink. But there are other constraints. The ones I know (and I believe those are the only that exists) are outlives constraints, lifetime constraints and mutable xor shared constraints.
Outlive constraints are generated either because they are written as bounds ('a: 'b, T: 'a), or because the control flow necessitates them. For example. If we push a reference &'a str to a vector Vec<&'b str>, we know 'a: 'b.
Lifetime constraints arise because of the lifetime of variables. If a variable is dropped before another one, its lifetime is smaller, and this creates a constraint.
Mutable xor shared constraints are generated to ensure there are no overlapping mutable references.
Back to your snippet. Let's annotate the lifetimes (using imaginary syntax. I also ignored a bunch of lifetimes):
fn main() {
let mut s: 'a = String::from("outer");
let mut v: Vec<'b> + 'c = Vec::new();
v.push(&'d mut s);
{
let mut s: 'e = String::from("inner");
v.push(&'f mut s);
}
&'g v; // I replaced `println!()` with this since this is equivalent for borrows.
}
Our constraints (note, I'm not claiming this is what the borrow checker will actually do. It's only a demonstration):
'd: 'b, 'f: 'b // pushed into the vector
'e: 'f // the value lifetime
'e == L6..7 // the value lifetime
'b: 'c // with T<'a>, 'a always outlives T
'c: 'g // because of the borrow
'g == L10 // this is where it happens
If you try to resolve this system, you will get L6..7: L10, which is clearly false. This is why the borrow checker rejects this program.
If we omit the last line, though, we omit the 'c: 'g and 'g == L10, constraints, and then the system has a solution.