The Coq mailing list

[Adam Chlipala <adam AT chlipala.net>]

And I just want to suggest the way that _I_ would write this function, 
which involves no proofs and no extra type annotations.

Fixpoint next (n : nat) z (t : test z) : test (z+1) -> Z :=
  match n with
    | 0%nat => fun _ => 3
    | S n' =>
      match t with
        | down _ d => fun _ => next n' _ d (down _ d)
        | up   _ u => fun _ => 3
      end
  end.

If you read CPDT, you will learn the tricks you need for almost every 
dependently-typed function to be this easy to write.  If you try to 
extrapolate from experience in normal functional programming, it will 
probably take a _lot_ of experimenting to get there.

(I can anticipate some reservations about the above code taking 
advantage of some aspect of the simplified function definition you 
gave.  If this code _did_ use the function's second [test] argument in 
an interesting way, it really would be available with the appropriate 
type in the appropriate places.)