Fix #6956: Uncaught exception in bytecode compilation

We also make the code of [compact] in kernel/univ.ml a bit clearer.

1 files changed, 14 insertions, 33 deletions

diff --git a/kernel/univ.ml b/kernel/univ.ml
index be21381b7..ea3a52295 100644
--- a/kernel/univ.ml
+++ b/kernel/univ.ml
@@ -490,39 +490,6 @@ struct
     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
@@ -1208,6 +1175,20 @@ let abstract_cumulativity_info (univs, variance) =
   let subst, univs = abstract_universes univs in
   subst, (univs, variance)
 
+let rec compact_univ s vars i u =
+  match u with
+  | [] -> (s, List.rev vars)
+  | (lvl, _) :: u ->
+    match Level.var_index lvl with
+    | Some k when not (LMap.mem lvl s) ->
+      let lvl' = Level.var i in
+      compact_univ (LMap.add lvl lvl' s) (k :: vars) (i+1) u
+    | _ -> compact_univ s vars i u
+
+let compact_univ u =
+  let (s, s') = compact_univ LMap.empty [] 0 u in
+  (subst_univs_level_universe s u, s')
+
 (** Pretty-printing *)
 
 let pr_constraints prl = Constraint.pr prl