On Aug 27, 2018, at 8:16 PM, Eric Seidel <eric@seidel.io> wrote:

That being said, I'm less concerned about the overloading of the function arrow because Simon seems confident that we can reliably hide it when -XLinearTypes is disabled, even if datatypes are inferred linear. That makes it opt-in complexity, which I don't have a problem with.

I agree that this is opt-in complexity. The problem is that you can't opt-in partially. That is, if someone doesn't care about levity polymorphism or multiplicity polymorphism, then they're OK. If someone cares about both, they're OK. But if someone cares only about one (which is quite sensible in either direction), then they currently have to care about both. If we imagine yet more indices on arrows (e.g. what if we track whether term-level functions are injective? what if we put roles on arrows? both are conceivable) then the situation is worse. Now might be the right time to think about a structure where we can continue to add indices to arrows without overwhelming the cognitive load.