相关模式匹配-压缩两个向量

如何在Coq中压缩两个向量？我尝试了下面的代码，但遇到了问题：

Require Import Vectors.Vector.
Import VectorNotations.

(* Non exhaustive pattern-matching: no clause found for patterns [], _ :: _ *)
Fail Fixpoint zip {A B : Type} {n : nat} (a : t A n) (b : t B n) : t (A * B) n :=
match a, b with
| ha :: ta, hb :: tb => (ha, hb) :: zip ta tb
| [], [] => []
end.

(* The term "tb" has type "t B n1" while it is expected to have type "t B n0"
   (cannot unify "n1" and "n0"). *)
Fail Fixpoint zip {A B : Type} {n : nat} (a : t A n) (b : t B n) : t (A * B) n :=
match a, b with
| ha :: ta, hb :: tb => (ha, hb) :: zip ta tb
| _, _ => []
end.

(* The term "a" has type "t A n" while it is expected to have type "t A (S k)". *)
Fail Fixpoint zip {A B : Type} {n : nat} (a : t A n) (b : t B n) : t (A * B) n :=
match n with
| (S k) => ((fst (uncons (a : t A (S k)))), (fst (uncons b))) ::
           zip (snd (uncons a)) (snd (uncons b))
| O => []
end.

那么如何使类型检查器假定两个向量的长度相等呢？