diff --git a/iris/bi/derived_connectives.v b/iris/bi/derived_connectives.v
index c912772eff1b2706b862c3323efcebe1e5b8fefb..959e3c27087b8cc0631a9129ea3edd22cabeed71 100644
--- a/iris/bi/derived_connectives.v
+++ b/iris/bi/derived_connectives.v
@@ -86,16 +86,7 @@ The class of [Separable] propositions is useful for BIs with a degenerative
 persistence modality, i.e., without [BiPersistentlyTrue : True ⊢ <pers> True],
 see https://gitlab.mpi-sws.org/iris/iris/-/merge_requests/843. For those BIs,
 the only persistent proposition is [False], but emp/plain and friends are still
-[Separable].
-
-We do not provide instances that close [Separable] under the BI connectives, we
-only provide the following instances:
-
-- [pure_separable : Separable ⌜φ⌝]
-- [persistent_separable P : Persistent P → Separable P]
-- [plain_separable P : Plain P → Separable P], necessary because
-  [plain_persistent : Plain P → Persistent P] is not an instance, but a
-  [Hint Immediate]. *)
+[Separable]. *)
 Class Separable {PROP : bi} (P : PROP) :=
   separable Q : <absorb> P ∧ Q ⊢ <affine> P ∗ Q.
 Global Arguments Separable {_} _%I : simpl never.
diff --git a/iris/bi/derived_laws.v b/iris/bi/derived_laws.v
index e44e518a46fadddd9139df2067bf3e354905705e..bddb71c556dab4252c2d1491b2e517fdf4cff45f 100644
--- a/iris/bi/derived_laws.v
+++ b/iris/bi/derived_laws.v
@@ -951,18 +951,21 @@ Proof.
   intros ?? Q. rewrite absorbingly_or affinely_or.
   by rewrite and_or_r sep_or_r 2!separable.
 Qed.
-Global Instance affinely_separable P : Separable P → Separable (<affine> P).
-Proof. rewrite /bi_affinely. apply _. Qed.
 Global Instance sep_separable P1 P2 :
   Separable P1 → Separable P2 → Separable (P1 ∗ P2).
 Proof.
   intros ?? Q. rewrite absorbingly_sep sep_and -assoc 2!separable assoc.
   by rewrite affinely_sep_2.
 Qed.
+Global Instance affinely_separable P : Separable P → Separable (<affine> P).
+Proof. rewrite /bi_affinely. apply _. Qed.
 Global Instance absorbingly_separable P : Separable P → Separable (<absorb> P).
 Proof.
   intros ? Q. by rewrite absorbingly_idemp separable -absorbingly_intro.
 Qed.
+Global Instance from_option_separable {A} P (Ψ : A → PROP) (mx : option A) :
+  (∀ x, Separable (Ψ x)) → Separable P → Separable (from_option Ψ P mx).
+Proof. destruct mx; apply _. Qed.
 
 (* Pure stuff *)
 Lemma pure_elim φ Q R : (Q ⊢ ⌜φ⌝) → (φ → Q ⊢ R) → Q ⊢ R.
@@ -1139,7 +1142,9 @@ Proof.
   apply persistently_and_sep_elim.
 Qed.
 
-Global Instance persistent_separable P : Persistent P → Separable P.
+(** High cost, should only be used if no other [Separable] instances can be
+applied *)
+Global Instance persistent_separable P : Persistent P → Separable P | 100.
 Proof.
   rewrite /Persistent /Separable=> HP Q.
   by rewrite {1}HP absorbingly_elim_persistently persistently_and_sep_elim_emp.
@@ -1264,39 +1269,45 @@ End persistently_affine_bi.
 (* Persistence instances *)
 Global Instance pure_persistent φ : Persistent (PROP:=PROP) ⌜φ⌝.
 Proof. by rewrite /Persistent persistently_pure. Qed.
+Global Hint Cut [_* persistent_separable pure_persistent] : typeclass_instances.
 Global Instance emp_persistent : Persistent (PROP:=PROP) emp.
 Proof. rewrite /Persistent. apply persistently_emp_intro. Qed.
