Upon further reflection, I don't think 'local/global correctness' distinction this was expressed very well or very usefully. The 'hole' example papers over so many details as to be misleading.

So here's another, hopefully better expression:

Rust's type system wrt lifetimes is not very expressive, compared with 'dynamically-typed' c. It can't represent things like 'the value returned by this function must remain alive for no more than 15 successive invocations of this function'.