diff --git a/theories/program_logic/ectx_language.v b/theories/program_logic/ectx_language.v
index dd0fff9916907272b5ec725d8065efec28b11b1c..68b183168668cd92099dae4a8812588c743fed6a 100644
--- a/theories/program_logic/ectx_language.v
+++ b/theories/program_logic/ectx_language.v
@@ -201,7 +201,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 c23bfbef329e4a621c812c7205624ea7e7da7491..603d216516f1f8c2bb60ae876a68106f656f33f7 100644
--- a/theories/program_logic/ectxi_language.v
+++ b/theories/program_logic/ectxi_language.v
@@ -137,8 +137,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 _ (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/hoare.v b/theories/program_logic/hoare.v
index ff46550fc76bb30a4302f841d4ec3316eccbf985..e2af2d5c1574b974a0ea0cf57d7a19ff1ef8ab5f 100644
--- a/theories/program_logic/hoare.v
+++ b/theories/program_logic/hoare.v
@@ -89,7 +89,7 @@ Proof.
   iIntros (v) "Hv". by iApply "HΦ".
 Qed.
 
-Lemma ht_bind `{!LanguageCtx Λ K} s E P Φ Φ' e :
+Lemma ht_bind `{!LanguageCtx K} s E P Φ Φ' e :
   {{ P }} e @ s; E {{ Φ }} ∧ (∀ v, {{ Φ v }} K (of_val v) @ s; E {{ Φ' }})
   ⊢ {{ P }} K e @ s; E {{ Φ' }}.
 Proof.
diff --git a/theories/program_logic/language.v b/theories/program_logic/language.v
index 483d9a244017fde0f647d2d079741c7ce7e7ce98..162ac66ba73e30af4def6a05ee82382c38761c8e 100644
--- a/theories/program_logic/language.v
+++ b/theories/program_logic/language.v
@@ -53,9 +53,8 @@ Class LanguageCtx {Λ : language} (K : expr Λ → expr Λ) := {
     to_val e1' = None → prim_step (K e1') σ1 κ e2 σ2 efs →
     ∃ e2', e2 = K e2' ∧ prim_step e1' σ1 κ e2' σ2 efs
 }.
-Arguments LanguageCtx : clear implicits.
 
-Instance language_ctx_id Λ : LanguageCtx Λ (@id (expr Λ)).
+Instance language_ctx_id Λ : LanguageCtx (@id (expr Λ)).
 Proof. constructor; naive_solver. Qed.
 
 Inductive atomicity := StronglyAtomic | WeaklyAtomic.
@@ -142,19 +141,19 @@ Section language.
     Atomic StronglyAtomic e → Atomic a e.
   Proof. unfold Atomic. destruct a; eauto using val_irreducible. Qed.
 
-  Lemma reducible_fill `{!LanguageCtx Λ K} e σ :
+  Lemma reducible_fill `{!@LanguageCtx Λ K} e σ :
     to_val e = None → reducible (K e) σ → reducible e σ.
   Proof.
     intros ? (e'&σ'&k&efs&Hstep); unfold reducible.
     apply fill_step_inv in Hstep as (e2' & _ & Hstep); eauto.
   Qed.
-  Lemma reducible_no_obs_fill `{!LanguageCtx Λ K} e σ :
+  Lemma reducible_no_obs_fill `{!@LanguageCtx Λ K} e σ :
     to_val e = None → reducible_no_obs (K e) σ → reducible_no_obs e σ.
   Proof.
     intros ? (e'&σ'&efs&Hstep); unfold reducible_no_obs.
     apply fill_step_inv in Hstep as (e2' & _ & Hstep); eauto.
   Qed.
-  Lemma irreducible_fill `{!LanguageCtx Λ K} e σ :
+  Lemma irreducible_fill `{!@LanguageCtx Λ K} e σ :
     to_val e = None → irreducible e σ → irreducible (K e) σ.
   Proof. rewrite -!not_reducible. naive_solver eauto using reducible_fill. Qed.
 
@@ -186,7 +185,7 @@ Section language.
   Class PureExec (φ : Prop) (n : nat) (e1 e2 : expr Λ) :=
     pure_exec : φ → relations.nsteps pure_step n e1 e2.
 
-  Lemma pure_step_ctx K `{!LanguageCtx Λ K} e1 e2 :
+  Lemma pure_step_ctx K `{!@LanguageCtx Λ K} e1 e2 :
     pure_step e1 e2 →
     pure_step (K e1) (K e2).
   Proof.
@@ -198,13 +197,13 @@ Section language.
       + edestruct (Hstep σ1 κ e2'' σ2 efs) as (? & -> & -> & ->); auto.
   Qed.
 
-  Lemma pure_step_nsteps_ctx K `{!LanguageCtx Λ K} n e1 e2 :
+  Lemma pure_step_nsteps_ctx K `{!@LanguageCtx Λ K} n e1 e2 :
     relations.nsteps pure_step n e1 e2 →
     relations.nsteps pure_step n (K e1) (K e2).
   Proof. induction 1; econstructor; eauto using pure_step_ctx. Qed.
 
   (* We do not make this an instance because it is awfully general. *)
-  Lemma pure_exec_ctx K `{!LanguageCtx Λ K} φ n e1 e2 :
+  Lemma pure_exec_ctx K `{!@LanguageCtx Λ K} φ n e1 e2 :
     PureExec φ n e1 e2 →
     PureExec φ n (K e1) (K e2).
   Proof. rewrite /PureExec; eauto using pure_step_nsteps_ctx. Qed.
diff --git a/theories/program_logic/total_weakestpre.v b/theories/program_logic/total_weakestpre.v
index 24173b69128f471c3da9ce39c880f3da29f5e134..3b964c1fe6e944f5b6d3e6692ca42aa7e55db2fc 100644
--- a/theories/program_logic/total_weakestpre.v
+++ b/theories/program_logic/total_weakestpre.v
@@ -147,7 +147,7 @@ Proof.
     iModIntro. iSplit; first done. iFrame "Hσ Hefs". by iApply twp_value'.
 Qed.
 
-Lemma twp_bind K `{!LanguageCtx Λ K} s E e Φ :
+Lemma twp_bind K `{!LanguageCtx K} s E e Φ :
   WP e @ s; E [{ v, WP K (of_val v) @ s; E [{ Φ }] }] -∗ WP K e @ s; E [{ Φ }].
 Proof.
   revert Φ. cut (∀ Φ', WP e @ s; E [{ Φ' }] -∗ ∀ Φ,
@@ -169,7 +169,7 @@ Proof.
   - by setoid_rewrite and_elim_r.
 Qed.
 
-Lemma twp_bind_inv K `{!LanguageCtx Λ K} s E e Φ :
+Lemma twp_bind_inv K `{!LanguageCtx K} s E e Φ :
   WP K e @ s; E [{ Φ }] -∗ WP e @ s; E [{ v, WP K (of_val v) @ s; E [{ Φ }] }].
 Proof.
   iIntros "H". remember (K e) as e' eqn:He'.
diff --git a/theories/program_logic/weakestpre.v b/theories/program_logic/weakestpre.v
index 47ba39abeb9d890e76dfdebbb99616bb33706335..f26a223b9bbdaa1f912e9d4c3ca16015bb1b51de 100644
--- a/theories/program_logic/weakestpre.v
+++ b/theories/program_logic/weakestpre.v
@@ -143,7 +143,7 @@ Proof.
   iIntros (v) "H". by iApply "H".
 Qed.
 
-Lemma wp_bind K `{!LanguageCtx Λ K} s E e Φ :
+Lemma wp_bind K `{!LanguageCtx K} s E e Φ :
   WP e @ s; E {{ v, WP K (of_val v) @ s; E {{ Φ }} }} ⊢ WP K e @ s; E {{ Φ }}.
 Proof.
   iIntros "H". iLöb as "IH" forall (E e Φ). rewrite wp_unfold /wp_pre.
@@ -160,7 +160,7 @@ Proof.
   iModIntro. iFrame "Hσ Hefs". by iApply "IH".
 Qed.
 
-Lemma wp_bind_inv K `{!LanguageCtx Λ K} s E e Φ :
+Lemma wp_bind_inv K `{!LanguageCtx K} s E e Φ :
   WP K e @ s; E {{ Φ }} ⊢ WP e @ s; E {{ v, WP K (of_val v) @ s; E {{ Φ }} }}.
 Proof.
   iIntros "H". iLöb as "IH" forall (E e Φ). rewrite !wp_unfold /wp_pre.