From 136fab07238b508c59a43d9b3cc68cbec7dc35e7 Mon Sep 17 00:00:00 2001
From: Leonardo de Moura <leonardo@microsoft.com>
Date: Tue, 14 Dec 2021 08:56:22 -0800
Subject: [PATCH] =?UTF-8?q?feat:=20improve=20error=20message=20for=20`let?=
 =?UTF-8?q?=20...=20=E2=86=90=20...`=20outside=20of=20a=20`do`?=
MIME-Version: 1.0
Content-Type: text/plain; charset=UTF-8
Content-Transfer-Encoding: 8bit

---
 src/Lean/Parser/Term.lean                      | 14 +++++++++++++-
 tests/lean/letArrowOutsideDo.lean              |  3 +++
 tests/lean/letArrowOutsideDo.lean.expected.out |  1 +
 3 files changed, 17 insertions(+), 1 deletion(-)
 create mode 100644 tests/lean/letArrowOutsideDo.lean
 create mode 100644 tests/lean/letArrowOutsideDo.lean.expected.out

diff --git a/src/Lean/Parser/Term.lean b/src/Lean/Parser/Term.lean
index 695a32dc31..82a51f6f53 100644
--- a/src/Lean/Parser/Term.lean
+++ b/src/Lean/Parser/Term.lean
@@ -169,7 +169,19 @@ def simpleBinderWithoutType := nodeWithAntiquot "simpleBinder" `Lean.Parser.Term
 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
+/-
+  Remark: the following `(" := " <|> matchAlts)` is a hack we use to produce a better error message at `letDecl`.
+  Consider this following example
+  ```
+  def myFun (n : Nat) : IO Nat :=
+    let q ← (10 : Nat)
+    n + q
+  ```
+  Without the hack, we get the error `expected '|'` at `←`. Reason: at `letDecl`, we use the parser `(letIdDecl <|> letPatDecl <|> letEqnsDecl)`,
+  `letIdDecl` and `letEqnsDecl` have the same prefix `letIdLhs`, but `letIdDecl` uses `atomic`.
+  Note that the hack relies on the fact that the parser `":="` never succeeds at `(" := " <|> matchAlts)`. It is there just to make sure we produce the error `expected ':=' or '|'`
+-/
+def letEqnsDecl := nodeWithAntiquot "letEqnsDecl" `Lean.Parser.Term.letEqnsDecl $ letIdLhs >> (" := " <|> matchAlts)
 -- Remark: we use `nodeWithAntiquot` here to make sure anonymous antiquotations (e.g., `$x`) are not `letDecl`
 def letDecl     := nodeWithAntiquot "letDecl" `Lean.Parser.Term.letDecl (notFollowedBy (nonReservedSymbol "rec") "rec" >> (letIdDecl <|> letPatDecl <|> letEqnsDecl))
 @[builtinTermParser] def «let» := leading_parser:leadPrec  withPosition ("let " >> letDecl) >> optSemicolon termParser
diff --git a/tests/lean/letArrowOutsideDo.lean b/tests/lean/letArrowOutsideDo.lean
new file mode 100644
index 0000000000..71ce43654c
--- /dev/null
+++ b/tests/lean/letArrowOutsideDo.lean
@@ -0,0 +1,3 @@
+def myFun (n : Nat) : IO Nat :=
+  let q ← (10 : Nat)
+  n + q
diff --git a/tests/lean/letArrowOutsideDo.lean.expected.out b/tests/lean/letArrowOutsideDo.lean.expected.out
new file mode 100644
index 0000000000..12d0a1aafa
--- /dev/null
+++ b/tests/lean/letArrowOutsideDo.lean.expected.out
@@ -0,0 +1 @@
+letArrowOutsideDo.lean:2:8: error: expected ':=' or '|'