It's all about the motive, baby

Motive.idr

import Data.Vect 

-- This is a paramorphism (aka primitive recursion) on Vectors 
foldr : (motive : (k : Nat) -> Vect k a -> Type) ->
        ((l : Nat) -> (x : a) -> (xs : Vect l a) -> motive l xs -> motive (S l) (x :: xs)) ->
        motive Z [] ->
        (vec : Vect n a) ->
        motive n vec
foldr {n = Z} motive step base [] = base
foldr {n = S k} motive step base (x :: xs) = step k x xs (foldr motive step base xs)