Warum akzeptiert Idris meine benutzerdefinierte Falte nicht?

Question

Hier ist ein Vektor, dessen Elemente durch die Länge des Vektors indiziert sind.

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

Ich möchte eine IxVect zusammenzufalten.

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) 

Ich erhalte den folgenden Fehler in dem Schritt Fall:

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

Ich bin verwirrt über das, was der Fehler, mir zu sagen versucht. Meine Definition von foldr sieht mir nicht falsch, und es funktioniert gut in 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) 

Warum wird nicht meine foldr Typprüfung in Idris?

Answer 1

Idris vermischt Ihre foldr mit der bereits bestehenden. Sie können dies lösen, indem Sie das rekursive foldr Vorkommen qualifizieren oder Ihr foldr umbenennen.