feat: expose diff at "synthesized type class instance is not definiti…

…onally equal" error This PR exposes the difference in "synthesized type class instance is not definitionally equal" errors.
leanprover · Nov 25, 2024 · ac6079b · ac6079b
1 parent ba3f2b3
commit ac6079b
Showing 1 changed file with 2 additions and 0 deletions.
diff --git a/src/Lean/Elab/Term.lean b/src/Lean/Elab/Term.lean
@@ -1079,7 +1079,9 @@ def synthesizeInstMVarCore (instMVar : MVarId) (maxResultSize? : Option Nat := n
         let oldValType ← inferType oldVal
         let valType ← inferType val
         unless (← isDefEq oldValType valType) do
+          let (oldValType, valType) ← addPPExplicitToExposeDiff oldValType valType
           throwError "synthesized type class instance type is not definitionally equal to expected type, synthesized{indentExpr val}\nhas type{indentExpr valType}\nexpected{indentExpr oldValType}{extraErrorMsg}"
+        let (oldVal, val) ← addPPExplicitToExposeDiff oldVal val
         throwError "synthesized type class instance is not definitionally equal to expression inferred by typing rules, synthesized{indentExpr val}\ninferred{indentExpr oldVal}{extraErrorMsg}"
     else
       unless (← isDefEq (mkMVar instMVar) val) do