fix: try to postpone if function type is not known

src/Init/Lean/Elab/TermApp.lean

@@ -111,6 +111,8 @@ private partial def elabAppArgsAux (ref : Syntax) (args : Array Arg) (expectedTy
 private def elabAppArgs (ref : Syntax) (f : Expr) (namedArgs : Array NamedArg) (args : Array Arg)
     (expectedType? : Option Expr) (explicit : Bool) : TermElabM Expr := do
 fType ← inferType ref f;
+fType ← instantiateMVars ref fType;
+tryPostponeIfMVar fType;
 let argIdx    := 0;
 let instMVars := #[];
 elabAppArgsAux ref args expectedType? explicit argIdx namedArgs instMVars fType f

tests/lean/run/frontend1.lean

@@ -155,3 +155,4 @@ f a
 #eval run "#check #[1, 2, 3].foldl (fun r a => (r.push a).push a) #[]"
 #eval run "#check #[1, 2, 3].foldl (fun r a => ((r.push a).push a).push a) #[]"
 #eval run "#check #[].push one $.push two $.push zero $.size.succ"
+#eval run "#check #[1, 2].foldl (fun r a => r.push a $.push a $.push a) #[]"