diff --git a/theories/program_logic/ectx_language.v b/theories/program_logic/ectx_language.v
index 40ea10294e51d48769898585b5f014be48f4ea41..9578d57857f3177cb4c7387b40c8844226278acb 100644
--- a/theories/program_logic/ectx_language.v
+++ b/theories/program_logic/ectx_language.v
@@ -176,7 +176,7 @@ Section ectx_language.
   Qed.
 
   (* Every evaluation context is a context. *)
-  Global Instance ectx_lang_ctx K : LanguageCtx _ (fill K).
+  Global Instance ectx_lang_ctx K : LanguageCtx (fill K).
   Proof.
     split; simpl.
     - eauto using fill_not_val.
diff --git a/theories/program_logic/ectxi_language.v b/theories/program_logic/ectxi_language.v
index 6c0f58131797ed3af973b5786d60120cbe546f36..c622cd164fec77c106c2a15a97be6779c39def36 100644
--- a/theories/program_logic/ectxi_language.v
+++ b/theories/program_logic/ectxi_language.v
@@ -114,8 +114,8 @@ Section ectxi_language.
     intros []%eq_None_not_Some. eapply fill_val, Hsub. by rewrite /= fill_app.
   Qed.
 
-  Global Instance ectxi_lang_ctx_item Ki : LanguageCtx _ (fill_item Ki).
-  Proof. change (LanguageCtx ectxi_lang (fill [Ki])). apply _. Qed.
+  Global Instance ectxi_lang_ctx_item Ki : LanguageCtx (fill_item Ki).
+  Proof. change (LanguageCtx (fill [Ki])). apply _. Qed.
 End ectxi_language.
 
 Arguments fill {_} _ _%E.
diff --git a/theories/program_logic/language.v b/theories/program_logic/language.v
index 6b1a9770cfaea45f512e355b6b84dd4deb3e7693..660965699c6e6b5d91f7a630b067b4129809a79d 100644
--- a/theories/program_logic/language.v
+++ b/theories/program_logic/language.v
@@ -39,7 +39,7 @@ Canonical Structure exprC Λ := leibnizC (expr Λ).
 
 Definition cfg (Λ : language) := (list (expr Λ) * state Λ)%type.
 
-Class LanguageCtx (Λ : language) (K : expr Λ → expr Λ) := {
+Class LanguageCtx {Λ : language} (K : expr Λ → expr Λ) := {
   fill_not_val e :
     to_val e = None → to_val (K e) = None;
   fill_step e1 σ1 e2 σ2 efs :
@@ -50,7 +50,7 @@ Class LanguageCtx (Λ : language) (K : expr Λ → expr Λ) := {
     ∃ e2', e2 = K e2' ∧ prim_step e1' σ1 e2' σ2 efs
 }.
 
-Instance language_ctx_id Λ : LanguageCtx Λ id.
+Instance language_ctx_id Λ : LanguageCtx (@id (expr Λ)).
 Proof. constructor; naive_solver. Qed.
 
 Section language.
diff --git a/theories/program_logic/weakestpre.v b/theories/program_logic/weakestpre.v
index 7d63d87bb8329059cf52bbb0a49e9e0155e79e85..97096107c17d524ba6b62b1660d6262b4373997a 100644
--- a/theories/program_logic/weakestpre.v
+++ b/theories/program_logic/weakestpre.v
@@ -174,7 +174,7 @@ Proof.
   iSplitR "H"; last iExact "H". iIntros (v) "H". by iApply "H".
 Qed.
 
-Lemma wp_bind K `{!LanguageCtx Λ K} E e Φ :
+Lemma wp_bind K `{!LanguageCtx K} E e Φ :
   WP e @ E {{ v, WP K (of_val v) @ E {{ Φ }} }} ⊢ WP K e @ E {{ Φ }}.
 Proof.
   iIntros "H". iLöb as "IH" forall (E e Φ). rewrite wp_unfold /wp_pre.
@@ -189,7 +189,7 @@ Proof.
   by iApply "IH".
 Qed.
 
-Lemma wp_bind_inv K `{!LanguageCtx Λ K} E e Φ :
+Lemma wp_bind_inv K `{!LanguageCtx K} E e Φ :
   WP K e @ E {{ Φ }} ⊢ WP e @ E {{ v, WP K (of_val v) @ E {{ Φ }} }}.
 Proof.
   iIntros "H". iLöb as "IH" forall (E e Φ). rewrite !wp_unfold /wp_pre.