From 2ee1821f13116a06d6ddc82667004f5b8e8d1bd1 Mon Sep 17 00:00:00 2001
From: Leonardo de Moura <leonardo@microsoft.com>
Date: Sun, 13 Sep 2020 13:41:43 -0700
Subject: [PATCH] fix: ensure `expectedType` at `fun` body

---
 src/Lean/Elab/Binders.lean    | 5 ++++-
 tests/lean/binsearch.lean     | 4 ++--
 tests/lean/run/array1.lean    | 8 ++++----
 tests/lean/run/coelambda.lean | 7 +++++++
 4 files changed, 17 insertions(+), 7 deletions(-)
 create mode 100644 tests/lean/run/coelambda.lean

diff --git a/src/Lean/Elab/Binders.lean b/src/Lean/Elab/Binders.lean
index 0532b3fa34..dbed857e20 100644
--- a/src/Lean/Elab/Binders.lean
+++ b/src/Lean/Elab/Binders.lean
@@ -435,7 +435,10 @@ else do
     withMacroExpansion stx newStx $ elabTerm newStx expectedType?
   else
     elabFunBinders binders expectedType? $ fun xs expectedType? => do
-      e ← elabTerm body expectedType?;
+      /- We ensure the expectedType here since it will force coercions to be applied if needed.
+         If we just use `elabTerm`, then we will need to a coercion `Coe (α → β) (α → δ)` whenever there is a coercion `Coe β δ`,
+         and another instance for the dependent version. -/
+      e ← elabTermEnsuringType body expectedType?;
       mkLambdaFVars xs e
 
 /- If `useLetExpr` is true, then a kernel let-expression `let x : type := val; body` is created.
diff --git a/tests/lean/binsearch.lean b/tests/lean/binsearch.lean
index d8ff922ca5..a3a411edc2 100644
--- a/tests/lean/binsearch.lean
+++ b/tests/lean/binsearch.lean
@@ -7,9 +7,9 @@ def tst (n : Nat) : IO Unit :=
 do
 let as := mkAssocArray n Array.empty;
 IO.println as;
-let as := as.qsort (fun a b => decide $ a.1 < b.1);
+let as := as.qsort (fun a b => a.1 < b.1);
 (2*n).forM $ fun i => do
-  let entry := as.binSearch (i, false) (fun a b => decide $ a.1 < b.1);
+  let entry := as.binSearch (i, false) (fun a b => a.1 < b.1);
   IO.println (">> " ++ toString i ++ " ==> " ++ toString entry)
 
 #eval tst 10
diff --git a/tests/lean/run/array1.lean b/tests/lean/run/array1.lean
index c8df726c83..60bd915c36 100644
--- a/tests/lean/run/array1.lean
+++ b/tests/lean/run/array1.lean
@@ -49,10 +49,10 @@ def tst : IO (List Nat) :=
 
 #eval tst
 
-#eval #[1, 3, 6, 2].getMax? (fun a b => decide $ a < b)
-#eval #[].getMax? (fun (a b : Nat) => decide $ a < b)
-#eval #[1, 8].getMax? (fun a b => decide $ a < b)
-#eval #[8, 1].getMax? (fun a b => decide $ a < b)
+#eval #[1, 3, 6, 2].getMax? (fun a b => a < b)
+#eval #[].getMax? (fun (a b : Nat) => a < b)
+#eval #[1, 8].getMax? (fun a b => a < b)
+#eval #[8, 1].getMax? (fun a b => a < b)
 
 #eval #[1, 6, 5, 3, 8, 2, 0].partition fun x => x % 2 == 0
 
diff --git a/tests/lean/run/coelambda.lean b/tests/lean/run/coelambda.lean
new file mode 100644
index 0000000000..d809d8f87c
--- /dev/null
+++ b/tests/lean/run/coelambda.lean
@@ -0,0 +1,7 @@
+new_frontend
+
+#eval #[2, 3, 1, 0].qsort fun a b => a < b
+#eval #[2, 3, 1, 0].qsort fun a b => let x := a; x < b
+#eval #[2, 3, 1, 0].qsort (· < ·)
+#eval #[2, 3, 1, 0].filter (· > 1)
+#eval #[2, 3, 1, 0].filter (2 > ·)