From 498660d627e405bd34f91b5e709d6acb68e577ed Mon Sep 17 00:00:00 2001
From: =?UTF-8?q?Maxime=20D=C3=A9n=C3=A8s?= <maxime.denes@inria.fr>
Date: Thu, 12 Dec 2019 14:04:50 +0100
Subject: [PATCH] Avoid unwanted subgoals when applying `from_assumption_exact`

---
 tests/proofmode.v                       |  3 +++
 theories/proofmode/class_instances_bi.v | 10 +++++++---
 2 files changed, 10 insertions(+), 3 deletions(-)

diff --git a/tests/proofmode.v b/tests/proofmode.v
index fe6b8969a..1332a8bb4 100644
--- a/tests/proofmode.v
+++ b/tests/proofmode.v
@@ -107,6 +107,9 @@ Proof. by iIntros. Qed.
 Lemma test_iAssumption_evar_ex_false : ∃ R, R ⊢ ∀ P, P.
 Proof. eexists. iIntros "?" (P). iAssumption. Qed.
 
+Lemma test_iApply_evar P Q R : (∀ Q, Q -∗ P) -∗ R -∗ P.
+Proof. iIntros "H1 H2". iApply "H1". iExact "H2". Qed.
+
 Lemma test_iAssumption_affine P Q R `{!Affine P, !Affine R} : P -∗ Q -∗ R -∗ Q.
 Proof. iIntros "H1 H2 H3". iAssumption. Qed.
 
diff --git a/theories/proofmode/class_instances_bi.v b/theories/proofmode/class_instances_bi.v
index b9aeb7523..468ea5adb 100644
--- a/theories/proofmode/class_instances_bi.v
+++ b/theories/proofmode/class_instances_bi.v
@@ -4,12 +4,16 @@ From iris.proofmode Require Import base modality_instances classes ltac_tactics.
 Set Default Proof Using "Type".
 Import bi.
 
-(** The following lemma is not an instance, but defined using a [Hint Extern] to
-enable the better unification algorithm. *)
+(** The lemma [from_assumption_exact is not an instance, but defined using
+[notypeclasses refine] through [Hint Extern] to enable the better unification
+algorithm. We use [shelve] to avoid the creation of unshelved goals for evars
+by [refine], which otherwise causes TC search to fail. Such unshelved goals are
+created for example when solving [FromAssumption p ?P ?Q] where both [?P] and
+[?Q] are evars. See [test_iApply_evar] in [tests/proofmode] for an example. *)
 Lemma from_assumption_exact {PROP : bi} p (P : PROP) : FromAssumption p P P.
 Proof. by rewrite /FromAssumption /= intuitionistically_if_elim. Qed.
 Hint Extern 0 (FromAssumption _ _ _) =>
-  notypeclasses refine (from_assumption_exact _ _) : typeclass_instances.
+  notypeclasses refine (from_assumption_exact _ _); shelve : typeclass_instances.
 
 Section bi_instances.
 Context {PROP : bi}.
-- 
GitLab