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, 6 insertions, 5 deletions

diff --git a/kernel/vmvalues.ml b/kernel/vmvalues.ml
index 1102cdec18..2d8a1d9761 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 ->