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

[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.