Ah great! So to summarize:

- we destroy a linear value either by destructuring it ourselves, or by calling a cleanup function that transitively destructures it

- we can make a type opaque to importers of our module, which precludes direct destructuring by the user

- the compiler forces the user to eventually destroy the linear value

- therefore the user must call our cleanup function

And it's our responsibility to ensure the function implements the correct cleanup logic.