To all the "why bother" rustaceans

In fact the whole reason Polonius (the newer checker GCC would like to adopt) is under development is that Rust's borrow checkers are checking a semantic constraint, which means Rice's theorem applies, the actual question we have (does this program obey the borrowing rules) is Undecidable.

Rust chooses to answer conservatively, Don't Know counts as No. All three borrow checkers, the one in Rust 1.0, the current one with Non-lexical lifetimes, and Polonius, are conservative, but each increases the range of correct Rust programs which successfully compile over the last.

The conservative choice offers safety, which is Rust's priority, at a cost of programmer inconvenience, which can be iteratively improved upon by working on the borrow checker. Thus, I believe Rust can and should specify that the actual rules are (basically) as you describe, but with a clarifying note that since these are semantic rules any compiler must be conservative. Maybe the note can specify that a conforming compiler must at least be able to allow X where X is some sane baseline of borrow simplicity.