Coq mutual fixpoint problem

CT.v

Section CT.
  Context {F : Set -> Set}.
  Class Functor := { fmap {a b : Set} : (a -> b) -> F a -> F b;
                     fmap_id {t : Set} : forall ft, fmap (fun a : t => a) ft = ft;
                     fmap_fusion {a b c : Set} : forall (f : a -> b) (g : b -> c) fa, fmap g (fmap f fa) = fmap (fun e => g (f e)) fa 
                   }.

  Class Pure `{Functor} := { pure {t : Set} : t -> F t }.
  Class Applicative `{Pure} := { zip {a b : Set} : F a -> F b -> F (a * b)%type;
                                 ap {a b : Set} : F (a -> b) -> F a -> F b := fun ff fa => fmap (fun t => match t with (f, e) => f e end) (zip ff fa);
                                 zipWith {a b c : Set} : (a -> b -> c) -> F a -> F b -> F c := fun f fa fb => ap (fmap f fa) fb
                               }. (* leaving the laws off for now *)

  Class Pointed `{Functor} := { point {t : Set} : F t }.
End CT.
                                             

Demo.v

Require Import CT.
Require Import VectorUtils.
Require Import ListUtils.

Inductive t1 : Set :=
| a1 : t1
| a2 {n} : Vector.t t1 n -> t1
| a3 {n} : Vector.t t2 n -> t1
with t2 : Set :=
     | b1 : t2
     | b2 {n} : Vector.t t1 n -> t2
     | b3 {n} : Vector.t t2 n -> t2.

Inductive t3 : Set :=
| c1 : t3 -> t3 -> t3 
| c2 {n} : Vector.t t1 n -> t3
| c3 {n} : Vector.t t2 n -> t3.

Inductive t4 : Set :=
| d1 : t4
| d2 : t4 -> t4 -> t4
| d3 {n} : Vector.t t4 n -> t4
| d4 {n} : Vector.t t4 n -> t4.

Fixpoint f1 f : list t1 :=
  match f with
  | d1 => [a1]
  | d2 x x0 => f1 x ++ f1 x0
  | d3 x => map a2 (VectorUtils.traverse (fun g => f1 g) x)   
  | d4 x => map a3 (VectorUtils.traverse f2 x)
  end
with f2 f : list t2 :=
  match f with
  | d1 => [b1]
  | d2 x x0 => f2 x ++ f2 x0
  | d3 x => map b2 (VectorUtils.traverse f1 x)
  | d4 x => map b3 (VectorUtils.traverse f2 x)
  end.

ListUtils.v

Require Import CT.
Require Import Lists.List.
Import ListNotations.
Module ListUtils.
  Global Program Instance list_Functor : @Functor list := {| fmap := map;
                                                             fmap_id := map_id;
                                                             fmap_fusion := map_map
                                                          |}.
  Global Instance list_Pointed : @Pointed list _ := {| point := @nil |}.
  Global Instance list_Pure : @Pure list _ := {| pure _ a := [a] |}.
  Global Instance list_Applicative : @Applicative list _ _ := {| zip := @combine |}.
End ListUtils.

VectorUtils.v

Require Import CT.
Require Import ListUtils.
Require Export Vectors.Vector.

Import VectorNotations. 
Module VectorUtils.
  Global Program Instance vector_Functor {n} : @Functor (fun t => Vector.t t n) := {| fmap _ _ f := map f;
                                                                                |}. 
  Next Obligation. induction ft; simpl; f_equal; auto. Defined.
  Next Obligation. induction fa; simpl; f_equal; auto. Defined.
  Global Instance vector_Pointed : @Pointed (fun t => Vector.t t 0) _ := {| point := nil |}.
  Global Instance vector_Pure : @Pure (fun t => Vector.t t 1) _ := {| pure _ x := [x] |}.

  Program Definition sequence {F} {t : Set} {n} `{Applicative F} : Vector.t (F t) n -> F (Vector.t t n).
  intros v. induction v. eapply pure; trivial.  apply (@point (fun f => Vector.t f 0) _ _). exact (ap (fmap (fun a b => a :: b) h) IHv).
  Defined.
  Program Definition traverse {F} {t u : Set} {n} `{Applicative F} (f : t -> F u) : Vector.t t n -> F (Vector.t u n) :=
    fun v => sequence (fmap f v).
End VectorUtils.