feat: failing macros to show error from first registered rule (#3771)

fixes #3770

Also start `rfl` with a `fail` message that is hopefully more helpful
than what we get now (see updated test output). This would be a cheaper
way to address #3302 without changing the implementation of rfl (as
tried in #3714).

src/Init/Tactics.lean

@@ -354,6 +354,9 @@ macro:1 x:tactic tk:" <;> " y:tactic:2 : tactic => `(tactic|
     with_annotate_state $tk skip
     all_goals $y:tactic)
 
+/-- `fail msg` is a tactic that always fails, and produces an error using the given message. -/
+syntax (name := fail) "fail" (ppSpace str)? : tactic
+
 /-- `eq_refl` is equivalent to `exact rfl`, but has a few optimizations. -/
 syntax (name := eqRefl) "eq_refl" : tactic
 
@@ -365,8 +368,12 @@ for new reflexive relations.
 Remark: `rfl` is an extensible tactic. We later add `macro_rules` to try different
 reflexivity theorems (e.g., `Iff.rfl`).
 -/
-macro "rfl" : tactic => `(tactic| eq_refl)
+macro "rfl" : tactic => `(tactic| fail "The rfl tactic failed. Possible reasons:
+- The goal is not a reflexive relation (neither `=` nor a relation with a @[refl] lemma).
+- The arguments of the relation are not equal.
+Try using the reflexivitiy lemma for your relation explicitly, e.g. `exact Eq.rfl`.")
 
+macro_rules | `(tactic| rfl) => `(tactic| eq_refl)
 macro_rules | `(tactic| rfl) => `(tactic| exact HEq.rfl)
 
 /--
@@ -907,9 +914,6 @@ example : ∀ x : Nat, x = x := by unhygienic
 -/
 macro "unhygienic " t:tacticSeq : tactic => `(tactic| set_option tactic.hygienic false in $t)
 
-/-- `fail msg` is a tactic that always fails, and produces an error using the given message. -/
-syntax (name := fail) "fail" (ppSpace str)? : tactic
-
 /--
 `checkpoint tac` acts the same as `tac`, but it caches the input and output of `tac`,
 and if the file is re-elaborated and the input matches, the tactic is not re-run and

src/Lean/Elab/Tactic/Basic.lean

@@ -158,8 +158,9 @@ partial def evalTactic (stx : Syntax) : TacticM Unit := do
     | _ => throwError m!"unexpected tactic{indentD stx}"
 where
     throwExs (failures : Array EvalTacticFailure) : TacticM Unit := do
-     if let some fail := failures[0]? then
-       -- Recall that `failures[0]` is the highest priority evalFn/macro
+     if h : 0 < failures.size  then
+       -- For macros we want to report the error from the first registered / last tried rule (#3770)
+       let fail := failures[failures.size-1]
        fail.state.restore (restoreInfo := true)
        throw fail.exception -- (*)
      else

tests/lean/run/issue3770.lean

@@ -0,0 +1,23 @@
+macro "foo" : tactic => `(tactic|fail "first")
+macro_rules | `(tactic|foo) => `(tactic|exact 1)
+macro_rules | `(tactic|foo) => `(tactic|fail "middle")
+macro_rules | `(tactic|foo) => `(tactic|exact 2)
+macro_rules | `(tactic|foo) => `(tactic|fail "last")
+
+def what_is_foo : Nat := by foo
+
+/-- info: 2 -/
+#guard_msgs in
+#eval what_is_foo
+
+
+macro "bar" : tactic => `(tactic|fail "first")
+macro_rules | `(tactic|bar) => `(tactic|fail "middle")
+macro_rules | `(tactic|bar) => `(tactic|fail "last")
+
+/--
+error: first
+⊢ Nat
+-/
+#guard_msgs in
+def what_is_bar : Nat := by bar

tests/lean/runTacticMustCatchExceptions.lean.expected.out

@@ -1,36 +1,39 @@
-runTacticMustCatchExceptions.lean:2:25-2:28: error: type mismatch
-  Iff.rfl
-has type
-  ?m ↔ ?m : Prop
-but is expected to have type
-  1 ≤ a + b : Prop
-runTacticMustCatchExceptions.lean:3:25-3:28: error: type mismatch
-  Iff.rfl
-has type
-  ?m ↔ ?m : Prop
-but is expected to have type
-  a + b ≤ b : Prop
-runTacticMustCatchExceptions.lean:4:25-4:28: error: type mismatch
-  Iff.rfl
-has type
-  ?m ↔ ?m : Prop
-but is expected to have type
-  b ≤ 2 : Prop
-runTacticMustCatchExceptions.lean:9:18-9:21: error: type mismatch
-  Iff.rfl
-has type
-  ?m ↔ ?m : Prop
-but is expected to have type
-  1 ≤ a + b : Prop
-runTacticMustCatchExceptions.lean:10:14-10:17: error: type mismatch
-  Iff.rfl
-has type
-  ?m ↔ ?m : Prop
-but is expected to have type
-  a + b ≤ b : Prop
-runTacticMustCatchExceptions.lean:11:14-11:17: error: type mismatch
-  Iff.rfl
-has type
-  ?m ↔ ?m : Prop
-but is expected to have type
-  b ≤ 2 : Prop
+runTacticMustCatchExceptions.lean:2:25-2:28: error: The rfl tactic failed. Possible reasons:
+- The goal is not a reflexive relation (neither `=` nor a relation with a @[refl] lemma).
+- The arguments of the relation are not equal.
+Try using the reflexivitiy lemma for your relation explicitly, e.g. `exact Eq.rfl`.
+a b : Nat
+⊢ 1 ≤ a + b
+runTacticMustCatchExceptions.lean:3:25-3:28: error: The rfl tactic failed. Possible reasons:
+- The goal is not a reflexive relation (neither `=` nor a relation with a @[refl] lemma).
+- The arguments of the relation are not equal.
+Try using the reflexivitiy lemma for your relation explicitly, e.g. `exact Eq.rfl`.
+a b : Nat
+this : 1 ≤ a + b
+⊢ a + b ≤ b
+runTacticMustCatchExceptions.lean:4:25-4:28: error: The rfl tactic failed. Possible reasons:
+- The goal is not a reflexive relation (neither `=` nor a relation with a @[refl] lemma).
+- The arguments of the relation are not equal.
+Try using the reflexivitiy lemma for your relation explicitly, e.g. `exact Eq.rfl`.
+a b : Nat
+this✝ : 1 ≤ a + b
+this : a + b ≤ b
+⊢ b ≤ 2
+runTacticMustCatchExceptions.lean:9:18-9:21: error: The rfl tactic failed. Possible reasons:
+- The goal is not a reflexive relation (neither `=` nor a relation with a @[refl] lemma).
+- The arguments of the relation are not equal.
+Try using the reflexivitiy lemma for your relation explicitly, e.g. `exact Eq.rfl`.
+a b : Nat
+⊢ 1 ≤ a + b
+runTacticMustCatchExceptions.lean:10:14-10:17: error: The rfl tactic failed. Possible reasons:
+- The goal is not a reflexive relation (neither `=` nor a relation with a @[refl] lemma).
+- The arguments of the relation are not equal.
+Try using the reflexivitiy lemma for your relation explicitly, e.g. `exact Eq.rfl`.
+a b : Nat
+⊢ a + b ≤ b
+runTacticMustCatchExceptions.lean:11:14-11:17: error: The rfl tactic failed. Possible reasons:
+- The goal is not a reflexive relation (neither `=` nor a relation with a @[refl] lemma).
+- The arguments of the relation are not equal.
+Try using the reflexivitiy lemma for your relation explicitly, e.g. `exact Eq.rfl`.
+a b : Nat
+⊢ b ≤ 2