Merge PR #9155: Fix race condition triggered by fresh universe generation

19 files changed, 117 insertions, 86 deletions

diff --git a/checker/values.ml b/checker/values.ml
index dcb2bca81a..863f965896 100644
--- a/checker/values.ml
+++ b/checker/values.ml
@@ -93,9 +93,9 @@ let v_cons = v_tuple "constructor" [|v_ind;Int|]
 
 
 (** kernel/univ *)
-
+let v_level_global = v_tuple "Level.Global.t" [|v_dp;Int|]
 let v_raw_level = v_sum "raw_level" 2 (* Prop, Set *) 
-  [|(*Level*)[|Int;v_dp|]; (*Var*)[|Int|]|]
+  [|(*Level*)[|v_level_global|]; (*Var*)[|Int|]|]
 let v_level = v_tuple "level" [|Int;v_raw_level|] 
 let v_expr = v_tuple "levelexpr" [|v_level;Int|]
 let v_univ = List v_expr
diff --git a/engine/termops.mli b/engine/termops.mli
index eef8452e64..7920af8e0e 100644
--- a/engine/termops.mli
+++ b/engine/termops.mli
@@ -290,7 +290,7 @@ val is_Prop : Evd.evar_map -> constr -> bool
 val is_Set : Evd.evar_map -> constr -> bool
 val is_Type : Evd.evar_map -> constr -> bool
 
-val reference_of_level : Evd.evar_map -> Univ.Level.t -> Libnames.qualid
+val reference_of_level : Evd.evar_map -> Univ.Level.t -> Libnames.qualid option
 
 (** Combinators on judgments *)
 
diff --git a/engine/uState.ml b/engine/uState.ml
index 6aecc368e6..185283225c 100644
--- a/engine/uState.ml
+++ b/engine/uState.ml
@@ -324,12 +324,14 @@ let constrain_variables diff ctx =
 let qualid_of_level uctx =
   let map, map_rev = uctx.uctx_names in 
     fun l ->
-      try Libnames.qualid_of_ident (Option.get (Univ.LMap.find l map_rev).uname)
+      try Some (Libnames.qualid_of_ident (Option.get (Univ.LMap.find l map_rev).uname))
       with Not_found | Option.IsNone ->
         UnivNames.qualid_of_level l
 
 let pr_uctx_level uctx l =
