I don't see how, in the presence of unrestricted function types, you can tag values as linear unless you have a separate kind for linear values. I'd be interested to know how Rust does it.