[Agda] primitive recursion over the natural numbers

[Ed Morehouse]

I'm quite new to agda, so please forgive me if I'm overlooking the obvious.

I wanted dependent primitive recursion over the natural numbers, which I defined 
like this:


   recNat : (A : Nat -> Set) -> A zero -> ((i : Nat) -> A i -> A (suc i)) -> (n 
: Nat) -> A n
   recNat A z s zero = z
   recNat A z s (suc n) = s n (recNat A z s n)

Then I tried it out on a vector ( ([0] , _:::_) are my vector (nil , cons) ).
This worked as I expected:

   recNat (Vec Nat) [0] (\ n v -> (n ::: v)) 5

But the eta equivalent:

   recNat (Vec Nat) [0] _:::_ 5

yields the error:

   The metavariable _839 cannot depend on i
   because it does not depend on any variables
   when checking that the expression _:::_ has type
   (i : Nat) -> Vec Nat i -> Vec Nat (suc i)

I don't understand why there should be a difference.

Next I noticed that when the result type does not depend on Nat, that is, when A 
is a constant function, agda seems to be able to reliably infer the first 
argument of recNat.  For example, this worked fine ( ([] , _::_) are my list 
(nil , cons) ):

   recNat _ [] _::_ 5

(even the issue above doesn't come up).  How can I check (prove or disprove) 
that agda can always infer the first argument in this case?

Then I defined the following:


   constType : (B : Set) -> {A : Set} -> A -> Set
   constType B a = B

   recNatConst : {A : Set} -> A -> (Nat -> A -> A) -> Nat -> A
   recNatConst = recNat (constType _)

which I suppose should be equivalent to non-dependent primitive recursion over 
the naturals.

I realize that, in general, the first argument to recNat is not inferable, but I 
wonder if when A is--i'm not really sure about terminology here--maybe, an 
inductive family, then the first argument could be inferable.  Concretely, I'm 
asking is there a function:


   recNatInd : {A : ???} -> A zero -> ((i : Nat) -> A i -> A (suc i) ) -> (n : 
Nat) -> A n

such that

   recNatInd [0] (\ n v -> (n ::: v)) 5

normalizes to a value?


Thanks to anyone who made it through all that and is willing to help.


-Ed