Merge PR #8124: Fix #8121: anomalies in native_compute with let and evars.

9 files changed, 72 insertions, 26 deletions

diff --git a/kernel/nativecode.ml b/kernel/nativecode.ml
index cc35a70cbf..ad10c86945 100644
--- a/kernel/nativecode.ml
+++ b/kernel/nativecode.ml
@@ -1067,12 +1067,11 @@ let ml_of_instance instance u =
      let tyn = fresh_lname Anonymous in
      let i = push_symbol (SymbMeta mv) in
      MLapp(MLprimitive Mk_meta, [|get_meta_code i; MLlocal tyn|])
-  | Levar(evk,ty,args) ->
-     let tyn = fresh_lname Anonymous in
+  | Levar(evk, args) ->
      let i = push_symbol (SymbEvar evk) in
+     (** Arguments are *not* reversed in evar instances in native compilation *)
      let args = MLarray(Array.map (ml_of_lam env l) args) in
-     MLlet(tyn, ml_of_lam env l ty,
-       MLapp(MLprimitive Mk_evar, [|get_evar_code i;MLlocal tyn; args|]))
+     MLapp(MLprimitive Mk_evar, [|get_evar_code i; args|])
   | Lprod(dom,codom) ->
       let dom = ml_of_lam env l dom in
       let codom = ml_of_lam env l codom in
@@ -1749,7 +1748,7 @@ let pp_mllam fmt l =
     | Mk_cofix(start) -> Format.fprintf fmt "mk_cofix_accu %i" start
     | Mk_rel i -> Format.fprintf fmt "mk_rel_accu %i" i
     | Mk_var id ->
-        Format.fprintf fmt "mk_var_accu (Names.id_of_string \"%s\")" (string_of_id id)
+        Format.fprintf fmt "mk_var_accu (Names.Id.of_string \"%s\")" (string_of_id id)
     | Mk_proj -> Format.fprintf fmt "mk_proj_accu"
     | Is_int -> Format.fprintf fmt "is_int"
     | Cast_accu -> Format.fprintf fmt "cast_accu"
diff --git a/kernel/nativeconv.ml b/kernel/nativeconv.ml
index 931b8bbc86..c75dde843e 100644
--- a/kernel/nativeconv.ml
+++ b/kernel/nativeconv.ml
@@ -64,7 +64,7 @@ and conv_atom env pb lvl a1 a2 cu =
     match a1, a2 with
     | Ameta (m1,_), Ameta (m2,_) ->
       if Int.equal m1 m2 then cu else raise NotConvertible
-    | Aevar (ev1,_,args1), Aevar (ev2,_,args2) ->
+    | Aevar (ev1, args1), Aevar (ev2, args2) ->
       if Evar.equal ev1 ev2 then
         Array.fold_right2 (conv_val env CONV lvl) args1 args2 cu
       else raise NotConvertible
diff --git a/kernel/nativeinstr.mli b/kernel/nativeinstr.mli
index 5075bd3d14..2d8e2ba2f0 100644
--- a/kernel/nativeinstr.mli
+++ b/kernel/nativeinstr.mli
@@ -25,7 +25,7 @@ and lambda =
   | Lrel          of Name.t * int 
   | Lvar          of Id.t
   | Lmeta         of metavariable * lambda (* type *)
-  | Levar         of Evar.t * lambda (* type *) * lambda array (* arguments *)
+  | Levar         of Evar.t * lambda array (* arguments *)
   | Lprod         of lambda * lambda 
   | Llam          of Name.t array * lambda  
   | Llet          of Name.t * lambda * lambda
diff --git a/kernel/nativelambda.ml b/kernel/nativelambda.ml
index cec0ee57d5..122fe95df4 100644
--- a/kernel/nativelambda.ml
+++ b/kernel/nativelambda.ml
@@ -23,7 +23,6 @@ exception NotClosed
 
 type evars =
     { evars_val : existential -> constr option;
-      evars_typ : existential -> types;
       evars_metas : metavariable -> types }
 
 (*s Constructors *)
@@ -88,7 +87,7 @@ let get_const_prefix env c =
 let rec map_lam_with_binders g f n lam =
   match lam with
   | Lrel _ | Lvar _  | Lconst _ | Lproj _ | Lval _ | Lsort _ | Lind _
