Univs: more robust Universe/Constraint decls #4816

This fixes the declarations of constraints, universes
and assumptions:
- global constraints can refer to global universes only,
- polymorphic universes, constraints and assumptions can only be
  declared inside sections, when all the section's
  variables/universes are polymorphic as well.
- monomorphic assumptions may only be declared in section contexts
  which are not parameterized by polymorphic universes/assumptions.

Add fix for part 1 of bug #4816

6 files changed, 55 insertions, 12 deletions

diff --git a/doc/refman/Universes.tex b/doc/refman/Universes.tex
index a08cd1475a..36518e6fae 100644
--- a/doc/refman/Universes.tex
+++ b/doc/refman/Universes.tex
@@ -201,7 +201,8 @@ universes and explicitly instantiate polymorphic definitions.
 In the monorphic case, this command declares a new global universe named
 {\ident}. It supports the polymorphic flag only in sections, meaning the
 universe quantification will be discharged on each section definition
-independently.
+independently. One cannot mix polymorphic and monomorphic declarations
+in the same section.
 
 \subsection{\tt Constraint {\ident} {\textit{ord}} {\ident}.
   \comindex{Constraint}
@@ -212,6 +213,7 @@ The order relation can be one of $<$, $\le$ or $=$. If consistent,
 the constraint is then enforced in the global environment. Like
 \texttt{Universe}, it can be used with the \texttt{Polymorphic} prefix
 in sections only to declare constraints discharged at section closing time.
+One cannot declare a global constraint on polymorphic universes.
 
 \begin{ErrMsgs}
 \item \errindex{Undeclared universe {\ident}}.
diff --git a/library/declare.ml b/library/declare.ml
index b0df32b8de..84284fd182 100644
--- a/library/declare.ml
+++ b/library/declare.ml
@@ -440,8 +440,9 @@ let cache_universes (p, l) =
   let glob = Universes.global_universe_names () in
   let glob', ctx =
     List.fold_left (fun ((idl,lid),ctx) (id, lev) ->
-		    ((Idmap.add id lev idl, Univ.LMap.add lev id lid),
-		     Univ.ContextSet.add_universe lev ctx))
+        ((Idmap.add id (p, lev) idl,
+          Univ.LMap.add lev id lid),
+         Univ.ContextSet.add_universe lev ctx))
       (glob, Univ.ContextSet.empty) l
   in
     Global.push_context_set p ctx;
@@ -457,6 +458,12 @@ let input_universes : universe_decl -> Libobject.obj =
       classify_function = (fun a -> Keep a) }
 
 let do_universe poly l =
+  let in_section = Lib.sections_are_opened () in
+  let () =
+    if poly && not in_section then
+      user_err_loc (Loc.ghost, "Constraint",
+                    str"Cannot declare polymorphic universes outside sections")
+  in
   let l =
     List.map (fun (l, id) ->
 	      let lev = Universes.new_univ_level (Global.current_dirpath ()) in
@@ -485,14 +492,30 @@ let input_constraints : constraint_decl -> Libobject.obj =
 let do_constraint poly l =
   let u_of_id =
     let names, _ = Universes.global_universe_names () in
-      fun (loc, id) ->
-	try Idmap.find id names
-	with Not_found ->
-	  user_err_loc (loc, "Constraint", str "Undeclared universe " ++ pr_id id)
+    fun (loc, id) ->
+    try Idmap.find id names
+    with Not_found ->
+      user_err_loc (loc, "Constraint", str "Undeclared universe " ++ pr_id id)
+  in
+  let in_section = Lib.sections_are_opened () in
+  let () =
+    if poly && not in_section then
+      user_err_loc (Loc.ghost, "Constraint",
+                    str"Cannot declare polymorphic constraints outside sections")
+  in
+  let check_poly loc p loc' p' =
+    if poly then ()
+    else if p || p' then
+      let loc = if p then loc else loc' in
+      user_err_loc (loc, "Constraint",
+                    str "Cannot declare a global constraint on " ++
+                    str "a polymorphic universe, use "
+                    ++ str "Polymorphic Constraint instead")
   in
   let constraints = List.fold_left (fun acc (l, d, r) ->
-    let lu = u_of_id l and ru = u_of_id r in
-      Univ.Constraint.add (lu, d, ru) acc)
+     let p, lu = u_of_id l and p', ru = u_of_id r in
+     check_poly (fst l) p (fst r) p';
+     Univ.Constraint.add (lu, d, ru) acc)
     Univ.Constraint.empty l
   in
     Lib.add_anonymous_leaf (input_constraints (poly, constraints))
diff --git a/library/universes.ml b/library/universes.ml
index c4eb2afcbb..75cbd5604b 100644
--- a/library/universes.ml
+++ b/library/universes.ml
@@ -13,10 +13,11 @@ open Term
 open Environ
 open Univ
 open Globnames
+open Decl_kinds
 
 (** Global universe names *)
 type universe_names = 
-    Univ.universe_level Idmap.t * Id.t Univ.LMap.t
+  (polymorphic * Univ.universe_level) Idmap.t * Id.t Univ.LMap.t
 
 let global_universes =
   Summary.ref ~name:"Global universe names"
diff --git a/library/universes.mli b/library/universes.mli
index 53cf5f3844..a5740ec49f 100644
--- a/library/universes.mli
+++ b/library/universes.mli
@@ -19,7 +19,7 @@ val is_set_minimization : unit -> bool
 
 (** Global universe name <-> level mapping *)
 type universe_names = 
-  Univ.universe_level Idmap.t * Id.t Univ.LMap.t
+  (Decl_kinds.polymorphic * Univ.universe_level) Idmap.t * Id.t Univ.LMap.t
 
 val global_universe_names : unit -> universe_names
 val set_global_universe_names : universe_names -> unit
diff --git a/pretyping/pretyping.ml b/pretyping/pretyping.ml
index efc42aab76..378294c984 100644
--- a/pretyping/pretyping.ml
+++ b/pretyping/pretyping.ml
@@ -143,7 +143,7 @@ let interp_universe_level_name evd (loc,s) =
       with Not_found ->
 	try 
 	  let id = try Id.of_string s with _ -> raise Not_found in
-	  evd, Idmap.find id names
+          evd, snd (Idmap.find id names)
 	with Not_found -> 
 	  if not (is_strict_universe_declarations ()) then
   	    new_univ_level_variable ~loc ~name:s univ_rigid evd
diff --git a/test-suite/bugs/closed/4816.v b/test-suite/bugs/closed/4816.v
new file mode 100644
index 0000000000..86597c88fa
--- /dev/null
+++ b/test-suite/bugs/closed/4816.v
@@ -0,0 +1,17 @@
+Section foo.
+Polymorphic Universes A B.
+Fail Constraint A <= B.
+End foo.
+(* gives an anomaly Universe undefined *)
+
+Universes X Y.
+Section Foo.
+  Polymorphic Universes Z W.
+  Polymorphic Constraint W < Z.
+
+  Fail Definition bla := Type@{W}.
+  Polymorphic Definition bla := Type@{W}.
+  Section Bar.
+    Fail Constraint X <= Z.
+  End Bar.
+End Foo.