diff --git a/theories/utils/switch.v b/theories/utils/switch.v
index d988a225c7f284845530e952adeeca5d647fb0e1..4e4c60298e67ace7da129105af18a81059e3f42b 100644
--- a/theories/utils/switch.v
+++ b/theories/utils/switch.v
@@ -54,7 +54,9 @@ Qed.
 Lemma switch_lams_spec `{heapGS Σ} y i n ws vs e Φ :
   length vs = n →
   WP subst_map (map_string_seq y i vs ∪ ws) e {{ Φ }} -∗
-  WP subst_map ws (switch_lams y i n e) {{ w, WP fill (AppLCtx <$> vs) w {{ Φ }} }}.
+  WP subst_map ws (switch_lams y i n e) {{ w, WP fill (AppLCtx <$> vs) (w : val) {{ Φ }} }}.
+  (* FIXME: Once we depend on Coq 8.13, make WP notation use [v closed binder]
+       so that we can add a type annotation at the [w] binder here. *)
 Proof.
   iIntros (<-) "H".
   iInduction vs as [|v vs] "IH" forall (i ws); csimpl.