MetaM の中で throw ができないという問題

[Seasawher]

section
  open Lean Parser

  /-- `s : String` をパースして `Syntax` の項を得る。`cat` は構文カテゴリ。-/
  def parse (cat : Name) (s : String) : MetaM Syntax := do
    ofExcept <| runParserCategory (← getEnv) cat s

  /-- 文字列をパースするコマンド -/
  macro "#parse " s:str : command => `(command|
    #eval show MetaM Unit from do
      let cats := #[`tactic, `term, `command, `doElem]
      for cat in cats do
        try
          let stx ← parse cat $s
          IO.println <| toString stx
          return
        catch _ =>
          continue
      throw <| IO.userError s!"failed to parse {$s}"
      -- IO.println s!"failed to parse {$s}"
    )
end

-- 単に連結するとパース不可でエラーになる
/-⋆-//--
error: failed to synthesize
  MonadExcept IO.Error Lean.MetaM
Additional diagnostic information may be available using the `set_option diagnostics true` command.
-/
#guard_msgs in --#
#parse "1 ⋄ 2 ⋄ 3"