Loss of Linearity in Interaction of Abstract Interfaces and Linear State Transformer Monad

[Lichborne]

A full explanation of and a minimal case for reproducing the problem can be found here: https://github.com/Lichborne/IdrisLinearityIssue/blob/main/ErrorExamples.idr Depends only on Data.Linear.LVect and Data.Linear.Notation

Steps to Reproduce

Firstly, we create a linear state transformer monad as in the file, with the usual functions. In the real-life cenario, there are two slightly different versions, but this is sufficient to get the issue.

public export
data LStateT: (initialType : Type) -> (finalType : Type) -> (returnType : Type) -> Type where
  MkLST : (initialType -@ (LPair finalType returnType)) -@ LStateT initialType finalType returnType

Then, we have two separate abstract interfaces

||| some abstract interface, dummy
interface AbstractInterface (0 t : Nat -> Type) where
        run : LStateT (t m) (t m) (LVect n Nat) -@ (LVect n Nat)
  
||| some other abstract interface
interface OuterInterface (0 t : Nat -> Type) where
        |||some function from LVect to LStateT
        outerFunc : {n : Nat} -> {i : Nat} -> (LVect i Nat) -@ LStateT (t n) (t n) (LVect i Nat)

Then, we attempt to first use the above, and then take the LVect out and move it up and do something with it in the outer interface. innerFuncDummy is just a dummy function on the inner interface. See ErrorExamples.idr.

doubleLayerFunc : OuterInterface t => (n : Nat) -> (m: Nat) -> LVect n Nat -@ LStateT (t (m)) (t (m)) (LVect n Nat)
doubleLayerFunc 0 m [] = pure []
doubleLayerFunc (S k) m qs = do
        lvec <- outerFunc (run $ innerFuncDummy {i = (S k)} {n = m} (qs))
        pure lvec

Expected Behavior

Type-checks.

Observed Behavior

Fails to check that qs is linear ("use of non-linear qs in a linear context").

I hope I am doing something wrong here. Otherwise, qs is clearly linear, used in a linear context, so it seems to me that this should be alright.