This is wonderful, can't wait to use it for my own code. :) Though at the moment the semantics isn't entirely clear to me. For instance, in the protocol exampl

This is wonderful, can't wait to use it for my own code. :) Though at the moment the semantics isn't entirely clear to me. For instance, in the protocol example, shouldn't the pair be using multiplicative linear conjunction? It doesn't matter so much for a function receiving two Ints, but what's the semantics for a function receiving multiple ressources? I guess you can use an impredicative encoding, e.g. A ⊗ B = forall C. (A ⊸ B ⊸ C) ⊸ C but isn't it more usable if it's built into the compiler?