Extensible macros and error message

Stream: Is there code for X?

[Joachim Breitner]

Consider this way of extending a tactic like rfl:

macro "test" : tactic => `(tactic| eq_refl)
macro_rules | `(tactic| test) => `(tactic| exact HEq.rfl)
example : P := by test

This produces the error message

type mismatch
  HEq.rfl
has type
  HEq ?m.1135 ?m.1135 : Prop
but is expected to have type
  P : Sort ?u.1128

which is not really helpful for the user that wrote rfl.

Without the second line you get

tactic 'rfl' failed, equality expected
  P
P: Sort ?u.547
⊢ P

which is a bit better.

Ideally, though, one should be able to indicate that “if all registered rfl tactics fail, print message …”.
Unfortunately, it seems that macro_rules tries all expansions in sequence, firstly declared first, and then presents the error message from the last one, so one cannot reliably achieve this by adding fail "…" as the first macro.

Is there a simple way out? I can do it with two macros, one to be called by the user, and one to be extended, but I wonder if there is a better idiom:

macro "testImpl" : tactic => `(tactic| eq_refl)
macro_rules | `(tactic| testImpl) => `(tactic| exact HEq.rfl) -- extend this only!
macro "test" : tactic => `(tactic| testImpl)
macro_rules | `(tactic| test) => `(tactic| fail "test failed")
example : P := by test

[Damiano Testa]

This has come up before. I think that the rule is that the attempts are made in reverse chronological order, until one tactic succeeds. If they all fail, the error message is the one of the first tactic.

Not always this is ideal, but this I think is the status quo.