The Coq mailing list

["Eelis van der Weegen" <eelis AT eelis.net>]

In Coq 8.1beta, sort-polymorphism on inductive families was added. list is
now of type Type->Type, which used to be Set->Set. We can now have a (list
Set) of type Type, while (list nat) remains of type Set as before.
Personally I think this is pretty neat.

In Coq 8.0 I used the following definition for length-limited lists:

  Definition lim_list (limit: nat) (A: Set) := { l: list A | length l <=
limit }.

This still works, but it does not allow us to make a limited-length list
of Sets. I figured it would be nice to update lim_list to cover list's
newfound genericity by changing "Set" to "Type", corresponding to what was
done for list itself:

  Definition lim_list (limit: nat) (A: Type) := { l: list A | length l <=
limit }.

This definition is accepted and we can now make for example (lim_last 5
Set) of type Type. However, it appears the sort-polymorphism has been
lost: (lim_list 3 nat) is now also of type Type, while we would have
wanted it to be of type Set.

This leads to my first question: is it possible to define a family of
limited-length lists similar to lim_list above, but in such a way that it
benefits from the same sort-polymorphism that list now features?

My second question involves the display of sort-polymorphic types. Consider:

  Inductive X (A: Type): Type := x: A -> X A.
  Definition Y := X.
  Check X.
  Check Y.

For both X and Y, Check displays Type->Type. However, the following tests
reveal that the types of X and Y are not quite that identical, as X's
sort-polymorphism has been lost in Y:

  Definition test1: Set := X nat. (* ok, accepted by Coq *)
  Definition test2: Set := Y nat.
    (* Error:  The term "Y nat" has type "Type" while it is expected to
have type "Set" *)

This leads to my second question: Is there a way to make visible this
difference between the types of X and Y?

Regards,

Eelis