From 3f32d9eb0b6e00a626fca50381fe21745ff4bc38 Mon Sep 17 00:00:00 2001
From: Leonardo de Moura <leonardo@microsoft.com>
Date: Thu, 30 Jan 2020 14:09:37 -0800
Subject: [PATCH] fix: closes #111

---
 src/Init/Lean/Elab/TermApp.lean |  6 +++---
 tests/lean/run/111.lean         | 11 +++++++++++
 2 files changed, 14 insertions(+), 3 deletions(-)
 create mode 100644 tests/lean/run/111.lean

diff --git a/src/Init/Lean/Elab/TermApp.lean b/src/Init/Lean/Elab/TermApp.lean
index 1f5131d58e..ae9076e482 100644
--- a/src/Init/Lean/Elab/TermApp.lean
+++ b/src/Init/Lean/Elab/TermApp.lean
@@ -217,9 +217,9 @@ private partial def elabAppArgsAux : ElabAppArgsCtx → Expr → Expr → TermEl
         if h : ctx.argIdx < ctx.args.size then do
           argElab ← elabArg ctx.ref e (ctx.args.get ⟨ctx.argIdx, h⟩) d;
           elabAppArgsAux { argIdx := ctx.argIdx + 1, .. ctx } (mkApp e argElab) (b.instantiate1 argElab)
-        else match d.getOptParamDefault? with
-          | some defVal => elabAppArgsAux ctx (mkApp e defVal) (b.instantiate1 defVal)
-          | none        =>
+        else match ctx.explicit, d.getOptParamDefault? with
+          | false, some defVal => elabAppArgsAux ctx (mkApp e defVal) (b.instantiate1 defVal)
+          | _, _               =>
             -- TODO: tactic auto param
             if ctx.namedArgs.isEmpty then
               finalize ()
diff --git a/tests/lean/run/111.lean b/tests/lean/run/111.lean
new file mode 100644
index 0000000000..4b3689b086
--- /dev/null
+++ b/tests/lean/run/111.lean
@@ -0,0 +1,11 @@
+import Init.Lean
+new_frontend
+open Lean
+#check mkNullNode  -- Lean.Syntax
+#check mkNullNode #[]  -- Lean.Syntax
+#check @mkNullNode
+#check
+ let f : Array Syntax → Syntax := @mkNullNode;
+ f #[]
+
+#check let f := @mkNullNode; f #[]