From db8eaad410074b0bd2967c69012312948e84d37f Mon Sep 17 00:00:00 2001
From: Leonardo de Moura <leonardo@microsoft.com>
Date: Wed, 29 Jan 2020 03:50:21 -0800
Subject: [PATCH] fix: propagate only

---
 src/Init/Lean/Elab/TermApp.lean | 8 +++++++-
 1 file changed, 7 insertions(+), 1 deletion(-)

diff --git a/src/Init/Lean/Elab/TermApp.lean b/src/Init/Lean/Elab/TermApp.lean
index 3f903b4ea9..c80fe39221 100644
--- a/src/Init/Lean/Elab/TermApp.lean
+++ b/src/Init/Lean/Elab/TermApp.lean
@@ -83,7 +83,13 @@ private partial def elabAppArgsAux (ref : Syntax) (args : Array Arg) (expectedTy
 | argIdx, namedArgs, instMVars, eType, e => do
   let finalize : Unit → TermElabM Expr := fun _ => do {
     -- all user explicit arguments have been consumed
-    e ← ensureHasTypeAux ref expectedType? eType e;
+    match expectedType? with
+    | none              => pure ()
+    | some expectedType => do {
+      -- Try to propagate expected type. Ignore if types are not definitionally equal, caller must handle it.
+      isDefEq ref expectedType eType;
+      pure ()
+    };
     synthesizeAppInstMVars ref instMVars;
     pure e
   };