Merge PR coq#19114: Using more often names of universes in universe i…

…nconsistency message, if possible Reviewed-by: SkySkimmer Co-authored-by: SkySkimmer <[email protected]>
SkySkimmer · Jun 7, 2024 · e2017e1 · e2017e1
2 parents f71d773 + 482f851
commit e2017e1
Show file tree

Hide file tree

Showing 6 changed files with 78 additions and 55 deletions.
diff --git a/engine/uState.ml b/engine/uState.ml
@@ -32,7 +32,7 @@ open Quality
 
 let sort_inconsistency ?explain cst l r =
   let explain = Option.map (fun p -> UGraph.Other p) explain in
-  raise (UGraph.UniverseInconsistency (cst, l, r, explain))
+  raise (UGraph.UniverseInconsistency (None, (cst, l, r, explain)))
 
 module QState : sig
   type t
@@ -234,6 +234,46 @@ let is_empty uctx =
   ContextSet.is_empty uctx.local &&
   UnivFlex.is_empty uctx.univ_variables
 
+let id_of_level uctx l =
+  try (Level.Map.find l (snd (snd uctx.names))).uname
+  with Not_found -> None
+
+let id_of_qvar uctx l =
+  try (QVar.Map.find l (fst (snd uctx.names))).uname
+  with Not_found -> None
+
+let qualid_of_qvar_names (bind, (qrev,_)) l =
+  try Some (Libnames.qualid_of_ident (Option.get (QVar.Map.find l qrev).uname))
+  with Not_found | Option.IsNone ->
+    None (* no global qvars *)
+
+let qualid_of_level_names (bind, (_,urev)) l =
+  try Some (Libnames.qualid_of_ident (Option.get (Level.Map.find l urev).uname))
+  with Not_found | Option.IsNone ->
+    UnivNames.qualid_of_level bind l
+
+let qualid_of_level uctx l = qualid_of_level_names uctx.names l
+
+let pr_uctx_qvar_names names l =
+  match qualid_of_qvar_names names l with
+  | Some qid -> Libnames.pr_qualid qid
+  | None -> QVar.raw_pr l
+
+let pr_uctx_level_names names l =
+  match qualid_of_level_names names l with
+  | Some qid -> Libnames.pr_qualid qid
+  | None -> Level.raw_pr l
+
+let pr_uctx_level uctx l = pr_uctx_level_names uctx.names l
+
+let pr_uctx_qvar uctx l = pr_uctx_qvar_names uctx.names l
+
+let merge_constraints uctx cstrs g =
+  try UGraph.merge_constraints cstrs g
+  with UGraph.UniverseInconsistency (_, i) ->
+    let printers = (pr_uctx_qvar uctx, pr_uctx_level uctx) in
+    raise (UGraph.UniverseInconsistency (Some printers, i))
+
 let uname_union s t =
   if s == t then s
   else
@@ -280,7 +320,7 @@ let union uctx uctx' =
           (if local == uctx.local then uctx.universes
            else
              let cstrsr = ContextSet.constraints uctx'.local in
-             UGraph.merge_constraints cstrsr (declarenew uctx.universes));
+             merge_constraints uctx cstrsr (declarenew uctx.universes));
         minim_extra = extra}
 
 let context_set uctx = uctx.local
@@ -373,7 +413,7 @@ let { Goptions.get = drop_weak_constraints } =
 
 let level_inconsistency cst l r =
   let mk u = Sorts.sort_of_univ @@ Universe.make u in
-  raise (UGraph.UniverseInconsistency (cst, mk l, mk r, None))
+  raise (UGraph.UniverseInconsistency (None, (cst, mk l, mk r, None)))
 
 let nf_universe uctx u =
   UnivSubst.(subst_univs_universe (UnivFlex.normalize_univ_variable uctx.univ_variables)) u
