Cool. Actually I should know more about this since I took a lecture series with Krishnaswami on this topic. He combines the two type systems in a way that makes

Cool. Actually I should know more about this since I took a lecture series with Krishnaswami on this topic. He combines the two type systems in a way that makes sense and can produce a programming language. But yes, for the linearity control you'd need to model variables within the type system and indirect to a function handling h's resource relationship instead of using it directly. Formally I would like to compare linear types and dependent types and their ability to encode or not each other. I don't know what the tools for that are.