diff --git a/CHANGELOG.md b/CHANGELOG.md
index 27839101b1bbed519bc9a24e7138ce005c2edf34..38dd45048df071d59cd47ad1dfc2fd85cfe23289 100644
--- a/CHANGELOG.md
+++ b/CHANGELOG.md
@@ -74,6 +74,14 @@ Coq 8.11 is no longer supported in this version of Iris.
 * `iMod`/`iModIntro` show proper error messages when they fail due to mask
   mismatches. To support this, the proofmode typeclass `FromModal` now takes an
   additional pure precondition.
+* Fix performance of `iFrame` in logics without `BiAffine`.
+  To adjust your code if you use such logics and define `Frame` instances,
+  ensure these instances to have priority at least 2: they should have either at
+  least 2 (non-dependent) premises, or an explicit priority.
+  References: docs for `frame_here_absorbing` in
+  [iris/proofmode/frame_instances.v](iris/proofmode/frame_instances.v) and
+  https://coq.inria.fr/refman/addendum/type-classes.html#coq:cmd.Instance. (by
+  Paolo G. Giarrusso, BedRock Systems)
 
 **Changes in `bi`:**
 
diff --git a/iris/bi/lib/fractional.v b/iris/bi/lib/fractional.v
index 5c33516a98db11e4b8d90888688e5fe7a953460e..05dee6eeab90b4479539ed5c8335e4a0431b4aec 100644
--- a/iris/bi/lib/fractional.v
+++ b/iris/bi/lib/fractional.v
@@ -181,7 +181,7 @@ Section fractional.
   Global Instance frame_fractional p R r Φ P q RES:
     AsFractional R Φ r → AsFractional P Φ q →
     FrameFractionalHyps p R Φ RES r q →