+Global Hint Cut [_* persistent_separable emp_persistent] : typeclass_instances.
 Global Instance and_persistent P Q :
   Persistent P → Persistent Q → Persistent (P ∧ Q).
 Proof. intros. by rewrite /Persistent persistently_and -!persistent. Qed.
+Global Hint Cut [_* persistent_separable and_persistent] : typeclass_instances.
 Global Instance or_persistent P Q :
   Persistent P → Persistent Q → Persistent (P ∨ Q).
 Proof. intros. by rewrite /Persistent persistently_or -!persistent. Qed.
+Global Hint Cut [_* persistent_separable or_persistent] : typeclass_instances.
 Global Instance forall_persistent `{!BiPersistentlyForall PROP} {A} (Ψ : A → PROP) :
   (∀ x, Persistent (Ψ x)) → Persistent (∀ x, Ψ x).
 Proof.
   intros. rewrite /Persistent persistently_forall.
   apply forall_mono=> x. by rewrite -!persistent.
 Qed.
+(** No [Hint Cut] because [Separable] is not closed under [∀]. *)
 Global Instance exist_persistent {A} (Ψ : A → PROP) :
   (∀ x, Persistent (Ψ x)) → Persistent (∃ x, Ψ x).
 Proof.
   intros. rewrite /Persistent persistently_exist.
   apply exist_mono=> x. by rewrite -!persistent.
 Qed.
-
+Global Hint Cut [_* persistent_separable exist_persistent] : typeclass_instances.
 Global Instance sep_persistent P Q :
   Persistent P → Persistent Q → Persistent (P ∗ Q).
 Proof. intros. by rewrite /Persistent -persistently_sep_2 -!persistent. Qed.
-
 Global Instance affinely_persistent P : Persistent P → Persistent (<affine> P).
 Proof. rewrite /bi_affinely. apply _. Qed.
-
+Global Hint Cut [_* persistent_separable affinely_persistent] : typeclass_instances.
 Global Instance absorbingly_persistent P : Persistent P → Persistent (<absorb> P).
 Proof. rewrite /bi_absorbingly. apply _. Qed.
+Global Hint Cut [_* persistent_separable absorbingly_persistent] : typeclass_instances.
 Global Instance from_option_persistent {A} P (Ψ : A → PROP) (mx : option A) :
   (∀ x, Persistent (Ψ x)) → Persistent P → Persistent (from_option Ψ P mx).
 Proof. destruct mx; apply _. Qed.
+Global Hint Cut [_* persistent_separable from_option_persistent] : typeclass_instances.
 
 (* The intuitionistic modality *)
 Global Instance intuitionistically_ne : NonExpansive (@bi_intuitionistically PROP).
diff --git a/iris/bi/internal_eq.v b/iris/bi/internal_eq.v
index 4f19ba89b2ab0b0ee64c956983fa1f5874a50418..29ba50fe8899475330d486a8f7ae577a8c30ac42 100644
--- a/iris/bi/internal_eq.v
+++ b/iris/bi/internal_eq.v
@@ -229,6 +229,7 @@ Section internal_eq_derived.
   Global Instance internal_eq_persistent {A : ofe} (a b : A) :
     Persistent (PROP:=PROP) (a ≡ b).
   Proof. by intros; rewrite /Persistent persistently_internal_eq. Qed.
+  Global Hint Cut [persistent_separable internal_eq_persistent] : typeclasses_instances.
 
   Global Instance internal_eq_separable {A : ofe} (a b : A) :
     Separable (PROP:=PROP) (a ≡ b).
diff --git a/iris/bi/plainly.v b/iris/bi/plainly.v
index f91d9ffdead1749ac104d88953d374a5748dcaf5..9e9c7ffb3a5cba07a7e4b7f35c16064c5063628d 100644
--- a/iris/bi/plainly.v
+++ b/iris/bi/plainly.v
@@ -373,7 +373,9 @@ Section plainly_derived.
   Lemma plain_persistent P : Plain P → Persistent P.
   Proof. intros. by rewrite /Persistent -plainly_elim_persistently. Qed.
 
-  Global Instance plain_separable P : Plain P → Separable P.
+  (** High cost, should only be used if no other [Separable] instances can be
+  applied *)
+  Global Instance plain_separable P : Plain P → Separable P | 100.
   Proof. intros. by apply persistent_separable, plain_persistent. Qed.
 
   Global Instance impl_persistent `{!BiPersistentlyImplPlainly PROP} P Q :
