From f8bfe88d6b80c79b2527b3ce488d2a3f565b035f Mon Sep 17 00:00:00 2001
From: Leonardo de Moura <leonardo@microsoft.com>
Date: Sun, 2 Feb 2020 21:54:44 -0800
Subject: [PATCH] fix: consume unnecessary let-decls at `isDefEq`

Make sure we solve unification constraints such as `(let x := v; ?m) =?= ?m`
---
 src/Init/Lean/Meta/ExprDefEq.lean |  7 +++++++
 tests/lean/run/meta2.lean         | 11 +++++++++++
 2 files changed, 18 insertions(+)

diff --git a/src/Init/Lean/Meta/ExprDefEq.lean b/src/Init/Lean/Meta/ExprDefEq.lean
index 4bb049bf1a..2a0c5f4c66 100644
--- a/src/Init/Lean/Meta/ExprDefEq.lean
+++ b/src/Init/Lean/Meta/ExprDefEq.lean
@@ -1074,8 +1074,15 @@ unstuckMVar t (fun t => isExprDefEqAux t s) $
 unstuckMVar s (fun s => isExprDefEqAux t s) $
 pure false
 
+/- Remove unnecessary let-decls -/
+private def consumeLet : Expr → Expr
+| e@(Expr.letE _ _ _ b _) => if b.hasLooseBVars then b else consumeLet b
+| e                       => e
+
 partial def isExprDefEqAuxImpl : Expr → Expr → MetaM Bool
 | t, s => do
+  let t := consumeLet t;
+  let s := consumeLet s;
   trace `Meta.isDefEq.step $ fun _ => t ++ " =?= " ++ s;
   tryL (isDefEqQuick t s) $
   tryL (isDefEqProofIrrel t s) $
diff --git a/tests/lean/run/meta2.lean b/tests/lean/run/meta2.lean
index c2bc11021b..ea6f40e2f2 100644
--- a/tests/lean/run/meta2.lean
+++ b/tests/lean/run/meta2.lean
@@ -22,6 +22,7 @@ do v? ← getExprMVarAssignment? m.mvarId!;
 def nat   := mkConst `Nat
 def boolE := mkConst `Bool
 def succ  := mkConst `Nat.succ
+def zero  := mkConst `Nat.zero
 def add   := mkConst `Nat.add
 def io    := mkConst `IO
 def type  := mkSort levelOne
@@ -505,3 +506,13 @@ withLocalDecl `x nat BinderInfo.default $ fun x => do
   pure ()
 
 #eval tst30
+
+def tst31 : MetaM Unit := do
+print "----- tst31 -----";
+m ← mkFreshExprMVar nat;
+let t := mkLet `x nat zero m;
+print t;
+check $ isDefEq t m;
+pure ()
+
+#eval tst31