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