13.2 About patterns of parametric types

When matching objects of a parametric type, constructors in patterns do not expect the parameter arguments. Their value is deduced during expansion.

Consider for example the polymorphic lists:

Coq < Inductive List [A:Set] :Set :=
Coq < nil:(List A)
Coq < | cons:A->(List A)->(List A).
List_ind is defined
List_rec is defined
List_rect is defined
List is defined

We can check the function tail:

Coq < Check [l:(List nat)]Cases l of
Coq <                              nil        => (nil nat)
Coq <                           | (cons _ l') => l'
Coq <                            end.
[l:(List nat)]Cases l of
                nil => (nil nat)
              | (cons _ l') => l'
              end
     : (List nat)->(List nat)

When we use parameters in patterns there is an error message:

Coq < Check [l:(List nat)]Cases l of
Coq <                              (nil nat)      => (nil nat)
Coq <                           | (cons nat _ l') => l'
Coq <                            end.
Toplevel input, characters 6-169
> ..... [l:(List nat)]Cases l of
>                              (nil nat)      => (nil nat)
>                           | (cons nat _ l') => l'
>                            end
Error: In pattern (nil nat) the constructor nil expects 0 arguments.