diff --git a/iris/bi/weakestpre.v b/iris/bi/weakestpre.v
index 3bcc9cfe9dcc497299278dab3522443882ee6984..3cd29fc52051c89fb664640c69d42fb19d510598 100644
--- a/iris/bi/weakestpre.v
+++ b/iris/bi/weakestpre.v
@@ -1,8 +1,25 @@
 From stdpp Require Export coPset.
 From iris.bi Require Import interface derived_connectives.
-From iris.program_logic Require Import language.
 From iris.prelude Require Import options.
 
+(** We define a canonical structure tying together the two types that are
+relevant for us: expressions and values.  This helps [Wp] typeclass inference.
+*)
+Structure pre_language := PreLanguage {
+  expr : Type;
+  val : Type;
+}.
+
+Declare Scope expr_scope.
+Delimit Scope expr_scope with E.
+Bind Scope expr_scope with expr.
+
+Declare Scope val_scope.
+Delimit Scope val_scope with V.
+Bind Scope val_scope with val.
+
+(** We have some specialized notaton related to stuckness, so we need to define
+that type here. *)
 Inductive stuckness := NotStuck | MaybeStuck.
 
 Definition stuckness_leb (s1 s2 : stuckness) : bool :=
@@ -14,9 +31,6 @@ Global Instance stuckness_le : SqSubsetEq stuckness := stuckness_leb.
 Global Instance stuckness_le_po : PreOrder stuckness_le.
 Proof. split; by repeat intros []. Qed.
 
-Definition stuckness_to_atomicity (s : stuckness) : atomicity :=
-  if s is MaybeStuck then StronglyAtomic else WeaklyAtomic.
-
 (** Weakest preconditions [WP e @ s ; E {{ Φ }}] have an additional argument [s]
 of arbitrary type [A], that can be chosen by the one instantiating the [Wp] type
 class. This argument can be used for e.g. the stuckness bit (as in Iris) or
@@ -28,12 +42,12 @@ and [s] to be [NotStuck] or [MaybeStuck].  This will fail to typecheck if [A] is
 not [stuckness].  If we ever want to use the notation [WP e @ E {{ Φ }}] with a
 different [A], the plan is to generalize the notation to use [Inhabited] instead
 to pick a default value depending on [A]. *)
-Class Wp (Λ : language) (PROP A : Type) :=
+Class Wp (Λ : pre_language) (PROP A : Type) :=
   wp : A → coPset → expr Λ → (val Λ → PROP) → PROP.
 Global Arguments wp {_ _ _ _} _ _ _%E _%I.
 Global Instance: Params (@wp) 7 := {}.
 
-Class Twp (Λ : language) (PROP A : Type) :=
+Class Twp (Λ : pre_language) (PROP A : Type) :=
   twp : A → coPset → expr Λ → (val Λ → PROP) → PROP.
 Global Arguments twp {_ _ _ _} _ _ _%E _%I.
 Global Instance: Params (@twp) 7 := {}.
diff --git a/iris/program_logic/adequacy.v b/iris/program_logic/adequacy.v
index 199e6aef438bf6c7edab80ef6667ff523d1f2ff5..b5ca6abb5660b15efa5a8cf3f4fbeea9d4344220 100644
--- a/iris/program_logic/adequacy.v
+++ b/iris/program_logic/adequacy.v
@@ -116,6 +116,8 @@ Proof.
 Qed.
 End adequacy.
 
