The Coq mailing list

[Stefan Monnier <monnier AT iro.umontreal.ca>]

> Definition gfoldT
>   (N:Type -> Type)
>   (M:Type -> Type)
>   (var : forall A:Type, M A -> N A)
>   (app : forall A:Type, N A -> N A -> N A)
>   (lam : forall A:Type, N (Incr A) -> N A)
>   (k   : forall A:Type, Incr (M A) -> M (Incr A))
>   : forall B:Type, Term (M B) -> N B :=

>   fix f (B:Type) (z:Term (M B)) {struct z} : N B := 
>     match z in Term MB return MB = (M B) -> N B with
>     | Var MB x   => fun (H:_) => var B (eq_rect (MB) idt x (M B) H)
>     | App MB x y => fun (H:_) => app B (f B (eq_rect MB Term x (M B) H))
>                                        (f B (eq_rect MB Term y (M B) H))
>     | Lam MB x   => fun (H:_) => lam B (f (Incr B) (mapT (k B)
>                                        (eq_rect MB (Term <.> Incr) x (M B) 
> H)))
>     end (refl_equal (M B))
>   .

> (*
> This definition elicits the following error:

> Recursive call to f has principal argument equal to
> "mapT (k B) (eq_rect MB (Term <.> Incr) x (M B) H)"
> instead of x
> *) 

Yes, the problem here is that your recursion is not syntactically of the
form recognized by Coq.  IIRC, to make it recognizable, you have to
restructure your code to receive "z:Term MB" as well as an additional
argument of type "MB = (M B)".


        Stefan