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

1 files changed, 126 insertions, 0 deletions

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
+ *)