@@ -657,7 +697,7 @@ let add_universe_constraints uctx cstrs =
   { uctx with
     local = (univs, Constraints.union local local');
     univ_variables = vars;
-    universes = UGraph.merge_constraints local' uctx.universes;
+    universes = merge_constraints uctx local' uctx.universes;
     sort_variables = sorts;
     minim_extra = extra; }
 
@@ -726,40 +766,6 @@ let constrain_variables diff uctx =
   let local, vars = UnivFlex.constrain_variables diff uctx.univ_variables uctx.local in
   { uctx with local; univ_variables = vars }
 
-let id_of_level uctx l =
-  try (Level.Map.find l (snd (snd uctx.names))).uname
-  with Not_found -> None
-
-let id_of_qvar uctx l =
-  try (QVar.Map.find l (fst (snd uctx.names))).uname
-  with Not_found -> None
-
-let qualid_of_qvar_names (bind, (qrev,_)) l =
-  try Some (Libnames.qualid_of_ident (Option.get (QVar.Map.find l qrev).uname))
-  with Not_found | Option.IsNone ->
-    None (* no global qvars *)
-
-let qualid_of_level_names (bind, (_,urev)) l =
-  try Some (Libnames.qualid_of_ident (Option.get (Level.Map.find l urev).uname))
-  with Not_found | Option.IsNone ->
-    UnivNames.qualid_of_level bind l
-
-let qualid_of_level uctx l = qualid_of_level_names uctx.names l
-
-let pr_uctx_qvar_names names l =
-  match qualid_of_qvar_names names l with
-  | Some qid -> Libnames.pr_qualid qid
-  | None -> QVar.raw_pr l
-
-let pr_uctx_level_names names l =
-  match qualid_of_level_names names l with
-  | Some qid -> Libnames.pr_qualid qid
-  | None -> Level.raw_pr l
-
-let pr_uctx_level uctx l = pr_uctx_level_names uctx.names l
-
-let pr_uctx_qvar uctx l = pr_uctx_qvar_names uctx.names l
-
 type ('a, 'b, 'c) gen_universe_decl = {
   univdecl_qualities : 'a;
   univdecl_extensible_qualities : bool;
@@ -857,7 +863,7 @@ let check_universe_context_set ~prefix levels names =
 
 let check_implication uctx cstrs cstrs' =
   let gr = initial_graph uctx in
-  let grext = UGraph.merge_constraints cstrs gr in
+  let grext = merge_constraints uctx cstrs gr in
   let cstrs' = Constraints.filter (fun c -> not (UGraph.check_constraint grext c)) cstrs' in
   if Constraints.is_empty cstrs' then ()
   else CErrors.user_err
@@ -979,7 +985,7 @@ let merge ?loc ~sideff rigid uctx uctx' =
   in
   let initial = declare uctx.initial_universes in
   let univs = declare uctx.universes in
-  let universes = UGraph.merge_constraints (ContextSet.constraints uctx') univs in
+  let universes = merge_constraints uctx (ContextSet.constraints uctx') univs in
   let uctx =
     match rigid with
     | UnivRigid -> uctx
@@ -1049,7 +1055,7 @@ let merge_seff uctx uctx' =
   in
   let initial_universes = declare uctx.initial_universes in
   let univs = declare uctx.universes in
-  let universes = UGraph.merge_constraints (ContextSet.constraints uctx') univs in
+  let universes = merge_constraints uctx (ContextSet.constraints uctx') univs in
   { uctx with universes; initial_universes }
 
 let emit_side_effects eff u =

diff --git a/engine/univSubst.ml b/engine/univSubst.ml
@@ -92,42 +92,42 @@ let enforce_eq_sort s1 s2 cst = match s1, s2 with
 | (SProp, SProp) | (Prop, Prop) | (Set, Set) -> cst
 | (((Prop | Set | Type _ | QSort _) as s1), (Prop | SProp as s2))
 | ((Prop | SProp as s1), ((Prop | Set | Type _ | QSort _) as s2)) ->
-  raise (UGraph.UniverseInconsistency (Eq, s1, s2, None))
+  raise (UGraph.UniverseInconsistency (None, (Eq, s1, s2, None)))
 | (Set | Type _), (Set | Type _) ->
   enforce_eq (get_algebraic s1) (get_algebraic s2) cst
 | QSort (q1, u1), QSort (q2, u2) ->
   if QVar.equal q1 q2 then enforce_eq u1 u2 cst
-  else raise (UGraph.UniverseInconsistency (Eq, s1, s2, None))
+  else raise (UGraph.UniverseInconsistency (None, (Eq, s1, s2, None)))
 | (QSort _, (Set | Type _)) | ((Set | Type _), QSort _) ->
-  raise (UGraph.UniverseInconsistency (Eq, s1, s2, None))
+  raise (UGraph.UniverseInconsistency (None, (Eq, s1, s2, None)))
 
 let enforce_leq_sort s1 s2 cst = match s1, s2 with
 | (SProp, SProp) | (Prop, Prop) | (Set, Set) -> cst
 | (Prop, (Set | Type _)) -> cst
 | (((Prop | Set | Type _ | QSort _) as s1), (Prop | SProp as s2))
 | ((SProp as s1), ((Prop | Set | Type _ | QSort _) as s2)) ->
-  raise (UGraph.UniverseInconsistency (Le, s1, s2, None))
+  raise (UGraph.UniverseInconsistency (None, (Le, s1, s2, None)))
 | (Set | Type _), (Set | Type _) ->
   enforce_leq (get_algebraic s1) (get_algebraic s2) cst
 | QSort (q1, u1), QSort (q2, u2) ->
   if QVar.equal q1 q2 then enforce_leq u1 u2 cst
-  else raise (UGraph.UniverseInconsistency (Eq, s1, s2, None))
+  else raise (UGraph.UniverseInconsistency (None, (Eq, s1, s2, None)))
 | (QSort _, (Set | Type _)) | ((Prop | Set | Type _), QSort _) ->
-  raise (UGraph.UniverseInconsistency (Eq, s1, s2, None))
+  raise (UGraph.UniverseInconsistency (None, (Eq, s1, s2, None)))
 
 let enforce_leq_alg_sort s1 s2 g = match s1, s2 with
 | (SProp, SProp) | (Prop, Prop) | (Set, Set) -> Constraints.empty, g
 | (Prop, (Set | Type _)) -> Constraints.empty, g
 | (((Prop | Set | Type _ | QSort _) as s1), (Prop | SProp as s2))
 | ((SProp as s1), ((Prop | Set | Type _ | QSort _) as s2)) ->
-  raise (UGraph.UniverseInconsistency (Le, s1, s2, None))
+  raise (UGraph.UniverseInconsistency (None, (Le, s1, s2, None)))
 | (Set | Type _), (Set | Type _) ->
   UGraph.enforce_leq_alg (get_algebraic s1) (get_algebraic s2) g
 | QSort (q1, u1), QSort (q2, u2) ->
   if QVar.equal q1 q2 then UGraph.enforce_leq_alg u1 u2 g
-  else raise (UGraph.UniverseInconsistency (Eq, s1, s2, None))
+  else raise (UGraph.UniverseInconsistency (None, (Eq, s1, s2, None)))
 | (QSort _, (Set | Type _)) | ((Prop | Set | Type _), QSort _) ->
-  raise (UGraph.UniverseInconsistency (Eq, s1, s2, None))
+  raise (UGraph.UniverseInconsistency (None, (Eq, s1, s2, None)))
 
 let enforce_univ_constraint (u,d,v) =
   match d with

diff --git a/kernel/uGraph.ml b/kernel/uGraph.ml
@@ -39,7 +39,8 @@ type explanation =
   | Path of path_explanation
   | Other of Pp.t
 
-type univ_inconsistency = constraint_type * Sorts.t * Sorts.t * explanation option
+type univ_variable_printers = (Sorts.QVar.t -> Pp.t) * (Level.t -> Pp.t)
+type univ_inconsistency = univ_variable_printers option * (constraint_type * Sorts.t * Sorts.t * explanation option)
 
 exception UniverseInconsistency of univ_inconsistency
 
@@ -102,7 +103,7 @@ let enforce_constraint cst g = match enforce_constraint0 cst g with
     let (u, c, v) = cst in
     let e = lazy (G.get_explanation cst g.graph) in
     let mk u = Sorts.sort_of_univ @@ Universe.make u in
-    raise (UniverseInconsistency (c, mk u, mk v, Some (Path e)))
+    raise (UniverseInconsistency (None, (c, mk u, mk v, Some (Path e))))
   else g
 | Some g -> g
 
@@ -152,7 +153,7 @@ let enforce_leq_alg u v g =
   | Inr ((u, c, v), g) ->
     let e = lazy (G.get_explanation (u, c, v) g.graph) in
     let mk u = Sorts.sort_of_univ @@ Universe.make u in
-    let e = UniverseInconsistency (c, mk u, mk v, Some (Path e)) in
+    let e = UniverseInconsistency (None, (c, mk u, mk v, Some (Path e))) in
     raise e
 
 module Bound =
@@ -275,7 +276,11 @@ let pr_universes prl g = pr_pmap Pp.mt (pr_arc prl) g
 
 open Pp
 
-let explain_universe_inconsistency prq prl (o,u,v,p : univ_inconsistency) =
+let explain_universe_inconsistency default_prq default_prl (printers, (o,u,v,p) : univ_inconsistency) =
+  let prq, prl = match printers with
+    | Some (prq, prl) -> prq, prl
+    | None -> default_prq, default_prl
+  in
   let pr_uni u = match u with
   | Sorts.Set -> str "Set"
   | Sorts.Prop -> str "Prop"

diff --git a/kernel/uGraph.mli b/kernel/uGraph.mli
@@ -50,7 +50,8 @@ type explanation =
   | Path of path_explanation
   | Other of Pp.t
 
-type univ_inconsistency = constraint_type * Sorts.t * Sorts.t * explanation option
+type univ_variable_printers = (Sorts.QVar.t -> Pp.t) * (Level.t -> Pp.t)
+type univ_inconsistency = univ_variable_printers option * (constraint_type * Sorts.t * Sorts.t * explanation option)
 
 exception UniverseInconsistency of univ_inconsistency
 

diff --git a/test-suite/output/UnivBinders.out b/test-suite/output/UnivBinders.out
@@ -251,3 +251,6 @@ Arguments MutualI1' A%type_scope
 Arguments C1' A%type_scope p1
 Arguments MutualI2' A%type_scope
 Arguments C2' A%type_scope p2
+File "./output/UnivBinders.v", line 208, characters 0-33:
+The command has indeed failed with message:
+Universe inconsistency. Cannot enforce a < a because a = a.
diff --git a/test-suite/output/UnivBinders.v b/test-suite/output/UnivBinders.v
@@ -200,3 +200,11 @@ with MutualI2' (A:Type) := C2' (p2 : MutualI1' A).
 Print MutualI2'.
 
 End MutualTypes.
+
+Module Inconsistency.
+
+Set Universe Polymorphism.
+Definition g@{a b} := Type@{a} : Type@{b}.
+Fail Definition h@{a} := g@{a a}.
+
+End Inconsistency.