From f8667d35c3b15fa362ec0fb41f8c0a4d6bd007ab Mon Sep 17 00:00:00 2001
From: Robbert Krebbers <mail@robbertkrebbers.nl>
Date: Tue, 9 Aug 2022 16:04:26 +0200
Subject: [PATCH] Add instance for `FromSep (tc_opaque P) Q1 Q2` and update
 comment.

---
 iris/proofmode/classes.v | 12 +++++++++---
 1 file changed, 9 insertions(+), 3 deletions(-)

diff --git a/iris/proofmode/classes.v b/iris/proofmode/classes.v
index 9596b66ca..e5c8570f1 100644
--- a/iris/proofmode/classes.v
+++ b/iris/proofmode/classes.v
@@ -625,10 +625,16 @@ Global Instance from_wand_tc_opaque {PROP : bi} (P Q1 Q2 : PROP) :
   FromWand P Q1 Q2 → FromWand (tc_opaque P) Q1 Q2 := id.
 Global Instance into_wand_tc_opaque {PROP : bi} p q (R P Q : PROP) :
   IntoWand p q R P Q → IntoWand p q (tc_opaque R) P Q := id.
-(* Higher cost than [from_and_sep] so that [iCombine] does not loop.
-   FIXME: this comment is outdated and [from_and_sep] does not exist any more. *)
+
+(* This instance has a very high cost. The tactic [iCombine] will look for
+[FromSep ?P Q1 Q2]. If the cost of this instance is low (and in particular,
+lower than the default instance [from_sep_sep], which picks [?P := Q1 * Q2]),
+then TC search would diverge. *)
+Global Instance from_sep_tc_opaque {PROP : bi} (P Q1 Q2 : PROP) :
+  FromSep P Q1 Q2 → FromSep (tc_opaque P) Q1 Q2 | 102 := id.
+
 Global Instance from_and_tc_opaque {PROP : bi} (P Q1 Q2 : PROP) :
-  FromAnd P Q1 Q2 → FromAnd (tc_opaque P) Q1 Q2 | 102 := id.
+  FromAnd P Q1 Q2 → FromAnd (tc_opaque P) Q1 Q2 := id.
 Global Instance into_and_tc_opaque {PROP : bi} p (P Q1 Q2 : PROP) :
   IntoAnd p P Q1 Q2 → IntoAnd p (tc_opaque P) Q1 Q2 := id.
 Global Instance into_sep_tc_opaque {PROP : bi} (P Q1 Q2 : PROP) :
-- 
GitLab