From bfca7e32e0bf6432d1cbc67b72549467fe1e03f4 Mon Sep 17 00:00:00 2001
From: Leonardo de Moura <leonardo@microsoft.com>
Date: Thu, 19 Dec 2019 14:20:56 -0800
Subject: [PATCH] fix: try to postpone if function type is not known

---
 src/Init/Lean/Elab/TermApp.lean | 2 ++
 tests/lean/run/frontend1.lean   | 1 +
 2 files changed, 3 insertions(+)

diff --git a/src/Init/Lean/Elab/TermApp.lean b/src/Init/Lean/Elab/TermApp.lean
index 01d061abaa..48544a5822 100644
--- a/src/Init/Lean/Elab/TermApp.lean
+++ b/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
diff --git a/tests/lean/run/frontend1.lean b/tests/lean/run/frontend1.lean
index 53ac7bcaec..5fb1d3cdbc 100644
--- a/tests/lean/run/frontend1.lean
+++ b/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) #[]"