chore: fix tests output

src/Lean/Meta/Tactic/Subst.lean

@@ -52,9 +52,9 @@ def substCore (mvarId : MVarId) (hFVarId : FVarId) (symm := false) (fvarSubst :
           if clearH then
             let mvarId ← mvarId.clear hFVarId
             let mvarId ← mvarId.clear aFVarId
-            pure ({}, mvarId)
+            pure (fvarSubst, mvarId)
           else
-            pure ({}, mvarId)
+            pure (fvarSubst, mvarId)
         else
           mvarId.withContext do
             let mvarDecl   ← mvarId.getDecl

src/Lean/Meta/Tactic/UnifyEq.lean

@@ -53,8 +53,13 @@ def unifyEq? (mvarId : MVarId) (eqFVarId : FVarId) (subst : FVarSubst := {})
         /- Remark: we use `let rec` here because otherwise the compiler would generate an insane amount of code.
           We can remove the `rec` after we fix the eagerly inlining issue in the compiler. -/
         let rec substEq (symm : Bool) := do
-          /- Remark: `substCore` fails if the equation is of the form `x = x` -/
-          if let some (subst, mvarId) ← observing? (substCore mvarId eqFVarId symm subst) then
+          /-
+          Remark: `substCore` fails if the equation is of the form `x = x`
+          We use `(tryToSkip := true)` to ensure we avoid unnecessary `Eq.rec`s in user code.
+          Recall that `Eq.rec`s can negatively affect term reduction performance in the kernel and elaborator.
+          See issue https://github.com/leanprover/lean4/issues/2552 for an example.
+          -/
+          if let some (subst, mvarId) ← observing? (substCore mvarId eqFVarId symm subst (tryToSkip := true)) then
             return some { mvarId, subst }
           else if (← isDefEq a b) then
             /- Skip equality -/

tests/lean/1616.lean.expected.out

@@ -1,8 +1,3 @@
-1616.lean:9:23-9:39: error: don't know how to synthesize implicit argument
-  @Linear ?m (?m :: ?m) ?m (?m :: ?m) (Cover.left c)
-context:
-c : Cover ?m ?m ?m
-⊢ List ?m
 1616.lean:10:24-10:41: error: don't know how to synthesize implicit argument
   @Linear ?m ?m (?m :: ?m) (?m :: ?m) (Cover.right c)
 context:
@@ -13,33 +8,28 @@ c : Cover ?m ?m ?m
 context:
 c : Cover ?m ?m ?m
 ⊢ Type u_1
-1616.lean:10:24-10:41: error: don't know how to synthesize implicit argument
-  @Linear ?m ?m (?m :: ?m) (?m :: ?m) (Cover.right c)
-context:
-c : Cover ?m ?m ?m
-⊢ List ?m
-1616.lean:9:23-9:39: error: don't know how to synthesize implicit argument
-  @Linear ?m (?m :: ?m) ?m (?m :: ?m) (Cover.left c)
-context:
-c : Cover ?m ?m ?m
-⊢ List ?m
 1616.lean:9:31-9:38: error: don't know how to synthesize implicit argument
   @Cover.left ?m ?m ?m ?m ?m c
 context:
 c : Cover ?m ?m ?m
 ⊢ Type u_1
+1616.lean:9:23-9:39: error: don't know how to synthesize implicit argument
+  @Linear ?m (?m :: ?m) ?m (?m :: ?m) (Cover.left c)
+context:
+c : Cover ?m ?m ?m
+⊢ List ?m
 1616.lean:10:24-10:41: error: don't know how to synthesize implicit argument
   @Linear ?m ?m (?m :: ?m) (?m :: ?m) (Cover.right c)
 context:
 c : Cover ?m ?m ?m
 ⊢ List ?m
-1616.lean:10:32-10:40: error: don't know how to synthesize implicit argument
-  @Cover.right ?m ?m ?m ?m ?m c
+1616.lean:9:11-9:19: error: don't know how to synthesize implicit argument
+  @Linear ?m ?m ?m ?m c
 context:
 c : Cover ?m ?m ?m
 ⊢ Type u_1
-1616.lean:9:11-9:19: error: don't know how to synthesize implicit argument
-  @Linear ?m ?m ?m ?m c
+1616.lean:10:32-10:40: error: don't know how to synthesize implicit argument
+  @Cover.right ?m ?m ?m ?m ?m c
 context:
 c : Cover ?m ?m ?m
 ⊢ Type u_1
@@ -48,3 +38,13 @@ c : Cover ?m ?m ?m
 context:
 c : Cover ?m ?m ?m
 ⊢ Type u_1
+1616.lean:10:24-10:41: error: don't know how to synthesize implicit argument
+  @Linear ?m ?m (?m :: ?m) (?m :: ?m) (Cover.right c)
+context:
+c : Cover ?m ?m ?m
+⊢ List ?m
+1616.lean:9:23-9:39: error: don't know how to synthesize implicit argument
+  @Linear ?m (?m :: ?m) ?m (?m :: ?m) (Cover.left c)
+context:
+c : Cover ?m ?m ?m
+⊢ List ?m

tests/lean/jason1.lean.expected.out

@@ -1,3 +1,31 @@
+jason1.lean:46:40-46:57: error: don't know how to synthesize implicit argument
+  @TySyntaxLayer.top G T EG getCtx (?m G T Tm EG ET ETm EGrfl getCtx getTy GAlgebra TAlgebra getTyStep Γ✝)
+context:
+G T Tm : Type
+EG : G → G → Type
+ET : T → T → Type
+ETm : Tm → Tm → Type
+EGrfl : {Γ : G} → EG Γ Γ
+getCtx : T → G
+getTy : Tm → T
+GAlgebra : CtxSyntaxLayer G T EG getCtx → G
+TAlgebra : TySyntaxLayer G T EG getCtx → T
+Γ✝ : G
+⊢ G
+jason1.lean:48:71-48:88: error: don't know how to synthesize implicit argument
+  @TySyntaxLayer.nat G T EG getCtx (?m G T Tm EG ET ETm EGrfl getCtx getTy GAlgebra TAlgebra getTyStep Γ✝)
+context:
+G T Tm : Type
+EG : G → G → Type
+ET : T → T → Type
+ETm : Tm → Tm → Type
+EGrfl : {Γ : G} → EG Γ Γ
+getCtx : T → G
+getTy : Tm → T
+GAlgebra : CtxSyntaxLayer G T EG getCtx → G
+TAlgebra : TySyntaxLayer G T EG getCtx → T
+Γ✝ : G
+⊢ G
 jason1.lean:48:119-48:124: error: don't know how to synthesize implicit argument
   @EGrfl
     (getCtx
@@ -48,21 +76,7 @@ GAlgebra : CtxSyntaxLayer G T EG getCtx → G
 TAlgebra : TySyntaxLayer G T EG getCtx → T
 Γ✝ : G
 ⊢ G
-jason1.lean:46:40-46:57: error: don't know how to synthesize implicit argument
-  @TySyntaxLayer.top G T EG getCtx (?m G T Tm EG ET ETm EGrfl getCtx getTy GAlgebra TAlgebra getTyStep Γ✝)
-context:
-G T Tm : Type
-EG : G → G → Type
-ET : T → T → Type
-ETm : Tm → Tm → Type
-EGrfl : {Γ : G} → EG Γ Γ
-getCtx : T → G
-getTy : Tm → T
-GAlgebra : CtxSyntaxLayer G T EG getCtx → G
-TAlgebra : TySyntaxLayer G T EG getCtx → T
-Γ✝ : G
-⊢ G
-jason1.lean:48:71-48:88: error: don't know how to synthesize implicit argument
+jason1.lean:48:100-48:117: error: don't know how to synthesize implicit argument
   @TySyntaxLayer.nat G T EG getCtx (?m G T Tm EG ET ETm EGrfl getCtx getTy GAlgebra TAlgebra getTyStep Γ✝)
 context:
 G T Tm : Type
@@ -108,17 +122,3 @@ GAlgebra : CtxSyntaxLayer G T EG getCtx → G
 TAlgebra : TySyntaxLayer G T EG getCtx → T
 Γ✝ : G
 ⊢ G
-jason1.lean:48:100-48:117: error: don't know how to synthesize implicit argument
-  @TySyntaxLayer.nat G T EG getCtx (?m G T Tm EG ET ETm EGrfl getCtx getTy GAlgebra TAlgebra getTyStep Γ✝)
-context:
-G T Tm : Type
-EG : G → G → Type
-ET : T → T → Type
-ETm : Tm → Tm → Type
-EGrfl : {Γ : G} → EG Γ Γ
-getCtx : T → G
-getTy : Tm → T
-GAlgebra : CtxSyntaxLayer G T EG getCtx → G
-TAlgebra : TySyntaxLayer G T EG getCtx → T
-Γ✝ : G
-⊢ G

tests/lean/run/2552.lean

@@ -0,0 +1,44 @@
+@[inline] def decidable_of_iff {b : Prop} (a : Prop) (h : a ↔ b) [Decidable a] : Decidable b :=
+  decidable_of_decidable_of_iff h
+
+theorem LE.le.lt_or_eq_dec {a b : Nat} (hab : a ≤ b) : a < b ∨ a = b :=
+by cases hab
+   · exact .inr rfl
+   · refine .inl ?_ ; refine Nat.succ_le_succ ?_ ; assumption
+
+section succeeds_using_match
+
+local instance decidableBallLT :
+  ∀ (n : Nat) (P : ∀ k, k < n → Prop) [∀ n h, Decidable (P n h)], Decidable (∀ n h, P n h)
+| 0, _, _ => isTrue fun _ => (by cases ·)
+| (n+1), P, H =>
+  match decidableBallLT n (P · <| Nat.le_succ_of_le ·) with
+  | isFalse h => isFalse (h fun _ _ => · _ _)
+  | isTrue h =>
+    match H n Nat.le.refl with
+    | isFalse p => isFalse (p <| · _ _)
+    | isTrue p => isTrue fun _ h' => (Nat.le_of_lt_succ h').lt_or_eq_dec.elim (h _) (· ▸ p)
+
+set_option maxHeartbeats 5000
+example : ∀ a, a < 9 → ∀ b, b < 9 → ∀ c, c < 9 → a ^ 2 + b ^ 2 + c ^ 2 ≠ 7 := by decide
+
+end succeeds_using_match
+
+section fails_with_timeout
+
+-- we change `match decidableBallLT` to `by cases decidableBallLT' ... exact`:
+local instance decidableBallLT' :
+  ∀ (n : Nat) (P : ∀ k, k < n → Prop) [∀ n h, Decidable (P n h)], Decidable (∀ n h, P n h)
+| 0, _, _ => isTrue fun _ => (by cases ·)
+| (n+1), P, H => by
+  cases decidableBallLT' n (P · <| Nat.le_succ_of_le ·) with
+  | isFalse h => exact isFalse (h fun _ _ => · _ _)
+  | isTrue h =>
+    exact match H n Nat.le.refl with
+    | isFalse p => isFalse (p <| · _ _)
+    | isTrue p => isTrue fun _ h' => (Nat.le_of_lt_succ h').lt_or_eq_dec.elim (h _) (· ▸ p)
+
+set_option maxHeartbeats 5000
+example : ∀ a, a < 9 → ∀ b, b < 9 → ∀ c, c < 9 → a ^ 2 + b ^ 2 + c ^ 2 ≠ 7 := by decide
+
+end fails_with_timeout