-  | Lconstruct _ | Llazy | Lforce | Lmeta _ | Levar _ -> lam
+  | Lconstruct _ | Llazy | Lforce | Lmeta _ -> lam
   | Lprod(dom,codom) -> 
       let dom' = f n dom in
       let codom' = f n codom in
@@ -139,6 +138,9 @@ let rec map_lam_with_binders g f n lam =
   | Luint u ->
     let u' = map_uint g f n u in
     if u == u' then lam else Luint u'
+  | Levar (evk, args) ->
+    let args' = Array.Smart.map (f n) args in
+    if args == args' then lam else Levar (evk, args')
 
 and map_uint g f n u =
   match u with
@@ -386,13 +388,10 @@ let is_lazy env prefix t =
 
 let evar_value sigma ev = sigma.evars_val ev
 
-let evar_type sigma ev = sigma.evars_typ ev
-
 let meta_type sigma mv = sigma.evars_metas mv
 
 let empty_evars =
   { evars_val = (fun _ -> None);
-    evars_typ = (fun _ -> assert false);
     evars_metas = (fun _ -> assert false) }
 
 let empty_ids = [||]
@@ -420,9 +419,8 @@ let rec lambda_of_constr cache env sigma c =
   | Evar (evk,args as ev) ->
      (match evar_value sigma ev with
      | None ->
-	let ty = evar_type sigma ev in
         let args = Array.map (lambda_of_constr cache env sigma) args in
-        Levar(evk, lambda_of_constr cache env sigma ty, args)
+        Levar(evk, args)
      | Some t -> lambda_of_constr cache env sigma t)
 
   | Cast (c, _, _) -> lambda_of_constr cache env sigma c
diff --git a/kernel/nativelambda.mli b/kernel/nativelambda.mli
index efe1700cd7..7b20258929 100644
--- a/kernel/nativelambda.mli
+++ b/kernel/nativelambda.mli
@@ -15,7 +15,6 @@ open Nativeinstr
 (** This file defines the lambda code generation phase of the native compiler *)
 type evars =
     { evars_val : existential -> constr option;
-      evars_typ : existential -> types;
       evars_metas : metavariable -> types }
 
 val empty_evars : evars
diff --git a/kernel/nativevalues.ml b/kernel/nativevalues.ml
index 91f6add1c3..3bf23f1468 100644
--- a/kernel/nativevalues.ml
+++ b/kernel/nativevalues.ml
@@ -63,7 +63,7 @@ type atom =
   | Acofixe of t array * t array * int * t
   | Aprod of Name.t * t * (t -> t)
   | Ameta of metavariable * t
-  | Aevar of Evar.t * t * t array
+  | Aevar of Evar.t * t array
   | Aproj of (inductive * int) * accumulator
 
 let accumulate_tag = 0
@@ -135,8 +135,8 @@ let mk_prod_accu s dom codom =
 let mk_meta_accu mv ty =
   mk_accu (Ameta (mv,ty))
 
-let mk_evar_accu ev ty args =
-  mk_accu (Aevar (ev,ty,args))
+let mk_evar_accu ev args =
+  mk_accu (Aevar (ev, args))
 
 let mk_proj_accu kn c = 
   mk_accu (Aproj (kn,c))
diff --git a/kernel/nativevalues.mli b/kernel/nativevalues.mli
index 6bbf15160c..10689941e8 100644
--- a/kernel/nativevalues.mli
+++ b/kernel/nativevalues.mli
@@ -53,7 +53,7 @@ type atom =
   | Acofixe of t array * t array * int * t
   | Aprod of Name.t * t * (t -> t)
   | Ameta of metavariable * t
-  | Aevar of Evar.t * t (* type *) * t array (* arguments *)
+  | Aevar of Evar.t * t array (* arguments *)
   | Aproj of (inductive * int) * accumulator
 
 (* Constructors *)
@@ -70,7 +70,7 @@ val mk_prod_accu : Name.t -> t -> t -> t
 val mk_fix_accu : rec_pos  -> int -> t array -> t array -> t
 val mk_cofix_accu : int -> t array -> t array -> t
 val mk_meta_accu : metavariable -> t
