Fix interpretation of global universes in univdecl constraints.

Also nicer error when the constraints are impossible.

6 files changed, 41 insertions, 24 deletions

diff --git a/pretyping/pretyping.ml b/pretyping/pretyping.ml
index ffbc21a5e..a9bff5bf6 100644
--- a/pretyping/pretyping.ml
+++ b/pretyping/pretyping.ml
@@ -177,6 +177,14 @@ let _ =
 	    optwrite = (:=) Universes.set_minimization })
 
 (** Miscellaneous interpretation functions *)
+let interp_known_universe_level evd id =
+  try
+    let level = Evd.universe_of_name evd id in
+    level
+  with Not_found ->
+    let names, _ = Global.global_universe_names () in
+    snd (Id.Map.find id names)
+
 let interp_universe_level_name ~anon_rigidity evd (loc, s) =
   match s with
   | Anonymous ->
@@ -195,13 +203,7 @@ let interp_universe_level_name ~anon_rigidity evd (loc, s) =
 	    with UGraph.AlreadyDeclared -> evd
 	  in evd, level
      else
-       try
-         let level = Evd.universe_of_name evd id in
-         evd, level
-       with Not_found ->
-       try
-         let names, _ = Global.global_universe_names () in
-         evd, snd (Id.Map.find id names)
+       try evd, interp_known_universe_level evd id
        with Not_found ->
          if not (is_strict_universe_declarations ()) then
            new_univ_level_variable ?loc ~name:id univ_rigid evd
@@ -218,6 +220,15 @@ let interp_universe ?loc evd = function
 	(evd', Univ.sup u (Univ.Universe.make l)))
     (evd, Univ.Universe.type0m) l
 
+let interp_known_level_info ?loc evd = function
+  | None | Some (_, Anonymous) ->
+    user_err ?loc ~hdr:"interp_known_level_info"
+      (str "Anonymous universes not allowed here.")
+  | Some (loc, Name id) ->
+    try interp_known_universe_level evd id
+    with Not_found ->
+      user_err ?loc ~hdr:"interp_known_level_info" (str "Undeclared universe " ++ Id.print id)
+
 let interp_level_info ?loc evd : Misctypes.level_info -> _ = function
   | None -> new_univ_level_variable ?loc univ_rigid evd
   | Some (loc,s) -> interp_universe_level_name ~anon_rigidity:univ_flexible evd (Loc.tag ?loc s)
@@ -466,6 +477,11 @@ let pretype_id pretype k0 loc env evdref lvar id =
 (*************************************************************************)
 (* Main pretyping function                                               *)
 
+let interp_known_glob_level ?loc evd = function
+  | GProp -> Univ.Level.prop
+  | GSet -> Univ.Level.set
+  | GType s -> interp_known_level_info ?loc evd s
+
 let interp_glob_level ?loc evd : Misctypes.glob_level -> _ = function
   | GProp -> evd, Univ.Level.prop
   | GSet -> evd, Univ.Level.set
diff --git a/pretyping/pretyping.mli b/pretyping/pretyping.mli
index b2735ee22..d0fb5cad9 100644
--- a/pretyping/pretyping.mli
+++ b/pretyping/pretyping.mli
@@ -20,6 +20,9 @@ open Glob_term
 open Ltac_pretype
 open Evardefine
 
+val interp_known_glob_level : ?loc:Loc.t -> Evd.evar_map ->
+  Misctypes.glob_level -> Univ.Level.t
+
 (** An auxiliary function for searching for fixpoint guard indexes *)
 
 val search_guard :
diff --git a/pretyping/univdecls.ml b/pretyping/univdecls.ml
index a5266125a..3cf32d7ff 100644
--- a/pretyping/univdecls.ml
+++ b/pretyping/univdecls.ml
@@ -6,9 +6,8 @@
 (*         *       GNU Lesser General Public License Version 2.1        *)
 (************************************************************************)
 
-open Pp
-open CErrors
 open Names
+open CErrors
 
 (** Local universes and constraints declarations *)
 type universe_decl =
@@ -22,27 +21,16 @@ let default_univ_decl =
     univdecl_extensible_constraints = true }
 
 let interp_univ_constraints env evd cstrs =
-  let open Misctypes in
-  let u_of_id x =
-    match x with
-    | Misctypes.GProp -> Loc.tag Univ.Level.prop
-    | GSet  -> Loc.tag Univ.Level.set
-    | GType None | GType (Some (_, Anonymous)) ->
-       user_err ~hdr:"interp_constraint"
-                     (str "Cannot declare constraints on anonymous universes")
-    | GType (Some (loc, Name id)) ->
-       try loc, Evd.universe_of_name evd id
-       with Not_found ->
-         user_err ?loc ~hdr:"interp_constraint" (str "Undeclared universe " ++ Id.print id)
-  in
   let interp (evd,cstrs) (u, d, u') =
-    let lloc, ul = u_of_id u and rloc, u'l = u_of_id u' in
+    let ul = Pretyping.interp_known_glob_level evd u in
+    let u'l = Pretyping.interp_known_glob_level evd u' in
     let cstr = (ul,d,u'l) in
     let cstrs' = Univ.Constraint.add cstr cstrs in
     try let evd = Evd.add_constraints evd (Univ.Constraint.singleton cstr) in
         evd, cstrs'
     with Univ.UniverseInconsistency e ->
-      user_err  ~hdr:"interp_constraint" (str "Universe inconsistency" (* TODO *))
+      user_err ~hdr:"interp_constraint"
+        (Univ.explain_universe_inconsistency (Termops.pr_evd_level evd) e)
   in
   List.fold_left interp (evd,Univ.Constraint.empty) cstrs
 
diff --git a/test-suite/output/UnivBinders.out b/test-suite/output/UnivBinders.out
index a2857294b..9eb162fc0 100644
--- a/test-suite/output/UnivBinders.out
+++ b/test-suite/output/UnivBinders.out
@@ -86,6 +86,8 @@ The command has indeed failed with message:
 Universe instance should have length 0
 The command has indeed failed with message:
 This object does not support universe names.
+The command has indeed failed with message:
+Cannot enforce v < u because u < gU < gV < v
 Monomorphic bind_univs.mono = Type@{u}
      : Type@{u+1}
 (* {u} |=  *)
diff --git a/test-suite/output/UnivBinders.v b/test-suite/output/UnivBinders.v
index 013f215b5..a65a1fdf3 100644
--- a/test-suite/output/UnivBinders.v
+++ b/test-suite/output/UnivBinders.v
@@ -56,6 +56,10 @@ Fail Print mono@{E}.
 (* Not everything can be printed with custom universe names. *)
 Fail Print Coq.Init.Logic@{E}.
 
+(* Nice error when constraints are impossible. *)
+Monomorphic Universes gU gV. Monomorphic Constraint gU < gV.
+Fail Lemma foo@{u v|u < gU, gV < v, v < u} : nat.
+
 (* Universe binders survive through compilation, sections and modules. *)
 Require bind_univs.
 Print bind_univs.mono.
diff --git a/test-suite/success/polymorphism.v b/test-suite/success/polymorphism.v
index c09a60a4d..b3f9a4994 100644
--- a/test-suite/success/polymorphism.v
+++ b/test-suite/success/polymorphism.v
@@ -202,6 +202,10 @@ Module binders.
     exact Type@{i}.
   Qed.
 
+  Monomorphic Universe M.
+  Fail Definition with_mono@{u|} : Type@{M} := Type@{u}.
+  Definition with_mono@{u|u < M} : Type@{M} := Type@{u}.
+
 End binders.
     
 Section cats.