diff --git a/iris/algebra/cmra.v b/iris/algebra/cmra.v
index 7824e3ac84e51dddbe0d5ba12a73241b8260741e..2b735510d1e850fc24b25a5d2185c0f8194c6197 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' {
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.