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.

1 files changed, 35 insertions, 2 deletions

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