tests/lean/syntheticHolesAsPatterns.lean.expected.out

@@ -1,11 +1,3 @@
-syntheticHolesAsPatterns.lean:7:30-7:31: error: don't know how to synthesize placeholder
-context:
-α✝ β : Type
-a✝ : α✝
-x : Fam2 α✝ β
-α : Type
-a : α
-⊢ α
 syntheticHolesAsPatterns.lean:8:30-8:31: error: don't know how to synthesize placeholder
 context:
 α β : Type
@@ -13,9 +5,10 @@ a✝ : α
 x : Fam2 α β
 a n : Nat
 ⊢ Nat
-syntheticHolesAsPatterns.lean:12:18-12:19: error: don't know how to synthesize placeholder
+syntheticHolesAsPatterns.lean:7:30-7:31: error: don't know how to synthesize placeholder
 context:
 α✝ β : Type
+a✝ : α✝
 x : Fam2 α✝ β
 α : Type
 a : α
@@ -26,3 +19,10 @@ context:
 x : Fam2 α β
 n a : Nat
 ⊢ Nat
+syntheticHolesAsPatterns.lean:12:18-12:19: error: don't know how to synthesize placeholder
+context:
+α✝ β : Type
+x : Fam2 α✝ β
+α : Type
+a : α
+⊢ α