diff --git a/CHANGELOG.md b/CHANGELOG.md
index 420d3949fb4354fc3b6c5a0b55d6b7f8969c9090..a8934aa4ba15a9758226261bc2370b442cf5b0ac 100644
--- a/CHANGELOG.md
+++ b/CHANGELOG.md
@@ -81,6 +81,8 @@ Coq development, but not every API-breaking change is listed.  Changes marked
 * The tactic `iAssumption` also recognizes assumptions `⊢ P` in the Coq context.
 * Add notion `ofe_iso A B` that states that OFEs `A` and `B` are isomorphic.
 * Make use of `ofe_iso` in the COFE solver.
+* The functions `{o,r,ur}Functor_diag` are no longer coercions, and renamed into
+  `{o,r,ur}Functor_apply` to better match their intent.
 
 **Changes in heap_lang:**
 
diff --git a/_CoqProject b/_CoqProject
index 900568c5eac3877854e6f7d9ea9a896536c66b9a..d2742fd1994f27135471d50b0da4cd0746da6abc 100644
--- a/_CoqProject
+++ b/_CoqProject
@@ -8,8 +8,6 @@
 -arg -w -arg -convert_concl_no_check
 # "Declare Scope" does not exist yet in 8.9.
 -arg -w -arg -undeclared-scope
-# We have ambiguous paths, and live with it.
--arg -w -arg -ambiguous-paths
 
 theories/algebra/monoid.v
 theories/algebra/cmra.v
diff --git a/theories/algebra/cmra.v b/theories/algebra/cmra.v
index f2ed6b23cd30d5d0c3a79abd8e086f57c1c68534..b0f608cc58b6b1617f985a785ab302e26386ae88 100644
--- a/theories/algebra/cmra.v
+++ b/theories/algebra/cmra.v
@@ -800,9 +800,8 @@ Class rFunctorContractive (F : rFunctor) :=
   rFunctor_contractive `{!Cofe A1, !Cofe A2, !Cofe B1, !Cofe B2} :>
     Contractive (@rFunctor_map F A1 _ A2 _ B1 _ B2 _).
 
-Definition rFunctor_diag (F: rFunctor) (A: ofeT) `{!Cofe A} : cmraT :=
+Definition rFunctor_apply (F: rFunctor) (A: ofeT) `{!Cofe A} : cmraT :=
   rFunctor_car F A A.
-Coercion rFunctor_diag : rFunctor >-> Funclass.
 
 Program Definition constRF (B : cmraT) : rFunctor :=
   {| rFunctor_car A1 _ A2 _ := B; rFunctor_map A1 _ A2 _ B1 _ B2 _ f := cid |}.
@@ -838,9 +837,8 @@ Class urFunctorContractive (F : urFunctor) :=
   urFunctor_contractive `{!Cofe A1, !Cofe A2, !Cofe B1, !Cofe B2} :>
     Contractive (@urFunctor_map F A1 _ A2 _ B1 _ B2 _).
 
-Definition urFunctor_diag (F: urFunctor) (A: ofeT) `{!Cofe A} : ucmraT :=
+Definition urFunctor_apply (F: urFunctor) (A: ofeT) `{!Cofe A} : ucmraT :=
   urFunctor_car F A A.
-Coercion urFunctor_diag : urFunctor >-> Funclass.
 
 Program Definition constURF (B : ucmraT) : urFunctor :=
   {| urFunctor_car A1 _ A2 _ := B; urFunctor_map A1 _ A2 _ B1 _ B2 _ f := cid |}.
