Update test

Author: nomeata

tests/lean/run/issue10749.lean

@@ -12,7 +12,7 @@ def test (a : List Nat) : Nat :=
 /--
 info: def test.match_1.{u_1} : (motive : List Nat → Sort u_1) →
   (a : List Nat) → ((x : List Nat) → motive x) → (Unit → motive []) → motive a :=
-fun motive a h_1 h_2 => h_1 a
+fun motive a h_1 h_2 => List.casesOn a (h_1 []) fun head tail => h_1 (head :: tail)
 -/
 #guard_msgs in #print test.match_1
 
@@ -31,7 +31,7 @@ info: def test2.match_1.{u_1} : (motive : List Nat → List Nat → Sort u_1) 
             (tail : List Nat) → (head_1 : Nat) → (tail_1 : List Nat) → motive (head :: tail) (head_1 :: tail_1)) →
           motive a b :=
 fun motive a b h_1 h_2 h_3 =>
-  List.casesOn a (h_1 b) fun head tail =>
+  List.casesOn a (List.casesOn b (h_1 []) fun head tail => h_1 (head :: tail)) fun head tail =>
     List.casesOn b (h_2 (head :: tail)) fun head_1 tail_1 => h_3 head tail head_1 tail_1
 -/
 #guard_msgs in #print test2.match_1
@@ -51,7 +51,8 @@ info: def test3.match_1.{u_1} : (motive : List Nat → Bool → Sort u_1) →
       ((x : List Nat) → motive x true) →
         ((x : Bool) → motive [] x) → ((x : List Nat) → (x_1 : Bool) → motive x x_1) → motive a b :=
 fun motive a b h_1 h_2 h_3 =>
-  Bool.casesOn b (List.casesOn a (h_2 false) fun head tail => h_3 (head :: tail) false) (h_1 a)
+  List.casesOn a (Bool.casesOn b (h_2 false) (h_1 [])) fun head tail =>
+    Bool.casesOn b (h_3 (head :: tail) false) (h_1 (head :: tail))
 -/
 #guard_msgs in #print test3.match_1
 
@@ -78,14 +79,29 @@ info: def test4.match_1.{u_1} : (motive : Bool → Bool → Bool → Bool → Bo
             ((x x_5 x_6 x_7 : Bool) → motive true x x_5 x_6 x_7) →
               ((x x_5 x_6 x_7 x_8 : Bool) → motive x x_5 x_6 x_7 x_8) → motive x x_1 x_2 x_3 x_4 :=
 fun motive x x_1 x_2 x_3 x_4 h_1 h_2 h_3 h_4 h_5 h_6 =>
-  Bool.casesOn x_4
-    (Bool.casesOn x_3
+  Bool.casesOn x
+    (Bool.casesOn x_1
       (Bool.casesOn x_2
-        (Bool.casesOn x_1 (Bool.casesOn x (h_6 false false false false false) (h_5 false false false false))
-          (h_4 x false false false))
-        (h_3 x x_1 false false))
-      (h_2 x x_1 x_2 false))
-    (h_1 x x_1 x_2 x_3)
+        (Bool.casesOn x_3 (Bool.casesOn x_4 (h_6 false false false false false) (h_1 false false false false))
+          (Bool.casesOn x_4 (h_2 false false false false) (h_1 false false false true)))
+        (Bool.casesOn x_3 (Bool.casesOn x_4 (h_3 false false false false) (h_1 false false true false))
+          (Bool.casesOn x_4 (h_2 false false true false) (h_1 false false true true))))
+      (Bool.casesOn x_2
+        (Bool.casesOn x_3 (Bool.casesOn x_4 (h_4 false false false false) (h_1 false true false false))
+          (Bool.casesOn x_4 (h_2 false true false false) (h_1 false true false true)))
+        (Bool.casesOn x_3 (Bool.casesOn x_4 (h_3 false true false false) (h_1 false true true false))
+          (Bool.casesOn x_4 (h_2 false true true false) (h_1 false true true true)))))
+    (Bool.casesOn x_1
+      (Bool.casesOn x_2
+        (Bool.casesOn x_3 (Bool.casesOn x_4 (h_5 false false false false) (h_1 true false false false))
+          (Bool.casesOn x_4 (h_2 true false false false) (h_1 true false false true)))
+        (Bool.casesOn x_3 (Bool.casesOn x_4 (h_3 true false false false) (h_1 true false true false))
+          (Bool.casesOn x_4 (h_2 true false true false) (h_1 true false true true))))
+      (Bool.casesOn x_2
+        (Bool.casesOn x_3 (Bool.casesOn x_4 (h_4 true false false false) (h_1 true true false false))
+          (Bool.casesOn x_4 (h_2 true true false false) (h_1 true true false true)))
+        (Bool.casesOn x_3 (Bool.casesOn x_4 (h_3 true true false false) (h_1 true true true false))
+          (Bool.casesOn x_4 (h_2 true true true false) (h_1 true true true true)))))
 -/
 #guard_msgs in
 #print test4.match_1

tests/lean/run/issue10794.lean

@@ -1,19 +1,15 @@
 /--
-error: Dependent elimination failed: Type mismatch when solving this alternative: it has type
-  motive false
-but is expected to have type
-  motive b✝
+error: Dependent match elimination failed: Could not solve constraints
+  true ≋ false
 -/
 #guard_msgs in
 def test1 b := match b with
   | .(false) => 1
   | true => 2
 
 /--
-error: Dependent elimination failed: Type mismatch when solving this alternative: it has type
-  motive false ⋯
-but is expected to have type
-  motive x✝¹ x✝
+error: Dependent match elimination failed: Could not solve constraints
+  true ≋ false
 -/
 #guard_msgs in
 def test2 : (b : Bool) → (h : b = false) → Nat

tests/lean/run/match1.lean

@@ -137,9 +137,9 @@ partial def natToBin' : (n : Nat) → List Bool
 /--
 error: Tactic `cases` failed with a nested error:
 Dependent elimination failed: Failed to solve equation
-  n✝¹.succ = n✝.add n✝
+  Nat.zero = n✝.add n✝
 at case `Parity.even` after processing
-  (Nat.succ _), _
+  Nat.zero, _
 the dependent pattern matcher can solve the following kinds of equations
 - <var> = <term> and <term> = <var>
 - <term> = <term> where the terms are definitionally equal

tests/lean/run/matchOverlapInaccesible.lean

@@ -16,9 +16,9 @@ else
 /--
 error: Tactic `cases` failed with a nested error:
 Dependent elimination failed: Failed to solve equation
-  n✝¹.succ = n✝.add n✝
+  Nat.zero = n✝.add n✝
 at case `Parity.even` after processing
-  (Nat.succ _), _
+  Nat.zero, _
 the dependent pattern matcher can solve the following kinds of equations
 - <var> = <term> and <term> = <var>
 - <term> = <term> where the terms are definitionally equal
@@ -48,14 +48,14 @@ inductive Parity : MyNat -> Type
 
 def parity (n : MyNat) : Parity n := sorry
 
-set_option trace.Meta.Match.match true
+-- set_option trace.Meta.Match.match true
 
 /--
 error: Tactic `cases` failed with a nested error:
 Dependent elimination failed: Failed to solve equation
-  a✝.succ = sorry n✝ n✝
+  zero = sorry n✝ n✝
 at case `Parity.even` after processing
-  (succ _), _
+  zero, _
 the dependent pattern matcher can solve the following kinds of equations
 - <var> = <term> and <term> = <var>
 - <term> = <term> where the terms are definitionally equal