+Implicit Types Λ : language.
+
 (** Iris's generic adequacy result *)
 Theorem wp_strong_adequacy Σ Λ `{!invPreG Σ} es σ1 n κs t2 σ2 φ
         (num_laters_per_step : nat → nat) :
diff --git a/iris/program_logic/ectx_language.v b/iris/program_logic/ectx_language.v
index a30b5a7d6edc7833cf2d26cccf4d245f7bee0f65..af8388bb3186babc22b9c8920975180efca1667a 100644
--- a/iris/program_logic/ectx_language.v
+++ b/iris/program_logic/ectx_language.v
@@ -141,7 +141,9 @@ Section ectx_language.
       apply eq_None_not_Some. by intros ?%fill_val%eq_None_not_Some.
   Qed.
 
-  Canonical Structure ectx_lang : language := Language ectx_lang_mixin.
+  Canonical Structure ectx_lang : language :=
+    Language (pre:=PreLanguage (expr Λ) (val Λ)) ectx_lang_mixin.
+  Canonical Structure ectxi_pre_lang := PreOfLanguage ectx_lang.
 
   Definition head_atomic (a : atomicity) (e : expr Λ) : Prop :=
     ∀ σ κ e' σ' efs,
@@ -322,5 +324,5 @@ Note that this trick no longer works when we switch to canonical projections
 because then the pattern match [let '...] will be desugared into projections. *)
 Definition LanguageOfEctx (Λ : ectxLanguage) : language :=
   let '@EctxLanguage E V C St K of_val to_val empty comp fill head mix := Λ in
-  @Language E V St K of_val to_val _
+  @Language (PreLanguage E V) St K of_val to_val _
     (@ectx_lang_mixin (@EctxLanguage E V C St K of_val to_val empty comp fill head mix)).
diff --git a/iris/program_logic/ectxi_language.v b/iris/program_logic/ectxi_language.v
index 55dc11ff86a7cef2ba7e0a97000a0513df372c68..c880b87f6e2983600e0b3ef696affdd912ff885a 100644
--- a/iris/program_logic/ectxi_language.v
+++ b/iris/program_logic/ectxi_language.v
@@ -139,6 +139,7 @@ Section ectxi_language.
 
   Canonical Structure ectxi_lang_ectx := EctxLanguage ectxi_lang_ectx_mixin.
   Canonical Structure ectxi_lang := LanguageOfEctx ectxi_lang_ectx.
+  Canonical Structure ectxi_pre_lang := PreOfLanguage ectxi_lang.
 
   Lemma fill_not_val K e : to_val e = None → to_val (fill K e) = None.
   Proof. rewrite !eq_None_not_Some. eauto using fill_val. Qed.
diff --git a/iris/program_logic/language.v b/iris/program_logic/language.v
index 280a6d36b5d44f1f87444a040d7bbf1799fed112..ef58c636123a5e6239d4e8e1c8287340c0e8ef15 100644
--- a/iris/program_logic/language.v
+++ b/iris/program_logic/language.v
@@ -1,6 +1,12 @@
 From iris.algebra Require Export ofe.
+From iris.bi Require Export weakestpre.
 From iris.prelude Require Import options.
 
+(** TAKE CARE: When you define a [language] canonical structure for your
+language, you need to also define a corresponding [pre_language] canonical
+structure. Use the coercion [PreOfLanguage] as defined in the bottom of this
+file for doing that. *)
+
 Section language_mixin.
   Context {expr val state observation : Type}.
   Context (of_val : val → expr).
@@ -18,32 +24,23 @@ Section language_mixin.
 End language_mixin.
 
 Structure language := Language {
-  expr : Type;
-  val : Type;
+  pre :> pre_language; (* Avoid having two [val] and [expr] projections. *)
   state : Type;
   observation : Type;
-  of_val : val → expr;
-  to_val : expr → option val;
-  prim_step : expr → state → list observation → expr → state → list expr → Prop;
+  of_val : val pre → expr pre;
+  to_val : expr pre → option (val pre);
+  prim_step : expr pre → state → list observation → expr pre → state → list (expr pre) → Prop;
   language_mixin : LanguageMixin of_val to_val prim_step
 }.
 
-Declare Scope expr_scope.
-Delimit Scope expr_scope with E.
-Bind Scope expr_scope with expr.
-
-Declare Scope val_scope.
-Delimit Scope val_scope with V.
-Bind Scope val_scope with val.
-
-Global Arguments Language {_ _ _ _ _ _ _} _.
+Global Arguments Language {_ _ _ _ _ _} _.
 Global Arguments of_val {_} _.
 Global Arguments to_val {_} _.
 Global Arguments prim_step {_} _ _ _ _ _ _.
 
-Canonical Structure stateO Λ := leibnizO (state Λ).
-Canonical Structure valO Λ := leibnizO (val Λ).
-Canonical Structure exprO Λ := leibnizO (expr Λ).
+Canonical Structure stateO (Λ : language) := leibnizO (state Λ).
+Canonical Structure valO (Λ : language) := leibnizO (val Λ).
+Canonical Structure exprO (Λ : language) := leibnizO (expr Λ).
 
 Definition cfg (Λ : language) := (list (expr Λ) * state Λ)%type.
 
@@ -58,11 +55,14 @@ Class LanguageCtx {Λ : language} (K : expr Λ → expr Λ) := {
     ∃ e2', e2 = K e2' ∧ prim_step e1' σ1 κ e2' σ2 efs
 }.
 
-Global Instance language_ctx_id Λ : LanguageCtx (@id (expr Λ)).
+Global Instance language_ctx_id (Λ : language) : LanguageCtx (@id (expr Λ)).
 Proof. constructor; naive_solver. Qed.
 
 Inductive atomicity := StronglyAtomic | WeaklyAtomic.
 
+Definition stuckness_to_atomicity (s : stuckness) : atomicity :=
+  if s is MaybeStuck then StronglyAtomic else WeaklyAtomic.
+
 Section language.
   Context {Λ : language}.
   Implicit Types v : val Λ.
@@ -331,3 +331,14 @@ End language.
 Global Arguments step_atomic {Λ ρ1 κ ρ2}.
 
 Notation pure_steps_tp := (Forall2 (rtc pure_step)).
+
+(* This definition makes sure that the fields of the [pre_language] record do not
+refer to the projections of the [language] record but to the actual fields
+of the [language] record. This is crucial for canonical structure search to
+work.
+
+Note that this trick no longer works when we switch to canonical projections
+because then the pattern match [let '...] will be desugared into projections. *)
+Definition PreOfLanguage (Λ : language) : pre_language :=
+  let '@Language (PreLanguage E V) St K of_val to_val prim mix := Λ in
+  PreLanguage E V.
diff --git a/iris_heap_lang/lang.v b/iris_heap_lang/lang.v
index bb686c72bbabec9c44fc49ff9cc1287d1281c9c5..b5c9b52a39f96341dc54db861ff3f2b30115086b 100644
--- a/iris_heap_lang/lang.v
+++ b/iris_heap_lang/lang.v
@@ -748,6 +748,7 @@ End heap_lang.
 Canonical Structure heap_ectxi_lang := EctxiLanguage heap_lang.heap_lang_mixin.
 Canonical Structure heap_ectx_lang := EctxLanguageOfEctxi heap_ectxi_lang.
 Canonical Structure heap_lang := LanguageOfEctx heap_ectx_lang.
+Canonical Structure heap_pre_lang := PreOfLanguage heap_lang.
 
 (* Prefer heap_lang names over ectx_language names. *)
 Export heap_lang.
diff --git a/tests/atomic.ref b/tests/atomic.ref
index 859bb6deb7e32902cf459b362c807d7e09ea45b6..6fdd318171d270f332470c2ed93bbcf4f23051e6 100644
--- a/tests/atomic.ref
+++ b/tests/atomic.ref
@@ -32,7 +32,7 @@ Tactic failure: iAuIntro: not all spatial assumptions are laterable.
   Σ : gFunctors
   heapG0 : heapG Σ
   P : val → iProp Σ
-  Φ : language.val heap_lang → iProp Σ
+  Φ : weakestpre.val heap_ectx_lang → iProp Σ
   ============================
   "AU" : AU << ∀ x : val, P x >> @ ⊤, ∅ << ∃ y : val, P y, COMM Φ #() >>
   --------------------------------------∗
@@ -43,7 +43,7 @@ Tactic failure: iAuIntro: not all spatial assumptions are laterable.
   Σ : gFunctors
   heapG0 : heapG Σ
   P : val → iProp Σ
-  Φ : language.val heap_lang → iProp Σ
+  Φ : weakestpre.val heap_ectx_lang → iProp Σ
   ============================
   _ : AACC << ∀ x : val, P x
               ABORT AU << ∀ x : val, P x >> @ ⊤, ∅
@@ -64,7 +64,7 @@ Tactic failure: iAuIntro: not all spatial assumptions are laterable.
   Σ : gFunctors
   heapG0 : heapG Σ
   l : loc
-  Φ : language.val heap_lang → iProp Σ
+  Φ : weakestpre.val heap_ectx_lang → iProp Σ
   ============================
   "AU" : AU << ∀ x : val, l ↦ x >> @ ⊤, ∅ << l ↦ x, COMM Φ #() >>
   --------------------------------------∗
@@ -75,7 +75,7 @@ Tactic failure: iAuIntro: not all spatial assumptions are laterable.
   Σ : gFunctors
   heapG0 : heapG Σ
   l : loc
-  Φ : language.val heap_lang → iProp Σ
+  Φ : weakestpre.val heap_ectx_lang → iProp Σ
   ============================
   _ : AACC << ∀ x : val, l ↦ x
               ABORT AU << ∀ x : val, l ↦ x >> @ ⊤, ∅ << l ↦ x, COMM Φ #() >> >> 
@@ -95,7 +95,7 @@ Tactic failure: iAuIntro: not all spatial assumptions are laterable.
   Σ : gFunctors
   heapG0 : heapG Σ
   l : loc
-  Φ : language.val heap_lang → iProp Σ
+  Φ : weakestpre.val heap_ectx_lang → iProp Σ
   ============================
   "AU" : AU << l ↦ #() >> @ ⊤, ∅ << ∃ y : val, l ↦ y, COMM Φ #() >>
   --------------------------------------∗
@@ -106,7 +106,7 @@ Tactic failure: iAuIntro: not all spatial assumptions are laterable.
   Σ : gFunctors
   heapG0 : heapG Σ
   l : loc
-  Φ : language.val heap_lang → iProp Σ
+  Φ : weakestpre.val heap_ectx_lang → iProp Σ
   ============================
   _ : AACC << l ↦ #()
               ABORT AU << l ↦ #() >> @ ⊤, ∅
@@ -127,7 +127,7 @@ Tactic failure: iAuIntro: not all spatial assumptions are laterable.
   Σ : gFunctors
   heapG0 : heapG Σ
   l : loc
-  Φ : language.val heap_lang → iProp Σ
+  Φ : weakestpre.val heap_ectx_lang → iProp Σ
   ============================
   "AU" : AU << l ↦ #() >> @ ⊤, ∅ << l ↦ #(), COMM Φ #() >>
   --------------------------------------∗
@@ -138,7 +138,7 @@ Tactic failure: iAuIntro: not all spatial assumptions are laterable.
   Σ : gFunctors
   heapG0 : heapG Σ
   l : loc
-  Φ : language.val heap_lang → iProp Σ
+  Φ : weakestpre.val heap_ectx_lang → iProp Σ
   ============================
   _ : AACC << l ↦ #()
               ABORT AU << l ↦ #() >> @ ⊤, ∅ << l ↦ #(), COMM Φ #() >> >> 
@@ -162,7 +162,7 @@ Tactic failure: iAuIntro: not all spatial assumptions are laterable.
   Σ : gFunctors
   heapG0 : heapG Σ
   l : loc
-  Φ : language.val heap_lang → iProp Σ
+  Φ : weakestpre.val heap_ectx_lang → iProp Σ
   ============================
   "AU" : AU << ∀ x : val, l ↦ x ∗ l ↦ x >> @ ⊤, ∅
             << ∃ y : val, l ↦ y, COMM Φ #() >>
@@ -183,7 +183,7 @@ Tactic failure: iAuIntro: not all spatial assumptions are laterable.
   Σ : gFunctors
   heapG0 : heapG Σ
   l : loc
-  Φ : language.val heap_lang → iProp Σ
+  Φ : weakestpre.val heap_ectx_lang → iProp Σ
   ============================
   "AU" : AU << ∀ x : val, l ↦ x ∗ l ↦ x ∗ l ↦ x ∗ l ↦ x ∗ l ↦ x ∗ l ↦ x >>
             @ ⊤, ∅ << ∃ y : val, l ↦ y, COMM Φ #() >>
@@ -205,7 +205,7 @@ Tactic failure: iAuIntro: not all spatial assumptions are laterable.
   Σ : gFunctors
   heapG0 : heapG Σ
   l : loc
-  Φ : language.val heap_lang → iProp Σ
+  Φ : weakestpre.val heap_ectx_lang → iProp Σ
   ============================
   _ : AU << ∀ xx : val, l ↦ xx ∗ l ↦ xx ∗ l ↦ xx >> @ ⊤, ∅
          << ∃ yyyy : val, l ↦ yyyy
@@ -228,7 +228,7 @@ Tactic failure: iAuIntro: not all spatial assumptions are laterable.
   Σ : gFunctors
   heapG0 : heapG Σ
   l : loc
-  Φ : language.val heap_lang → iProp Σ
+  Φ : weakestpre.val heap_ectx_lang → iProp Σ
   ============================
   "AU" : AU << ∀ x : val, l ↦ x ∗ l ↦ x ∗ l ↦ x ∗ l ↦ x >> @ ⊤, ∅
             << l ↦ x, COMM Φ #() >>
@@ -251,7 +251,7 @@ Tactic failure: iAuIntro: not all spatial assumptions are laterable.
   heapG0 : heapG Σ
   l : loc
   x : val
-  Φ : language.val heap_lang → iProp Σ
+  Φ : weakestpre.val heap_ectx_lang → iProp Σ
   ============================
   "AU" : AU << l ↦ x ∗ l ↦ x ∗ l ↦ x ∗ l ↦ x ∗ l ↦ x ∗ l ↦ x >> @ ⊤, ∅
             << ∃ y : val, l ↦ y, COMM Φ #() >>
@@ -274,7 +274,7 @@ Tactic failure: iAuIntro: not all spatial assumptions are laterable.
   heapG0 : heapG Σ
   l : loc
   x : val
-  Φ : language.val heap_lang → iProp Σ
+  Φ : weakestpre.val heap_ectx_lang → iProp Σ
   ============================
   "AU" : AU << l ↦ x ∗ l ↦ x ∗ l ↦ x ∗ l ↦ x ∗ l ↦ x ∗ l ↦ x >> @ ⊤, ∅
             << l ↦ #(), COMM Φ #() >>
@@ -297,7 +297,7 @@ Tactic failure: iAuIntro: not all spatial assumptions are laterable.
   heapG0 : heapG Σ
   l : loc
   xx, yyyy : val
-  Φ : language.val heap_lang → iProp Σ
+  Φ : weakestpre.val heap_ectx_lang → iProp Σ
   ============================
   "AU" : AU << l ↦ xx ∗ l ↦ xx ∗ l ↦ xx ∗ l ↦ xx ∗ l ↦ xx ∗ l ↦ xx ∗ l ↦ xx >>
             @ ⊤, ∅ << l ↦ yyyy, COMM Φ #() >>
@@ -321,7 +321,7 @@ Tactic failure: iAuIntro: not all spatial assumptions are laterable.
   heapG0 : heapG Σ
   l : loc
   xx, yyyy : val
-  Φ : language.val heap_lang → iProp Σ
+  Φ : weakestpre.val heap_ectx_lang → iProp Σ
   ============================
   "AU" : AU << l ↦ xx ∗ l ↦ xx ∗ l ↦ xx >> @ ⊤, ∅
             << l ↦ yyyy ∗ l ↦ xx ∗ l ↦ xx ∗ l ↦ xx ∗ l ↦ xx ∗ l ↦ xx ∗ l ↦ xx,
@@ -336,7 +336,7 @@ Tactic failure: iAuIntro: not all spatial assumptions are laterable.
   Σ : gFunctors
   heapG0 : heapG Σ
   P : val → iProp Σ
-  Φ : language.val heap_lang → iProp Σ
+  Φ : weakestpre.val heap_ectx_lang → iProp Σ
   ============================
   "AU" : ∃ x : val,
            P x
diff --git a/tests/heap_lang.ref b/tests/heap_lang.ref
index 64e37382064e716331fc28ad29f4b1d9f4bea613..4b3308817b31b8a1c636facdedf76cf8addb9e0f 100644
--- a/tests/heap_lang.ref
+++ b/tests/heap_lang.ref
@@ -292,7 +292,7 @@ WP #() #() @ E ∖ ↑N {{ _, |={E ∖ ↑N}=> ▷ P ∗ True }}
   Σ : gFunctors
   heapG0 : heapG Σ
   fun1, fun2, fun3 : expr
-  Φ : language.val heap_lang → iPropI Σ
+  Φ : weakestpre.val heap_pre_lang → iPropI Σ
   ============================
   --------------------------------------∗
   WP let: "val1" := fun1 #() in
@@ -305,7 +305,7 @@ WP #() #() @ E ∖ ↑N {{ _, |={E ∖ ↑N}=> ▷ P ∗ True }}
   Σ : gFunctors
   heapG0 : heapG Σ
   fun1, fun2, fun3 : expr
-  Φ : language.val heap_lang → iPropI Σ
+  Φ : weakestpre.val heap_pre_lang → iPropI Σ
   E : coPset
   ============================
   --------------------------------------∗