Soy nuevo en Idris. Estoy experimentando con tipos y mi tarea es hacer una "cebolla": una función que toma dos argumentos: un número y lo que sea y pone lo que sea enList anidado tal cantidad de veces.

Por ejemplo, el resultado paramkOnion 3 "Hello World" debiera ser[[["Hello World"]]]. He hecho tal función, este es mi código:

onionListType : Nat -> Type -> Type
onionListType Z b = b
onionListType (S a) b = onionListType a (List b)

mkOnionList : (x : Nat) -> y -> onionListType x y 
mkOnionList Z a = a
mkOnionList (S n) a = mkOnionList n [a]

prn : (Show a) => a -> IO (); 
prn a = putStrLn $ show a;

main : IO()
main = do
    prn $ mkOnionList 3 4
    prn $ mkOnionList 2 'a'
    prn $ mkOnionList 5 "Hello"
    prn $ mkOnionList 0 3.14

El resultado del trabajo del programa:

[[[4]]]  
[['a']]  
[[[[["Hello"]]]]]  
3.14

Esto es exactamente lo que necesito. Pero cuando hago lo mismo, pero cambio Nat a Integer así

onionListTypeI : Integer -> Type -> Type
onionListTypeI 0 b = b
onionListTypeI a b = onionListTypeI (a-1) (List b)

mkOnionListI : (x : Integer) -> y -> onionListTypeI x y 
mkOnionListI 0 a = a
mkOnionListI n a = mkOnionListI (n-1) [a]

Me sale un error:

When checking right hand side of mkOnionListI with expected type   
    onionListTypeI 0 y

Type mismatch between  
    y (Type of a) and   
    onionListTypeI 0 y (Expected type)

¿Por qué falla la verificación de tipo?

Creo que esto es porqueInteger puede tomar valores negativos yType no se puede calcular en caso de valores negativos. Si tengo razón, ¿cómo entiende esto el compilador?