Is nested pattern matching not possible?

Stream: lean4

[Daniel Fabian]

I'm trying out lean 4 and I'm getting an error in a pattern that I thought should work:

inductive color
| red
| black

inductive node where
| leaf : node
| tree (color : color) : node

def balance : color → node → node
-- the following line fails with: invalid pattern variable, must be atomic
| color.red, node.tree color.red => node.leaf
-- the following line works fine
--| color.red, node.tree anyColor => node.leaf
| _, _ => node.leaf

Any idea why this doesn't work?

[Julian Berman]

This seems to work for me (well produce no errors at least) on Lean (version 4.0.0-nightly-2021-03-13, commit 472c5fb900ea, Release)

[Daniel Fabian]

indeed, when I updated lean4, I no longer get the error, so it must have been fixed recently. Interesting.