Correction d'une incohérence de typage des inductifs polymorphes: les

contraintes bornant par le haut le type de l'inductif (ce qui peut
arriver quand l'inductif est argument d'une constante) étaient
oubliées : on pouvait se retrouver avec des inductifs dont le type des
constructeurs, une fois instancié par des paramètres) n'était plus
typable (seul leur réduit, après expansion des constantes, était
typable). [kernel, test-suite]

+ Affichage des inductifs (via Print) en prenant la forme utilisateur des
  constructeurs.
+ Correction warning dans compilation gallina.ml.



git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@11266 85f007b7-540e-0410-9357-904b9bb8a0f7

1 files changed, 25 insertions, 0 deletions

diff --git a/test-suite/failure/universes3.v b/test-suite/failure/universes3.v
new file mode 100644
index 000000000..427cec190
--- /dev/null
+++ b/test-suite/failure/universes3.v
@@ -0,0 +1,25 @@
+(* This example (found by coqchk) checks that an inductive cannot be
+   polymorphic if its constructors induce upper universe constraints.
+   Here: I cannot be polymorphic because its type is less than the
+   type of the argument of impl. *)
+
+Definition Type1 := Type.
+Definition Type3 : Type1 := Type.                       (* Type3 < Type1 *)
+Definition Type4 := Type.
+Definition impl (A B:Type3) : Type4 := A->B.           (* Type3 <= Type4 *)
+Inductive I (B:Type (*6*)) := C : B -> impl Prop (I B).
+    (* Type(6) <= Type(7)     because I contains, via C, elements in B
+       Type(7) <=  Type3      because (I B) is argument of impl
+       Type(4) <=  Type(7)    because type of C less than I (see remark below)
+
+       where Type(7) is the auxiliary level used to infer the type of I
+*)
+
+(* We cannot enforce Type1 < Type(6) while we already have 
+   Type(6) <= Type(7) < Type3 < Type1 *)
+Definition J := I Type1.
+
+(* Open question: should the type of an inductive be the max of the
+   types of the _arguments_ of its constructors (here B and Prop,
+   after unfolding of impl), or of the max of types of the
+   constructors itself (here B -> impl Prop (I B)), as done above. *)