-    Frame p R P RES.
+    Frame p R P RES. (* No explicit priority, as default prio > [frame_here]'s 1. *)
   Proof.
     rewrite /Frame=>-[HR _][->?]H.
     revert H HR=>-[Q q0 q0' r0|Q q0 q0' r0|q0].
diff --git a/iris/program_logic/total_weakestpre.v b/iris/program_logic/total_weakestpre.v
index 3b8c9d06cb473f9984e3afd0b09f2be513e538a8..d33ca14ebff44e96878ee9d996b02897dfd87a2a 100644
--- a/iris/program_logic/total_weakestpre.v
+++ b/iris/program_logic/total_weakestpre.v
@@ -284,7 +284,7 @@ Section proofmode_classes.
 
   Global Instance frame_twp p s E e R Φ Ψ :
     (∀ v, Frame p R (Φ v) (Ψ v)) →
-    Frame p R (WP e @ s; E [{ Φ }]) (WP e @ s; E [{ Ψ }]).
+    Frame p R (WP e @ s; E [{ Φ }]) (WP e @ s; E [{ Ψ }]) | 2.
   Proof. rewrite /Frame=> HR. rewrite twp_frame_l. apply twp_mono, HR. Qed.
 
   Global Instance is_except_0_wp s E e Φ : IsExcept0 (WP e @ s; E [{ Φ }]).
diff --git a/iris/program_logic/weakestpre.v b/iris/program_logic/weakestpre.v
index 59fbded04904986bf8f6555e890d10384dec0bd0..22b5565f05e5d1b9de07ecb037563be7ff251386 100644
--- a/iris/program_logic/weakestpre.v
+++ b/iris/program_logic/weakestpre.v
@@ -366,7 +366,7 @@ Section proofmode_classes.
 
   Global Instance frame_wp p s E e R Φ Ψ :
     (∀ v, Frame p R (Φ v) (Ψ v)) →
-    Frame p R (WP e @ s; E {{ Φ }}) (WP e @ s; E {{ Ψ }}).
+    Frame p R (WP e @ s; E {{ Φ }}) (WP e @ s; E {{ Ψ }}) | 2.
   Proof. rewrite /Frame=> HR. rewrite wp_frame_l. apply wp_mono, HR. Qed.
 
   Global Instance is_except_0_wp s E e Φ : IsExcept0 (WP e @ s; E {{ Φ }}).
diff --git a/iris/proofmode/frame_instances.v b/iris/proofmode/frame_instances.v
index 178576f4dca3c98d5890d684fafe87134c9273ea..1f3408ff299ff733c7310ab081c756b8d573797a 100644
--- a/iris/proofmode/frame_instances.v
+++ b/iris/proofmode/frame_instances.v
@@ -19,6 +19,12 @@ Section bi.
 Context {PROP : bi}.
 Implicit Types P Q R : PROP.
 (* Frame *)
+(**
+When framing [R] against itself, we leave [True] if possible (via
+[frame_here_absorbing] or [frame_affinely_here_absorbing]) since it is a weaker
+goal. Otherwise we leave [emp] via [frame_here].
+Only if all those options fail, we start decomposing [R], via instances like
+[frame_exist]. To ensure that, all other instances must have priority > 1. *)
 Global Instance frame_here_absorbing p R : Absorbing R → Frame p R R True | 0.
 Proof. intros. by rewrite /Frame intuitionistically_if_elim sep_elim_l. Qed.
 Global Instance frame_here p R : Frame p R R emp | 1.
@@ -36,7 +42,7 @@ Proof.
 Qed.
 
 Global Instance frame_here_pure_persistent a φ Q :
-  FromPure a Q φ → Frame true ⌜φ⌝ Q emp.
+  FromPure a Q φ → Frame true ⌜φ⌝ Q emp | 2.
 Proof.
   rewrite /FromPure /Frame /= => <-. rewrite right_id.
   by rewrite -affinely_affinely_if intuitionistically_affinely.
@@ -44,7 +50,7 @@ Qed.
 Global Instance frame_here_pure a φ Q :
   FromPure a Q φ →
   TCOr (TCEq a false) (BiAffine PROP) →
-  Frame false ⌜φ⌝ Q emp.
+  Frame false ⌜φ⌝ Q emp | 2. (* Same prio as default. *)
 Proof.
   rewrite /FromPure /Frame => <- [->|?] /=.
   - by rewrite right_id.
@@ -62,13 +68,15 @@ Global Instance make_embed_default `{BiEmbed PROP PROP'} P :
 Proof. by rewrite /MakeEmbed. Qed.
 
 Global Instance frame_embed `{BiEmbed PROP PROP'} p P Q (Q' : PROP') R :
-  Frame p R P Q → MakeEmbed Q Q' → Frame p ⎡R⎤ ⎡P⎤ Q'.
+  Frame p R P Q → MakeEmbed Q Q' →
+  Frame p ⎡R⎤ ⎡P⎤ Q' | 2. (* Same prio as default. *)
 Proof.
   rewrite /Frame /MakeEmbed => <- <-.
   rewrite embed_sep embed_intuitionistically_if_2 => //.
 Qed.
 Global Instance frame_pure_embed `{BiEmbed PROP PROP'} p P Q (Q' : PROP') φ :
-  Frame p ⌜φ⌝ P Q → MakeEmbed Q Q' → Frame p ⌜φ⌝ ⎡P⎤ Q'.
+  Frame p ⌜φ⌝ P Q → MakeEmbed Q Q' →
+  Frame p ⌜φ⌝ ⎡P⎤ Q' | 2. (* Same prio as default. *)
 Proof. rewrite /Frame /MakeEmbed -embed_pure. apply (frame_embed p P Q). Qed.
 
 Global Instance make_sep_emp_l P : KnownLMakeSep emp P P.
@@ -102,20 +110,20 @@ Qed.
 Global Instance frame_big_sepL_cons {A} p (Φ : nat → A → PROP) R Q l x l' :
   IsCons l x l' →
   Frame p R (Φ 0 x ∗ [∗ list] k ↦ y ∈ l', Φ (S k) y) Q →
-  Frame p R ([∗ list] k ↦ y ∈ l, Φ k y) Q.
+  Frame p R ([∗ list] k ↦ y ∈ l, Φ k y) Q | 2. (* Same prio as default. *)
 Proof. rewrite /IsCons=>->. by rewrite /Frame big_sepL_cons. Qed.
 Global Instance frame_big_sepL_app {A} p (Φ : nat → A → PROP) R Q l l1 l2 :
   IsApp l l1 l2 →
   Frame p R (([∗ list] k ↦ y ∈ l1, Φ k y) ∗
            [∗ list] k ↦ y ∈ l2, Φ (length l1 + k) y) Q →
-  Frame p R ([∗ list] k ↦ y ∈ l, Φ k y) Q.
+  Frame p R ([∗ list] k ↦ y ∈ l, Φ k y) Q | 2. (* Same prio as default. *)
 Proof. rewrite /IsApp=>->. by rewrite /Frame big_sepL_app. Qed.
 
 Global Instance frame_big_sepL2_cons {A B} p (Φ : nat → A → B → PROP)
     R Q l1 x1 l1' l2 x2 l2' :
   IsCons l1 x1 l1' → IsCons l2 x2 l2' →
   Frame p R (Φ 0 x1 x2 ∗ [∗ list] k ↦ y1;y2 ∈ l1';l2', Φ (S k) y1 y2) Q →
-  Frame p R ([∗ list] k ↦ y1;y2 ∈ l1;l2, Φ k y1 y2) Q.
+  Frame p R ([∗ list] k ↦ y1;y2 ∈ l1;l2, Φ k y1 y2) Q. (* Default prio > 1. *)
 Proof. rewrite /IsCons=>-> ->. by rewrite /Frame big_sepL2_cons. Qed.
 Global Instance frame_big_sepL2_app {A B} p (Φ : nat → A → B → PROP)
     R Q l1 l1' l1'' l2 l2' l2'' :
@@ -127,7 +135,7 @@ Proof. rewrite /IsApp /Frame=>-> -> ->. apply wand_elim_l', big_sepL2_app. Qed.
 
 Global Instance frame_big_sepMS_disj_union `{Countable A} p (Φ : A → PROP) R Q X1 X2 :
   Frame p R (([∗ mset] y ∈ X1, Φ y) ∗ [∗ mset] y ∈ X2, Φ y) Q →
-  Frame p R ([∗ mset] y ∈ X1 ⊎ X2, Φ y) Q.
+  Frame p R ([∗ mset] y ∈ X1 ⊎ X2, Φ y) Q | 2.
 Proof. by rewrite /Frame big_sepMS_disj_union. Qed.
 
 Global Instance make_and_true_l P : KnownLMakeAnd True P P.
@@ -192,7 +200,7 @@ Global Instance frame_or_persistent progress1 progress2 R P1 P2 Q1 Q2 Q :
 Proof. rewrite /Frame /MakeOr => <- <- _ <-. by rewrite -sep_or_l. Qed.
 
 Global Instance frame_wand p R P1 P2 Q2 :
-  Frame p R P2 Q2 → Frame p R (P1 -∗ P2) (P1 -∗ Q2).
+  Frame p R P2 Q2 → Frame p R (P1 -∗ P2) (P1 -∗ Q2) | 2.
 Proof.
   rewrite /Frame=> ?. apply wand_intro_l.
   by rewrite assoc (comm _ P1) -assoc wand_elim_r.
@@ -207,7 +215,8 @@ Proof. by rewrite /MakeAffinely. Qed.
 
 Global Instance frame_affinely p R P Q Q' :
   TCOr (TCEq p true) (Affine R) →
-  Frame p R P Q → MakeAffinely Q Q' → Frame p R (<affine> P) Q'.
+  Frame p R P Q → MakeAffinely Q Q' →
+  Frame p R (<affine> P) Q'. (* Default prio > 1 *)
 Proof.
   rewrite /Frame /MakeAffinely=> -[->|?] <- <- /=;
     by rewrite -{1}(affine_affinely (_ R)) affinely_sep_2.
@@ -230,7 +239,8 @@ Global Instance make_intuitionistically_default P :
 Proof. by rewrite /MakeIntuitionistically. Qed.
 
 Global Instance frame_intuitionistically R P Q Q' :
-  Frame true R P Q → MakeIntuitionistically Q Q' → Frame true R (□ P) Q'.
+  Frame true R P Q → MakeIntuitionistically Q Q' →
+  Frame true R (â–¡ P) Q' | 2. (* Same prio as default. *)
 Proof.
   rewrite /Frame /MakeIntuitionistically=> <- <- /=.
   rewrite -intuitionistically_sep_2 intuitionistically_idemp //.
@@ -247,7 +257,8 @@ Global Instance make_absorbingly_default P : MakeAbsorbingly P (<absorb> P) | 10
 Proof. by rewrite /MakeAbsorbingly. Qed.
 
 Global Instance frame_absorbingly p R P Q Q' :
-  Frame p R P Q → MakeAbsorbingly Q Q' → Frame p R (<absorb> P) Q'.
+  Frame p R P Q → MakeAbsorbingly Q Q' →
+  Frame p R (<absorb> P) Q' | 2. (* Same prio as default. *)
 Proof.
   rewrite /Frame /MakeAbsorbingly=> <- <- /=. by rewrite absorbingly_sep_r.
 Qed.
@@ -264,7 +275,8 @@ Global Instance make_persistently_default P :
 Proof. by rewrite /MakePersistently. Qed.
 
 Global Instance frame_persistently R P Q Q' :
-  Frame true R P Q → MakePersistently Q Q' → Frame true R (<pers> P) Q'.
+  Frame true R P Q → MakePersistently Q Q' →
+  Frame true R (<pers> P) Q' | 2. (* Same prio as default. *)
 Proof.
   rewrite /Frame /MakePersistently=> <- <- /=.
   rewrite -persistently_and_intuitionistically_sep_l.
@@ -273,20 +285,20 @@ Proof.
 Qed.
 
 Global Instance frame_exist {A} p R (Φ Ψ : A → PROP) :
-  (∀ a, Frame p R (Φ a) (Ψ a)) → Frame p R (∃ x, Φ x) (∃ x, Ψ x).
+  (∀ a, Frame p R (Φ a) (Ψ a)) → Frame p R (∃ x, Φ x) (∃ x, Ψ x) | 2.
 Proof. rewrite /Frame=> ?. by rewrite sep_exist_l; apply exist_mono. Qed.
 Global Instance frame_texist {TT : tele} p R (Φ Ψ : TT → PROP) :
-  (∀ x, Frame p R (Φ x) (Ψ x)) → Frame p R (∃.. x, Φ x) (∃.. x, Ψ x).
+  (∀ x, Frame p R (Φ x) (Ψ x)) → Frame p R (∃.. x, Φ x) (∃.. x, Ψ x) | 2.
 Proof. rewrite /Frame !bi_texist_exist. apply frame_exist. Qed.
 Global Instance frame_forall {A} p R (Φ Ψ : A → PROP) :
-  (∀ a, Frame p R (Φ a) (Ψ a)) → Frame p R (∀ x, Φ x) (∀ x, Ψ x).
+  (∀ a, Frame p R (Φ a) (Ψ a)) → Frame p R (∀ x, Φ x) (∀ x, Ψ x) | 2.
 Proof. rewrite /Frame=> ?. by rewrite sep_forall_l; apply forall_mono. Qed.
 Global Instance frame_tforall {TT : tele} p R (Φ Ψ : TT → PROP) :
-  (∀ x, Frame p R (Φ x) (Ψ x)) → Frame p R (∀.. x, Φ x) (∀.. x, Ψ x).
+  (∀ x, Frame p R (Φ x) (Ψ x)) → Frame p R (∀.. x, Φ x) (∀.. x, Ψ x) | 2.
 Proof. rewrite /Frame !bi_tforall_forall. apply frame_forall. Qed.
 
 Global Instance frame_impl_persistent R P1 P2 Q2 :
-  Frame true R P2 Q2 → Frame true R (P1 → P2) (P1 → Q2).
+  Frame true R P2 Q2 → Frame true R (P1 → P2) (P1 → Q2) | 2.
 Proof.
   rewrite /Frame /= => ?. apply impl_intro_l.
   by rewrite -persistently_and_intuitionistically_sep_l assoc (comm _ P1) -assoc impl_elim_r
@@ -294,7 +306,7 @@ Proof.
 Qed.
 Global Instance frame_impl R P1 P2 Q2 :
   Persistent P1 → Absorbing P1 →
-  Frame false R P2 Q2 → Frame false R (P1 → P2) (P1 → Q2).
+  Frame false R P2 Q2 → Frame false R (P1 → P2) (P1 → Q2). (* Default prio > 1 *)
 Proof.
   rewrite /Frame /==> ???. apply impl_intro_l.
   rewrite {1}(persistent P1) persistently_and_intuitionistically_sep_l assoc.
@@ -305,7 +317,8 @@ Qed.
 Global Instance frame_eq_embed `{!BiEmbed PROP PROP', !BiInternalEq PROP,
     !BiInternalEq PROP', !BiEmbedInternalEq PROP PROP'}
     p P Q (Q' : PROP') {A : ofe} (a b : A) :
-  Frame p (a ≡ b) P Q → MakeEmbed Q Q' → Frame p (a ≡ b) ⎡P⎤ Q'.
+  Frame p (a ≡ b) P Q → MakeEmbed Q Q' →
+  Frame p (a ≡ b) ⎡P⎤ Q'. (* Default prio > 1 *)
 Proof. rewrite /Frame /MakeEmbed -embed_internal_eq. apply (frame_embed p P Q). Qed.
 
 Global Instance make_laterN_true n : @KnownMakeLaterN PROP n True True | 0.
@@ -318,24 +331,26 @@ Proof. by rewrite /MakeLaterN. Qed.
 
 Global Instance frame_later p R R' P Q Q' :
   TCNoBackTrack (MaybeIntoLaterN true 1 R' R) →
-  Frame p R P Q → MakeLaterN 1 Q Q' → Frame p R' (▷ P) Q'.
+  Frame p R P Q → MakeLaterN 1 Q Q' →
+  Frame p R' (â–· P) Q'. (* Default prio > 1 *)
 Proof.
   rewrite /Frame /MakeLaterN /MaybeIntoLaterN=>-[->] <- <-.
   by rewrite later_intuitionistically_if_2 later_sep.
 Qed.
 Global Instance frame_laterN p n R R' P Q Q' :
   TCNoBackTrack (MaybeIntoLaterN true n R' R) →
-  Frame p R P Q → MakeLaterN n Q Q' → Frame p R' (▷^n P) Q'.
+  Frame p R P Q → MakeLaterN n Q Q' →
+  Frame p R' (â–·^n P) Q'. (* Default prio > 1 *)
 Proof.
   rewrite /Frame /MakeLaterN /MaybeIntoLaterN=>-[->] <- <-.
   by rewrite laterN_intuitionistically_if_2 laterN_sep.
 Qed.
 
 Global Instance frame_bupd `{BiBUpd PROP} p R P Q :
-  Frame p R P Q → Frame p R (|==> P) (|==> Q).
+  Frame p R P Q → Frame p R (|==> P) (|==> Q) | 2.
 Proof. rewrite /Frame=><-. by rewrite bupd_frame_l. Qed.
 Global Instance frame_fupd `{BiFUpd PROP} p E1 E2 R P Q :
-  Frame p R P Q → Frame p R (|={E1,E2}=> P) (|={E1,E2}=> Q).
+  Frame p R P Q → Frame p R (|={E1,E2}=> P) (|={E1,E2}=> Q) | 2.
 Proof. rewrite /Frame=><-. by rewrite fupd_frame_l. Qed.
 
 Global Instance make_except_0_True : @KnownMakeExcept0 PROP True True.
@@ -344,7 +359,8 @@ Global Instance make_except_0_default P : MakeExcept0 P (â—‡ P) | 100.
 Proof. by rewrite /MakeExcept0. Qed.
 
 Global Instance frame_except_0 p R P Q Q' :
-  Frame p R P Q → MakeExcept0 Q Q' → Frame p R (◇ P) Q'.
+  Frame p R P Q → MakeExcept0 Q Q' →
+  Frame p R (â—‡ P) Q' | 2. (* Same prio as default *)
 Proof.
   rewrite /Frame /MakeExcept0=><- <-.
   by rewrite except_0_sep -(except_0_intro (â–¡?p R)).
diff --git a/iris/proofmode/monpred.v b/iris/proofmode/monpred.v
index 7073ed8d2c779a779b7fc6e3f050052de1b8b651..bc90575eda6adfe2ba37f35821893d96164c7649 100644
--- a/iris/proofmode/monpred.v
+++ b/iris/proofmode/monpred.v
@@ -364,7 +364,7 @@ Qed.
 
 (* Framing. *)
 Global Instance frame_monPred_at_enter p i 𝓡 P 𝓠 :
-  FrameMonPredAt p i 𝓡 P 𝓠 → Frame p 𝓡 (P i) 𝓠.
+  FrameMonPredAt p i 𝓡 P 𝓠 → Frame p 𝓡 (P i) 𝓠 | 2.
 Proof. intros. done. Qed.
 Global Instance frame_monPred_at_here p P i j :
   IsBiIndexRel i j → FrameMonPredAt p j (P i) P emp | 0.
diff --git a/iris_heap_lang/derived_laws.v b/iris_heap_lang/derived_laws.v
index 66a870aa54a5a58768076e1893e79d0c5b267c44..f1627aa097c34f03a16de836f2b744bb6055d692 100644
--- a/iris_heap_lang/derived_laws.v
+++ b/iris_heap_lang/derived_laws.v
@@ -73,7 +73,7 @@ Qed.
 
 Global Instance array_cons_frame l dq v vs R Q :
   Frame false R (l ↦{dq} v ∗ (l +ₗ 1) ↦∗{dq} vs) Q →
-  Frame false R (l ↦∗{dq} (v :: vs)) Q.
+  Frame false R (l ↦∗{dq} (v :: vs)) Q | 2.
 Proof. by rewrite /Frame array_cons. Qed.
 
 Lemma update_array l dq vs off v :