Почему Идрис не примет мою обычную складку?

Question

Вот вектор, элементы которого индексируются по длине вектора.

data IxVect : (n : Nat) -> (a : Nat -> Type) -> Type where 
    Nil : IxVect 0 a 
    (::) : a n -> IxVect n a -> IxVect (S n) a 

Я хочу, чтобы сложить в IxVect.

total 
foldr : {b : Nat -> Type} -> ({m : Nat} -> a m -> b m -> b (S m)) -> b Z -> IxVect n a -> b n 
foldr f z Nil = z 
foldr f z (x :: xs) = f x (foldr f z xs) 

Я получаю следующее сообщение об ошибке в шаге случае:

test.idr:9:25: 
When elaborating right hand side of Main.foldr: 
Can't convert 
     (Nat -> Type) -> Type 
with 
     Type -> Type 

Я смущен о том, что пытается ошибка сказать мне. Мое определение foldr не смотрит мне неправильным, и он прекрасно работает в Haskell:

data Nat = Z | S Nat 

data IxVect n a where 
    Nil :: IxVect Z a 
    Cons :: a n -> IxVect n a -> IxVect (S n) a 

foldr :: (forall m. a m -> b m -> b (S m)) -> b Z -> IxVect n a -> b n 
foldr f z Nil = z 
foldr f z (Cons x xs) = f x (foldr f z xs) 

Почему не будет мой foldr тип проверки в Идрис?

Answer 1

Идрис смешивает ваш foldr с уже существующим. Вы можете решить эту проблему, указав рекурсивное событие foldr или переименовав foldr.

foldr : 
    {n : Nat} -> {a, b : Nat -> Type} 
    -> ({m : Nat} -> a m -> b m -> b (S m)) -> b Z -> IxVect n a -> b n 
foldr f z Nil = z 
foldr f z (x :: xs) = f x (Main.foldr f z xs)