From 200a38e20c8cf09290ae8c2e8d0c2d1ac42d40ec Mon Sep 17 00:00:00 2001
From: Leonardo de Moura <leonardo@microsoft.com>
Date: Tue, 28 Sep 2021 18:10:25 -0700
Subject: [PATCH] feat: improve `letIdLhs` parser

The extra space is only really needed to distinguish an array update (NIY)
```
let x[i] := ...
```
from a declaration taking an instance argument
```
let f [Monad m] := ...
```

closes #696
---
 src/Lean/Parser/Term.lean |  2 +-
 tests/lean/run/696.lean   | 20 ++++++++++++++++++++
 2 files changed, 21 insertions(+), 1 deletion(-)
 create mode 100644 tests/lean/run/696.lean

diff --git a/src/Lean/Parser/Term.lean b/src/Lean/Parser/Term.lean
index 163275cf91..3f8ccb2562 100644
--- a/src/Lean/Parser/Term.lean
+++ b/src/Lean/Parser/Term.lean
@@ -166,7 +166,7 @@ def simpleBinderWithoutType := nodeWithAntiquot "simpleBinder" `Lean.Parser.Term
   (many1 binderIdent >> pushNone)
 
 /- Remark: we use `checkWsBefore` to ensure `let x[i] := e; b` is not parsed as `let x [i] := e; b` where `[i]` is an `instBinder`. -/
-def letIdLhs    : Parser := ident >> checkWsBefore "expected space before binders" >> many (ppSpace >> (simpleBinderWithoutType <|> bracketedBinder)) >> optType
+def letIdLhs    : Parser := ident >> notFollowedBy (checkNoWsBefore "" >> "[") "space is required before instance '[...]' binders to distinguish them from array updates `let x[i] := e; ...`" >> many (ppSpace >> (simpleBinderWithoutType <|> bracketedBinder)) >> optType
 def letIdDecl   := nodeWithAntiquot "letIdDecl"   `Lean.Parser.Term.letIdDecl   $ atomic (letIdLhs >> " := ") >> termParser
 def letPatDecl  := nodeWithAntiquot "letPatDecl"  `Lean.Parser.Term.letPatDecl  $ atomic (termParser >> pushNone >> optType >> " := ") >> termParser
 def letEqnsDecl := nodeWithAntiquot "letEqnsDecl" `Lean.Parser.Term.letEqnsDecl $ letIdLhs >> matchAlts
diff --git a/tests/lean/run/696.lean b/tests/lean/run/696.lean
new file mode 100644
index 0000000000..9c473b60d6
--- /dev/null
+++ b/tests/lean/run/696.lean
@@ -0,0 +1,20 @@
+def four1 := double 2
+where double (n : Nat) : Nat := 2 * n
+
+def four2 := double 2
+where double : Nat → Nat := fun n => 2 * n
+
+def four3 := double 2
+where double(n : Nat) : Nat := 2 * n
+
+def four4 := double 2
+where double: Nat → Nat := fun n => 2 * n
+
+def four5 := let double(n : Nat) : Nat := 2 * n
+             double 2
+
+def four6 := let double: Nat → Nat := fun n => 2 * n
+             double 2
+
+def four7 := let rec double: Nat → Nat := fun n => 2 * n
+             double 2