Fix #5761: cbv on undefined evars under binders produces unbound rel

When an evar is undefined we need to substitute inside the evar instance.

With help from @herbelin and @psteckler to identify the issue from a
large test case.

2 files changed, 151 insertions, 15 deletions

diff --git a/pretyping/cbv.ml b/pretyping/cbv.ml
index 3a2eac7e7..95de96926 100644
--- a/pretyping/cbv.ml
+++ b/pretyping/cbv.ml
@@ -208,25 +208,32 @@ and reify_value = function (* reduction under binders *)
   | STACK (n,v,stk) ->
       lift n (reify_stack (reify_value v) stk)
   | CBN(t,env) ->
-    t
-      (* map_constr_with_binders subs_lift (cbv_norm_term) env t *)
-  | LAM (n,ctxt,b,env) ->
-      List.fold_left (fun c (n,t)  -> mkLambda (n, t, c)) b ctxt
+    apply_env env t
+  | LAM (k,ctxt,b,env) ->
+    apply_env env @@
+    List.fold_left (fun c (n,t) ->
+        mkLambda (n, t, c)) b ctxt
   | FIXP ((lij,(names,lty,bds)),env,args) ->
-      mkApp
-        (mkFix (lij,
-		(names,
-		 lty,
-		 bds)),
-         Array.map reify_value args)
+    let fix = mkFix (lij, (names, lty, bds)) in
+    mkApp (apply_env env fix, Array.map reify_value args)
   | COFIXP ((j,(names,lty,bds)),env,args) ->
-      mkApp
-        (mkCoFix (j,
-		  (names,lty,bds)),
-         Array.map reify_value args)
+    let cofix = mkCoFix (j, (names,lty,bds)) in
+    mkApp (apply_env env cofix, Array.map reify_value args)
   | CONSTR (c,args) ->
       mkApp(mkConstructU c, Array.map reify_value args)
 
