Coq adding a new variable instead of using the correct one -

i'm working on own implementation of vectors in coq, , i'm running bizarre problem.

here code far:

inductive fin : nat -> type :=   |fz : forall n, fin (s n)   |fs : forall n, fin n -> fin (s n).  definition emptyf(a : type) : fin 0 -> a.   intro e; inversion e. defined.  inductive vec(a : type) : nat -> type :=   |nil  : vec 0   |cons : forall n, -> vec n -> vec (s n).  definition head(a : type)(n : nat)(v : vec (s n)) : :=   match v   |cons _ =>   end.  definition tail(a : type)(n : nat)(v : vec (s n)) : vec n :=   match v   |cons _ w => w   end.  fixpoint index(a : type)(n : nat) : vec n -> fin n -> :=   match n n return vec n -> fin n ->   |0   => fun _ => emptyf _   |s m => fun v => match                      |fz _ => head v                      |fs j => index (tail v) j                      end   end. 

everything tail compiles fine, when try compile index, receive following error:

error: in environment index : forall (a : type) (n : nat), vec n -> fin n -> a : type n : nat m : nat v : vec (s m) : fin (s m) n0 : nat j : fin n0 term "j" has type "fin n0" while expected have type "fin m". 

clearly, culprit coq introduces new variable n0 instead of assigning j type fin m, though possible type j result in i being built j. idea why happen, , how might able resolve issue?

i find vec , fin hard use in general, these days use 'i_n , n.-tuples t math-comp, naturals , lists irrelevant proof attached. however, if want continue fun of complex pattern matches, try define stronger pattern matching principle:

definition fin_case t m (i : fin m) : t -> (fin (pred m) -> t) -> t :=   match   | fz _   => fun fn fz => fn   | fs _ j => fun fn fz => fz j   end. 

once have fin_case, function definition works:

fixpoint index (a : type) (n : nat) : vec n -> fin n -> :=   match n n return vec n -> fin n ->   | 0   => fun _ => emptyf _   | s m => fun v => fin_case (head v) (index (tail v))   end.