fix: mkFreshExprMVar

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

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"