The Coq mailing list

[Adam Chlipala <adam AT chlipala.net>]

Adam Koprowski wrote:
> (*
>     However, when I try to generalize this to heterogenous lists I hit
>   two problems (the listing is a tad longer so I attach it to this mail):
>   1) Coq does not recognize that the principal argument is decreasing
>      in the recursive call (although clearly it does).
>   2) even when we forget about this, I run into Universe inconsistency
>      problem...
>
>    Any help appreciated,
>
>     Adam
>
> *)

First, a simple type annotation gets Coq to accept your definition of 
[hlist_combine], with no need for [Program].  This is the [: id t] 
explicit ascription, which helps avoid the need to solve a higher-order 
unification problem.  You could get the same effect by applying [HCons] 
with the [B] parameter specified explicitly.

  Fixpoint hlist_combine t (l : list t)
    : forall ts, list (hlist id ts) -> list (hlist id (t::ts)) :=
    match l return
      forall ts, list (hlist id ts) -> list (hlist id (t::ts))
    with
    | [] => fun _ _ => []
    | x::xs => fun _ l' =>
        map (fun y_i => (x : id t) ::: y_i) l' ++ hlist_combine xs l'
    end.

For the universe inconsistency, I'm a bit stumped by this one, but there 
is an easy workaround that is probably acceptable.  The following type 
works fine, apparently because Coq's fake universe polymorphism 
elaborates it differently.

  forall l : list Type, hlist (fun T => list T) l -> list (hlist id l)

Finally, here's a (probable) definition of your final 
[hlist_prod_tuple].  I haven't thought through whether this does exactly 
what you want, but it probably provides a starting point.

  Fixpoint hlist_prod_tuple (l : list Type) (hl : hlist (fun T => list 
T) l) : list (hlist id l) :=
    match hl in hlist _ l return list (hlist id l) with
      | HNil => [HNil]
      | HCons _ _ v hl' => hlist_combine v (hlist_prod_tuple hl')
    end.

It's generally better to write a function as explicitly recursive in an 
[hlist], rather than just on the [hlist]'s [list] index, when possible.