[throwawaymaths]

no you just need analysis with a dependent type system (which linear types are a subset of). it doesn't have to be in the compiler. there was a proof of concept here a few months ago:

https://news.ycombinator.com/item?id=42923829

https://news.ycombinator.com/item?id=43199265