The Coq mailing list

[Matej Kosik <5764c029b688c1c0d24a2e97cd764f AT gmail.com>]

Hi,

I am reading the Reference Manual
(Section 4.5.1 : Representing an inductive definition)
(subsection : Inductive definitions with parameters)
https://coq.inria.fr/distrib/current/refman/Reference-Manual006.html#sec190

I would like to ask a question concerning this passage:

        "Generally one want consider lists of elements of different types.
         ...
         One possible way to do that would be to define the type List 
inductively
         as being an inductive family of type Set → Set:

           Ind()(List : Set → Set := nil : (∀ A : Set, List A), cons : (∀ A : 
Set, A → List A → List A))

         There are drawbacks to this point of view.
         The information which says that for any A, (List A) is an 
inductively defined Set *has be lost*.
        "

The last sentence is used as a motivation for the need to discriminate 
between parameters and arguments.
I am not sure if I understand the argument.

If I consider a concrete example (corresponding to the above definition):

        Inductive list1 : Type -> Type :=
        | nil1 : forall A : Type, list1 A
        | cons1 : forall A : Type, A -> list1 A -> list1 A.

I fail to see what is "lost".

I can construct values of this type:

        Check nil1 nat.
        Check cons1 nat 5 (nil1 nat).

I can work with those values normally.
E.g.:

        Definition is_empty (A:Type) (l : list1 A) :=
          match l with
          | nil1 _ => true
          | cons1 _ _ _ => false
          end.

        Compute is_empty nat (nil1 nat).
        Compute is_empty nat (cons1 nat 5 (nil1 nat)).


I am curious, why is "list1" as defined above inferior to "list" as it 
appears in the standard library?