invalid patterns from local variables

Stream: lean4

[Jason Gross]

inductive Foo (Name : Type) where
| foo (x : Name)
structure Name where
  name : Unit
def bar : Foo Name → Type
| Foo.foo (Name.mk name) => _
-- 6:12: invalid pattern, constructor or constant marked with '[matchPattern]' expected

Is this expected? I realize that Name here is picking up the argument to Foo, which I guess is in context when elaborating the constructor patterns? (Btw, is there a way to see how it's elaborating Name.mk name? set_option trace.Elab true doesn't seem to do it, even with set_option pp.all true.) But that Name should perhaps be instantiated with the global Name?

[Leonardo de Moura]

Pushed a fix https://github.com/leanprover/lean4/commit/0e3aa2c29bab5e9321656920ac852cafd49a5344