From 72217e388467d1764e438d03d541f38868ef2984 Mon Sep 17 00:00:00 2001
From: Ralf Jung <jung@mpi-sws.org>
Date: Mon, 15 Aug 2022 09:28:41 -0400
Subject: [PATCH] fix Known with not-Known Make instances

---
 iris/proofmode/class_instances_make.v | 16 ++++++++++++----
 iris/proofmode/classes_make.v         |  5 ++++-
 2 files changed, 16 insertions(+), 5 deletions(-)

diff --git a/iris/proofmode/class_instances_make.v b/iris/proofmode/class_instances_make.v
index df86ed206..bb638daf7 100644
--- a/iris/proofmode/class_instances_make.v
+++ b/iris/proofmode/class_instances_make.v
@@ -85,10 +85,14 @@ Proof. by rewrite /MakeOr. Qed.
   to avoid [emp] in goals involving affine BIs, we give [make_affinely_affine]
   a lower cost than [make_affinely_True].
 - [make_affinely_default] adds the modality. This is the default instance since
-  it can always be used, and thus has the highest cost. *)
+  it can always be used, and thus has the highest cost.
+  (For this last point, the cost of the [KnownMakeAffinely] instances does not
+  actually matter, since this is a [MakeAffinely] instance, i.e. an instance of
+  a different class. What really matters is that the [known_make_affinely]
+  instance has a lower cost than [make_affinely_default].) *)
 
 Global Instance make_affinely_affine P :
-  QuickAffine P → MakeAffinely P P | 0.
+  QuickAffine P → KnownMakeAffinely P P | 0.
 Proof. apply affine_affinely. Qed.
 Global Instance make_affinely_True : @KnownMakeAffinely PROP True emp | 1.
 Proof. by rewrite /KnownMakeAffinely /MakeAffinely affinely_True_emp. Qed.
@@ -105,10 +109,14 @@ Proof. by rewrite /MakeAffinely. Qed.
   it does not really matter since goals in affine BIs typically do not contain
   occurrences of [emp] to start with.
 - [make_absorbingly_default] adds the modality. This is the default instance
-  since it can always be used, and thus has the highest cost. *)
+  since it can always be used, and thus has the highest cost.
+  (For this last point, the cost of the [KnownMakeAbsorbingly] instances does not
+  actually matter, since this is a [MakeAbsorbingly] instance, i.e. an instance of
+  a different class. What really matters is that the [known_make_absorbingly]
+  instance has a lower cost than [make_absorbingly_default].) *)
 
 Global Instance make_absorbingly_absorbing P :
-  QuickAbsorbing P → MakeAbsorbingly P P | 0.
+  QuickAbsorbing P → KnownMakeAbsorbingly P P | 0.
 Proof. apply absorbing_absorbingly. Qed.
 Global Instance make_absorbingly_emp : @KnownMakeAbsorbingly PROP emp True | 1.
 Proof.
diff --git a/iris/proofmode/classes_make.v b/iris/proofmode/classes_make.v
index 7d0bda7a2..4af72163f 100644
--- a/iris/proofmode/classes_make.v
+++ b/iris/proofmode/classes_make.v
@@ -35,7 +35,10 @@ evar, then [MakeX] will not instantiate it arbitrarily.
 The reason for this is that if given an evar, these classes would typically
 try to instantiate this evar with some arbitrary logical constructs such as
 [emp] or [True]. Therefore, we use a [Hint Mode] to disable all the instances
-that would have this behavior. *)
+that would have this behavior.
+
+In practice this means that usually only the default instance should use [MakeX],
+and most specialized instances should use [KnownMakeX]. *)
 From iris.bi Require Export bi.
 From iris.prelude Require Import options.
 
-- 
GitLab