Fix #8119: anomalies in vm_compute with let and evars.

There were actually two broken things with VM + evars, the fixes are:
- Do not pass let-bound arguments to evars.
- Use the right order for evar arguments.

Native compilation seems to be suffering from the same shortcomings, I will
open a separate bug and adapt the PR.

3 files changed, 52 insertions, 0 deletions

diff --git a/kernel/cbytegen.ml b/kernel/cbytegen.ml
index 6677db2fd9..981444ac5e 100644
--- a/kernel/cbytegen.ml
+++ b/kernel/cbytegen.ml
@@ -501,6 +501,9 @@ let rec compile_lam env cenv lam sz cont =
       if Array.is_empty args then
         compile_fv_elem cenv (FVevar evk) sz cont
       else
+        (** Arguments are reversed in evar instances *)
+        let args = Array.copy args in
+        let () = Array.rev args in
         comp_app compile_fv_elem (compile_lam env) cenv (FVevar evk) args sz cont
 
   | Lconst (kn,u) -> compile_constant env cenv kn u [||] sz cont
diff --git a/pretyping/vnorm.ml b/pretyping/vnorm.ml
index c944080503..255707dc7b 100644
--- a/pretyping/vnorm.ml
+++ b/pretyping/vnorm.ml
@@ -209,6 +209,9 @@ and nf_evar env sigma evk stk =
   | Zapp args :: stk ->
     (** We assume that there is no consecutive Zapp nodes in a VM stack. Is that
         really an invariant? *)
+    (** Let-bound arguments are present in the evar arguments but not in the
+        type, so we turn the let into a product. *)
+    let hyps = Context.Named.drop_bodies hyps in
     let fold accu d = Term.mkNamedProd_or_LetIn d accu in
     let t = List.fold_left fold concl hyps in
     let t, args = nf_args env sigma args t in
diff --git a/test-suite/bugs/closed/8119.v b/test-suite/bugs/closed/8119.v
new file mode 100644
index 0000000000..c6329a7328
--- /dev/null
+++ b/test-suite/bugs/closed/8119.v
@@ -0,0 +1,46 @@
+Require Import Coq.Strings.String.
+
+Section T.
+  Eval vm_compute in let x := tt in _.
+(* Error: Anomaly "Uncaught exception Constr.DestKO." Please report at http://coq.inria.fr/bugs/. *)
+  Eval vm_compute in let _ := Set in _.
+(* Error: Anomaly "Uncaught exception Constr.DestKO." Please report at http://coq.inria.fr/bugs/. *)
+  Eval vm_compute in let _ := Prop in _.
+(* Error: Anomaly "Uncaught exception Constr.DestKO." Please report at http://coq.inria.fr/bugs/. *)
+End T.
+
+Section U0.
+  Let n : unit := tt.
+  Eval vm_compute in _.
+(* Error: Anomaly "Uncaught exception Constr.DestKO." Please report at http://coq.inria.fr/bugs/. *)
+  Goal exists tt : unit, tt = tt. eexists. vm_compute. Abort.
+(* Error: Anomaly "Uncaught exception Constr.DestKO." Please report at http://coq.inria.fr/bugs/. *)
+End U0.
+
+Section S0.
+  Let LF : string := String (Coq.Strings.Ascii.Ascii false true false true false false false false) "".
+  Eval vm_compute in _.
+(* Error: Anomaly "Uncaught exception Constr.DestKO." Please report at http://coq.inria.fr/bugs/. *)
+  Goal exists tt : unit, tt = tt. eexists. vm_compute. Abort.
+(* Error: Anomaly "Uncaught exception Constr.DestKO." Please report at http://coq.inria.fr/bugs/. *)
+End S0.
+
+Class T := { }.
+Section S1.
+  Context {p : T}.
+  Let LF : string := String (Coq.Strings.Ascii.Ascii false true false true false false false false) "".
+  Eval vm_compute in _.
+(* Error: Anomaly "Uncaught exception Not_found." Please report at http://coq.inria.fr/bugs/. *)
+  Goal exists tt : unit, tt = tt. eexists. vm_compute. Abort.
+(* Error: Anomaly "Uncaught exception Not_found." Please report at http://coq.inria.fr/bugs/. *)
+End S1.
+
+Class M := { m : Type }.
+Section S2.
+  Context {p : M}.
+  Let LF : string := String (Coq.Strings.Ascii.Ascii false true false true false false false false) "".
+  Eval vm_compute in _.
+(* Error: Anomaly "File "pretyping/vnorm.ml", line 60, characters 9-15: Assertion failed." *)
+  Goal exists tt : unit, tt = tt. eexists. vm_compute. Abort.
+(* Error: Anomaly "File "pretyping/vnorm.ml", line 60, characters 9-15: Assertion failed." *)
+End S2.