-val mk_evar_accu : Evar.t -> t -> t array -> t
+val mk_evar_accu : Evar.t -> t array -> t
 val mk_proj_accu : (inductive * int) -> accumulator -> t
 val upd_cofix : t -> t -> unit
 val force_cofix : t -> t 
diff --git a/pretyping/nativenorm.ml b/pretyping/nativenorm.ml
index 5df41ef76a..246acfc92e 100644
--- a/pretyping/nativenorm.ml
+++ b/pretyping/nativenorm.ml
@@ -354,9 +354,8 @@ and nf_atom_type env sigma atom =
       let env = push_rel (LocalAssum (n,dom)) env in
       let codom,s2 = nf_type_sort env sigma (codom vn) in
       mkProd(n,dom,codom), Typeops.type_of_product env n s1 s2
-  | Aevar(evk,ty,args) ->
-    let ty = nf_type env sigma ty in
-    nf_evar env sigma evk ty args
+  | Aevar(evk,args) ->
+    nf_evar env sigma evk args
   | Ameta(mv,ty) ->
      let ty = nf_type env sigma ty in
      mkMeta mv, ty
@@ -398,22 +397,27 @@ and  nf_predicate env sigma ind mip params v pT =
       mkLambda(name,dom,body)
     | _ -> nf_type env sigma v
 
-and nf_evar env sigma evk ty args =
+and nf_evar env sigma evk args =
   let evi = try Evd.find sigma evk with Not_found -> assert false in
   let hyps = Environ.named_context_of_val (Evd.evar_filtered_hyps evi) in
+  let ty = EConstr.Unsafe.to_constr @@ Evd.evar_concl evi in
   if List.is_empty hyps then begin
     assert (Int.equal (Array.length args) 0);
     mkEvar (evk, [||]), ty
   end
   else
+    (** 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 ty hyps in
     let ty, args = nf_args env sigma args t in
-    mkEvar (evk, Array.of_list args), ty
+    (** nf_args takes arguments in the reverse order but produces them in the
+        correct one, so we have to reverse them again for the evar node *)
+    mkEvar (evk, Array.rev_of_list args), ty
 
 let evars_of_evar_map sigma =
   { Nativelambda.evars_val = Evd.existential_opt_value0 sigma;
-    Nativelambda.evars_typ = Evd.existential_type0 sigma;
     Nativelambda.evars_metas = Evd.meta_type0 sigma }
 
 (* fork perf process, return profiler's process id *)
diff --git a/test-suite/bugs/closed/8121.v b/test-suite/bugs/closed/8121.v
new file mode 100644
index 0000000000..99267612ca
--- /dev/null
+++ b/test-suite/bugs/closed/8121.v
@@ -0,0 +1,46 @@
+Require Import Coq.Strings.String.
+
+Section T.
+  Eval native_compute in let x := tt in _.
+(* Error: Anomaly "Uncaught exception Constr.DestKO." Please report at http://coq.inria.fr/bugs/. *)
+  Eval native_compute in let _ := Set in _.
+(* Error: Anomaly "Uncaught exception Constr.DestKO." Please report at http://coq.inria.fr/bugs/. *)
+  Eval native_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 native_compute in _.
+(* Error: Anomaly "Uncaught exception Constr.DestKO." Please report at http://coq.inria.fr/bugs/. *)
+  Goal exists tt : unit, tt = tt. eexists. native_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 native_compute in _.
+(* Error: Anomaly "Uncaught exception Constr.DestKO." Please report at http://coq.inria.fr/bugs/. *)
+  Goal exists tt : unit, tt = tt. eexists. native_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 native_compute in _.
+(* Error: Anomaly "Uncaught exception Not_found." Please report at http://coq.inria.fr/bugs/. *)
+  Goal exists tt : unit, tt = tt. eexists. native_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 native_compute in _.
+(* Error: Anomaly "File "pretyping/vnorm.ml", line 60, characters 9-15: Assertion failed." *)
+  Goal exists tt : unit, tt = tt. eexists. native_compute. Abort.
+(* Error: Anomaly "File "pretyping/vnorm.ml", line 60, characters 9-15: Assertion failed." *)
+End S2.