Type-safe linear maybeToList

Question

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])

Answer 1

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.