[tomhoule]

I can't claim to know the details, but my understanding is that the interaction of linear typing with dependent types is an open research problem (see the quantitative type theory papers, for example). It's also a burden on the user rather than the runtime, so it's a tradeoff.

[xiphias2]

Is it still a big burden if the theorem prover can automate checking that a function can be evaluated without ref counting / garbage collector? I understand that it's a very hard problem though.