From 02acdee9cef014802e7a8055ea346c97004c0a53 Mon Sep 17 00:00:00 2001
From: Leonardo de Moura <leonardo@microsoft.com>
Date: Thu, 26 Mar 2020 14:32:12 -0700
Subject: [PATCH] feat: disable implicit lambda insertion for `fun` containing
 `{}` or `[]`

cc @Kha
---
 src/Init/Lean/Elab/Term.lean     | 10 +++++++++-
 tests/lean/run/newfrontend1.lean | 28 +++++++++++++++++++---------
 2 files changed, 28 insertions(+), 10 deletions(-)

diff --git a/src/Init/Lean/Elab/Term.lean b/src/Init/Lean/Elab/Term.lean
index a532d13cbf..1e5e15521d 100644
--- a/src/Init/Lean/Elab/Term.lean
+++ b/src/Init/Lean/Elab/Term.lean
@@ -750,11 +750,19 @@ match_syntax stx with
 private def isExplicitApp (stx : Syntax) : Bool :=
 stx.getKind == `Lean.Parser.Term.app && isExplicit (stx.getArg 0)
 
+/--
+  Return true if `stx` if a lambda abstraction containing a `{}` or `[]` binder annotation.
+  Example: `fun {α} (a : α) => a` -/
+private def isLambdaWithImplicit (stx : Syntax) : Bool :=
+match_syntax stx with
+| `(fun $binders* => $body) => binders.any $ fun b => b.isOfKind `Lean.Parser.Term.implicitBinder || b.isOfKind `Lean.Parser.Term.instBinder
+| _                         => false
+
 /--
   Return true with `expectedType` is of the form `{a : α} → β` or `[a : α] → β`, and
   `stx` is not `@f` nor `@f arg1 ...` -/
 def useImplicitLambda? (stx : Syntax) (expectedType? : Option Expr) (implicitLambda : Bool) : TermElabM (Option Expr) :=
-if !implicitLambda || isExplicit stx || isExplicitApp stx then pure none
+if !implicitLambda || isExplicit stx || isExplicitApp stx || isLambdaWithImplicit stx then pure none
 else match expectedType? with
   | some expectedType => do
     expectedType ← whnfForall stx expectedType;
diff --git a/tests/lean/run/newfrontend1.lean b/tests/lean/run/newfrontend1.lean
index 0fb0cf2fe5..5b83599338 100644
--- a/tests/lean/run/newfrontend1.lean
+++ b/tests/lean/run/newfrontend1.lean
@@ -250,16 +250,16 @@ def id4 : {α : Type} → α → α :=
 fun x => id1 x
 
 def id5 : {α : Type} → α → α :=
-@(fun α x => id1 x)
+fun {α} x => id1 x
 
 def id6 : {α : Type} → α → α :=
-@(fun α x => id1 x)
+@(fun {α} x => id1 x)
 
 def id7 : {α : Type} → α → α :=
-@(fun α x => @id α x)
+fun {α} x => @id α x
 
 def id8 : {α : Type} → α → α :=
-@(fun α x => id (@id α x))
+fun {α} x => id (@id α x)
 
 def altTst1 {m σ} [Alternative m] [Monad m] : Alternative (StateT σ m) :=
 ⟨StateT.failure, StateT.orelse⟩
@@ -268,7 +268,7 @@ def altTst2 {m σ} [Alternative m] [Monad m] : Alternative (StateT σ m) :=
 ⟨@(fun α => StateT.failure), @(fun α => StateT.orelse)⟩
 
 def altTst3 {m σ} [Alternative m] [Monad m] : Alternative (StateT σ m) :=
-⟨@(fun α => StateT.failure), @(fun α => StateT.orelse)⟩
+⟨fun {α} => StateT.failure, fun {α} => StateT.orelse⟩
 
 def altTst4 {m σ} [Alternative m] [Monad m] : Alternative (StateT σ m) :=
 ⟨@StateT.failure _ _ _ _, @StateT.orelse _ _ _ _⟩
@@ -308,19 +308,29 @@ def tst1 : {α : Type} → α → α :=
 
 syntax ident "==>" term : term
 
+syntax "{" ident "}" "==>" term : term
+
 macro_rules
-| `($x:ident ==> $b) => `(fn $x => $b)
+| `($x:ident ==> $b)   => `(fn $x => $b)
+| `({$x:ident} ==> $b) => `(fun {$x:ident} => $b)
 
 #check x ==> x+1
 
-def tst2 : {α : Type} → α → α :=
+def tst2a : {α : Type} → α → α :=
 @(α ==> a ==> a)
 
-#check @tst2
+def tst2b : {α : Type} → α → α :=
+{α} ==> a ==> a
 
-def tst3 : {α : Type} → {β : Type} → α → β → α × β :=
+#check @tst2a
+#check @tst2b
+
+def tst3a : {α : Type} → {β : Type} → α → β → α × β :=
 @(α ==> @(β ==> a ==> b ==> (a, b)))
 
+def tst3b : {α : Type} → {β : Type} → α → β → α × β :=
+{α} ==> {β} ==> a ==> b ==> (a, b)
+
 syntax "function" (term:max)+ "=>" term : term
 
 macro_rules