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.

[gallais]

What's the type of innerFuncDummy? Can you please provide a self-contained file.

[Lichborne]

What's the type of innerFuncDummy? Can you please provide a self-contained file.

Hi! Thanks so much for your response. The self-contained file is linked at the very top, I will put it here again: https://github.com/Lichborne/IdrisLinearityIssue/blob/main/ErrorExamples.idr

innerFuncDummy is a dummy function : AbstractInterface t => (i : Nat) -> (m: Nat) -> LVect i Nat -@ LStateT (t m) (t m) (LVect i Nat), that is;

innerFuncDummy : AbstractInterface t => (i : Nat) -> (m: Nat) -> LVect i Nat -@ LStateT (t m) (t m) (LVect i Nat)
innerFuncDummy 0 m any = pure any
innerFuncDummy (S k) m (q::qs) = pure (q::qs)   

In the real-life scenario, there is a function here that actually does something, which is why this is included, but in this case it's just lifting to the right context.

Hope this helps.

[gallais]

innerFuncDummy takes three arguments. The first two are (i : Nat) and (m: Nat) but you used the names i and n to refer to them. Consequently qs is typechecked as if it were the m argument, which has an unrestricted quantity. Hence the error.

Writing innerFuncDummy {i = (S k), m = m} qs instead, I'm not sure why I still get the error.

Ditching the named application style entirely, innerFuncDummy (S k) m qs gives us a different error:

Can't find an implementation for AbstractInterface ?t.

Moving on to innerFuncDummy {t} (S k) m qs as t cannot be solved gives us

Can't find an implementation for AbstractInterface t.

Adding a AbstractInterface t => constraint to the type of doubleLayerFunc we get code that works.

There seems to be an issue with the way named application is elaborated.

[Lichborne]

Dear gallais,

Thanks so much! Hope I did not waste your time.

Best, Lichborne

[gallais]

Not at all, there does seem to be a bug hiding behind the non-bug of the shrunken case. Thanks for taking the time to submit a self-contained reproducer, sorry I did not notice it upon first read.