+and apply_env env t =
+  match kind t with
+  | Rel i ->
+    begin match expand_rel i env with
+      | Inl (k, v) ->
+        reify_value (shift_value k v)
+      | Inr (k,_) ->
+        mkRel k
+    end
+  | _ ->
+    map_with_binders subs_lift apply_env env t
+
 (* The main recursive functions
  *
  * Go under applications and cases/projections (pushed in the stack), 
@@ -290,7 +297,10 @@ let rec norm_head info env t stack =
   | Evar ev ->
       (match evar_value info.infos.i_cache ev with
           Some c -> norm_head info env c stack
-        | None -> (VAL(0, t), stack))
+        | None ->
+          let e, xs = ev in
+          let xs' = Array.map (apply_env env) xs in
+          (VAL(0, mkEvar (e,xs')), stack))
 
   (* non-neutral cases *)
   | Lambda _ ->
diff --git a/test-suite/bugs/closed/5761.v b/test-suite/bugs/closed/5761.v
new file mode 100644
index 000000000..6f28d1981
--- /dev/null
+++ b/test-suite/bugs/closed/5761.v
@@ -0,0 +1,126 @@
+Set Primitive Projections.
+Record mix := { a : nat ; b : a = a ; c : nat ; d : a = c ; e : nat ; f : nat }.
+Ltac strip_args T ctor :=
+  lazymatch type of ctor with
+  | context[T]
+    => match eval cbv beta in ctor with
+       | ?ctor _ => strip_args T ctor
+       | _ => ctor
+       end
+  end.
+Ltac get_ctor T :=
+  let full_ctor := constr:(ltac:(let x := fresh in intro x; econstructor; apply
+x) : T -> T) in
+  let ctor := constr:(fun x : T => ltac:(let v := strip_args T (full_ctor x) in
+exact v)) in
+  lazymatch ctor with
+  | fun _ => ?ctor => ctor
+  end.
+Ltac uncurry_domain f :=
+  lazymatch type of f with
+  | forall (a : ?A) (b : @ ?B a), _
+    => uncurry_domain (fun ab : { a : A & B a } => f (projT1 ab) (projT2 ab))
+  | _ => eval cbv beta in f
+  end.
+Ltac get_of_sigma T :=
+  let ctor := get_ctor T in
+  uncurry_domain ctor.
+Ltac repeat_existT :=
+  lazymatch goal with
+  | [ |- sigT _ ] => simple refine (existT _ _ _); [ repeat_existT | shelve ]
+  | _ => shelve
+  end.
+ Ltac prove_to_of_sigma_goal of_sigma :=
+  let v := fresh "v" in
+  simple refine (exist _ _ (fun v => _ : id _ (of_sigma v) = v));
+  try unfold of_sigma;
+  [ intro v; destruct v; repeat_existT
+  | cbv beta;
+    repeat match goal with
+           | [ |- context[projT2 ?k] ]
+             => let x := fresh "x" in
+                is_var k;
+                destruct k as [k x]; cbn [projT1 projT2]
+           end;
+    unfold id; reflexivity ].
+Ltac prove_to_of_sigma of_sigma :=
+  constr:(
+    ltac:(prove_to_of_sigma_goal of_sigma)
+    : { to_sigma : _ | forall v, id to_sigma (of_sigma v) = v }).
+Ltac get_to_sigma_gen of_sigma :=
+  let v := prove_to_of_sigma of_sigma in
+  eval hnf in (proj1_sig v).
+Ltac get_to_sigma T :=
+  let of_sigma := get_of_sigma T in
+  get_to_sigma_gen of_sigma.
+Definition to_sigma := ltac:(let v := get_to_sigma mix in exact v).
+(* Error:
+In nested Ltac calls to "get_to_sigma", "get_to_sigma_gen",
+"prove_to_of_sigma",
+"(_ : {to_sigma : _ | forall v, id to_sigma (of_sigma v) = v})" (with
+of_sigma:=fun
+            ab : {_
+                 : {_
+                   : {ab : {_ : {a : nat & a = a} & nat} &
+                     projT1 (projT1 ab) = projT2 ab} & nat} & nat} =>
+          {|
+          a := projT1 (projT1 (projT1 (projT1 (projT1 ab))));
+          b := projT2 (projT1 (projT1 (projT1 (projT1 ab))));
+          c := projT2 (projT1 (projT1 (projT1 ab)));
+          d := projT2 (projT1 (projT1 ab));
+          e := projT2 (projT1 ab);
+          f := projT2 ab |}) and "prove_to_of_sigma_goal", last call failed.
+Anomaly "Uncaught exception Not_found." Please report at
+http://coq.inria.fr/bugs/.
+frame @  file "toplevel/coqtop.ml", line 640, characters 6-22
+frame @  file "list.ml", line 73, characters 12-15
+frame @  file "toplevel/vernac.ml", line 344, characters 2-13
+frame @  file "toplevel/vernac.ml", line 308, characters 14-75
+raise @  file "lib/exninfo.ml", line 63, characters 8-15
+frame @  file "lib/flags.ml", line 141, characters 19-40
+raise @  file "lib/exninfo.ml", line 63, characters 8-15
+frame @  file "lib/flags.ml", line 11, characters 15-18
+raise @  file "lib/exninfo.ml", line 63, characters 8-15
+frame @  file "toplevel/vernac.ml", line 167, characters 6-16
+frame @  file "toplevel/vernac.ml", line 151, characters 26-39
+frame @  file "stm/stm.ml", line 2365, characters 2-35
+raise @  file "lib/exninfo.ml", line 63, characters 8-15
+frame @  file "stm/stm.ml", line 2355, characters 4-48
+frame @  file "stm/stm.ml", line 2321, characters 4-100
+raise @  file "lib/exninfo.ml", line 63, characters 8-15
+frame @  file "stm/stm.ml", line 832, characters 6-10
+frame @  file "stm/stm.ml", line 2206, characters 10-32
+raise @  file "lib/exninfo.ml", line 63, characters 8-15
+frame @  file "stm/stm.ml", line 975, characters 8-81
+raise @  file "lib/exninfo.ml", line 63, characters 8-15
+frame @  file "vernac/vernacentries.ml", line 2216, characters 10-389
+frame @  file "lib/flags.ml", line 141, characters 19-40
+raise @  file "lib/exninfo.ml", line 63, characters 8-15
+frame @  file "lib/flags.ml", line 11, characters 15-18
+frame @  file "vernac/command.ml", line 150, characters 4-56
+frame @  file "interp/constrintern.ml", line 2046, characters 2-73
+frame @  file "pretyping/pretyping.ml", line 1194, characters 19-77
+frame @  file "pretyping/pretyping.ml", line 1155, characters 8-72
+frame @  file "pretyping/pretyping.ml", line 628, characters 23-65
+frame @  file "plugins/ltac/tacinterp.ml", line 2095, characters 21-61
+frame @  file "proofs/pfedit.ml", line 178, characters 6-22
+raise @  file "lib/exninfo.ml", line 63, characters 8-15
+frame @  file "proofs/pfedit.ml", line 174, characters 8-36
+frame @  file "proofs/proof.ml", line 351, characters 4-30
+raise @  file "lib/exninfo.ml", line 63, characters 8-15
+frame @  file "engine/proofview.ml", line 1222, characters 8-12
+frame @  file "plugins/ltac/tacinterp.ml", line 2020, characters 19-36
+frame @  file "plugins/ltac/tacinterp.ml", line 618, characters 4-70
+raise @  file "lib/exninfo.ml", line 63, characters 8-15
+frame @  file "plugins/ltac/tacinterp.ml", line 214, characters 6-9
+frame @  file "pretyping/pretyping.ml", line 1198, characters 19-62
+frame @  file "pretyping/pretyping.ml", line 1155, characters 8-72
+raise @  unknown
+frame @  file "pretyping/pretyping.ml", line 628, characters 23-65
+frame @  file "plugins/ltac/tacinterp.ml", line 2095, characters 21-61
+frame @  file "proofs/pfedit.ml", line 178, characters 6-22
+raise @  file "lib/exninfo.ml", line 63, characters 8-15
+frame @  file "proofs/pfedit.ml", line 174, characters 8-36
+frame @  file "proofs/proof.ml", line 351, characters 4-30
+raise @  file "lib/exninfo.ml", line 63, characters 8-15
+ *)