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

@@ -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) $

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