How to use data from Maybe as Vect size variable

Question

I'm trying to write a simple program that asks the user about the list size and shows content from that list by index also by the user's input. But I've stuck. I have a function that builds a list by a number. Now I want to create another function that uses Maybe Nat as input and returns Maybe (Vect n Nat). But I have no idea how to accomplish this. Here is the code:

module Main

import Data.Fin
import Data.Vect
import Data.String

getList: (n: Nat) -> Vect n Nat
getList Z = []
getList (S k) = (S k) :: getList k 

mbGetList : (Maybe Nat) -> Maybe (Vect n Nat)
mbGetList mbLen = case mbLen of
    Just len => Just (getList len)
    Nothing => Nothing

main : IO ()
main = do 
    len <- readNum
    -- list <- mbGetList len
    putStrLn (show len)

And here is the error:

   |
55 |     Just len => Just (getList len)
   |                       ~~~~~~~~~~~
When checking right hand side of Main.case block in mbGetList at main.idr:54:24-28 with expected type
        Maybe (Vect n Nat)

When checking argument n to function Main.getList:
        Type mismatch between
                n (Inferred value)
        and
                len (Given value)

I've tried to declare an implicit variable. The code compiles, but I can't use it (at least throw repl). Also, I've tried to use dependant pair and also failed. Maybe I should use Dec instead of Maybe? But how??? Another attempt was a try to use map function. But in that case, I have an error like that: Can't infer argument n to Functor.

So, what I've missed?

Answer 1

This answer doesn't feel optimal, but here goes

mbGetList : (mbLen: Maybe Nat) -> case mbLen of
  (Just len) => Maybe (Vect len Nat)
  Nothing => Maybe (Vect Z Nat)
mbGetList (Just len) = Just (getList len)
mbGetList Nothing = Nothing

I think the difficulty comes from the fact that there's no well-defined length for the Vect if you don't have a valid input