fix: ensure expectedType at fun body

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.

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

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
 

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 > ·)