Finish fixing setoid rewrite under anonymous lambdas (hopefully)

Fix #13246

Not sure if this is the right thing to do, but it seems to work.

1 files changed, 69 insertions, 0 deletions

diff --git a/test-suite/bugs/closed/bug_13246.v b/test-suite/bugs/closed/bug_13246.v
new file mode 100644
index 0000000000..11f5baaaf4
--- /dev/null
+++ b/test-suite/bugs/closed/bug_13246.v
@@ -0,0 +1,69 @@
+Axiom _0: Prop.
+
+From Coq Require Export Morphisms Setoid Utf8.
+
+Class Equiv A := equiv: relation A.
+
+Reserved Notation "P ⊢ Q" (at level 99, Q at level 200, right associativity).
+Reserved Notation "P ⊣⊢ Q" (at level 95, no associativity).
+Reserved Notation "■ P" (at level 20, right associativity).
+
+(** Define the scope *)
+Declare Scope bi_scope.
+Delimit Scope bi_scope with I.
+
+Structure bi :=
+  Bi { bi_car :> Type;
+       bi_entails : bi_car → bi_car → Prop;
+       bi_impl : bi_car → bi_car → bi_car;
+       bi_forall : ∀ A, (A → bi_car) → bi_car; }.
+
+Declare Instance bi_equiv `{PROP:bi} : Equiv (bi_car PROP).
+
+Arguments bi_car : simpl never.
+Arguments bi_entails {PROP} _%I _%I : simpl never, rename.
+Arguments bi_impl {PROP} _%I _%I : simpl never, rename.
+Arguments bi_forall {PROP _} _%I : simpl never, rename.
+
+Notation "P ⊢ Q" := (bi_entails P%I Q%I) .
+Notation "P ⊣⊢ Q" := (equiv (A:=bi_car _) P%I Q%I) .
+
+Infix "→" := bi_impl : bi_scope.
+Notation "∀ x .. y , P" :=
+  (bi_forall (λ x, .. (bi_forall (λ y, P)) ..)%I) : bi_scope.
+
+(* bug disappears if definitional class *)
+Class Plainly (PROP : bi) := { plainly : PROP -> PROP; }.
+Notation "■ P" := (plainly P) : bi_scope.
+
+Section S.
+  Context {I : Type} {PROP : bi} `(Plainly PROP).
+
+  Lemma plainly_forall `{Plainly PROP} {A} (Ψ : A → PROP) : (∀ a, ■ (Ψ a)) ⊣⊢ ■ (∀ a, Ψ a).
+  Proof. Admitted.
+
+  Global Instance entails_proper :
+    Proper (equiv ==> equiv ==> iff) (bi_entails : relation PROP).
+  Proof. Admitted.
+
+  Global Instance impl_proper :
+    Proper (equiv ==> equiv ==> equiv) (@bi_impl PROP).
+  Proof. Admitted.
+
+  Global Instance forall_proper A :
+    Proper (pointwise_relation _ equiv ==> equiv) (@bi_forall PROP A).
+  Proof. Admitted.
+
+  Declare Instance PROP_Equivalence: Equivalence (@equiv PROP _).
+
+  Set Mangle Names.
+  Lemma foo (P : I -> PROP) K:
+    K ⊢ ∀ (j : I)
+          (_ : Prop) (* bug disappears if this is removed *)
+      , (∀ i0, ■ P i0) → P j.
+  Proof.
+    setoid_rewrite plainly_forall.
+    (* retype in case the tactic did some nonsense *)
+    match goal with |- ?T => let _ := type of T in idtac end.
+  Abort.
+End S.