pure_exec_ctx is a too general instance

theories/program_logic/ectx_language.v

@@ -205,6 +205,12 @@ Section ectx_language.
       eexists e2', σ2, efs. by apply head_prim_step.
     - intros σ1 e2' σ2 efs ? ?%head_reducible_prim_step; eauto.
   Qed.
+
+  Global Instance pure_exec_fill K e1 e2 φ :
+    PureExec φ e1 e2 →
+    PureExec φ (fill K e1) (fill K e2).
+  Proof. apply: pure_exec_ctx. Qed.
+
 End ectx_language.
 
 Arguments ectx_lang : clear implicits.

theories/program_logic/language.v

@@ -140,7 +140,8 @@ Section language.
     PureExec P e1 e2.
   Proof. intros HPE. split; intros; eapply HPE; eauto. Qed.
 
-  Global Instance pure_exec_ctx K `{LanguageCtx Λ K} e1 e2 φ :
+  (* We do not make this an instance because it is awfully general. *)
+  Lemma pure_exec_ctx K `{LanguageCtx Λ K} e1 e2 φ :
     PureExec φ e1 e2 →
     PureExec φ (K e1) (K e2).
   Proof.