The Coq mailing list

[Lauri Alanko <la AT iki.fi>]

On Sun, May 10, 2009 at 01:00:25PM +0200, Matej Kosik wrote:
> There is, however, one thing I do not understand. How could the type of
> the whole term (`list nat' or `list bool') be `Set' instead of `Type' as
> the type of the `list' function suggests?

This is explained in the manual:

http://www.lix.polytechnique.fr/coq/distrib/current/refman/Reference-Manual006.html#@default345

Enabling universe printing helps figure what's going on here.

Coq < Set Printing Universes.
Coq < Check list.
list
     : Type (* Coq.Lists.List.1 *) -> Type (* max(0, Coq.Lists.List.1) *)

The gist of it is that the sort of "list X" is the sort of X, _except_
if the sort of X is Prop (that's what the "max 0" is for):

Coq < Check (list True).
list True
     : Set

With single-constructor datatypes there's no such limitation:

Coq < Check prod.
prod
     : Type (* Coq.Init.Datatypes.22 *) ->
       Type (* Coq.Init.Datatypes.22 *) -> Type (* Coq.Init.Datatypes.22 *)

Coq < Check (prod True False).
(True * False)%type
     : Prop

What I find a bit inconsistent, though, is that the manual says that
Set : Type(0), but the way the universe constraints are expressed, it
seems that Set _is_ Type(0). Not a very big deal, though.


Lauri