diff --git a/CHANGELOG.md b/CHANGELOG.md
index 0c19f8792b17a0332b0967710a50f8a92db5c7fb..607fdf3d9218bbec8a0d23bd0c8950d49eb250c8 100644
--- a/CHANGELOG.md
+++ b/CHANGELOG.md
@@ -31,6 +31,8 @@ Coq 8.11 is no longer supported in this version of Iris.
   `Dist`, `Op`, `Valid`, `ValidN`, `Unit`, `PCore` now use an `Hint Extern`
   based on `refine` instead of `apply`, in order to use Coq's newer unification
   algorithm.
+* Set `Hint Mode` for the classes `OfeDiscrete`, `Unit`, `CmraMorphism`,
+  `rFunctorContractive`, `urFunctorContractive`.
 
 **Changes in `bi`:**
 
diff --git a/iris/algebra/agree.v b/iris/algebra/agree.v
index 2421f83326bf2b050df89b330ad6a21012ae5bec..306eb8a8d0530d8b80d757067cf8ff96f10b9029 100644
--- a/iris/algebra/agree.v
+++ b/iris/algebra/agree.v
@@ -121,7 +121,7 @@ Proof.
 Qed.
 Local Instance agree_op_ne : NonExpansive2 (@op (agree A) _).
 Proof. by intros n x1 x2 Hx y1 y2 Hy; rewrite Hy !(comm _ _ y2) Hx. Qed.
-Local Instance agree_op_proper : Proper ((≡) ==> (≡) ==> (≡)) op := ne_proper_2 _.
+Local Instance agree_op_proper : Proper ((≡) ==> (≡) ==> (≡)) (op (A := agree A)) := ne_proper_2 _.
 
 Lemma agree_included x y : x ≼ y ↔ y ≡ x ⋅ y.
 Proof.
diff --git a/iris/algebra/cmra.v b/iris/algebra/cmra.v
index 7824e3ac84e51dddbe0d5ba12a73241b8260741e..5dde79ec0062a1db155c08bc5836e40071a0b7a5 100644
--- a/iris/algebra/cmra.v
+++ b/iris/algebra/cmra.v
@@ -181,12 +181,13 @@ Global Instance: Params (@core) 2 := {}.
 
 (** * CMRAs with a unit element *)
 Class Unit (A : Type) := ε : A.
+Global Hint Mode Unit ! : typeclass_instances.
 Global Arguments ε {_ _}.
 
 Record UcmraMixin A `{Dist A, Equiv A, PCore A, Op A, Valid A, Unit A} := {
   mixin_ucmra_unit_valid : ✓ (ε : A);
-  mixin_ucmra_unit_left_id : LeftId (≡) ε (⋅);
-  mixin_ucmra_pcore_unit : pcore ε ≡ Some ε
+  mixin_ucmra_unit_left_id : LeftId (≡@{A}) ε (⋅);
+  mixin_ucmra_pcore_unit : pcore ε ≡@{option A} Some ε
 }.
 
 Structure ucmra := Ucmra' {
@@ -250,6 +251,7 @@ Class CmraMorphism {A B : cmra} (f : A → B) := {
   cmra_morphism_pcore x : f <$> pcore x ≡ pcore (f x);
   cmra_morphism_op x y : f (x ⋅ y) ≡ f x ⋅ f y
 }.
+Global Hint Mode CmraMorphism - - ! : typeclass_instances.
 Global Arguments cmra_morphism_validN {_ _} _ {_} _ _ _.
 Global Arguments cmra_morphism_pcore {_ _} _ {_} _.
 Global Arguments cmra_morphism_op {_ _} _ {_} _ _.
@@ -807,6 +809,7 @@ Bind Scope rFunctor_scope with rFunctor.
 Class rFunctorContractive (F : rFunctor) :=
   rFunctor_map_contractive `{!Cofe A1, !Cofe A2, !Cofe B1, !Cofe B2} :>
     Contractive (@rFunctor_map F A1 _ A2 _ B1 _ B2 _).
+Global Hint Mode rFunctorContractive ! : typeclass_instances.
 
 Definition rFunctor_apply (F: rFunctor) (A: ofe) `{!Cofe A} : cmra :=
   rFunctor_car F A A.
@@ -898,6 +901,7 @@ Bind Scope urFunctor_scope with urFunctor.
 Class urFunctorContractive (F : urFunctor) :=
   urFunctor_map_contractive `{!Cofe A1, !Cofe A2, !Cofe B1, !Cofe B2} :>
     Contractive (@urFunctor_map F A1 _ A2 _ B1 _ B2 _).
+Global Hint Mode urFunctorContractive ! : typeclass_instances.
 
 Definition urFunctor_apply (F: urFunctor) (A: ofe) `{!Cofe A} : ucmra :=
   urFunctor_car F A A.
diff --git a/iris/algebra/ofe.v b/iris/algebra/ofe.v
index 65dab9152f935aa475f266b435956908ccf95e77..29271bc6e4d63c89cb8f2e1e52f6e4e55e371848 100644
--- a/iris/algebra/ofe.v
+++ b/iris/algebra/ofe.v
@@ -110,6 +110,7 @@ Global Hint Mode Discrete + ! : typeclass_instances.
 Global Instance: Params (@Discrete) 1 := {}.
 
 Class OfeDiscrete (A : ofe) := ofe_discrete_discrete (x : A) :> Discrete x.
+Global Hint Mode OfeDiscrete ! : typeclass_instances.
 
 (** OFEs with a completion *)
 Record chain (A : ofe) := {
diff --git a/iris_staging/algebra/list.v b/iris_staging/algebra/list.v
index b764171fe3e111c3c8af20122f6110ef8de34f75..36fa11fd2b3ba6462693910cd81dbf3d3671e9e9 100644
--- a/iris_staging/algebra/list.v
+++ b/iris_staging/algebra/list.v
@@ -364,7 +364,7 @@ Section properties.
     ✓ x → (l, ε) ~l~> (l ++ [x], {[length l := x]}).
   Proof.
     move => ?.
-    have -> : ({[length l := x]} ≡ {[length l := x]} ⋅ ε) by rewrite right_id.
+    have -> : ({[length l := x]} ≡@{list A} {[length l := x]} ⋅ ε) by rewrite right_id.
     rewrite -list_singletonM_snoc. apply op_local_update => ??.
     rewrite list_singletonM_snoc app_validN cons_validN. split_and? => //; [| constructor].
     by apply cmra_valid_validN.