Improve error messages of `iApply` and write some docs.

tests/proofmode.ref

@@ -521,3 +521,29 @@ In nested Ltac calls to "iApply (open_constr)",
 "tac" (bound to fun H => iApplyHyp H) and "iApplyHyp (constr)", last call
 failed.
 Tactic failure: iApply: cannot apply P.
+"iApply_fail_not_affine_1"
+     : string
+The command has indeed failed with message:
+In nested Ltac calls to "iApply (open_constr)",
+"iPoseProofCore (open_constr) as (constr) (constr) (tactic)",
+"<iris.proofmode.ltac_tactics.iPoseProofCore_go>",
+"<iris.proofmode.ltac_tactics.iPoseProofCore_go>",
+"<iris.proofmode.ltac_tactics.iPoseProofCore_go>", 
+"goal_tac" (bound to fun _ => spec_tac ltac:(()); [ .. | tac Htmp ]), 
+"tac" (bound to fun H => iApplyHyp H) and "iApplyHyp (constr)", last call
+failed.
+Tactic failure: iApply: Q
+not absorbing and the remaining hypotheses not affine.
+"iApply_fail_not_affine_2"
+     : string
+The command has indeed failed with message:
+In nested Ltac calls to "iApply (open_constr)",
+"iPoseProofCore (open_constr) as (constr) (constr) (tactic)",
+"<iris.proofmode.ltac_tactics.iPoseProofCore_go>",
+"<iris.proofmode.ltac_tactics.iPoseProofCore_go>",
+"<iris.proofmode.ltac_tactics.iPoseProofCore_go>", 
+"goal_tac" (bound to fun _ => spec_tac ltac:(()); [ .. | tac Htmp ]), 
+"tac" (bound to fun H => iApplyHyp H) and "iApplyHyp (constr)", last call
+failed.
+Tactic failure: iApply: Q
+not absorbing and the remaining hypotheses not affine.

tests/proofmode.v

@@ -741,4 +741,11 @@ Check "iApply_fail".
 Lemma iApply_fail P Q : P -∗ Q.
 Proof. iIntros "HP". Fail iApply "HP". Abort.
 
+Check "iApply_fail_not_affine_1".
+Lemma iApply_fail_not_affine_1 P Q : P -∗ Q -∗ Q.
+Proof. iIntros "HP HQ". Fail iApply "HQ". Abort.
+
+Check "iApply_fail_not_affine_2".
+Lemma iApply_fail_not_affine_1 P Q R : P -∗ R -∗ (R -∗ Q) -∗ Q.
+Proof. iIntros "HP HR HQ". Fail iApply ("HQ" with "HR"). Abort.
 End error_tests.

theories/proofmode/ltac_tactics.v

@@ -819,20 +819,50 @@ Tactic Notation "iPoseProofCore" open_constr(lem)
   | false => iPoseProofCore_go Htmp t spec_tac; [..| tac Htmp ]
   end.
 
-(** * Apply *)
-Tactic Notation "iApplyHyp" constr(H) :=
-  let rec go H := first
+(** [iApply lem] takes an argument [lem : P₁ -∗ .. -∗ Pₙ -∗ Q] (after the
+specialization patterns in [lem] have been executed), where [Q] should match
+the goal, and generates new goals [P1] ... [Pₙ]. Depending on the number of
+premises [n], the tactic will have the following behavior:
+
+- If [n = 0], it will immediately solve the goal (i.e. it will not generate any
+  subgoals). When working in a general BI, this means that the tactic can fail
+  in case there are non-affine spatial hypotheses in the context prior to using
+  the [iApply] tactic. Note that if [n = 0], the tactic behaves exactly like
+  [iExact lem].
+- If [n > 0] it will generate a goals [P₁] ... [Pₙ]. All spatial hypotheses
+  will be transferred to the last goal, i.e. [Pₙ]; the other goals will receive
+  no spatial hypotheses. If you want to control more precisely how the spatial
+  hypotheses are subdivided, you should add additional introduction patterns to
+  [lem]. *)
+
+(* The helper [iApplyHypExact] takes care of the [n=0] case. It fails with level
+0 if we should proceed to the [n > 0] case, and with level 1 if there is an
+actual error. *)
+Local Ltac iApplyHypExact H :=
+  first
+    [eapply tac_assumption with _ H _ _; (* (i:=H) *)
+       [pm_reflexivity || fail 1
+       |iSolveTC || fail 1
+       |pm_reduce; iSolveTC]
+    |lazymatch iTypeOf H with
+     | Some (_,?Q) =>
+        fail 2 "iApply:" Q "not absorbing and the remaining hypotheses not affine"
+     end].
+Local Ltac iApplyHypLoop H :=
+  first
     [eapply tac_apply with _ H _ _ _;
       [pm_reflexivity
       |iSolveTC
-      |pm_prettify (* reduce redexes created by instantiation *)
-      ]
-    |iSpecializePat H "[]"; last go H] in
-  iExact H ||
-  go H ||
-  lazymatch iTypeOf H with
-  | Some (_,?Q) => fail "iApply: cannot apply" Q
-  end.
+      |pm_prettify (* reduce redexes created by instantiation *)]
+    |iSpecializePat H "[]"; last iApplyHypLoop H].
+
+Tactic Notation "iApplyHyp" constr(H) :=
+  first
+    [iApplyHypExact H
+    |iApplyHypLoop H
+    |lazymatch iTypeOf H with
+     | Some (_,?Q) => fail 1 "iApply: cannot apply" Q
+     end].
 
 Tactic Notation "iApply" open_constr(lem) :=
   iPoseProofCore lem as false true (fun H => iApplyHyp H).