quote4 match error

Stream: lean4

[David Renshaw]

import Lean
import Qq.Match

open Lean Elab.Tactic
open Qq

-- this works
def foo (p : Q(Prop)) : TacticM Unit := match p with
| ~q(($a : Prop) ∧ ($b : Prop)) => pure ()
| _ => pure ()

-- this doesn't work
def bar (p : Q(Prop)) : TacticM Unit := match p with
| ~q(($a : Prop) → ($b : Prop)) => do pure ()
| _ => pure ()

/-
application type mismatch
  sorryAx (TacticM Unit)
argument has type
  Type
but function has type
  (α : Sort u_1) → optParam Bool false → α
-/

What's going on here? Why can't I match on (_ -> _) ?