From fd24345005953bc42fd9b8ff6af75900829d6d90 Mon Sep 17 00:00:00 2001
From: Ralf Jung <jung@mpi-sws.org>
Date: Tue, 25 May 2021 15:02:12 +0200
Subject: [PATCH] better error when iMod fails due to mask mismatch

---
 iris/proofmode/class_instances_updates.v |  7 +++++++
 iris/proofmode/classes.v                 |  5 +++++
 iris/proofmode/ltac_tactics.v            |  5 ++++-
 tests/proofmode.ref                      | 10 ++++++++++
 tests/proofmode.v                        | 15 +++++++++------
 5 files changed, 35 insertions(+), 7 deletions(-)

diff --git a/iris/proofmode/class_instances_updates.v b/iris/proofmode/class_instances_updates.v
index b0ab10ecc..e0f110a4f 100644
--- a/iris/proofmode/class_instances_updates.v
+++ b/iris/proofmode/class_instances_updates.v
@@ -161,6 +161,13 @@ Proof.
   by rewrite /ElimModal intuitionistically_if_elim
     fupd_frame_r wand_elim_r fupd_trans.
 Qed.
+Global Instance elim_modal_fupd_fupd_wrong_mask `{!BiFUpd PROP} p E0 E1 E2 E3 P Q :
+  ElimModal
+    (pm_error "Goal and eliminated modality must have the same mask.
+Use [iMod (fupd_mask_subseteq E2)] to adjust the mask of your goal to [E2]")
+    p false
+    (|={E1,E2}=> P) False (|={E0,E3}=> Q) False | 100.
+Proof. intros []. Qed.
 
 Global Instance add_modal_bupd `{!BiBUpd PROP} P Q : AddModal (|==> P) P (|==> Q).
 Proof. by rewrite /AddModal bupd_frame_r wand_elim_r bupd_trans. Qed.
diff --git a/iris/proofmode/classes.v b/iris/proofmode/classes.v
index 5e4a5e981..3b8ce451f 100644
--- a/iris/proofmode/classes.v
+++ b/iris/proofmode/classes.v
@@ -5,6 +5,11 @@ From iris.proofmode Require Export ident_name modalities.
 From iris.prelude Require Import options.
 Import bi.
 
+(** Use this as precondition on "failing" instances of typeclasses that have
+pure preconditions (such as [ElimModal]), if you want a nice error to be shown
+when this instances is picked as part of some proof mode tactic. *)
+Definition pm_error (s : string) := False.
+
 Class FromAssumption {PROP : bi} (p : bool) (P Q : PROP) :=
   from_assumption : □?p P ⊢ Q.
 Global Arguments FromAssumption {_} _ _%I _%I : simpl never.
diff --git a/iris/proofmode/ltac_tactics.v b/iris/proofmode/ltac_tactics.v
index 5aa750a9e..275e549f5 100644
--- a/iris/proofmode/ltac_tactics.v
+++ b/iris/proofmode/ltac_tactics.v
@@ -28,7 +28,10 @@ Ltac iSolveTC :=
 (** Tactic used for solving side-conditions arising from TC resolution in [iMod]
 and [iInv]. *)
 Ltac iSolveSideCondition :=
-  split_and?; try solve [ fast_done | solve_ndisj | iSolveTC ].
+  lazymatch goal with
+  | |- pm_error ?err => fail "" err
+  | _ => split_and?; try solve [ fast_done | solve_ndisj | iSolveTC ]
+  end.
 
 (** Used for printing [string]s and [ident]s. *)
 Ltac pretty_ident H :=
diff --git a/tests/proofmode.ref b/tests/proofmode.ref
index f273b13bb..32acfe20d 100644
--- a/tests/proofmode.ref
+++ b/tests/proofmode.ref
@@ -707,6 +707,16 @@ Tactic failure: iRevert: k is used in hypothesis "Hk".
      : string
 The command has indeed failed with message:
 Tactic failure: iLöb: no 'BiLöb' instance found.
+"iMod_mask_mismatch"
+     : string
+The command has indeed failed with message:
+Tactic failure: 
+"Goal and eliminated modality must have the same mask.
+Use [iMod (fupd_mask_subseteq E2)] to adjust the mask of your goal to [E2]".
+The command has indeed failed with message:
+Tactic failure: 
+"Goal and eliminated modality must have the same mask.
+Use [iMod (fupd_mask_subseteq E2)] to adjust the mask of your goal to [E2]".
 "test_pure_name"
      : string
 1 goal
diff --git a/tests/proofmode.v b/tests/proofmode.v
index 9d5336d56..27ad69efc 100644
--- a/tests/proofmode.v
+++ b/tests/proofmode.v
@@ -1389,16 +1389,19 @@ Proof. intros Hk. Fail iRevert (k). Abort.
 Check "iRevert_dep_var".
 Lemma iRevert_dep_var (k : nat) (Φ : nat → PROP) : Φ k -∗ Φ (S k).
 Proof. iIntros "Hk". Fail iRevert (k). Abort.
-End error_tests.
-
-Section error_tests_bi.
-Context {PROP : bi}.
-Implicit Types P Q R : PROP.
 
 Check "iLöb_no_BiLöb".
 Lemma iLöb_no_BiLöb P : ⊢ P.
 Proof. Fail iLöb as "IH". Abort.
-End error_tests_bi.
+
+Check "iMod_mask_mismatch".
+Lemma iMod_mask_mismatch `{!BiFUpd PROP} E1 E2 (P : PROP) :
+  (|={E2}=> P) ⊢ |={E1}=> P.
+Proof.
+  Fail iIntros ">HP".
+  iIntros "HP". Fail iMod "HP".
+Abort.
+End error_tests.
 
 Section pure_name_tests.
 Context {PROP : bi}.
-- 
GitLab