> there’s not a single concrete example of how linear types would help real-life code

Given what Rust has achieved in terms of memory management, that seems like a strange claim to make?

There are also some rather concrete examples here:

http://edsko.net/2017/01/08/linearity-in-haskell/