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

5 files changed, 50 insertions, 22 deletions

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 *)