diff --git a/tests/algebra.v b/tests/algebra.v
index 92c42c4b4f6f9e9071dafaad733c00d9fbd49169..cff006b35fb5dad5262206b75e9b9286d69c142f 100644
--- a/tests/algebra.v
+++ b/tests/algebra.v
@@ -1,3 +1,4 @@
+From iris.algebra Require Import auth excl.
 From iris.base_logic.lib Require Import invariants.
 
 (** Make sure that the same [Equivalence] instance is picked for Leibniz OFEs
@@ -34,3 +35,16 @@ Proof.
   - apply _.
   - reflexivity.
 Qed.
+
+(** Regression test for <https://gitlab.mpi-sws.org/iris/iris/issues/255>. *)
+Definition testR := authR (prodUR
+        (prodUR
+          (optionUR (exclR unitO))
+          (optionUR (exclR unitO)))
+        (optionUR (agreeR (boolO)))).
+Section test_prod.
+  Context `{!inG Σ testR}.
+  Lemma test_prod_persistent γ :
+    Persistent (PROP:=iPropI Σ) (own γ (◯((None, None), Some (to_agree true)))).
+  Proof. apply _. Qed.
+End test_prod.
diff --git a/theories/algebra/cmra.v b/theories/algebra/cmra.v
index 08d4ef1176a1577aede6a388b35e73f11f8be645..2944df3d03d3981e40ea0bb4eb03537473ec6306 100644
--- a/theories/algebra/cmra.v
+++ b/theories/algebra/cmra.v
@@ -1170,7 +1170,9 @@ Section prod.
     CmraDiscrete A → CmraDiscrete B → CmraDiscrete prodR.
   Proof. split. apply _. by intros ? []; split; apply cmra_discrete_valid. Qed.
 
-  Global Instance pair_core_id x y :
+  (* FIXME(Coq #6294): This is not an instance because we need it to use the new
+  unification. *)
+  Lemma pair_core_id x y :
     CoreId x → CoreId y → CoreId (x,y).
   Proof. by rewrite /CoreId prod_pcore_Some'. Qed.
 
@@ -1189,6 +1191,9 @@ Section prod.
   Proof. move=>? [??] [_ ?] [_ /=?]. eauto. Qed.
 End prod.
 
+(* Registering as [Hint Extern] with new unification. *)
+Hint Extern 4 (CoreId _) => notypeclasses refine (pair_core_id _ _ _ _) : typeclass_instances.
+
 Arguments prodR : clear implicits.
 
 Section prod_unit.
diff --git a/theories/bi/embedding.v b/theories/bi/embedding.v
index bbf87f95dfbc71b2f9277ad45185f87e5776cf6d..92bce3d7b52b5747d7a5f9c81b6dbd6fbbe1fb69 100644
--- a/theories/bi/embedding.v
+++ b/theories/bi/embedding.v
@@ -324,4 +324,4 @@ End sbi_embed.
 [class_apply @bi_embed_plainly] shelves the [BiPlainly] premise, making proof
 search for the other premises fail. See the proof of [monPred_objectively_plain]
 for an example where it would fail with a regular [Instance].*)
-Hint Extern 4 (Plain ⎡_⎤) => eapply @embed_plain : typeclass_instances.
+Hint Extern 4 (Plain _) => notypeclasses refine (embed_plain _ _) : typeclass_instances.
diff --git a/theories/bi/plainly.v b/theories/bi/plainly.v
index e957761743aff18bb61a54637df262a05d6a3075..093b731bd444200e23b37944c9da484cb3207129 100644
--- a/theories/bi/plainly.v
+++ b/theories/bi/plainly.v
@@ -633,4 +633,4 @@ Hint Immediate plain_persistent : typeclass_instances.
 [class_apply @impl_persistent] shelves the [BiPlainly] premise, making proof
 search for the other premises fail. See the proof of [coreP_persistent] for an
 example where it would fail with a regular [Instance].*)
-Hint Extern 4 (Persistent (_ → _)) => eapply @impl_persistent : typeclass_instances.
+Hint Extern 4 (Persistent _) => notypeclasses refine (impl_persistent _ _ _ _ _) : typeclass_instances.