# HG changeset patch
# User Adam Chlipala <adamc@hcoop.net>
# Date 1259608894 18000
# Node ID f15f7c4eebfe26cc6ae283c7234dfb3b0c091484
# Parent  d1e0a6d8eef1d36acf4adc64b2fe7910c30ed68d
Mention fake universe polymorphism

diff -r d1e0a6d8eef1 -r f15f7c4eebfe src/Universes.v
--- a/src/Universes.v	Tue Nov 24 07:54:38 2009 -0500
+++ b/src/Universes.v	Mon Nov 30 14:21:34 2009 -0500
@@ -291,12 +291,51 @@
  
 ]]
 
-The key benefit parameters bring us is the ability to avoid quantifying over types in the types of constructors.  Such quantification induces less-than constraints, while parameters only introduce less-than-or-equal-to constraints. *)
+The key benefit parameters bring us is the ability to avoid quantifying over types in the types of constructors.  Such quantification induces less-than constraints, while parameters only introduce less-than-or-equal-to constraints.
+
+Coq includes one more (potentially confusing) feature related to parameters.  While Gallina does not support real universe polymorphism, there is a convenience facility that mimics universe polymorphism in some cases.  We can illustrate what this means with a simple example. *)
+
+Inductive foo (A : Type) : Type :=
+| Foo : A -> foo A.
 
 (* begin hide *)
 Unset Printing Universes.
 (* end hide *)
 
+Check foo nat.
+(** %\vspace{-.15in}% [[
+  foo nat
+     : Set
+     ]] *)
+
+Check foo Set.
+(** %\vspace{-.15in}% [[
+  foo Set
+     : Type
+     ]] *)
+
+Check foo True.
+(** %\vspace{-.15in}% [[
+  foo True
+     : Prop
+ 
+     ]]
+
+  The basic pattern here is that Coq is willing to automatically build a "copied-and-pasted" version of an inductive definition, where some occurrences of [Type] have been replaced by [Set] or [Prop].  In each context, the type-checker tries to find the valid replacements that are lowest in the type hierarchy.  Automatic cloning of definitions can be much more convenient than manual cloning.  We have already taken advantage of the fact that we may re-use the same families of tuple and list types to form values in [Set] and [Type].
+
+  Imitation polymorphism can be confusing in some contexts.  For instance, it is what is responsible for this weird behavior. *)
+
+Inductive bar : Type := Bar : bar.
+
+Check bar.
+(** %\vspace{-.15in}% [[
+  bar
+     : Prop
+ 
+     ]]
+
+  The type that Coq comes up with may be used in strictly more contexts than the type one might have expected. *)
+
 
 (** * The [Prop] Universe *)