Idris: function works with Nat parameter and fails type checking with Integer parameter

I am new to Idris. I am experimenting with types and my task is to make an "onion": a function that takes two arguments: a number and whatever and puts whatever into List nested such number of times.

For example, the result for mkOnion 3 "Hello World" should be [[["Hello World"]]]. I've made such a function, this is my code:

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

The result of program work:

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

This is exactly what I need. But when I do the same, but change Nat to Integer like this

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]

I get an 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)

Why does type checking fails?

I think this is because Integer can take negative values and Type can't be computed in case of negative values. If I am right, how does the compiler understand this?

Solution

You are right, that the type can't be computed. But that is because the onionListTypeI is not total. You can check this in the REPL

*test> :total onionListTypeI
Main.onionListTypeI is possibly not total due to recursive path:
    Main.onionListTypeI, Main.onionListTypeI

(Or even better, demanding %default total in the source code, which would raise an error.)

Because the type constructor is not total, the compiler won't normalize onionListTypeI 0 y to y. It is not total, because of the case onionListTypeI a b = onionListTypeI (a-1) (List b). The compiler does only know that subtracting 1 from an Integer results to an Integer, but not which number exactly (unlike when doing it with a Nat). This is because arithmetic with Integer, Int, Double and the various Bits are defined with primary functions like prim__subBigInt. And if these functions wouldn't be blind, the compiler should have a problem with negative values, like you assumed.