Pattern matching limitations?

Stream: lean4

[François G. Dorais]

In the following example, the definition of Path.unmap fails with the terse message:

error: failed to compile pattern matching, constructor expected
f a:cross:

The Lean 3 analogue of this example works fine.

inductive Tree (α : Type _) : Type _
| leaf : α → Tree α
| branch : Tree α → Tree α → Tree α

inductive Path {α : Type _} : Tree α → Type _
| term (x : α) : Path (Tree.leaf x)
| left (tl tr : Tree α) : Path tl → Path (Tree.branch tl tr)
| right (tl tr : Tree α) : Path tr → Path (Tree.branch  tl tr)

section map
variables {α : Type _} {β : Type _} (f : α → β)

protected def Tree.map : Tree α → Tree β
| Tree.leaf x => Tree.leaf (f x)
| Tree.branch tl tr => Tree.branch (Tree.map tl) (Tree.map tr)

protected def Path.map : {t : Tree α} → Path t → Path (t.map f)
| Tree.leaf _, Path.term x => Path.term (f x)
| Tree.branch _ _, Path.left tl tr p => Path.left (tl.map f) (tr.map f) (Path.map p)
| Tree.branch _ _, Path.right tl tr p => Path.right (tl.map f) (tr.map f) (Path.map p)

protected def Path.unmap : {t : Tree α} → Path (t.map f) → Path t
| Tree.leaf x, Path.term _ => Path.term x
| Tree.branch tl tr, Path.left _ _ p => Path.left tl tr (Path.unmap p)
| Tree.branch tl tr, Path.right _ _ p => Path.right tl tr (Path.unmap p)

end map

This is testing the limits of Lean's pattern matching abilities. Indeed, I was pleasantly surprised when the original Lean 3 version of this worked smoothly. In any case, the Lean 4 error message isn't very detailed and doesn't help much with fixing the code. I don't know if there is a workaround I could use, or if this is work in progress. Thoughts?

[François G. Dorais]

Option trace.Meta.Match shows that Lean 4 does correctly fill in the blanks. I haven't yet found an option to trace where the compiler fails.

[Leonardo de Moura]

Thanks. Pushed a fix, and added your example to the test suite.

[François G. Dorais]

Thank you Leo!