diff --git a/theories/algebra/cofe_solver.v b/theories/algebra/cofe_solver.v
index 2cb91a39acb0122f2c9e5ee9d3953e6144dd9b17..f64b166540f9ff2986746d2599e09e1f51351546 100644
--- a/theories/algebra/cofe_solver.v
+++ b/theories/algebra/cofe_solver.v
@@ -4,20 +4,20 @@ Set Default Proof Using "Type".
 Record solution (F : oFunctor) := Solution {
   solution_car :> ofeT;
   solution_cofe : Cofe solution_car;
-  solution_iso :> ofe_iso (F solution_car _) solution_car;
+  solution_iso :> ofe_iso (oFunctor_apply F solution_car) solution_car;
 }.
 Existing Instance solution_cofe.
 
 Module solver. Section solver.
 Context (F : oFunctor) `{Fcontr : oFunctorContractive F}.
-Context `{Fcofe : ∀ (T : ofeT) `{!Cofe T}, Cofe (F T _)}.
-Context `{Finh : Inhabited (F unitO _)}.
+Context `{Fcofe : ∀ (T : ofeT) `{!Cofe T}, Cofe (oFunctor_apply F T)}.
+Context `{Finh : Inhabited (oFunctor_apply F unitO)}.
 Notation map := (oFunctor_map F).
 
 Fixpoint A' (k : nat) : { C : ofeT & Cofe C } :=
   match k with
   | 0 => existT (P:=Cofe) unitO _
-  | S k => existT (P:=Cofe) (F (projT1 (A' k)) (projT2 (A' k))) _
+  | S k => existT (P:=Cofe) (@oFunctor_apply F (projT1 (A' k)) (projT2 (A' k))) _
   end.
 Notation A k := (projT1 (A' k)).
 Local Instance A_cofe k : Cofe (A k) := projT2 (A' k).
@@ -176,7 +176,7 @@ Proof.
   - rewrite (ff_tower k (i - S k) X). by destruct (Nat.sub_add _ _ _).
 Qed.
 
-Program Definition unfold_chain (X : T) : chain (F T _) :=
+Program Definition unfold_chain (X : T) : chain (oFunctor_apply F T) :=
   {| chain_car n := map (project n,embed' n) (X (S n)) |}.
 Next Obligation.
   intros X n i Hi.
@@ -186,14 +186,14 @@ Next Obligation.
   rewrite f_S -oFunctor_compose.
   by apply (contractive_ne map); split=> Y /=; rewrite ?g_tower ?embed_f.
 Qed.
-Definition unfold (X : T) : F T _ := compl (unfold_chain X).
+Definition unfold (X : T) : oFunctor_apply F T := compl (unfold_chain X).
 Instance unfold_ne : NonExpansive unfold.
 Proof.
   intros n X Y HXY. by rewrite /unfold (conv_compl n (unfold_chain X))
     (conv_compl n (unfold_chain Y)) /= (HXY (S n)).
 Qed.
 
-Program Definition fold (X : F T _) : T :=
+Program Definition fold (X : oFunctor_apply F T) : T :=
   {| tower_car n := g n (map (embed' n,project n) X) |}.
 Next Obligation.
   intros X k. apply (_ : Proper ((≡) ==> (≡)) (g k)).
diff --git a/theories/algebra/ofe.v b/theories/algebra/ofe.v
index f8563361ea3e7f509f2665c8ceff7ccab8d60647..07b2993a16a0745c048bcac36d907b7832a3e29c 100644
--- a/theories/algebra/ofe.v
+++ b/theories/algebra/ofe.v
@@ -708,12 +708,10 @@ Class oFunctorContractive (F : oFunctor) :=
     Contractive (@oFunctor_map F A1 _ A2 _ B1 _ B2 _).
 Hint Mode oFunctorContractive ! : typeclass_instances.
 
-Definition oFunctor_diag (F: oFunctor) (A: ofeT) `{!Cofe A} : ofeT :=
+(** Not a coercion due to the [Cofe] type class argument, and to avoid
+ambiguous coercion paths, see https://gitlab.mpi-sws.org/iris/iris/issues/240. *)
+Definition oFunctor_apply (F: oFunctor) (A: ofeT) `{!Cofe A} : ofeT :=
   oFunctor_car F A A.
-(** Note that the implicit argument [Cofe A] is not taken into account when
-[oFunctor_diag] is used as a coercion. So, given [F : oFunctor] and [A : ofeT]
-one has to write [F A _]. *)
-Coercion oFunctor_diag : oFunctor >-> Funclass.
 
 Program Definition constOF (B : ofeT) : oFunctor :=
   {| oFunctor_car A1 A2 _ _ := B; oFunctor_map A1 _ A2 _ B1 _ B2 _ f := cid |}.
@@ -1498,7 +1496,7 @@ Section sigTOF.
   Qed.
 
   Program Definition sigTOF (F : A → oFunctor) : oFunctor := {|
-    oFunctor_car A CA B CB := sigTO (λ a, oFunctor_car (F a) A _ B CB);
+    oFunctor_car A CA B CB := sigTO (λ a, oFunctor_car (F a) A B);
     oFunctor_map A1 _ A2 _ B1 _ B2 _ fg := sigT_map (λ a, oFunctor_map (F a) fg)
   |}.
   Next Obligation.
@@ -1584,7 +1582,7 @@ Instance iso_ofe_trans_ne {A B C} : NonExpansive2 (iso_ofe_trans (A:=A) (B:=B) (
 Proof. intros n I1 I2 [] J1 J2 []; split; simpl; by f_equiv. Qed.
 
 Program Definition iso_ofe_cong (F : oFunctor) `{!Cofe A, !Cofe B}
-    (I : ofe_iso A B) : ofe_iso (F A _) (F B _) :=
+    (I : ofe_iso A B) : ofe_iso (oFunctor_apply F A) (oFunctor_apply F B) :=
   OfeIso (oFunctor_map F (ofe_iso_2 I, ofe_iso_1 I))
     (oFunctor_map F (ofe_iso_1 I, ofe_iso_2 I)) _ _.
 Next Obligation.
diff --git a/theories/base_logic/lib/iprop.v b/theories/base_logic/lib/iprop.v
index 50169bddc9318016d0c19a2d71b29b2a95295291..45fb5407c9553e0473aa302218d465c39d2f969c 100644
--- a/theories/base_logic/lib/iprop.v
+++ b/theories/base_logic/lib/iprop.v
@@ -120,7 +120,8 @@ Module Type iProp_solution_sig.
   Global Declare Instance iPreProp_cofe {Σ} : Cofe (iPrePropO Σ).
 
   Definition iResUR (Σ : gFunctors) : ucmraT :=
-    discrete_funUR (λ i, gmapUR gname (gFunctors_lookup Σ i (iPrePropO Σ) _)).
+    discrete_funUR (λ i,
+      gmapUR gname (rFunctor_apply (gFunctors_lookup Σ i) (iPrePropO Σ))).
   Notation iProp Σ := (uPred (iResUR Σ)).
   Notation iPropO Σ := (uPredO (iResUR Σ)).
   Notation iPropI Σ := (uPredI (iResUR Σ)).
@@ -142,7 +143,8 @@ Module Export iProp_solution : iProp_solution_sig.
   Global Instance iPreProp_cofe {Σ} : Cofe (iPrePropO Σ) := _.
 
   Definition iResUR (Σ : gFunctors) : ucmraT :=
-    discrete_funUR (λ i, gmapUR gname (gFunctors_lookup Σ i (iPrePropO Σ) _)).
+    discrete_funUR (λ i,
+      gmapUR gname (rFunctor_apply (gFunctors_lookup Σ i) (iPrePropO Σ))).
   Notation iProp Σ := (uPred (iResUR Σ)).
   Notation iPropO Σ := (uPredO (iResUR Σ)).
 
diff --git a/theories/base_logic/lib/own.v b/theories/base_logic/lib/own.v
index 82553775f792e2f3d7b22ae8335f816603fda501..357f2979e2877143d81fe06fa5dec31ddfba95ce 100644
--- a/theories/base_logic/lib/own.v
+++ b/theories/base_logic/lib/own.v
@@ -9,14 +9,15 @@ individual CMRAs instead of (lists of) CMRA *functors*. This additional class is
 needed because Coq is otherwise unable to solve type class constraints due to
 higher-order unification problems. *)
 Class inG (Σ : gFunctors) (A : cmraT) :=
