To come back to this point:
Well thatās exactly what I meant with extensions that let you express that t.v is borrowed. I guess Box<[i32] + 'a> is supposed to mean that the contents of the Box are borrowed for the lifetime 'a? (This specific syntax is already in use and means something different, but thatās not important.)
You canāt express in current Rust that something is borrowed, there is no syntax for it. You create the borrows and the compiler computes the loans from that. Thatās partly because it was never deemed important. Another reason is that loans are relatively complicated to describe: they can concern only parts of a value (e.g. a single field of a single field), there are several kinds of borrows (more than & and &mut), and there might be more dimensions Iām not even aware of since I never really worked on this part of the compiler. To give you an idea of the framework weāre talking about and into which proposed rules have to be integrated, librustc_borrowck's readme is a good start although itās probably pretty outdated by now.
But IMHO the most important issue is that the model is not complicated enough: e.g., there is no way to reason about āthe contents of a collectionā (e.g. you canāt extend a vec while you borrow one of its elements, but thatās because the methods you used to create the borrow create a borrow of the whole vec, and extending requires a mutable borrow). For example, before even tackling the problem this thread is about, I would expect a way to permit calling vec.len() while mutably borrowing vec[0].
There is also currently no way for the compiler to reason āokay this path of x is borrowed but itās still okay to move x because [ā¦]ā. Furthermore, non-lexical borrowing will probably make the whole story even more complicated.
To reiterate, none of the things Iām saying are supposed to imply that a sound static analysis is impossible, but all the complications Iām listing here (plus my inuition gained from fighting the borrow checker) make me pretty sure that it would require several big extensions, possibly even a departure from core tenets of the current lifetime system.