feat: improved calc error messages (#5719)

Makes the error messages report on RHSs and LHSs that do not match the
expected values when the relations are defeq. If the relations are not
defeq, the error message now no longer mentions the value of the whole
`calc` expression.

Adds a field to `mkCoe` with an optional callback to use to generate
error messages.

Note: it is tempting to try to make use of expected types when
elaborating the `calc` expression, but this runs into issue #2073.

Closes #4318

src/Lean/Elab/Calc.lean

@@ -10,10 +10,11 @@ namespace Lean.Elab.Term
 open Meta
 
 /--
-  Decompose `e` into `(r, a, b)`.
+Decompose `e` into `(r, a, b)`.
 
-  Remark: it assumes the last two arguments are explicit. -/
-def getCalcRelation? (e : Expr) : MetaM (Option (Expr × Expr × Expr)) :=
+Remark: it assumes the last two arguments are explicit.
+-/
+def getCalcRelation? (e : Expr) : MetaM (Option (Expr × Expr × Expr)) := do
   if e.getAppNumArgs < 2 then
     return none
   else
@@ -68,56 +69,102 @@ where
     | .node i k as => return .node i k (← as.mapM go)
     | _ => set false; return t
 
-def getCalcFirstStep (step0 : TSyntax ``calcFirstStep) : TermElabM (TSyntax ``calcStep) :=
+/-- View of a `calcStep`. -/
+structure CalcStepView where
+  ref : Syntax
+  /-- A relation term like `a ≤ b` -/
+  term : Term
+  /-- A proof of `term` -/
+  proof : Term
+  deriving Inhabited
+
+def mkCalcFirstStepView (step0 : TSyntax ``calcFirstStep) : TermElabM CalcStepView :=
   withRef step0 do
   match step0  with
-  | `(calcFirstStep| $term:term) =>
-    `(calcStep| $term = _ := rfl)
-  | `(calcFirstStep| $term := $proof) =>
-    `(calcStep| $term := $proof)
+  | `(calcFirstStep| $term:term)      => return { ref := step0, term := ← `($term = _), proof := ← ``(rfl)}
+  | `(calcFirstStep| $term := $proof) => return { ref := step0, term, proof}
   | _ => throwUnsupportedSyntax
 
-def getCalcSteps (steps : TSyntax ``calcSteps) : TermElabM (Array (TSyntax ``calcStep)) :=
+def mkCalcStepViews (steps : TSyntax ``calcSteps) : TermElabM (Array CalcStepView) :=
   match steps with
   | `(calcSteps|
         $step0:calcFirstStep
         $rest*) => do