@@ -452,30 +454,40 @@ Section plainly_derived.
   Proof. apply (big_opMS_commute _). Qed.
 
   (* Plainness instances *)
+  Global Instance plainly_plain P : Plain (â–  P).
+  Proof. by rewrite /Plain plainly_idemp. Qed.
+
   Global Instance pure_plain φ : Plain (PROP:=PROP) ⌜φ⌝.
   Proof. by rewrite /Plain plainly_pure. Qed.
+  Global Hint Cut [_* plain_separable pure_plain] : typeclass_instances.
   Global Instance emp_plain : Plain (PROP:=PROP) emp.
   Proof. apply plainly_emp_intro. Qed.
+  Global Hint Cut [_* plain_separable emp_plain] : typeclass_instances.
   Global Instance and_plain P Q : Plain P → Plain Q → Plain (P ∧ Q).
   Proof. intros. by rewrite /Plain plainly_and -!plain. Qed.
+  Global Hint Cut [_* plain_separable and_plain] : typeclass_instances.
   Global Instance or_plain P Q : Plain P → Plain Q → Plain (P ∨ Q).
   Proof. intros. by rewrite /Plain -plainly_or_2 -!plain. Qed.
+  Global Hint Cut [_* plain_separable or_plain] : typeclass_instances.
   Global Instance forall_plain {A} (Ψ : A → PROP) :
     (∀ x, Plain (Ψ x)) → Plain (∀ x, Ψ x).
   Proof.
     intros. rewrite /Plain plainly_forall. apply forall_mono=> x. by rewrite -plain.
   Qed.
+  (** No [Hint Cut] because [Separable] is not closed under ∀. *)
   Global Instance exist_plain {A} (Ψ : A → PROP) :
     (∀ x, Plain (Ψ x)) → Plain (∃ x, Ψ x).
   Proof.
     intros. rewrite /Plain -plainly_exist_2. apply exist_mono=> x. by rewrite -plain.
   Qed.
+  Global Hint Cut [_* plain_separable exist_plain] : typeclass_instances.
 
   Global Instance impl_plain P Q : Absorbing P → Plain P → Plain Q → Plain (P → Q).
   Proof.
     intros. by rewrite /Plain {2}(plain P) -plainly_impl_plainly -(plain Q)
                        (plainly_into_absorbingly P) absorbing.
   Qed.
+  (** No [Hint Cut] because [Separable] is not closed under [→]. *)
   Global Instance wand_plain P Q :
     Plain P → Plain Q → Absorbing Q → Plain (P -∗ Q).
   Proof.
@@ -484,24 +496,29 @@ Section plainly_derived.
       by rewrite affinely_plainly_elim.
     - apply plainly_mono, wand_intro_l. by rewrite sep_and impl_elim_r.
   Qed.
+  (** No [Hint Cut] because [Separable] is not closed under [-∗]. *)
   Global Instance sep_plain P Q : Plain P → Plain Q → Plain (P ∗ Q).
   Proof. intros. by rewrite /Plain -plainly_sep_2 -!plain. Qed.
+  Global Hint Cut [_* plain_separable sep_plain] : typeclass_instances.
 
-  Global Instance plainly_plain P : Plain (â–  P).
-  Proof. by rewrite /Plain plainly_idemp. Qed.
   Global Instance persistently_plain P : Plain P → Plain (<pers> P).
   Proof.
     rewrite /Plain=> HP. rewrite {1}HP plainly_persistently_elim persistently_elim_plainly //.
   Qed.
+  Global Hint Cut [_* plain_separable persistently_plain] : typeclass_instances.
   Global Instance affinely_plain P : Plain P → Plain (<affine> P).
   Proof. rewrite /bi_affinely. apply _. Qed.
+  Global Hint Cut [_* plain_separable affinely_plain] : typeclass_instances.
   Global Instance intuitionistically_plain P : Plain P → Plain (□ P).
   Proof. rewrite /bi_intuitionistically. apply _. Qed.
