fun+match with implicit

Stream: lean4

[Wojciech Nawrocki]

The fun+match syntax doesn't seem to work with implicit lambdas. For example

structure Foo where
  func {α : Type} : α → α

def inst1 : Foo where
  func a := a -- works

def inst2 : Foo where
  func := fun a => a -- works

def inst3 : Foo where
  func := fun
    | a => a
  /- type mismatch
    a
  has type
    Type : Type 1
  but is expected to have type
    x✝ → x✝ : Type -/

Is this expected or a bug?

[Mac]

@Wojciech Nawrocki This works:

def inst3 : Foo where
  func := fun
    | _, a => a

It appears that when using fun+match implicit arguments become part of the match.

[Mac]

I think this may be purposeful to make the result of the match affect the implicit arguments.