Dlaczego Idris nie zaakceptuje mojego spasowania?

Question

Oto wektor, którego elementy są indeksowane przez długość wektora.

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

Chcę złożyć 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) 

pojawia się następujący błąd w przypadku kroku:

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

jestem mylić co błąd próbuje mi powiedzieć. Moja definicja foldr nie wygląda źle na mnie, i to działa dobrze w 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) 

Dlaczego nie mój typ kontroli w foldr Idris?

Answer 1

Idris miesza twoje foldr z już istniejącym. Możesz rozwiązać ten problem, kwalifikując wystąpienie rekursywne foldr lub zmieniając nazwę swojego 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)