-  Libnames.pr_qualid (qualid_of_level uctx l)
+  match qualid_of_level uctx l with
+  | Some qid -> Libnames.pr_qualid qid
+  | None -> Univ.Level.pr l
 
 type ('a, 'b) gen_universe_decl = {
   univdecl_instance : 'a; (* Declared universes *)
@@ -533,7 +535,7 @@ let emit_side_effects eff u =
 
 let new_univ_variable ?loc rigid name
   ({ uctx_local = ctx; uctx_univ_variables = uvars; uctx_univ_algebraic = avars} as uctx) =
-  let u = UnivGen.new_univ_level () in
+  let u = UnivGen.fresh_level () in
   let ctx' = Univ.ContextSet.add_universe u ctx in
   let uctx', pred =
     match rigid with
diff --git a/engine/uState.mli b/engine/uState.mli
index ad0cd5c1bb..5170184ef4 100644
--- a/engine/uState.mli
+++ b/engine/uState.mli
@@ -188,6 +188,6 @@ val update_sigma_env : t -> Environ.env -> t
 (** {5 Pretty-printing} *)
 
 val pr_uctx_level : t -> Univ.Level.t -> Pp.t
-val qualid_of_level : t -> Univ.Level.t -> Libnames.qualid
+val qualid_of_level : t -> Univ.Level.t -> Libnames.qualid option
 
 val pr_weak : (Univ.Level.t -> Pp.t) -> t -> Pp.t
diff --git a/engine/univGen.ml b/engine/univGen.ml
index 130aa06f53..40c4c909fe 100644
--- a/engine/univGen.ml
+++ b/engine/univGen.ml
@@ -13,26 +13,25 @@ open Names
 open Constr
 open Univ
 
+type univ_unique_id = int
 (* Generator of levels *)
-type universe_id = DirPath.t * int
-
 let new_univ_id, set_remote_new_univ_id =
   RemoteCounter.new_counter ~name:"Universes" 0 ~incr:((+) 1)
-    ~build:(fun n -> Global.current_dirpath (), n)
+    ~build:(fun n -> n)
 
-let new_univ_level () =
-  let dp, id = new_univ_id () in
-  Univ.Level.make dp id
+let new_univ_global () =
+  Univ.Level.UGlobal.make (Global.current_dirpath ()) (new_univ_id ())
 
-let fresh_level () = new_univ_level ()
+let fresh_level () =
+  Univ.Level.make (new_univ_global ())
 
 (* TODO: remove *)
-let new_univ dp = Univ.Universe.make (new_univ_level dp)
-let new_Type dp = mkType (new_univ dp)
-let new_Type_sort dp = Type (new_univ dp)
+let new_univ () = Univ.Universe.make (fresh_level ())
+let new_Type () = mkType (new_univ ())
+let new_Type_sort () = Type (new_univ ())
 
 let fresh_instance auctx =
-  let inst = Array.init (AUContext.size auctx) (fun _ -> new_univ_level()) in
+  let inst = Array.init (AUContext.size auctx) (fun _ -> fresh_level()) in
   let ctx = Array.fold_right LSet.add inst LSet.empty in
   let inst = Instance.of_array inst in
   inst, (ctx, AUContext.instantiate inst auctx)
diff --git a/engine/univGen.mli b/engine/univGen.mli
index 8af5f8fdb0..b4598e10d0 100644
--- a/engine/univGen.mli
+++ b/engine/univGen.mli
@@ -15,14 +15,14 @@ open Univ
 
 
 (** The global universe counter *)
-type universe_id = DirPath.t * int
-
-val set_remote_new_univ_id : universe_id RemoteCounter.installer
+type univ_unique_id
+val set_remote_new_univ_id : univ_unique_id RemoteCounter.installer
+val new_univ_id : unit -> univ_unique_id (** for the stm *)
 
 (** Side-effecting functions creating new universe levels. *)
 
-val new_univ_id : unit -> universe_id
-val new_univ_level : unit -> Level.t
+val new_univ_global : unit -> Level.UGlobal.t
+val fresh_level : unit -> Level.t
 
 val new_univ : unit -> Universe.t
 [@@ocaml.deprecated "Use [new_univ_level]"]
diff --git a/engine/univNames.ml b/engine/univNames.ml
index 1019f8f0c2..19705f9d36 100644
--- a/engine/univNames.ml
+++ b/engine/univNames.ml
@@ -15,17 +15,15 @@ open Univ
 
 let qualid_of_level l =
   match Level.name l with
-  | Some (d, n as na)  ->
-    begin
-    try Nametab.shortest_qualid_of_universe na
-    with Not_found ->
-      let name = Id.of_string_soft (string_of_int n) in
-      Libnames.make_qualid d name
-    end
-  | None ->
-    Libnames.qualid_of_ident @@ Id.of_string_soft (Level.to_string l)
+  | Some qid  ->
+    (try Some (Nametab.shortest_qualid_of_universe qid)
+     with Not_found -> None)
+  | None -> None
 
-let pr_with_global_universes l = Libnames.pr_qualid (qualid_of_level l)
+let pr_with_global_universes l =
+  match qualid_of_level l with
+  | Some qid  -> Libnames.pr_qualid qid
+  | None -> Level.pr l
 
 (** Global universe information outside the kernel, to handle
     polymorphic universe names in sections that have to be discharged. *)
diff --git a/engine/univNames.mli b/engine/univNames.mli
index 6e68153ac2..e9c517babf 100644
--- a/engine/univNames.mli
+++ b/engine/univNames.mli
@@ -11,7 +11,7 @@
 open Univ
 
 val pr_with_global_universes : Level.t -> Pp.t
-val qualid_of_level : Level.t -> Libnames.qualid
+val qualid_of_level : Level.t -> Libnames.qualid option
 
 (** Local universe name <-> level mapping *)
 
diff --git a/interp/declare.ml b/interp/declare.ml
index 1e972d3e35..a809a856b9 100644
--- a/interp/declare.ml
+++ b/interp/declare.ml
@@ -469,7 +469,7 @@ type universe_source =
   | QualifiedUniv of Id.t (* global universe introduced by some global value *)
   | UnqualifiedUniv (* other global universe *)
 
-type universe_name_decl = universe_source * (Id.t * Nametab.universe_id) list
+type universe_name_decl = universe_source * (Id.t * Univ.Level.UGlobal.t) list
 
 let check_exists sp =
   if Nametab.exists_universe sp then
@@ -540,12 +540,8 @@ let do_universe poly l =
       user_err ~hdr:"Constraint"
                    (str"Cannot declare polymorphic universes outside sections")
   in
-  let l =
-    List.map (fun {CAst.v=id} ->
-      let lev = UnivGen.new_univ_id () in
-      (id, lev)) l
-  in
-  let ctx = List.fold_left (fun ctx (_,(dp,i)) -> Univ.LSet.add (Univ.Level.make dp i) ctx)
+  let l = List.map (fun {CAst.v=id} -> (id, UnivGen.new_univ_global ())) l in
+  let ctx = List.fold_left (fun ctx (_,qid) -> Univ.LSet.add (Univ.Level.make qid) ctx)
       Univ.LSet.empty l, Univ.Constraint.empty
   in
   let () = declare_universe_context poly ctx in
diff --git a/kernel/indtypes.ml b/kernel/indtypes.ml
index a4a02791b4..68d44f8782 100644
--- a/kernel/indtypes.ml
+++ b/kernel/indtypes.ml
@@ -218,7 +218,9 @@ let check_subtyping_arity_constructor env (subst : constr -> constr) (arcn : typ
 let check_subtyping cumi paramsctxt env_ar inds = 
     let numparams = Context.Rel.nhyps paramsctxt in
     let uctx = CumulativityInfo.univ_context cumi in
-    let new_levels = Array.init (UContext.size uctx) (Level.make DirPath.empty) in
+    let new_levels = Array.init (UContext.size uctx)
+        (fun i -> Level.make (Level.UGlobal.make DirPath.empty i))
+    in
     let lmap = Array.fold_left2 (fun lmap u u' -> LMap.add u u' lmap)
         LMap.empty (Instance.to_array @@ UContext.instance uctx) new_levels
     in
diff --git a/kernel/inductive.ml b/kernel/inductive.ml
index 9bbcf07f7e..05c5c0e821 100644
--- a/kernel/inductive.ml
+++ b/kernel/inductive.ml
@@ -593,10 +593,10 @@ let rec ienv_decompose_prod (env,_ as ienv) n c =
      ienv_decompose_prod ienv' (n-1) b
      | _ -> assert false
 
+let dummy_univ = Level.(make (UGlobal.make (DirPath.make [Id.of_string "implicit"]) 0))
+let dummy_implicit_sort = mkType (Universe.make dummy_univ)
 let lambda_implicit_lift n a =
-  let level = Level.make (DirPath.make [Id.of_string "implicit"]) 0 in
-  let implicit_sort = mkType (Universe.make level) in
-  let lambda_implicit a = mkLambda (Anonymous, implicit_sort, a) in
+  let lambda_implicit a = mkLambda (Anonymous, dummy_implicit_sort, a) in
   iterate lambda_implicit n (lift n a)
 
 (* This removes global parameters of the inductive types in lc (for
diff --git a/kernel/uGraph.ml b/kernel/uGraph.ml
index afdc8f1511..5fc8d0297f 100644
--- a/kernel/uGraph.ml
+++ b/kernel/uGraph.ml
@@ -921,7 +921,7 @@ let sort_universes g =
   let types = Array.init (max_lvl + 1) (function
     | 0 -> Level.prop
     | 1 -> Level.set
-    | n -> Level.make mp (n-2))
+    | n -> Level.make (Level.UGlobal.make  mp (n-2)))
   in
   let g = Array.fold_left (fun g u ->
     let g, u = safe_repr g u in
diff --git a/kernel/univ.ml b/kernel/univ.ml
index 2b3b4f9486..7b5ed05bda 100644
--- a/kernel/univ.ml
+++ b/kernel/univ.ml
@@ -36,10 +36,26 @@ open Util
 module RawLevel =
 struct
   open Names
+
+  module UGlobal = struct
+    type t = DirPath.t * int
+
+    let make dp i = (DirPath.hcons dp,i)
+
+    let equal (d, i) (d', i') = DirPath.equal d d' && Int.equal i i'
+
+    let hash (d,i) = Hashset.Combine.combine i (DirPath.hash d)
+
+    let compare (d, i) (d', i') =
+      let c = Int.compare i i' in
+      if Int.equal c 0 then DirPath.compare d d'
+      else c
+  end
+
   type t =
     | Prop
     | Set
-    | Level of int * DirPath.t
+    | Level of UGlobal.t
     | Var of int
 
   (* Hash-consing *)
@@ -49,8 +65,7 @@ struct
       match x, y with
       | Prop, Prop -> true
       | Set, Set -> true
-      | Level (n,d), Level (n',d') ->
-        Int.equal n n' && DirPath.equal d d'
+      | Level l, Level l' -> UGlobal.equal l l'
       | Var n, Var n' -> Int.equal n n'
       | _ -> false
 
@@ -62,7 +77,7 @@ struct
     | Set, Set -> 0
     | Set, _ -> -1
     | _, Set -> 1
-    | Level (i1, dp1), Level (i2, dp2) ->
+    | Level (dp1, i1), Level (dp2, i2) ->
       if i1 < i2 then -1
       else if i1 > i2 then 1
       else DirPath.compare dp1 dp2
@@ -83,9 +98,9 @@ struct
   let hcons = function
     | Prop as x -> x
     | Set as x -> x
-    | Level (n,d) as x -> 
+    | Level (d,n) as x ->
       let d' = Names.DirPath.hcons d in
-        if d' == d then x else Level (n,d')
+        if d' == d then x else Level (d',n)
     | Var _n as x -> x
 
   open Hashset.Combine
@@ -94,18 +109,18 @@ struct
     | Prop -> combinesmall 1 0
     | Set -> combinesmall 1 1
     | Var n -> combinesmall 2 n
-    | Level (n, d) -> combinesmall 3 (combine n (Names.DirPath.hash d))
+    | Level (d, n) -> combinesmall 3 (combine n (Names.DirPath.hash d))
 
 end
 
 module Level = struct
 
-  open Names
+  module UGlobal = RawLevel.UGlobal
 
   type raw_level = RawLevel.t =
   | Prop
   | Set
-  | Level of int * DirPath.t
+  | Level of UGlobal.t
   | Var of int
 
   (** Embed levels with their hash value *)
@@ -166,7 +181,7 @@ module Level = struct
     match data x with
     | Prop -> "Prop"
     | Set -> "Set"
-    | Level (n,d) -> Names.DirPath.to_string d^"."^string_of_int n
+    | Level (d,n) -> Names.DirPath.to_string d^"."^string_of_int n
     | Var n -> "Var(" ^ string_of_int n ^ ")"
 
   let pr u = str (to_string u)
@@ -185,11 +200,11 @@ module Level = struct
     match data u with
     | Var n -> Some n | _ -> None
 
-  let make m n = make (Level (n, Names.DirPath.hcons m))
+  let make qid = make (Level qid)
 
   let name u =
     match data u with
-    | Level (n, d) -> Some (d, n)
+    | Level (d, n) -> Some (d, n)
     | _ -> None
 end
 
diff --git a/kernel/univ.mli b/kernel/univ.mli
index de7b334ae4..512f38cedd 100644
--- a/kernel/univ.mli
+++ b/kernel/univ.mli
@@ -11,9 +11,22 @@
 (** Universes. *)
 module Level :
 sig
+
+  module UGlobal : sig
+    type t
+
+    val make : Names.DirPath.t -> int -> t
+    val equal : t -> t -> bool
+    val hash : t -> int
+    val compare : t -> t -> int
+
+  end
+  (** Qualified global universe level *)
+
   type t
   (** Type of universe levels. A universe level is essentially a unique name
-      that will be associated to constraints later on. *)
+      that will be associated to constraints later on. A level can be local to a
+      definition or global. *)
 
   val set : t
   val prop : t
@@ -34,9 +47,7 @@ sig
 
   val hash : t -> int
 
-  val make : Names.DirPath.t -> int -> t
-  (** Create a new universe level from a unique identifier and an associated
-      module path. *)
+  val make : UGlobal.t -> t
 
   val pr : t -> Pp.t
   (** Pretty-printing *)
@@ -48,7 +59,7 @@ sig
 
   val var_index : t -> int option
 
-  val name : t -> (Names.DirPath.t * int) option
+  val name : t -> UGlobal.t option
 end
 
 (** Sets of universe levels *)
diff --git a/library/nametab.ml b/library/nametab.ml
index e29c7b2960..f0f643d9b5 100644
--- a/library/nametab.ml
+++ b/library/nametab.ml
@@ -347,12 +347,10 @@ module DirTab = Make(DirPath')(GlobDirRef)
 type dirtab = DirTab.t
 let the_dirtab = Summary.ref ~name:"dirtab" (DirTab.empty : dirtab)
 
-type universe_id = DirPath.t * int
-
 module UnivIdEqual =
 struct
-  type t = universe_id
-  let equal (d, i) (d', i') = DirPath.equal d d' && Int.equal i i'
+  type t = Univ.Level.UGlobal.t
+  let equal = Univ.Level.UGlobal.equal
 end
 module UnivTab = Make(FullPath)(UnivIdEqual)
 type univtab = UnivTab.t
@@ -375,12 +373,9 @@ let the_modtyperevtab = Summary.ref ~name:"modtyperevtab" (MPmap.empty : mptrevt
 
 module UnivIdOrdered =
 struct
-  type t = universe_id
-  let hash (d, i) = i + DirPath.hash d
-  let compare (d, i) (d', i') =
-    let c = Int.compare i i' in
-    if Int.equal c 0 then DirPath.compare d d'
-    else c
+  type t = Univ.Level.UGlobal.t
+  let hash = Univ.Level.UGlobal.hash
+  let compare = Univ.Level.UGlobal.compare
 end
 
 module UnivIdMap = HMap.Make(UnivIdOrdered)
diff --git a/library/nametab.mli b/library/nametab.mli
index 24af07619d..b7926cf515 100644
--- a/library/nametab.mli
+++ b/library/nametab.mli
@@ -120,11 +120,9 @@ val push_modtype : visibility -> full_path -> ModPath.t -> unit
 val push_dir : visibility -> DirPath.t -> GlobDirRef.t -> unit
 val push_syndef : visibility -> full_path -> syndef_name -> unit
 
-type universe_id = DirPath.t * int
+module UnivIdMap : CMap.ExtS with type key = Univ.Level.UGlobal.t
 
-module UnivIdMap : CMap.ExtS with type key = universe_id
-
-val push_universe : visibility -> full_path -> universe_id -> unit
+val push_universe : visibility -> full_path -> Univ.Level.UGlobal.t -> unit
 
 (** {6 The following functions perform globalization of qualified names } *)
 
@@ -139,7 +137,7 @@ val locate_modtype : qualid -> ModPath.t
 val locate_dir : qualid -> GlobDirRef.t
 val locate_module : qualid -> ModPath.t
 val locate_section : qualid -> DirPath.t
-val locate_universe : qualid -> universe_id
+val locate_universe : qualid -> Univ.Level.UGlobal.t
 
 (** These functions globalize user-level references into global
    references, like [locate] and co, but raise a nice error message
@@ -196,7 +194,7 @@ val path_of_modtype : ModPath.t -> full_path
 
 (** A universe_id might not be registered with a corresponding user name.
     @raise Not_found if the universe was not introduced by the user. *)
-val path_of_universe : universe_id -> full_path
+val path_of_universe : Univ.Level.UGlobal.t -> full_path
 
 (** Returns in particular the dirpath or the basename of the full path
    associated to global reference *)
@@ -218,7 +216,7 @@ val shortest_qualid_of_global : ?loc:Loc.t -> Id.Set.t -> GlobRef.t -> qualid
 val shortest_qualid_of_syndef : ?loc:Loc.t -> Id.Set.t -> syndef_name -> qualid
 val shortest_qualid_of_modtype : ?loc:Loc.t -> ModPath.t -> qualid
 val shortest_qualid_of_module : ?loc:Loc.t -> ModPath.t -> qualid
-val shortest_qualid_of_universe : ?loc:Loc.t -> universe_id -> qualid
+val shortest_qualid_of_universe : ?loc:Loc.t -> Univ.Level.UGlobal.t -> qualid
 
 (** Deprecated synonyms *)
 
diff --git a/pretyping/detyping.ml b/pretyping/detyping.ml
index 33ced6d6e0..ce7c7c8702 100644
--- a/pretyping/detyping.ml
+++ b/pretyping/detyping.ml
@@ -589,8 +589,23 @@ let detype_cofix detype avoid env sigma n (names,tys,bodies) =
        Array.map (fun (_,_,ty) -> ty) v,
        Array.map (fun (_,bd,_) -> bd) v)
 
+(* TODO use some algebraic type with a case for unnamed univs so we
+   can cleanly detype them. NB: this corresponds to a hack in
+   Pretyping.interp_universe_level_name to convert Foo.xx strings into
+   universes. *)
+let hack_qualid_of_univ_level sigma l =
+  match Termops.reference_of_level sigma l with
+  | Some qid -> qid
+  | None ->
+    let path = String.split_on_char '.' (Univ.Level.to_string l) in
+    let path = List.rev_map Id.of_string_soft path in
+    Libnames.qualid_of_dirpath (DirPath.make path)
+
 let detype_universe sigma u =
-  let fn (l, n) = Some (Termops.reference_of_level sigma l, n) in
+  let fn (l, n) =
+    let qid = hack_qualid_of_univ_level sigma l in
+    Some (qid, n)
+  in
   Univ.Universe.map fn u
 
 let detype_sort sigma = function
@@ -611,7 +626,7 @@ let detype_anonymous = ref (fun ?loc n -> anomaly ~label:"detype" (Pp.str "index
 let set_detype_anonymous f = detype_anonymous := f
 
 let detype_level sigma l =
-  let l = Termops.reference_of_level sigma l in
+  let l = hack_qualid_of_univ_level sigma l in
   GType (UNamed l)
 
 let detype_instance sigma l = 
diff --git a/pretyping/pretyping.ml b/pretyping/pretyping.ml
index f5e48bcd39..2be0f73ea4 100644
--- a/pretyping/pretyping.ml
+++ b/pretyping/pretyping.ml
@@ -120,8 +120,8 @@ let interp_known_universe_level evd qid =
     if qualid_is_ident qid then Evd.universe_of_name evd @@ qualid_basename qid
     else raise Not_found
   with Not_found ->
-    let univ, k = Nametab.locate_universe qid in
-    Univ.Level.make univ k
+    let qid = Nametab.locate_universe qid in
+    Univ.Level.make qid
 
 let interp_universe_level_name ~anon_rigidity evd qid =
   try evd, interp_known_universe_level evd qid
@@ -140,7 +140,7 @@ let interp_universe_level_name ~anon_rigidity evd qid =
           user_err ?loc:qid.CAst.loc ~hdr:"interp_universe_level_name"
             (Pp.(str "Undeclared global universe: " ++ Libnames.pr_qualid qid))
       in
-      let level = Univ.Level.make dp num in
+      let level = Univ.Level.(make (UGlobal.make dp num)) in
       let evd =
         try Evd.add_global_univ evd level
         with UGraph.AlreadyDeclared -> evd
diff --git a/stm/asyncTaskQueue.ml b/stm/asyncTaskQueue.ml
index 94e04d1842..51166cf238 100644
--- a/stm/asyncTaskQueue.ml
+++ b/stm/asyncTaskQueue.ml
@@ -60,7 +60,7 @@ module Make(T : Task) () = struct
   type request = Request of T.request
 
   type more_data =
-    | MoreDataUnivLevel of UnivGen.universe_id list
+    | MoreDataUnivLevel of UnivGen.univ_unique_id list
 
   let slave_respond (Request r) =
     let res = T.perform r in