The Coq mailing list

[Bruno Barras <bruno.barras AT inria.fr>]

Adam Koprowski wrote:
>   (* list_prod_tuple [xs_1; ... xs_n] gives a list containing every 
>      list of the form [x_1; ... x_n] where [In x_1 xs_1], ... [In x_n 
> xs_n].
>    *)
>   Fixpoint list_prod_tuple (elts : list (list A)) : list (list A) :=
>     match elts with
>     | [] => []
>     | [x] => List.map (fun i => [i]) x
>     | x::xs => list_combine x (list_prod_tuple xs)
>     end.
Hello,

You have to be aware that dependent and non-dependent match have quite 
different heuristics. Here, since your second branch uses pattern [x], 
in the dependent case, the third branch's pattern is indeed (x::x0::xs0) 
(modulo renaming of pattern variables) and xs is replaced by (x0::xs0) 
in the rhs. Hence the error message.

Regarding the universe inconsistency, as Adam C. said, eta-expanding 
list does it:
 Variable hlist_prod_tuple_ax : forall l : list Type,
   hlist (fun A => list A) l -> list (hlist id l).
Eta-expansions creates a fresh universe (the type of A), and the 
sort-polymorphism now applies because list is applied to its parameter. 
When list is not expanded, then it belongs to a fixed universe that must 
be constrained somewhere else in your script.

Eta-expansion saved you this time, but there's probably something you 
don't expect in your definition of heterogeneous lists, and it'll 
probably bite you later on. You have

 Variable A : Type. (* Type_a *)
 Variable B : A -> Type (* Type_b *).
 Inductive hlist : list A -> Type (* Type_c *):=
 | HNil : hlist nil
 | HCons : forall x xs, B x -> hlist xs -> hlist (x::xs).

The predicativity constraint on hlist put hlist in a universe higher or 
equal to that of A (arguments x and xs of HCons). Formally,
 Type_c >= max(Type_a, Type_b).
In your case, A = Type_A, B= fun A (*:Type_A*) => list A,
so Type_a > Type_A and Type_b >= Type_A, so in the end Type_c > Type_A. 
Your hlist type lives in a universe strictly higher than the types of 
the arity!

In fact Adam C.'s definition of heterogeneous lists is useful when A 
(representing code of the arity types) lives in a universe lower than B 
(the decoding function): Type_a <= Type_b.

You can relax this constraint with the following definition (not 
resorting to the type encoding):

Inductive hlist (l:list Type (* Type_l *)) : Type (* Type_c *) :=
 HNil: l=nil -> hlist l
| HCons: l<>nil -> List.hd unit l -> hlist (List.tl l) -> hlist l.

Note that l is a (non-recursive) parameter, so it does not appear as a 
real argument of constructors. The only constraint is Type_c >= Type_l 
(because List.hd unit l : Type_l).

Hope this helps,

Bruno Barras.