I thought that maybeToList would be a good function to try Idris2's linearity feature on. I'm aware that maybeToVect would usually be a better choice, but I guess that its implementation wouldn't use the same approach of "linearly using all as in the container".
In linear Haskell, maybeToList :: Maybe a %1 -> [a] needs to use the x in the Just x case linearly, but for Idris2, the following incorrect implementation type-checks:
maybeToList : (1 _ : Maybe a) -> List a
maybeToList (Just x) = []
maybeToList Nothing = []
What signature can I use in Idris2 to get the same behavior here as with linear Haskell?
For reference, the signature of maybeToVect in idris-boot also allows incorrect implementations to type-check:
maybeToVect : Maybe elem -> (p ** Vect p elem)
maybeToVect Nothing = (_ ** [])
maybeToVect (Just j) = (_ ** [j])
Looks like the solution is a bit difficult at the moment, because Idris2 doesn't support multiplicity polymorphism:
The libs for Idris2 have both a linear list and a linear maybe. When switching my type signature to both of these types, the correct solution is indeed the only one that type-checks.