[kibwen]

I can offer no proof but I'm Pretty Sure that one could hack together linear types using procedural macros, though I can't posit how nice they would be to use nor how well they would interact with the rest of the language and ecosystem.

[mafribe]

Wouldn't that be a good path: start with initial experiments based on types-by-macros, and see how well that works. Can't be worse that C++'s template meta-programming.