Идрис: функция работает с параметром Nat и не проходит проверку типа с параметром Integer

Я новичок в Идрисе. Я экспериментирую с типами, и моя задача - создать «лук»: функцию, которая принимает два аргумента: число и все остальное и помещает все вList вложенное такое количество раз.

Например, результат дляmkOnion 3 "Hello World" должно быть[[["Hello World"]]], Я сделал такую ​​функцию, это мой код:

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

Результат работы программы:

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

Это именно то, что мне нужно. Но когда я делаю то же самое, но меняю Nat на Integer вот так

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]

Я получаю ошибку:

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)

Почему проверка типов не проходит?

Я думаю это потому чтоInteger может принимать отрицательные значения иType не может быть вычислено в случае отрицательных значений. Если я прав, как это понимает компилятор?

Ответы на вопрос(1)

Решение Вопроса

Вы правы, что тип не может быть вычислен. Но это потому, чтоonionListTypeI не тотально Вы можете проверить это в REPL

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

(Или даже лучше, требуя%default total в исходном коде, что приведет к ошибке.)

Поскольку конструктор типа не тотален, компилятор не нормализуетсяonionListTypeI 0 y вy, Это не тотально, из-за случаяonionListTypeI a b = onionListTypeI (a-1) (List b), Компилятор знает только, что вычитая 1 изInteger результаты кInteger, но не какое именно число (в отличие отNat). Это потому, что арифметика сInteger, Int, Double и различныеBits определяются с основными функциями, такими какprim__subBigInt, И если эти функции не будут слепыми, у компилятора должна быть проблема с отрицательными значениями, как вы и предполагали.

Ваш ответ на вопрос