Ah, the recursive TryMerge ⊠ instance was missing.

diaframe/steps/introduce_hyp.v

@@ -295,21 +295,6 @@ Section coq_tactics.
     rewrite HΔ //.
   Qed.
 
-  Global Instance mergable_persist_from_box P p P2 P3 :
-    MergePersist P p P2 P3 →
-    MergePersist (□ P)%I p P2 P3 | 5.
-  Proof.
-    rewrite /MergePersist => <-.
-    iIntros "[#$ $]".
-  Qed.
-  Global Instance mergable_consume_from_box P p P2 P3 :
-    MergeConsume P p P2 P3 →
-    MergeConsume (□ P)%I p P2 P3 | 5.
-  Proof.
-    rewrite /MergeConsume => <-.
-    iIntros "[#$ $]".
-  Qed.
-
   Lemma tac_introduce_hyp_not_mergable j Δ P1 a P1' R : 
     TCIf (TCAnd (IntoPersistent false P1 P1') (Affine P1))
         (TCEq a true) (TCAnd (TCEq a false) (TCEq P1' P1)) →

diaframe/steps/solve_instances.v

@@ -213,17 +213,34 @@ End drop_modal_instances.
 
 Section misc.
   Context {PROP : bi}.
+  Implicit Types P Q : PROP.
   (* TODO: where to put this? *)
 
-  Global Instance exclusive_prop_try_merge (Q : PROP) :
+  Global Instance exclusive_prop_try_merge Q :
     ExclusiveProp Q → TryMerge Q.
   Proof. exact (λ _, I). Qed.
 
-  Global Instance exclusive_prop_merge_false (Q : PROP) p : 
+  Global Instance exclusive_prop_merge_false Q p : 
     ExclusiveProp Q →
     MergeConsume Q p Q False%I.
   Proof.
     rewrite /ExclusiveProp /MergeConsume bi.intuitionistically_if_elim //.
   Qed.
+
+  Global Instance mergable_persist_from_box P p P2 P3 :
+    MergePersist P p P2 P3 →
+    MergePersist (□ P)%I p P2 P3 | 5.
+  Proof.
+    rewrite /MergePersist => <-.
+    iIntros "[#$ $]".
+  Qed.
+  Global Instance mergable_consume_from_box P p P2 P3 :
+    MergeConsume P p P2 P3 →
+    MergeConsume (□ P)%I p P2 P3 | 5.
+  Proof.
+    rewrite /MergeConsume => <-.
+    iIntros "[#$ $]".
+  Qed.
+  Global Instance try_merge_from_box P : TryMerge P → TryMerge (□ P)%I := id.
 End misc.