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

5 files changed, 76 insertions, 0 deletions

diff --git a/kernel/cbytegen.ml b/kernel/cbytegen.ml
index 4613cd3214..e336ea922d 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/kernel/context.ml b/kernel/context.ml
index 831dc850fb..4a7204b75c 100644
--- a/kernel/context.ml
+++ b/kernel/context.ml
@@ -149,6 +149,10 @@ struct
       | LocalAssum (na, ty) -> na, None, ty
       | LocalDef (na, v, ty) -> na, Some v, ty
 
+    let drop_body = function
+      | LocalAssum _ as d -> d
+      | LocalDef (na, v, ty) -> LocalAssum (na, ty)
+
   end
 
   (** Rel-context is represented as a list of declarations.
@@ -211,6 +215,8 @@ struct
       | Declaration.LocalAssum _ :: ctx -> aux (false::l) ctx
     in aux [] l
 
+  let drop_bodies l = List.Smart.map Declaration.drop_body l
+
   (** [extended_list n Γ] builds an instance [args] such that [Γ,Δ ⊢ args:Γ]
       with n = |Δ| and with the {e local definitions} of [Γ] skipped in
       [args]. Example: for [x:T, y:=c, z:U] and [n]=2, it gives [Rel 5, Rel 3]. *)
@@ -348,6 +354,10 @@ struct
       | id, None, ty -> LocalAssum (id, ty)
       | id, Some v, ty -> LocalDef (id, v, ty)
 
+    let drop_body = function
+      | LocalAssum _ as d -> d
+      | LocalDef (id, v, ty) -> LocalAssum (id, ty)
+
     let of_rel_decl f = function
       | Rel.Declaration.LocalAssum (na,t) ->
           LocalAssum (f na, t)
@@ -403,6 +413,8 @@ struct
   let to_vars l =
     List.fold_left (fun accu decl -> Id.Set.add (Declaration.get_id decl) accu) Id.Set.empty l
 
+  let drop_bodies l = List.Smart.map Declaration.drop_body l
+
   (** [instance_from_named_context Ω] builds an instance [args] such
       that [Ω ⊢ args:Ω] where [Ω] is a named context and with the local
       definitions of [Ω] skipped. Example: for [id1:T,id2:=c,id3:U], it
diff --git a/kernel/context.mli b/kernel/context.mli
index 957ac4b3d6..2b0d36cb8c 100644
--- a/kernel/context.mli
+++ b/kernel/context.mli
@@ -85,6 +85,9 @@ sig
     val fold_constr : ('c -> 'a -> 'a) -> ('c, 'c) pt -> 'a -> 'a
 
     val to_tuple : ('c, 't) pt -> Name.t * 'c option * 't
+
+    (** Turn [LocalDef] into [LocalAssum], identity otherwise. *)
+    val drop_body : ('c, 't) pt -> ('c, 't) pt
   end
 
   (** Rel-context is represented as a list of declarations.
@@ -129,6 +132,9 @@ sig
       and each {e local definition} is mapped to [false]. *)
   val to_tags : ('c, 't) pt -> bool list
 
+  (** Turn all [LocalDef] into [LocalAssum], leave [LocalAssum] unchanged. *)
+  val drop_bodies : ('c, 't) pt -> ('c, 't) pt
+
   (** [extended_list mk n Γ] builds an instance [args] such that [Γ,Δ ⊢ args:Γ]
       with n = |Δ| and with the {e local definitions} of [Γ] skipped in
       [args] where [mk] is used to build the corresponding variables.
@@ -202,6 +208,9 @@ sig
     val to_tuple : ('c, 't) pt -> Id.t * 'c option * 't
     val of_tuple : Id.t * 'c option * 't -> ('c, 't) pt
 
+    (** Turn [LocalDef] into [LocalAssum], identity otherwise. *)
+    val drop_body : ('c, 't) pt -> ('c, 't) pt
+
     (** Convert [Rel.Declaration.t] value to the corresponding [Named.Declaration.t] value.
         The function provided as the first parameter determines how to translate "names" to "ids". *)
     val of_rel_decl : (Name.t -> Id.t) -> ('c, 't) Rel.Declaration.pt -> ('c, 't) pt
@@ -249,6 +258,9 @@ sig
   (** Return the set of all identifiers bound in a given named-context. *)
   val to_vars : ('c, 't) pt -> Id.Set.t
 
+  (** Turn all [LocalDef] into [LocalAssum], leave [LocalAssum] unchanged. *)
+  val drop_bodies : ('c, 't) pt -> ('c, 't) pt
+
   (** [to_instance Ω] builds an instance [args] such
       that [Ω ⊢ args:Ω] where [Ω] is a named-context and with the local
       definitions of [Ω] skipped. Example: for [id1:T,id2:=c,id3:U], it
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.