Trying to clarify priorities of mergeing and splitting lemmas. Clearly, this is still not optimal.

opam.pins

-coq-iris https://gitlab.mpi-sws.org/FP/iris-coq 587cde167492b4b25f1d11ca7797c2087527abd6
+coq-iris https://gitlab.mpi-sws.org/FP/iris-coq be81fb92a76f31ca656f8dad37122843f58884cf

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

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 _ _ _ _) _) =>

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.

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.