-    let step0 ← getCalcFirstStep step0
-    pure (#[step0] ++ rest)
-  | _ => unreachable!
+    let mut steps := #[← mkCalcFirstStepView step0]
+    for step in rest do
+      let `(calcStep| $term := $proof) := step | throwUnsupportedSyntax
+      steps := steps.push { ref := step, term, proof }
+    return steps
+  | _ => throwUnsupportedSyntax
 
-def elabCalcSteps (steps : TSyntax ``calcSteps) : TermElabM Expr := do
+def elabCalcSteps (steps : Array CalcStepView) : TermElabM (Expr × Expr) := do
   let mut result? := none
   let mut prevRhs? := none
-  for step in ← getCalcSteps steps do
-    let `(calcStep| $pred := $proofTerm) := step | unreachable!
+  for step in steps do
     let type ← elabType <| ← do
       if let some prevRhs := prevRhs? then
-        annotateFirstHoleWithType pred (← inferType prevRhs)
+        annotateFirstHoleWithType step.term (← inferType prevRhs)
       else
-        pure pred
+        pure step.term
     let some (_, lhs, rhs) ← getCalcRelation? type |
-      throwErrorAt pred "invalid 'calc' step, relation expected{indentExpr type}"
+      throwErrorAt step.term "invalid 'calc' step, relation expected{indentExpr type}"
     if let some prevRhs := prevRhs? then
       unless (← isDefEqGuarded lhs prevRhs) do
-        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
+        throwErrorAt step.term "\
+          invalid 'calc' step, left-hand side is{indentD m!"{lhs} : {← inferType lhs}"}\n\
+          but previous right-hand side is{indentD m!"{prevRhs} : {← inferType prevRhs}"}"
+    let proof ← withFreshMacroScope do elabTermEnsuringType step.proof type
     result? := some <| ← do
       if let some (result, resultType) := result? then
         synthesizeSyntheticMVarsUsingDefault
-        withRef pred do mkCalcTrans result resultType proof type
+        withRef step.term do mkCalcTrans result resultType proof type
       else
         pure (proof, type)
     prevRhs? := rhs
-  return result?.get!.1
+  synthesizeSyntheticMVarsUsingDefault
+  return result?.get!
+
+def throwCalcFailure (steps : Array CalcStepView) (expectedType result : Expr) : MetaM α := do
+  let resultType := (← instantiateMVars (← inferType result)).headBeta
+  let some (r, lhs, rhs) ← getCalcRelation? resultType | unreachable!
+  if let some (er, elhs, erhs) ← getCalcRelation? expectedType then
+    if ← isDefEqGuarded r er then
+      let mut failed := false
+      unless ← isDefEqGuarded lhs elhs do
+        logErrorAt steps[0]!.term m!"\
+          invalid 'calc' step, left-hand side is{indentD m!"{lhs} : {← inferType lhs}"}\n\
+          but is expected to be{indentD m!"{elhs} : {← inferType elhs}"}"
+        failed := true
+      unless ← isDefEqGuarded rhs erhs do
+        logErrorAt steps.back.term m!"\
+          invalid 'calc' step, right-hand side is{indentD m!"{rhs} : {← inferType rhs}"}\n\
+          but is expected to be{indentD m!"{erhs} : {← inferType erhs}"}"
+        failed := true
+      if failed then
+        throwAbortTerm
+  throwTypeMismatchError "'calc' expression" expectedType resultType result
+
+/-!
+Warning! It is *very* tempting to try to improve `calc` so that it makes use of the expected type
+to unify with the LHS and RHS.
+Two people have already re-implemented `elabCalcSteps` trying to do so and then reverted the changes,
+not being aware of examples like /~https://github.com/leanprover/lean4/issues/2073
+
+The problem is that the expected type might need to be unfolded to get an accurate LHS and RHS.
+(Consider `≤` vs `≥`. Users expect to be able to use `calc` to prove `≥` using chained `≤`!)
+Furthermore, the types of the LHS and RHS do not need to be the same (consider `x ∈ S` as a relation),
+so we also cannot use the expected LHS and RHS as type hints.
+-/
 
 /-- Elaborator for the `calc` term mode variant. -/
 @[builtin_term_elab Lean.calc]
-def elabCalc : TermElab := fun stx expectedType? => do
-  let steps : TSyntax ``calcSteps := ⟨stx[1]⟩
-  let result ← elabCalcSteps steps
-  synthesizeSyntheticMVarsUsingDefault
-  let result ← ensureHasType expectedType? result
-  return result
+def elabCalc : TermElab
+  | `(calc%$tk $steps:calcSteps), expectedType? => withRef tk do
+    let steps ← mkCalcStepViews steps
+    let (result, _) ← elabCalcSteps steps
+    ensureHasTypeWithErrorMsgs expectedType? result
+      (mkImmedErrorMsg := fun _ => throwCalcFailure steps)
+      (mkErrorMsg := fun _ => throwCalcFailure steps)
+  | _, _ => throwUnsupportedSyntax
 
 end Lean.Elab.Term

src/Lean/Elab/SyntheticMVars.lean

@@ -219,10 +219,13 @@ def reportStuckSyntheticMVar (mvarId : MVarId) (ignoreStuckTC := false) : TermEl
           let mvarDecl ← getMVarDecl mvarId
           unless (← MonadLog.hasErrors) do
             throwError "typeclass instance problem is stuck, it is often due to metavariables{indentExpr mvarDecl.type}{extraErrorMsg}"
-    | .coe header expectedType e f? =>
+    | .coe header expectedType e f? mkErrorMsg? =>
       mvarId.withContext do
-        throwTypeMismatchError header expectedType (← inferType e) e f?
-          m!"failed to create type class instance for{indentExpr (← getMVarDecl mvarId).type}"
+        if let some mkErrorMsg := mkErrorMsg? then
+          throwError (← mkErrorMsg mvarId expectedType e)
+        else
+          throwTypeMismatchError header expectedType (← inferType e) e f?
+            m!"failed to create type class instance for{indentExpr (← getMVarDecl mvarId).type}"
     | _ => unreachable! -- TODO handle other cases.
 
 /--
@@ -386,7 +389,7 @@ mutual
     withRef mvarSyntheticDecl.stx do
     match mvarSyntheticDecl.kind with
     | .typeClass extraErrorMsg? => synthesizePendingInstMVar mvarId extraErrorMsg?
-    | .coe _header? expectedType e _f? => mvarId.withContext do
+    | .coe _header? expectedType e _f? _ => mvarId.withContext do
       if (← withDefault do isDefEq (← inferType e) expectedType) then
         -- Types may be defeq now due to mvar assignments, type class
         -- defaulting, etc.

src/Lean/Elab/Tactic/Calc.lean

@@ -12,25 +12,38 @@ open Meta
 
 /-- Elaborator for the `calc` tactic mode variant. -/
 @[builtin_tactic Lean.calcTactic]
-def evalCalc : Tactic := fun stx => withMainContext do
-  let steps : TSyntax ``calcSteps := ⟨stx[1]⟩
-  let target := (← getMainTarget).consumeMData
-  let tag ← getMainTag
-  let (val, mvarIds) ← withCollectingNewGoalsFrom (parentTag := tag) (tagSuffix := `calc) do
-    runTermElab do
-    let mut val ← Term.elabCalcSteps steps
-    let mut valType ← instantiateMVars (← 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
+def evalCalc : Tactic
+  | `(tactic| calc%$tk $steps:calcSteps) =>
+    withRef tk do
+    closeMainGoalUsing `calc (checkNewUnassigned := false) fun target tag => do
+    withTacticInfoContext steps do
+      let steps ← Term.mkCalcStepViews steps
+      let target := (← instantiateMVars target).consumeMData
+      let (val, mvarIds) ← withCollectingNewGoalsFrom (parentTag := tag) (tagSuffix := `calc) <| runTermElab do
+        let (val, valType) ← Term.elabCalcSteps steps
+        if (← isDefEq valType target) then
+          -- Immediately the right type, no need for further processing.
+          return val
+
+        let some (_, lhs, rhs) ← Term.getCalcRelation? valType | unreachable!
+        if let some (er, elhs, erhs) ← Term.getCalcRelation? target then
+          -- Feature: if the goal is `x ~ y`, try extending the `calc` with `_ ~ y` with a new "last step" goal.
+          if ← isDefEq lhs elhs <&&> isDefEq (← inferType rhs) (← inferType elhs) then
+            let lastStep := mkApp2 er rhs erhs
+            let lastStepGoal ← mkFreshExprSyntheticOpaqueMVar lastStep (tag := tag ++ `calc.step)
+            try
+              let (val', valType') ← Term.mkCalcTrans val valType lastStepGoal lastStep
+              if (← isDefEq valType' target) then
+                return val'
+            catch _ =>
+              pure ()
+
+        -- Calc extension failed, so let's go back and mimick the `calc` expression
+        Term.ensureHasTypeWithErrorMsgs target val
+          (mkImmedErrorMsg := fun _ => Term.throwCalcFailure steps)
+          (mkErrorMsg := fun _ => Term.throwCalcFailure steps)
+      pushGoals mvarIds
+      return val
+  | _ => throwUnsupportedSyntax
 
 end Lean.Elab.Tactic

src/Lean/Elab/Term.lean

@@ -46,11 +46,17 @@ inductive SyntheticMVarKind where
   regarding type class synthesis failure.
   -/
   | typeClass (extraErrorMsg? : Option MessageData)
-  /-- Use coercion to synthesize value for the metavariable.
-  if `f?` is `some f`, we produce an application type mismatch error message.
-  Otherwise, if `header?` is `some header`, we generate the error `(header ++ "has type" ++ eType ++ "but it is expected to have type" ++ expectedType)`
-  Otherwise, we generate the error `("type mismatch" ++ e ++ "has type" ++ eType ++ "but it is expected to have type" ++ expectedType)` -/
+  /--
+  Use coercion to synthesize value for the metavariable.
+  If synthesis fails, then throws an error.
+  - If `mkErrorMsg?` is provided, then the error `mkErrorMsg expectedType e` is thrown.
+    The `mkErrorMsg` function is allowed to throw an error itself.
+  - Otherwise, throws a default type mismatch error message.
+    If `header?` is not provided, the default header is "type mismatch".
+    If `f?` is provided, then throws an application type mismatch error.
+  -/
   | coe (header? : Option String) (expectedType : Expr) (e : Expr) (f? : Option Expr)
+      (mkErrorMsg? : Option (MVarId → Expr → Expr → MetaM MessageData))
   /-- Use tactic to synthesize value for metavariable. -/
   | tactic (tacticCode : Syntax) (ctx : SavedContext) (kind : TacticMVarKind)
   /-- Metavariable represents a hole whose elaboration has been postponed. -/
@@ -949,14 +955,14 @@ def applyAttributesAt (declName : Name) (attrs : Array Attribute) (applicationTi
 def applyAttributes (declName : Name) (attrs : Array Attribute) : TermElabM Unit :=
   applyAttributesCore declName attrs none
 
-def mkTypeMismatchError (header? : Option MessageData) (e : Expr) (eType : Expr) (expectedType : Expr) : TermElabM MessageData := do
+def mkTypeMismatchError (header? : Option MessageData) (e : Expr) (eType : Expr) (expectedType : Expr) : MetaM MessageData := do
   let header : MessageData := match header? with
     | some header => m!"{header} "
     | none        => m!"type mismatch{indentExpr e}\n"
   return m!"{header}{← mkHasTypeButIsExpectedMsg eType expectedType}"
 
 def throwTypeMismatchError (header? : Option MessageData) (expectedType : Expr) (eType : Expr) (e : Expr)
-    (f? : Option Expr := none) (_extraMsg? : Option MessageData := none) : TermElabM α := do
+    (f? : Option Expr := none) (_extraMsg? : Option MessageData := none) : MetaM α := do
   /-
     We ignore `extraMsg?` for now. In all our tests, it contained no useful information. It was
     always of the form:
@@ -1073,7 +1079,9 @@ def synthesizeInstMVarCore (instMVar : MVarId) (maxResultSize? : Option Nat := n
     else
       throwError "failed to synthesize{indentExpr type}{extraErrorMsg}{useDiagnosticMsg}"
 
-def mkCoe (expectedType : Expr) (e : Expr) (f? : Option Expr := none) (errorMsgHeader? : Option String := none) : TermElabM Expr := do
+def mkCoe (expectedType : Expr) (e : Expr) (f? : Option Expr := none) (errorMsgHeader? : Option String := none)
+    (mkErrorMsg? : Option (MVarId → (expectedType e : Expr) → MetaM MessageData) := none)
+    (mkImmedErrorMsg? : Option ((errorMsg? : Option MessageData) → (expectedType e : Expr) → MetaM MessageData) := none) : TermElabM Expr := do
   withTraceNode `Elab.coe (fun _ => return m!"adding coercion for {e} : {← inferType e} =?= {expectedType}") do
   try
     withoutMacroStackAtErr do
@@ -1082,11 +1090,24 @@ def mkCoe (expectedType : Expr) (e : Expr) (f? : Option Expr := none) (errorMsgH
       | .none => failure
       | .undef =>
         let mvarAux ← mkFreshExprMVar expectedType MetavarKind.syntheticOpaque
-        registerSyntheticMVarWithCurrRef mvarAux.mvarId! (.coe errorMsgHeader? expectedType e f?)
+        registerSyntheticMVarWithCurrRef mvarAux.mvarId! (.coe errorMsgHeader? expectedType e f? mkErrorMsg?)
         return mvarAux
   catch
-    | .error _ msg => throwTypeMismatchError errorMsgHeader? expectedType (← inferType e) e f? msg
-    | _            => throwTypeMismatchError errorMsgHeader? expectedType (← inferType e) e f?
+    | .error _ msg =>
+      if let some mkImmedErrorMsg := mkImmedErrorMsg? then
+        throwError (← mkImmedErrorMsg msg expectedType e)
+      else
+        throwTypeMismatchError errorMsgHeader? expectedType (← inferType e) e f? msg
+    | _            =>
+      if let some mkImmedErrorMsg := mkImmedErrorMsg? then
+        throwError (← mkImmedErrorMsg none expectedType e)
+      else
+        throwTypeMismatchError errorMsgHeader? expectedType (← inferType e) e f?
+
+def mkCoeWithErrorMsgs (expectedType : Expr) (e : Expr)
+    (mkImmedErrorMsg : (errorMsg? : Option MessageData) → (expectedType e : Expr) → MetaM MessageData)
+    (mkErrorMsg : MVarId → (expectedType e : Expr) → MetaM MessageData) : TermElabM Expr := do
+  mkCoe expectedType e (mkImmedErrorMsg? := mkImmedErrorMsg) (mkErrorMsg? := mkErrorMsg)
 
 /--
 If `expectedType?` is `some t`, then ensures `t` and `eType` are definitionally equal by inserting a coercion if necessary.
@@ -1101,6 +1122,15 @@ def ensureHasType (expectedType? : Option Expr) (e : Expr)
   else
     mkCoe expectedType e f? errorMsgHeader?
 
+def ensureHasTypeWithErrorMsgs (expectedType? : Option Expr) (e : Expr)
+    (mkImmedErrorMsg : (errorMsg? : Option MessageData) → (expectedType e : Expr) → MetaM MessageData)
+    (mkErrorMsg : MVarId → (expectedType e : Expr) → MetaM MessageData) : TermElabM Expr := do
+  let some expectedType := expectedType? | return e
+  if (← isDefEq (← inferType e) expectedType) then
+    return e
+  else
+    mkCoeWithErrorMsgs expectedType e mkImmedErrorMsg mkErrorMsg
+
 /--
   Create a synthetic sorry for the given expected type. If `expectedType? = none`, then a fresh
   metavariable is created to represent the type.

tests/lean/calcErrors.lean.expected.out

@@ -4,17 +4,17 @@ has type
   b + b = b + b : Prop
 but is expected to have type
   b + b = 0 + c + b : Prop
-calcErrors.lean:13:8-13:29: error: invalid 'calc' step, left-hand-side is
+calcErrors.lean:13:8-13:29: error: invalid 'calc' step, left-hand side is
   0 + c + b : Nat
-previous right-hand-side is
+but previous right-hand side is
   b + b : Nat
 calcErrors.lean:24:8-24:11: error: invalid 'calc' step, relation expected
   p a
 calcErrors.lean:31:8-31:13: error: invalid 'calc' step, failed to synthesize `Trans` instance
   Trans p p ?m
 Additional diagnostic information may be available using the `set_option diagnostics true` command.
-calcErrors.lean:41:7-41:12: error: invalid 'calc' step, left-hand-side is
+calcErrors.lean:41:7-41:12: error: invalid 'calc' step, left-hand side is
   γ : Sort u_1
-previous right-hand-side is
+but previous right-hand side is
   b : β
 calcErrors.lean:61:18-61:19: error: unexpected token '['; expected command