+  Global Hint Cut [_* plain_separable intuitionistically_plain] : typeclass_instances.
   Global Instance absorbingly_plain P : Plain P → Plain (<absorb> P).
   Proof. rewrite /bi_absorbingly. apply _. Qed.
+  Global Hint Cut [_* plain_separable absorbingly_plain] : typeclass_instances.
   Global Instance from_option_plain {A} P (Ψ : A → PROP) (mx : option A) :
     (∀ x, Plain (Ψ x)) → Plain P → Plain (from_option Ψ P mx).
   Proof. destruct mx; apply _. Qed.
+  Global Hint Cut [_* plain_separable from_option_plain] : typeclass_instances.
 
   Global Instance big_sepL_nil_plain `{!BiAffine PROP} {A} (Φ : nat → A → PROP) :
     Plain ([∗ list] k↦x ∈ [], Φ k x).
@@ -591,6 +608,7 @@ Section plainly_derived.
     Global Instance internal_eq_plain {A : ofe} (a b : A) :
       Plain (PROP:=PROP) (a ≡ b).
     Proof. by intros; rewrite /Plain plainly_internal_eq. Qed.
+    Global Hint Cut [plain_separable internal_eq_plain] : typeclass_instances.
   End internal_eq.
 
   Section prop_ext.
diff --git a/tests/bi.ref b/tests/bi.ref
index 27b5cb7da314682827854e7c3ab45e03ea45a9bb..e8fadfb33daa6873da5a4f3f91a562a146713e1e 100644
--- a/tests/bi.ref
+++ b/tests/bi.ref
@@ -20,3 +20,72 @@ P : PROP
 
 ?p : "Persistent (â–  P)"
 
+The command has indeed failed with message:
+Cannot infer this placeholder of type
+"Separable
+   (True
+    ∧ True
+      ∧ True
+        ∧ True
+          ∧ True
+            ∧ True
+              ∧ True
+                ∧ True
+                  ∧ True
+                    ∧ True
+                      ∧ True
+                        ∧ True
+                          ∧ True
+                            ∧ True
+                              ∧ True
+                                ∧ True
+                                  ∧ True
+                                    ∧ True
+                                      ∧ True
+                                        ∧ True
+                                          ∧ True
+                                            ∧ True
+                                              ∧ True
+                                                ∧ 
+                                                True
+                                                ∧ 
+                                                True
+                                                ∧ 
+                                                True
+                                                ∧ 
+                                                True
+                                                ∧ 
+                                                True
+                                                ∧ 
+                                                True
+                                                ∧ 
+                                                True
+                                                ∧ 
+                                                True
+                                                ∧ 
+                                                True
+                                                ∧ 
+                                                True
+                                                ∧ 
+                                                True
+                                                ∧ 
+                                                True
+                                                ∧ 
+                                                True
+                                                ∧ 
+                                                True
+                                                ∧ 
+                                                True
+                                                ∧ 
+                                                True
+                                                ∧ 
+                                                True
+                                                ∧ 
+                                                True
+                                                ∧ 
+                                                True ∧ True ∧ True ∧ ...)"
+(no type class instance found) in
+environment:
+PROP : bi
+BiPlainly0 : BiPlainly PROP
+P : PROP
diff --git a/tests/bi.v b/tests/bi.v
index 3e38ccce0141b0fe4696c2d13840e7c2170ea205..43d549360662ee29cee5700f671fdf62d9863f10 100644
--- a/tests/bi.v
+++ b/tests/bi.v
@@ -70,3 +70,12 @@ Proof. intros. eexists _. Fail apply _. Abort.
 Goal ∀ {PROP : bi} (P : PROP),
   ∃ plainly_instance, Persistent (@plainly PROP plainly_instance P).
 Proof. intros. eexists _. Fail apply _. Abort.
+
+(** Without the right [Hint Cut] declarations, this will backtrack on trying to
+establish that each conjunction is [Separable], [Persistent], and [Plain], i.e.,
+taking [100^3] steps. *)
+Lemma separable_big `{!BiPlainly PROP} (P : PROP) :
+  Separable (Nat.iter 100 (λ rec, True ∧ rec)%I P).
+Proof.
+  simpl. Fail apply _.
+Abort.