better error when iMod fails due to mask mismatch

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.

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.

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 :=

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

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}.