From e35f79feb5ee56ac634437d65d515a2f6620d7c7 Mon Sep 17 00:00:00 2001
From: Leonardo de Moura <leonardo@microsoft.com>
Date: Wed, 12 Feb 2020 12:26:24 -0800
Subject: [PATCH] feat: postpone only if inferred type is unknown and there are
 arguments

---
 src/Init/Lean/Elab/App.lean | 3 ++-
 1 file changed, 2 insertions(+), 1 deletion(-)

diff --git a/src/Init/Lean/Elab/App.lean b/src/Init/Lean/Elab/App.lean
index 313b603e40..30944ce5d9 100644
--- a/src/Init/Lean/Elab/App.lean
+++ b/src/Init/Lean/Elab/App.lean
@@ -271,7 +271,8 @@ private def elabAppArgs (ref : Syntax) (f : Expr) (namedArgs : Array NamedArg) (
 fType ← inferType ref f;
 fType ← instantiateMVars ref fType;
 trace `Elab.app.args ref $ fun _ => "explicit: " ++ toString explicit ++ ", " ++ f ++ " : " ++ fType;
-tryPostponeIfMVar fType;
+unless (namedArgs.isEmpty && args.isEmpty) $
+  tryPostponeIfMVar fType;
 elabAppArgsAux {ref := ref, args := args, expectedType? := expectedType?, explicit := explicit, namedArgs := namedArgs } f fType
 
 /-- Auxiliary inductive datatype that represents the resolution of an `LVal`. -/