avoid MakeIntuitionistically turning a True into emp for affine BI

iris/proofmode/class_instances_make.v

@@ -138,8 +138,17 @@ Proof.
   by rewrite /KnownMakeIntuitionistically /MakeIntuitionistically
     intuitionistically_emp.
 Qed.
+(** For affine BIs, we would prefer [□ True] to become [True] rather than [emp],
+so we have this instance with lower cost than the next. *)
+Global Instance make_intuitionistically_True_affine :
+  BiAffine PROP →
+  @KnownMakeIntuitionistically PROP True True | 0.
+Proof.
+  intros. rewrite /KnownMakeIntuitionistically /MakeIntuitionistically
+    intuitionistically_True_emp True_emp //.
+Qed.
 Global Instance make_intuitionistically_True :
-  @KnownMakeIntuitionistically PROP True emp | 0.
+  @KnownMakeIntuitionistically PROP True emp | 1.
 Proof.
   by rewrite /KnownMakeIntuitionistically /MakeIntuitionistically
     intuitionistically_True_emp.

tests/proofmode.ref

@@ -503,9 +503,9 @@ No applicable tactic.
 1 goal
   
   PROP : bi
-  H : BiAffine PROP
+  BiAffine0 : BiAffine PROP
   P, Q : PROP
-  H0 : Laterable Q
+  H : Laterable Q
   ============================
   "HP" : ▷ P
   "HQ" : Q
@@ -534,6 +534,17 @@ No applicable tactic.
   "H" : ⌜φ⌝ -∗ P
   --------------------------------------∗
   ⌜φ⌝ -∗ P
+"test_iFrame_not_add_emp_for_intuitionistically"
+     : string
+1 goal
+  
+  PROP : bi
+  BiAffine0 : BiAffine PROP
+  P : PROP
+  ============================
+  "H" : P
+  --------------------------------------□
+  ∃ _ : nat, True
 "elim_mod_accessor"
      : string
 1 goal

tests/proofmode.v

@@ -1261,7 +1261,7 @@ Proof.
   iIntros "[P _]". done.
 Qed.
 
-Lemma test_iModIntro_make_laterable `{BiAffine PROP} (P Q : PROP) :
+Lemma test_iModIntro_make_laterable `{!BiAffine PROP} (P Q : PROP) :
   Laterable Q →
   P -∗ Q -∗ make_laterable (▷ P ∗ Q).
 Proof.
@@ -1284,6 +1284,13 @@ Proof.
   iIntros (Hφ) "H". iRevert (Hφ). Show. done.
 Qed.
 
+(* Check that when framing things under the □ modality, we do not add [emp] in
+affine BIs. *)
+Check "test_iFrame_not_add_emp_for_intuitionistically".
+Lemma test_iFrame_not_add_emp_for_intuitionistically `{!BiAffine PROP} (P : PROP) :
+  □ P -∗ ∃ _ : nat, □ P.
+Proof. iIntros "#H". iFrame "H". Show. by iExists 0. Qed.
+
 End tests.
 
 Section parsing_tests.