Fix #6677: Critical bug with VM and universes

This bug was present since the first patch adding universe polymorphism
handling in the VM (Coq 8.5). Note that unsoundness can probably be
observed even without universe polymorphism.

6 files changed, 54 insertions, 23 deletions

diff --git a/dev/vm_printers.ml b/dev/vm_printers.ml
index f819d2e6a..b410d017d 100644
--- a/dev/vm_printers.ml
+++ b/dev/vm_printers.ml
@@ -61,7 +61,7 @@ and ppstack s =
 and ppatom a =
   match a with
   | Aid idk -> print_idkey idk
-  | Atype u -> print_string "Type(...)"
+  | Atype (u,l) -> print_string "Type(...)"
   | Aind(sp,i) ->  print_string "Ind(";
       print_string (MutInd.to_string sp);
       print_string ","; print_int i;
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 f72f6f26a..835dbee08 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 63bef1b81..f550872ba 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 ->