Perché Idris non accetta la mia piega personalizzata?

Question

Ecco un vettore i cui elementi sono indicizzati dalla lunghezza del vettore.

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

Voglio ripiegare un 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) 

ottengo il seguente errore nel caso passo:

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

Sono confuso su ciò che l'errore sta cercando di dirmi. La mia definizione di foldr non sembra sbagliato per me, e funziona bene 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) 

Perché non il mio foldr tipo si verifica nel Idris?

Answer 1

Idris sta mescolando il tuo foldr con quello già esistente. È possibile risolvere questo problema qualificando l'occorrenza ricorsiva foldr o rinominando lo 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)