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

9 files changed, 50 insertions, 4 deletions

diff --git a/kernel/indtypes.ml b/kernel/indtypes.ml
index cd9e2e81f4..5786e67d53 100644
--- a/kernel/indtypes.ml
+++ b/kernel/indtypes.ml
@@ -254,10 +254,13 @@ let typecheck_inductive env mie =
     array_fold_map2' (fun ((id,full_arity,ar_level),cn,info,lc,_) lev cst ->
       let sign, s = dest_arity env full_arity in
       let status,cst = match s with
-      | Type _ when ar_level <> None (* Explicitly polymorphic *) ->
+      | Type u when ar_level <> None (* Explicitly polymorphic *) 
+            && no_upper_constraints u cst ->
 	  (* The polymorphic level is a function of the level of the *)
 	  (* conclusions of the parameters *)
-	  Inr (param_ccls, lev), cst
+          (* We enforce [u >= lev] in case [lev] has a strict upper *)
+          (* constraints over [u] *)
+	  Inr (param_ccls, lev), enforce_geq u lev cst
       | Type u (* Not an explicit occurrence of Type *) ->
 	  Inl (info,full_arity,s), enforce_geq u lev cst
       | Prop Pos when engagement env <> Some ImpredicativeSet ->
diff --git a/kernel/inductive.ml b/kernel/inductive.ml
index 8ff8ddb85e..918a32c956 100644
--- a/kernel/inductive.ml
+++ b/kernel/inductive.ml
@@ -228,7 +228,9 @@ let arities_of_specif kn (mib,mip) =
 let arities_of_constructors ind specif = 
   arities_of_specif (fst ind) specif
 
-
+let type_of_constructors ind (mib,mip) =
+  let specif = mip.mind_user_lc in
+  Array.map (constructor_instantiate (fst ind) mib) specif
 
 (************************************************************************)
 
diff --git a/kernel/inductive.mli b/kernel/inductive.mli
index e63c7772c3..118d19830e 100644
--- a/kernel/inductive.mli
+++ b/kernel/inductive.mli
@@ -47,6 +47,9 @@ val type_of_constructor : constructor -> mind_specif -> types
 (* Return constructor types in normal form *)
 val arities_of_constructors : inductive -> mind_specif -> types array
 
+(* Return constructor types in user form *)
+val type_of_constructors : inductive -> mind_specif -> types array
+
 (* Transforms inductive specification into types (in nf) *)
 val arities_of_specif : mutual_inductive -> mind_specif -> types array 
 
diff --git a/kernel/univ.ml b/kernel/univ.ml
index 001ee3ea8a..a681210acf 100644
--- a/kernel/univ.ml
+++ b/kernel/univ.ml
@@ -550,6 +550,11 @@ let subst_large_constraint u u' v =
 let subst_large_constraints =
   List.fold_right (fun (u,u') -> subst_large_constraint u u')
 
+let no_upper_constraints u cst =
+  match u with
+  | Atom u -> Constraint.for_all (fun (u1,_,_) -> u1 <> u) cst
+  | Max _ -> anomaly "no_upper_constraints"
+
 (* Pretty-printing *)
 
 let num_universes g =
diff --git a/kernel/univ.mli b/kernel/univ.mli
index 1ce5329ab9..225dce9a6c 100644
--- a/kernel/univ.mli
+++ b/kernel/univ.mli
@@ -76,6 +76,8 @@ val subst_large_constraint : universe -> universe -> universe -> universe
 val subst_large_constraints : 
   (universe * universe) list -> universe -> universe
 
+val no_upper_constraints : universe -> constraints -> bool
+
 (*s Pretty-printing of universes. *)
 
 val pr_uni : universe -> Pp.std_ppcmds
diff --git a/parsing/prettyp.ml b/parsing/prettyp.ml
index 0a9447b46d..7e10264ef4 100644
--- a/parsing/prettyp.ml
+++ b/parsing/prettyp.ml
@@ -303,7 +303,7 @@ let build_inductive sp tyi =
     | Polymorphic ar ->
 	it_mkProd_or_LetIn (mkSort (Type ar.poly_level)) mip.mind_arity_ctxt in
   let arity = hnf_prod_applist env fullarity args in
-  let cstrtypes = arities_of_constructors env (sp,tyi) in
+  let cstrtypes = type_of_constructors env (sp,tyi) in
   let cstrtypes =
     Array.map (fun c -> hnf_prod_applist env c args) cstrtypes in
   let cstrnames = mip.mind_consnames in
diff --git a/pretyping/inductiveops.ml b/pretyping/inductiveops.ml
index 79d9e381ee..d4290c7641 100644
--- a/pretyping/inductiveops.ml
+++ b/pretyping/inductiveops.ml
@@ -31,6 +31,11 @@ let type_of_constructor env cstr =
   Inductive.lookup_mind_specif env (inductive_of_constructor cstr) in
  Inductive.type_of_constructor cstr specif
 
+(* Return constructor types in user form *)
+let type_of_constructors env ind =
+ let specif = Inductive.lookup_mind_specif env ind in
+  Inductive.type_of_constructors ind specif
+
 (* Return constructor types in normal form *)
 let arities_of_constructors env ind =
  let specif = Inductive.lookup_mind_specif env ind in
diff --git a/pretyping/inductiveops.mli b/pretyping/inductiveops.mli
index 3cc24a184f..46692b33b3 100644
--- a/pretyping/inductiveops.mli
+++ b/pretyping/inductiveops.mli
@@ -22,6 +22,7 @@ val type_of_inductive    : env -> inductive -> types
 
 (* Return type as quoted by the user *)
 val type_of_constructor  : env -> constructor -> types
+val type_of_constructors : env -> inductive -> types array
 
 (* Return constructor types in normal form *)
 val arities_of_constructors : env -> inductive -> types array
diff --git a/test-suite/failure/universes3.v b/test-suite/failure/universes3.v
new file mode 100644
index 0000000000..427cec1907
--- /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. *)