From e732eac89945c3452853c5fcba5ce653046770bf Mon Sep 17 00:00:00 2001
From: Leonardo de Moura <leonardo@microsoft.com>
Date: Mon, 10 Feb 2020 20:49:43 -0800
Subject: [PATCH] fix: but at `elimMVarDepsApp`

---
 src/Init/Lean/MetavarContext.lean |  2 +-
 tests/lean/run/meta2.lean         | 25 ++++++++++++++++++++++---
 2 files changed, 23 insertions(+), 4 deletions(-)

diff --git a/src/Init/Lean/MetavarContext.lean b/src/Init/Lean/MetavarContext.lean
index d8efa51bbf..58f9f5ea5a 100644
--- a/src/Init/Lean/MetavarContext.lean
+++ b/src/Init/Lean/MetavarContext.lean
@@ -811,7 +811,7 @@ private partial def elimMVarDepsApp (elimMVarDepsAux : Expr → M Expr) (xs : Ar
     let processDefault (newF : Expr) : M Expr := do {
       if newF.isLambda then do
         args ← args.mapM (visit elimMVarDepsAux);
-        pure $ newF.betaRev args.reverse
+        elimMVarDepsAux $ newF.betaRev args.reverse
       else if newF == f then do
         args ← args.mapM (visit elimMVarDepsAux);
         pure $ mkAppN newF args
diff --git a/tests/lean/run/meta2.lean b/tests/lean/run/meta2.lean
index e2b1886b74..89b9ca0cf6 100644
--- a/tests/lean/run/meta2.lean
+++ b/tests/lean/run/meta2.lean
@@ -556,13 +556,32 @@ pure ()
 #eval tst33
 
 def tst34 : MetaM Unit := do
-print "----- tst33 -----";
+print "----- tst34 -----";
 let type := mkSort levelOne;
 withLocalDecl `α type BinderInfo.default $ fun α => do
-  m ← mkFreshExprMVar α;
-  t ← approxDefEq $ mkLambda #[α] (mkArrow m m);
+  m ← mkFreshExprMVar type;
+  t ← mkLambda #[α] (mkArrow m m);
   print t;
   pure ()
 
 set_option pp.purify_metavars false
 #eval tst34
+
+def tst35 : MetaM Unit := do
+print "----- tst35 -----";
+let type := mkSort levelOne;
+withLocalDecl `α type BinderInfo.default $ fun α => do
+  m1 ← mkFreshExprMVar type;
+  m2 ← mkFreshExprMVar (mkArrow nat type);
+  let v := mkLambda `x BinderInfo.default nat m1;
+  assignExprMVar m2.mvarId! v;
+  let w := mkApp m2 zero;
+  t1 ← mkLambda #[α] (mkArrow w w);
+  print t1;
+  m3 ← mkFreshExprMVar type;
+  t2 ← mkLambda #[α] (mkArrow (mkBVar 0) (mkBVar 1));
+  print t2;
+  check $ isDefEq t1 t2;
+  pure ()
+
+#eval tst35