Idris: function works with Nat parameter and fails

Question

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?

Answer 1

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.