diff --git a/theories/typing/lft_contexts.v b/theories/typing/lft_contexts.v
index eec88edf6202ba2f77ae69e79052ea0e12812a21..aab3d1c2f56e98c5a1d3845c8af2f1593d0ae739 100644
--- a/theories/typing/lft_contexts.v
+++ b/theories/typing/lft_contexts.v
@@ -437,7 +437,16 @@ End elctx_incl.
 
 Arguments elctx_incl {_ _ _} _%EL _%LL _%EL _%EL.
 
-Ltac solve_typing := eauto 100 with lrust_typing typeclass_instances || fail.
+(* We first try to solve everything without the merging rules, and
+   then start from scratch with them.
+
+   The reason is that we want we want the search proof search for
+   [tctx_extract_hasty] to suceed even if the type is an evar, and
+   merging makes it diverge in this case. *)
+Ltac solve_typing :=
+  (eauto 100 with lrust_typing typeclass_instances; fail) ||
+  (eauto 100 with lrust_typing lrust_typing_merge typeclass_instances; fail).
+Create HintDb lrust_typing_merge.
 
 Hint Constructors Forall Forall2 elem_of_list : lrust_typing.
 Hint Resolve
diff --git a/theories/typing/product_split.v b/theories/typing/product_split.v
index a6a3262f20b4f184cdc3b971f60efe8d0a4c331b..154dca9f6e688d6fe2a454e22aea104ebfccb38f 100644
--- a/theories/typing/product_split.v
+++ b/theories/typing/product_split.v
@@ -388,14 +388,31 @@ Section product_split.
   Proof. auto using tctx_extract_merge_ptr_prod, tctx_merge_shr_prod. Qed.
 End product_split.
 
-(* We make sure that splitting and merging are applied after everything else. *)
+(* We make sure that splitting is tried before borrowing, so that not
+   the entire product is borrowed when only a part is needed. *)
 Hint Resolve tctx_extract_split_own_prod2 tctx_extract_split_uniq_prod2
              tctx_extract_split_shr_prod2 tctx_extract_split_own_prod
              tctx_extract_split_uniq_prod tctx_extract_split_shr_prod
-             tctx_extract_merge_own_prod2 tctx_extract_merge_uniq_prod2
-             tctx_extract_merge_shr_prod2 tctx_extract_merge_own_prod
-             tctx_extract_merge_uniq_prod tctx_extract_merge_shr_prod
-     | 100 : lrust_typing.
+    | 5 : lrust_typing.
+
+(* Merging is also tried after everything, except
+   [tctx_extract_hasty_further]. Moreover, it is placed in a
+   difference hint db. The reason is that it can make the proof search
+   diverge if the type is an evar. *)
+(* We declare them as [Hint Extern] instead of [Hint Resolve],
+   otherwise unification with unrelated goals takes forever to fail... *)
+Hint Extern 40 (tctx_extract_hasty _ _ _ (own _ (product2 _ _)) _ _) =>
+  eapply tctx_extract_merge_own_prod2 : lrust_typing_merge.
+Hint Extern 40 (tctx_extract_hasty _ _ _ (&uniq{_}product2 _ _) _ _) =>
+  eapply tctx_extract_merge_uniq_prod2 : lrust_typing_merge.
+Hint Extern 40 (tctx_extract_hasty _ _ _ (&shr{_}product2 _ _) _ _) =>
+  eapply tctx_extract_merge_shr_prod2 : lrust_typing_merge.
+Hint Extern 40 (tctx_extract_hasty _ _ _ (own _ (Π _)) _ _) =>
+  eapply tctx_extract_merge_own_prod : lrust_typing_merge.
+Hint Extern 40 (tctx_extract_hasty _ _ _ (&uniq{_}Π _) _ _) =>
+  eapply tctx_extract_merge_uniq_prod : lrust_typing_merge.
+Hint Extern 40 (tctx_extract_hasty _ _ _ (&shr{_}Π _) _ _) =>
+  eapply tctx_extract_merge_shr_prod : lrust_typing_merge.
 
 Hint Extern 0
      (tctx_extract_hasty _ _ _ _ (hasty_ptr_offsets _ _ _ _) _) =>
diff --git a/theories/typing/tests/unbox.v b/theories/typing/tests/unbox.v
index 73a22b1ac08c722717ecc3d6e74c9e2a14dfbbba..aca132b1ba7b570770cb0627f721681c5af8f10f 100644
--- a/theories/typing/tests/unbox.v
+++ b/theories/typing/tests/unbox.v
@@ -22,7 +22,7 @@ Section unbox.
     eapply type_deref; try solve_typing. by apply read_own_move. done.
       intros b'; simpl_subst.
     eapply type_deref_uniq_own; (try solve_typing)=>bx; simpl_subst.
-    eapply (type_letalloc_1 (&uniq{α}int)); (try solve_typing)=>r. simpl_subst.
+    eapply type_letalloc_1; (try solve_typing)=>r. simpl_subst.
     eapply type_delete; try solve_typing.
     eapply (type_jump [_]); solve_typing.
   Qed.
diff --git a/theories/typing/type_context.v b/theories/typing/type_context.v
index d9844bd93dc52fede8aa82bfe69d6f577b03a2ef..d0ac76e054d01769195f5fb195db5a8ae7e8a2c1 100644
--- a/theories/typing/type_context.v
+++ b/theories/typing/type_context.v
@@ -364,4 +364,4 @@ Hint Resolve tctx_extract_blocked_here tctx_extract_blocked_cons
    cannot enforce this using [Hint Resolve]. Cf:
        https://coq.inria.fr/bugs/show_bug.cgi?id=5299 *)
 Hint Extern 2 (tctx_extract_hasty _ _ _ _ ((_ ◁ _) :: _) _) =>
-  eapply tctx_extract_hasty_here_eq.
+  eapply tctx_extract_hasty_here_eq : lrust_typing.