pattern variable issue?

Stream: lean4

[Scott Kovach]

myId surprised me:

def myId : List α → List α
| List.nil => List.nil -- i.e. x => x

def constNil : List α → List α
| List.nil => List.nil
| List.cons x y => List.nil

def failing1 : List α → List α
| [] => List.nil

def failing2 : List α → List α
| x => List.nil
| foo.bar => List.nil -- "invalid pattern variable"

I'm guessing that's not intended?

[Wojciech Nawrocki]

The following also works:

def myId : List α → List α
| foo.bar => foo.bar

Yes, this probably shouldn't compile.

[Leonardo de Moura]

Pushed a fix: https://github.com/leanprover/lean4/commit/1ebf69e1634a75901bf9f47b7aeec6c8fc624072