The Coq mailing list

[Christian Doczkal <doczkal AT ps.uni-sb.de>]

Hello 

I have the following definitions: 

Require Import List.

Inductive hlist : list Type -> Type :=
| hnil : hlist nil
| hcons : forall (X:Type) Xs, X ->  hlist Xs -> hlist (X::Xs).

(* Abstractly, everything works as one would expect *)

Variable Tp' : Type.
Variable Tm' : Tp' -> Type.

Variable Ts' : (list Tp').
Check (hlist (map Tm' Ts')).

(* But given concrete instances for Tp/Tm I get typing errors *)

Inductive Tp : Type := i | ar : Tp -> Tp -> Tp.
Inductive Tm : Tp -> Type := 
  Var : forall sigma:Tp, nat -> Tm sigma
| Ap : forall sigma tau:Tp,Tm (ar sigma tau) -> Tm sigma -> Tm tau.

Variable Ts : list Tp.
Check (list Tp). (* Set *)
Check (hlist (map Tm Ts)). 
(* fails: The term "map Tm Ts" has type "list Set"
 while it is expected to have type "list Type". *)

Check also gives Tp:Set and Tm : Tp -> Set. (Type(0) if I set printing
for Universes) I guess this is part of the issue? What is really going
wrong here?

The second part (of course) works if I restrict hlist to "list Set". 

Is there any fix that does not involve restricting hlist?

-- 
Regards
Christian