20070530-3

You should be able to do this.

module Test where

data Nat : Set where
  zero : Nat
  suc  : Nat -> Nat

data Vec : Nat -> Set where
  []   : Vec zero
  _::_ : {n : Nat} -> Nat -> Vec n -> Vec (suc n)

f : (n : Nat) -> Vec n -> Nat
f n@._ [] = n