The Coq mailing list

["Luke Palmer" <lrpalmer AT gmail.com>]

Following a discussion on haskell-cafe, I decided I would try to write
a function which could take the outer product of a heterogeneous list
of lists.  When I finally wrote it, I got a "universe inconsistency"
error.  I understand that maybe this is not possible as I have phrased
it due to predicativity constraints or something, but I have no idea
why.  Could someone explain what is going on here?

Thanks!
Luke

Set Implicit Arguments.

(* Nothing special here, just a list type *)
Inductive List a : Type :=
| Nil : List a
| Cons : a -> List a -> List a.

Fixpoint map a b (f : a->b) (list : List a) : List b :=
  match list with
  | Nil => Nil _
  | Cons x xs => Cons (f x) (map f xs)
  end.

Fixpoint append a (list ys : List a) : List a :=
  match list with
  | Nil => ys
  | Cons x xs => Cons x (append xs ys)
  end.

Fixpoint concat a (list : List (List a)) : List a :=
  match list with
  | Nil => Nil _
  | Cons xs xss => append xs (concat xss)
  end.

Definition uncurry : forall a b c, (a -> b -> c) -> (a*b -> c)
  := fun _ _ _ f t => let (x,y) := t in f x y.


(* A heterogeneous list *)
Inductive Tuple : List Type -> Type :=
| TNil : Tuple (Nil _)
| TCons : forall t ts (x:t) (xs:Tuple ts), Tuple (Cons t ts).

Definition cross2 : forall a b, List a -> List b -> List (a * b) :=
  fun _ _ xs ys => concat (map (fun x => map (fun y => (x,y)) ys) xs).

Definition cross : forall ts, Tuple (map List ts) -> List (Tuple ts).
 intros.
 induction ts.
  exact (Cons TNil (Nil _)).
  simpl in X.
   inversion X.
   apply IHts in xs.
   exact (map (uncurry (TCons (t:=_) (ts:=_))) (cross2 x xs)).
Defined.
(* Oh no, universe inconsistency! *)