Multiplicity subtyping with dependent types can break linearity

[KyleDavidE]

trafficstars

Steps to Reproduce

badEq : ((x: Nat) -> Nat) = ((1 x:Nat) -> Nat)
badEq = Refl

Expected Behavior

The term should not typecheck because this can be used to cast (x: Nat) -> Nat to (1 x:Nat) -> Nat, this sort of trick could easily be used to make "safe" terms of type IO ((0 x: Type) -> IO x -> x) which could grotesquely break things.

Observed Behavior

It type checks, though it is of note that

1. If you reverse the order in the type definition, (i.e. badEq : ( (1 x:Nat) -> Nat ) = ( (x: Nat) -> Nat)) it does not type check
2. This doesn't work with erased arguments

[edwinb]

Hmm, this is a bit awkward. The subtyping rules are to allow you to pass linear functions to HOFs which don't have linearity constraints (but not vice-versa). But this suggests the rules are too liberal.

There's no subtyping rules between 0-multiplicity things and others, so I don't think this can cause erased things to be needed at run time, but if you can use it to pass non-linear functions in a context that requires linearity, that would be bad.

[KyleDavidE]

It seems to me that the linearity rules subtyping should only lift over (dependent) function types. In an ideal world it would also lift over positive functors, but I have no idea if that is possible.

The haskell-y way to solve this problem would be linearity polymorphism rather than subtyping but I can't imagine terms with linearity polymorphism would be pleasant to reason about.