Refining a Vecs invariants from program flow is interesting. I'm not sure if it's a good thing or not. It hides an interaction between references and dynamic co

Refining a Vecs invariants from program flow is interesting. I'm not sure if it's a good thing or not. It hides an interaction between references and dynamic container types, possibly "protecting" the programmer from understanding the semantics of the program. I also don't see in this particular case why the reference would be taken before the potential resizing push but used after the push. Maybe with a clearer use-case I could see the point? This would also introduce dynamic checks at compile time, since you need to run the program in order to compile it now, as the overload selection/precondition depends on the runtime state of the Vec. This necessarily requires a less-strict compilation/interpretation mode to be run before the borrow checker/other static analysis is done, since the static analysis can't know which function is being called. I suppose this is similar to compile-time programming. It strikes me also, that you could do all this at runtime if you wanted, simply by manually incrementing length if length < cap and assigning to the newly created spot.