Why won't Idris accept my custom fold?

Question

Here's a vector whose elements are indexed by the length of the vector.

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

I want to fold up an 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)

I get the following error in the step case:

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

I'm confused about what the error is trying to tell me. My definition of foldr doesn't look wrong to me, and it works just fine 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)

Why won't my foldr type check in Idris?

Answer 1

Idris is mixing up your foldr with the already existing one. You can solve this by qualifying the recursive foldr occurrence, or renaming your 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)