From ef449e816f1909dedced469a60e7d5dc5f4f546f Mon Sep 17 00:00:00 2001
From: Leonardo de Moura <leonardo@microsoft.com>
Date: Wed, 19 Jan 2022 14:29:04 -0800
Subject: [PATCH] chore: improve trace messages

---
 src/Lean/Meta/Match/Match.lean         | 6 +++---
 src/Lean/Meta/Tactic/Simp/Rewrite.lean | 2 +-
 2 files changed, 4 insertions(+), 4 deletions(-)

diff --git a/src/Lean/Meta/Match/Match.lean b/src/Lean/Meta/Match/Match.lean
index a45a43659d..e20a63e0f0 100644
--- a/src/Lean/Meta/Match/Match.lean
+++ b/src/Lean/Meta/Match/Match.lean
@@ -265,11 +265,11 @@ end Unify
 private def unify? (altFVarDecls : List LocalDecl) (a b : Expr) : MetaM (Option FVarSubst) := do
   let a ← instantiateMVars a
     let b ← instantiateMVars b
-    let (b, s) ← Unify.unify a b { altFVarDecls := altFVarDecls} |>.run {}
-    if b then
+    let (r, s) ← Unify.unify a b { altFVarDecls := altFVarDecls} |>.run {}
+    if r then
       pure s.fvarSubst
     else
-      trace[Meta.Match.unify] "failed to unify {a} =?= {b}"
+      trace[Meta.Match.unify] "failed to unify{indentExpr a}\nwith{indentExpr b}"
       pure none
 
 private def expandVarIntoCtor? (alt : Alt) (fvarId : FVarId) (ctorName : Name) : MetaM (Option Alt) :=
diff --git a/src/Lean/Meta/Tactic/Simp/Rewrite.lean b/src/Lean/Meta/Tactic/Simp/Rewrite.lean
index 5ea0507e67..8fcbad05ce 100644
--- a/src/Lean/Meta/Tactic/Simp/Rewrite.lean
+++ b/src/Lean/Meta/Tactic/Simp/Rewrite.lean
@@ -64,7 +64,7 @@ private def tryLemmaCore (lhs : Expr) (xs : Array Expr) (bis : Array BinderInfo)
         -- We do not report unification failures when `lhs` is a metavariable
         -- Example: `x = ()`
         -- TODO: reconsider if we want lemmas such as `(x : Unit) → x = ()`
-        trace[Meta.Tactic.simp.unify] "{lemma}, failed to unify {lhs} with {e}"
+        trace[Meta.Tactic.simp.unify] "{lemma}, failed to unify{indentExpr lhs}\nwith{indentExpr e}"
       return none
   /- Check whether we need something more sophisticated here.
      This simple approach was good enough for Mathlib 3 -/