-  InG { inG_id : gid Σ; inG_prf : A = gFunctors_lookup Σ inG_id (iPrePropO Σ) _ }.
+  InG { inG_id : gid Σ; inG_prf :
+    A = rFunctor_apply (gFunctors_lookup Σ inG_id) (iPrePropO Σ)}.
 Arguments inG_id {_ _} _.
 (** We use the mode [-] for [Σ] since there is always a unique [Σ]. We use the
 mode [!] for [A] since we can have multiple [inG]s for different [A]s, so we do
 not want Coq to pick one arbitrarily. *)
 Hint Mode inG - ! : typeclass_instances.
 
-Lemma subG_inG Σ (F : gFunctor) : subG F Σ → inG Σ (F (iPrePropO Σ) _).
+Lemma subG_inG Σ (F : gFunctor) : subG F Σ → inG Σ (rFunctor_apply F (iPrePropO Σ)).
 Proof. move=> /(_ 0%fin) /= [j ->]. by exists j. Qed.
 
 (** This tactic solves the usual obligations "subG ? Σ → {in,?}G ? Σ" *)
diff --git a/theories/base_logic/lib/saved_prop.v b/theories/base_logic/lib/saved_prop.v
index 3ba56d39827364e890f5ff2ad354a8610f1018f0..2f6252b7e5d88267a5c35565f16b5734a7eea50d 100644
--- a/theories/base_logic/lib/saved_prop.v
+++ b/theories/base_logic/lib/saved_prop.v
@@ -9,7 +9,7 @@ Import uPred.
    saved whatever-you-like. *)
 
 Class savedAnythingG (Σ : gFunctors) (F : oFunctor) := SavedAnythingG {
-  saved_anything_inG :> inG Σ (agreeR (F (iPrePropO Σ) _));
+  saved_anything_inG :> inG Σ (agreeR (oFunctor_apply F (iPrePropO Σ)));
   saved_anything_contractive : oFunctorContractive F (* NOT an instance to avoid cycles with [subG_savedAnythingΣ]. *)
 }.
 Definition savedAnythingΣ (F : oFunctor) `{!oFunctorContractive F} : gFunctors :=
@@ -20,14 +20,14 @@ Instance subG_savedAnythingΣ {Σ F} `{!oFunctorContractive F} :
 Proof. solve_inG. Qed.
 
 Definition saved_anything_own `{!savedAnythingG Σ F}
-    (γ : gname) (x : F (iPropO Σ) _) : iProp Σ :=
+    (γ : gname) (x : oFunctor_apply F (iPropO Σ)) : iProp Σ :=
   own γ (to_agree $ (oFunctor_map F (iProp_fold, iProp_unfold) x)).
 Typeclasses Opaque saved_anything_own.
 Instance: Params (@saved_anything_own) 4 := {}.
 
 Section saved_anything.
   Context `{!savedAnythingG Σ F}.
-  Implicit Types x y : F (iPropO Σ) _.
+  Implicit Types x y : oFunctor_apply F (iPropO Σ).
   Implicit Types γ : gname.
 
   Global Instance saved_anything_persistent γ x :