Merge PR #6713: Fix #6677: Critical bug with VM and universes

6 files changed, 58 insertions, 22 deletions

diff --git a/kernel/cbytegen.ml b/kernel/cbytegen.ml
index 5dab2932d..4a34dbcff 100644
--- a/kernel/cbytegen.ml
+++ b/kernel/cbytegen.ml
@@ -628,27 +628,17 @@ let rec compile_constr reloc c sz cont =
         of the structured constant, while the later (if any) will be applied as
         arguments. *)
      let open Univ in begin
-      let levels = Universe.levels u in
-      let global_levels =
-	LSet.filter (fun x -> Level.var_index x = None) levels
-      in
-      let local_levels =
-	List.map_filter (fun x -> Level.var_index x)
-	  (LSet.elements levels)
-      in
+      let u,s = Universe.compact u in
       (* We assume that [Universe.type0m] is a neutral element for [Universe.sup] *)
-      let uglob =
-	LSet.fold (fun lvl u -> Universe.sup u (Universe.make lvl)) global_levels Universe.type0m
-      in
-      if local_levels = [] then
-	compile_str_cst reloc (Bstrconst (Const_sorts (Sorts.Type uglob))) sz cont
+      if List.is_empty s then
+        compile_str_cst reloc (Bstrconst (Const_sorts (Sorts.Type u))) sz cont
       else
 	let compile_get_univ reloc idx sz cont =
           set_max_stack_size sz;
 	  compile_fv_elem reloc (FVuniv_var idx) sz cont
 	in
         comp_app compile_str_cst compile_get_univ reloc
-	  (Bstrconst (Const_type u)) (Array.of_list local_levels) sz cont
+          (Bstrconst (Const_type u)) (Array.of_list s) sz cont
     end
   | LetIn(_,xb,_,body) ->
       compile_constr reloc xb sz
diff --git a/kernel/csymtable.ml b/kernel/csymtable.ml
index 2bbb867cd..bbd284bc1 100644
--- a/kernel/csymtable.ml
+++ b/kernel/csymtable.ml
@@ -70,7 +70,7 @@ let rec eq_structured_constant c1 c2 = match c1, c2 with
 | Const_bn _, _ -> false
 | Const_univ_level l1 , Const_univ_level l2 -> Univ.Level.equal l1 l2
 | Const_univ_level _ , _ -> false
-| Const_type u1 , Const_type u2 -> Univ.Universe.equal u1 u2
+| Const_type u1, Const_type u2 -> Univ.Universe.equal u1 u2
 | Const_type _ , _ -> false
 
 let rec hash_structured_constant c =
diff --git a/kernel/univ.ml b/kernel/univ.ml
index 080bb7ad4..fbb047364 100644
--- a/kernel/univ.ml
+++ b/kernel/univ.ml
@@ -266,7 +266,7 @@ struct
   module Expr = 
   struct
     type t = Level.t * int
-	
+
     (* Hashing of expressions *)
     module ExprHash = 
     struct
@@ -487,7 +487,40 @@ struct
       | [] -> cons a l
     in 
       List.fold_right (fun a acc -> aux a acc) u []
-	
+
+  (** [max_var_pred p u] returns the maximum variable level in [u] satisfying
+      [p], -1 if not found *)
+  let rec max_var_pred p u =
+    let open Level in
+    match u with
+    | [] -> -1
+    | (v, _) :: u ->
+      match var_index v with
+      | Some i when p i -> max i (max_var_pred p u)
+      | _ -> max_var_pred p u
+
+  let rec remap_var u i j =
+    let open Level in
+    match u with
+    | [] -> []
+    | (v, incr) :: u when var_index v = Some i ->
+      (Level.var j, incr) :: remap_var u i j
+    | _ :: u -> remap_var u i j
+
+  let rec compact u max_var i =
+    if i >= max_var then (u,[]) else
+    let j = max_var_pred (fun j -> j < i) u in
+    if Int.equal i (j+1) then
+      let (u,s) = compact u max_var (i+1) in
+      (u, i :: s)
+    else
+      let (u,s) = compact (remap_var u i j) max_var (i+1) in
+      (u, j+1 :: s)
+
+  let compact u =
+    let max_var = max_var_pred (fun _ -> true) u in
+    compact u max_var 0
+
   (* Returns the formal universe that is greater than the universes u and v.
      Used to type the products. *)
   let sup x y = merge_univs x y
diff --git a/kernel/univ.mli b/kernel/univ.mli
index 77ebf5a11..c45ebe21c 100644
--- a/kernel/univ.mli
+++ b/kernel/univ.mli
@@ -125,6 +125,13 @@ sig
   val for_all : (Level.t * int -> bool) -> t -> bool
 
   val map : (Level.t * int -> 'a) -> t -> 'a list
+
+  (** [compact u] remaps local variables in [u] such that their indices become
+       consecutive. It returns the new universe and the mapping.
+       Example: compact [(Var 0, i); (Prop, 0); (Var 2; j))] =
+         [(Var 0,i); (Prop, 0); (Var 1; j)], [0; 2]
+  *)
+  val compact : t -> t * int list
 end
 
 type universe = Universe.t
diff --git a/kernel/vmvalues.ml b/kernel/vmvalues.ml
index 1102cdec1..2d8a1d976 100644
--- a/kernel/vmvalues.ml
+++ b/kernel/vmvalues.ml
@@ -8,6 +8,7 @@
 open Names
 open Sorts
 open Cbytecodes
+open Univ
 
 (*******************************************)
 (* Initalization of the abstract machine ***)
@@ -189,11 +190,11 @@ let rec whd_accu a stk =
   | i when Int.equal i type_atom_tag ->
      begin match stk with
      | [Zapp args] ->
-        let u = ref (Obj.obj (Obj.field at 0)) in
-        for i = 0 to nargs args - 1 do
-          u := Univ.Universe.sup !u (Univ.Universe.make (uni_lvl_val (arg args i)))
-        done;
-        Vsort (Type !u)
+        let args = Array.init (nargs args) (arg args) in
+        let u = Obj.obj (Obj.field at 0) in
+        let inst = Instance.of_array (Array.map uni_lvl_val args) in
+        let u = Univ.subst_instance_universe inst u in
+        Vsort (Type u)
      | _ -> assert false
      end
   | i when i <= max_atom_tag ->
diff --git a/test-suite/bugs/closed/6677.v b/test-suite/bugs/closed/6677.v
new file mode 100644
index 000000000..99e47bb87
--- /dev/null
+++ b/test-suite/bugs/closed/6677.v
@@ -0,0 +1,5 @@
+Set Universe Polymorphism.
+
+Definition T@{i} := Type@{i}.
+Fail Definition U@{i} := (T@{i} <: Type@{i}).
+Fail Definition eqU@{i j} : @eq T@{j} U@{i} T@{i} := eq_refl.