More test cases

Author: nomeata

tests/lean/run/match1.lean

@@ -162,6 +162,27 @@ match n, parity n with
 | _, Parity.even j => false :: natToBin j
 | _, Parity.odd  j => true  :: natToBin j
 
+-- Even with sparse matching, this can break
+
+/--
+error: Tactic `cases` failed with a nested error:
+Dependent elimination failed: Failed to solve equation
+  n✝¹.succ = n✝.add n✝
+at case `Parity.even` after processing
+  (Nat.succ _), _
+the dependent pattern matcher can solve the following kinds of equations
+- <var> = <term> and <term> = <var>
+- <term> = <term> where the terms are definitionally equal
+- <constructor> = <constructor>, examples: List.cons x xs = List.cons y ys, and List.cons x xs = List.nil
+-/
+#guard_msgs in
+partial def natToBinBad2 (n : Nat) : List Bool :=
+match n, parity n with
+| 0, _             => []
+| .succ 0, _       => [true]
+| _, Parity.even j => false :: natToBin j
+| _, Parity.odd  j => true  :: natToBin j
+
 partial def natToBin2 (n : Nat) : List Bool :=
 match n, parity n with
 | _, Parity.even 0 => []