error creating a macro for a tactic

Stream: lean4

[Arthur Paulino]

I'm trying to create a tactic to simulate what was done in the example below:

macro "test_tac " n:ident " with " h:ident : tactic =>
  `(tactic| cases $n with | zero => simp only [$h] | succ $n => ?_)

example (n : Nat) (h : n = n) : n = n := by
  cases n with | zero => simp only [h] | succ n => ?_
  simp

example (n : Nat) (h : n = n) : n = n := by
  test_tac n with h
  -- tactic 'induction' failed, major premise type is not an inductive type
  --   ?m.5768
  -- n : Nat
  -- h : n = n
  -- x✝ : ?m.5768
  -- ⊢ n = n
  simp

But Lean is complaining about an error I don't understand. I tried using set_option hygiene false in with no success. Help is appreciated :pray: