fix: unify goal before executing nested tactics in calc

Fixes #2095

src/Init/NotationExtra.lean

@@ -89,6 +89,7 @@ end
 
 -- enforce indentation of calc steps so we know when to stop parsing them
 syntax calcStep := ppIndent(colGe term " := " withPosition(term))
+syntax calcSteps := ppLine withPosition(calcStep) ppLine withPosition((calcStep ppLine)*)
 
 /-- Step-wise reasoning over transitive relations.
 ```
@@ -108,7 +109,7 @@ See [Theorem Proving in Lean 4][tpil4] for more information.
 
 [tpil4]: https://leanprover.github.io/theorem_proving_in_lean4/quantifiers_and_equality.html#calculational-proofs
 -/
-syntax (name := calc) "calc" ppLine withPosition(calcStep) ppLine withPosition((calcStep ppLine)*) : term
+syntax (name := calc) "calc" calcSteps : term
 
 /-- Step-wise reasoning over transitive relations.
 ```
@@ -131,7 +132,7 @@ See [Theorem Proving in Lean 4][tpil4] for more information.
 
 [tpil4]: https://leanprover.github.io/theorem_proving_in_lean4/quantifiers_and_equality.html#calculational-proofs
 -/
-syntax (name := calcTactic) "calc" ppLine withPosition(calcStep) ppLine withPosition((calcStep ppLine)*) : tactic
+syntax (name := calcTactic) "calc" calcSteps : tactic
 
 @[app_unexpander Unit.unit] def unexpandUnit : Lean.PrettyPrinter.Unexpander
   | `($(_)) => `(())

src/Lean/Elab/Calc.lean

@@ -54,9 +54,9 @@ See https://github.com/leanprover/lean4/issues/2040 for futher rationale.
 - `_ + 2 < 3` is annotated (not the best heuristic, ideally we'd like to annotate `_ + 2`)
 - `lt _ 3` is not, because it occurs after an identifier
 -/
-partial def annotateFirstHoleWithType (t : Syntax) (type : Expr) : TermElabM Syntax :=
+partial def annotateFirstHoleWithType (t : Term) (type : Expr) : TermElabM Term :=
   -- The state is true if we should annotate the immediately next hole with the type.
-  StateT.run' (go t) true
+  return ⟨← StateT.run' (go t) true⟩
 where
   go (t : Syntax) := do
     unless ← get do return t
@@ -67,37 +67,41 @@ where
     | .node i k as => return .node i k (← as.mapM go)
     | _ => set false; return t
 
-/--
-  Elaborate `calc`-steps
--/
-def elabCalcSteps (steps : Array Syntax) : TermElabM Expr := do
-  let mut proofs := #[]
-  let mut types  := #[]
+def getCalcSteps (steps : TSyntax ``calcSteps) : Array (TSyntax ``calcStep) :=
+  match steps with
+  | `(calcSteps| $step0 $rest*) => #[step0] ++ rest
+  | _ => unreachable!
+
+def elabCalcSteps (steps : TSyntax ``calcSteps) : TermElabM Expr := do
+  let mut result? := none
   let mut prevRhs? := none
-  for step in steps do
-    let mut pred := step[0]
-    if let some prevRhs := prevRhs? then
-      pred ← annotateFirstHoleWithType pred (← inferType prevRhs)
-    let type ← elabType pred
+  for step in getCalcSteps steps do
+    let `(calcStep| $pred := $proofTerm) := step | unreachable!
+    let type ← elabType <| ← do
+      if let some prevRhs := prevRhs? then
+        annotateFirstHoleWithType pred (← inferType prevRhs)
+      else
+        pure pred
     let some (_, lhs, rhs) ← getCalcRelation? type |
-      throwErrorAt step[0] "invalid 'calc' step, relation expected{indentExpr type}"
+      throwErrorAt pred "invalid 'calc' step, relation expected{indentExpr type}"
     if let some prevRhs := prevRhs? then
       unless (← isDefEqGuarded lhs prevRhs) do
-        throwErrorAt step[0] "invalid 'calc' step, left-hand-side is{indentD m!"{lhs} : {← inferType lhs}"}\nprevious right-hand-side is{indentD m!"{prevRhs} : {← inferType prevRhs}"}"
-    types := types.push type
-    let proof ← elabTermEnsuringType step[2] type
-    synthesizeSyntheticMVarsUsingDefault
-    proofs := proofs.push proof
+        throwErrorAt pred "invalid 'calc' step, left-hand-side is{indentD m!"{lhs} : {← inferType lhs}"}\nprevious right-hand-side is{indentD m!"{prevRhs} : {← inferType prevRhs}"}" -- "
+    let proof ← withFreshMacroScope do elabTermEnsuringType proofTerm type
+    result? := some <| ← do
+      if let some (result, resultType) := result? then
+        synthesizeSyntheticMVarsUsingDefault
+        withRef pred do mkCalcTrans result resultType proof type
+      else
+        pure (proof, type)
     prevRhs? := rhs
-  let mut result := proofs[0]!
-  let mut resultType := types[0]!
-  for i in [1:proofs.size] do
-    (result, resultType) ← withRef steps[i]![0] <| mkCalcTrans result resultType proofs[i]! types[i]!
-  return result
+  return result?.get!.1
 
 /-- Elaborator for the `calc` term mode variant. -/
 @[builtin_term_elab «calc»]
-def elabCalc : TermElab :=  fun stx expectedType? => do
-  let steps := #[stx[1]] ++ stx[2].getArgs
+def elabCalc : TermElab := fun stx expectedType? => do
+  let steps : TSyntax ``calcSteps := ⟨stx[1]⟩
   let result ← elabCalcSteps steps
-  ensureHasType expectedType? result
+  synthesizeSyntheticMVarsUsingDefault
+  let result ← ensureHasType expectedType? result
+  return result

src/Lean/Elab/Tactic/Calc.lean

@@ -9,40 +9,25 @@ import Lean.Elab.Tactic.ElabTerm
 namespace Lean.Elab.Tactic
 open Meta
 
-def elabCalcSteps (steps : Array Syntax) : TacticM Expr := do
-  /- If error recovery is disabled, we disable `Term.withoutErrToSorry` -/
-  if (← read).recover then
-    go
-  else
-    Term.withoutErrToSorry go
-where
-  go : TermElabM Expr := do
-    let e ← Term.elabCalcSteps steps
-    Term.synthesizeSyntheticMVars (mayPostpone := false)
-    instantiateMVars e
-
 /-- Elaborator for the `calc` tactic mode variant. -/
 @[builtin_tactic calcTactic]
-def evalCalc : Tactic := fun stx => do
-  withMainContext do
-    let steps := #[stx[1]] ++ stx[2].getArgs
-    let (val, mvarIds) ← withCollectingNewGoalsFrom (tagSuffix := `calc) do
-      let target ← getMainTarget
-      let val ← elabCalcSteps steps
-      let valType ← inferType val
-      if (← isDefEq valType target) then
-        return val
-      else
-        let throwFailed {α} : TacticM α :=
-          throwError "'calc' tactic failed, has type{indentExpr valType}\nbut it is expected to have type{indentExpr target}"
-        let some (_, _, rhs) ← Term.getCalcRelation? valType | throwFailed
-        let some (r, _, rhs') ← Term.getCalcRelation? target | throwFailed
-        let lastStep := mkApp2 r rhs rhs'
-        let lastStepGoal ← mkFreshExprSyntheticOpaqueMVar lastStep (tag := (← getMainTag) ++ `calc.step)
-        let (val, valType) ← Term.mkCalcTrans val valType lastStepGoal lastStep
-        unless (← isDefEq valType target) do throwFailed
-        return val
-    let val ← instantiateMVars val
-    let mvarId ← getMainGoal
-    mvarId.assign val
-    replaceMainGoal mvarIds
+def evalCalc : Tactic := fun stx => withMainContext do
+  let steps : TSyntax ``calcSteps := ⟨stx[1]⟩
+  let (val, mvarIds) ← withCollectingNewGoalsFrom (tagSuffix := `calc) do
+    let target ← getMainTarget
+    let tag ← getMainTag
+    runTermElab do
+    let mut val ← Term.elabCalcSteps steps
+    let mut valType ← inferType val
+    unless (← isDefEq valType target) do
+      let rec throwFailed :=
+        throwError "'calc' tactic failed, has type{indentExpr valType}\nbut it is expected to have type{indentExpr target}"
+      let some (_, _, rhs) ← Term.getCalcRelation? valType | throwFailed
+      let some (r, _, rhs') ← Term.getCalcRelation? target | throwFailed
+      let lastStep := mkApp2 r rhs rhs'
+      let lastStepGoal ← mkFreshExprSyntheticOpaqueMVar lastStep (tag := tag ++ `calc.step)
+      (val, valType) ← Term.mkCalcTrans val valType lastStepGoal lastStep
+      unless (← isDefEq valType target) do throwFailed
+    return val
+  (← getMainGoal).assign val
+  replaceMainGoal mvarIds

src/Lean/Elab/Tactic/ElabTerm.lean

@@ -15,20 +15,26 @@ open Meta
 
 /-! # `elabTerm` for Tactics and basic tactics that use it. -/
 
-/-- Elaborate `stx` in the current `MVarContext`. If given, the `expectedType` will be used to help
-elaboration but not enforced (use `elabTermEnsuringType` to enforce an expected type). -/
-def elabTerm (stx : Syntax) (expectedType? : Option Expr) (mayPostpone := false) : TacticM Expr := do
+/--
+Runs a term elaborator inside a tactic.
+
+This function ensures that term elaboration fails when backtracking,
+i.e., in `first| tac term | other`.
+-/
+def runTermElab (k : TermElabM α) (mayPostpone := false) : TacticM α := do
   /- If error recovery is disabled, we disable `Term.withoutErrToSorry` -/
   if (← read).recover then
     go
   else
     Term.withoutErrToSorry go
 where
-  go : TermElabM Expr :=
-    withRef stx do -- <|
-      let e ← Term.elabTerm stx expectedType?
-      Term.synthesizeSyntheticMVars mayPostpone
-      instantiateMVars e
+  go := k <* Term.synthesizeSyntheticMVars (mayPostpone := mayPostpone)
+
+/-- Elaborate `stx` in the current `MVarContext`. If given, the `expectedType` will be used to help
+elaboration but not enforced (use `elabTermEnsuringType` to enforce an expected type). -/
+def elabTerm (stx : Syntax) (expectedType? : Option Expr) (mayPostpone := false) : TacticM Expr :=
+  withRef stx do instantiateMVars <| ← runTermElab (mayPostpone := mayPostpone) do
+    Term.elabTerm stx expectedType?
 
 /-- Elaborate `stx` in the current `MVarContext`. If given, the `expectedType` will be used to help
 elaboration and then a `TypeMismatchError` will be thrown if the elaborated type doesn't match.  -/

tests/lean/run/2095.lean

@@ -0,0 +1,11 @@
+-- works
+example : 3 < 5 :=
+  calc
+    _ < 4 := by decide
+    _ < _ := by decide
+
+-- fails
+example : 3 < 5 := by
+  calc
+    _ < 4 := by decide
+    _ < _ := by decide