The Coq mailing list

[Adam Chlipala <adamc AT cs.berkeley.edu>]

My understanding is that sort polymorphism is not a genuine feature of 
CIC, or whatever the specific logic behind Coq is called these days. 
Rather, this feature is more like a "macro system" added on top as a 
convenience.  Sometimes, the type checker is able to notice that you are 
using a definition in a way that can be made more general, and it 
creates a new definition of the associated inductive type with a 
different sort.  You as the user don't need to worry about this 
definition duplication, as the system manages it for you, giving the 
illusion of "real" polymorphism.

Once a "sort polymorphic" identifier is hidden inside a definition, 
later users don't see it, and so the system doesn't apply the 
extra-redefinition trick in those cases.

I don't know how sort polymorphism is implemented; it might be in a way 
that makes it look like the polymorphism is "real."  I think the 
metatheory is trickier with "real" sort polymorphism, though, and it's 
easiest to treat this as a smart macro system.

Brian Aydemir wrote:
> Hi everyone,
>
> I have a question about sort polymorphism in Coq 8.1.  Consider the 
> following example.
>
> (* *** *)
>
> Parameter bind : Set.
>
> Definition env := list.
>
> Print env.         (* env        : Type -> Type *)
> Check (env bind).  (* env bind   : Type *)
> Check (list bind). (* list bind  : Set *)
>
> (* *** *)
>
> My question: why are (env bind) and (list bind) assigned different 
> sorts?  The two are convertible with each other.  It seems strange that 
> "wrapping" list behind a Definition would all of a sudden change the 
> sorts that are assigned to entities.  What exactly is going on here?