From fc5fb07fc39ccd014482a297a009715cbd82d70f Mon Sep 17 00:00:00 2001
From: Leonardo de Moura <leonardo@microsoft.com>
Date: Thu, 19 Dec 2019 11:13:22 -0800
Subject: [PATCH] fix: `mkFreshExprMVar`

---
 src/Init/Lean/Elab/Term.lean  | 2 +-
 tests/lean/run/frontend1.lean | 6 +++++-
 2 files changed, 6 insertions(+), 2 deletions(-)

diff --git a/src/Init/Lean/Elab/Term.lean b/src/Init/Lean/Elab/Term.lean
index a75f2c8d13..48bed0da19 100644
--- a/src/Init/Lean/Elab/Term.lean
+++ b/src/Init/Lean/Elab/Term.lean
@@ -240,7 +240,7 @@ def mkFreshLevelMVar (ref : Syntax) : TermElabM Level := liftMetaM ref $ Meta.mk
 def mkFreshExprMVar (ref : Syntax) (type? : Option Expr := none) (kind : MetavarKind := MetavarKind.natural) (userName? : Name := Name.anonymous) : TermElabM Expr :=
 match type? with
 | some type => liftMetaM ref $ Meta.mkFreshExprMVar type userName? kind
-| none      => liftMetaM ref $ do u ← Meta.mkFreshLevelMVar; Meta.mkFreshExprMVar (mkSort u) userName? kind
+| none      => liftMetaM ref $ do u ← Meta.mkFreshLevelMVar; type ← Meta.mkFreshExprMVar (mkSort u); Meta.mkFreshExprMVar type userName? kind
 def getLevel (ref : Syntax) (type : Expr) : TermElabM Level := liftMetaM ref $ Meta.getLevel type
 def mkForall (ref : Syntax) (xs : Array Expr) (e : Expr) : TermElabM Expr := liftMetaM ref $ Meta.mkForall xs e
 def mkLambda (ref : Syntax) (xs : Array Expr) (e : Expr) : TermElabM Expr := liftMetaM ref $ Meta.mkLambda xs e
diff --git a/tests/lean/run/frontend1.lean b/tests/lean/run/frontend1.lean
index f79ed4916c..293d66a456 100644
--- a/tests/lean/run/frontend1.lean
+++ b/tests/lean/run/frontend1.lean
@@ -2,7 +2,6 @@ import Init.Lean.Elab
 open Lean
 open Lean.Elab
 
-
 def run (input : String) (failIff : Bool := true) : MetaIO Unit :=
 do env  ← MetaIO.getEnv;
    opts ← MetaIO.getOptions;
@@ -143,6 +142,11 @@ x + y + z
 def foo {α β} (a : α) (b : β) (a' : α) : α :=
 a
 
+def bla {α β} (f : α → β) (a : α) : β :=
+f a
+
 -- #check fun x => foo x x.w s4 -- fails in old elaborator
+-- #check bla (fun x => x.w) s4 -- fails in the old elaborator
 
 #eval run "#check fun x => foo x x.w s4"
+#eval run "#check bla (fun x => x.w) s4"