From d289ed653d6da7e3ff2e8a8f47007b4e7dcf7d1d Mon Sep 17 00:00:00 2001
From: Guillaume ALLAIS <guillaume.allais@ens-lyon.org>
Date: Tue, 31 Aug 2021 19:04:23 +0100
Subject: [PATCH] [ fix #1887 ] Parse `_ <-` as DoBind instead of DoBinPat

---
 src/Idris/Parser.idr               |  6 +++---
 src/Libraries/Text/Parser.idr      |  5 +++++
 tests/Main.idr                     |  1 +
 tests/idris2/basic061/IgnoreDo.idr | 16 ++++++++++++++++
 tests/idris2/basic061/expected     |  8 ++++++++
 tests/idris2/basic061/input        |  4 ++++
 tests/idris2/basic061/run          |  3 +++
 7 files changed, 40 insertions(+), 3 deletions(-)
 create mode 100644 tests/idris2/basic061/IgnoreDo.idr
 create mode 100644 tests/idris2/basic061/expected
 create mode 100644 tests/idris2/basic061/input
 create mode 100755 tests/idris2/basic061/run

diff --git a/src/Idris/Parser.idr b/src/Idris/Parser.idr
index 1746220c7..1f42157be 100644
--- a/src/Idris/Parser.idr
+++ b/src/Idris/Parser.idr
@@ -843,13 +843,13 @@ mutual
 
   validPatternVar : Name -> EmptyRule ()
   validPatternVar (UN n)
-      = if lowerFirst n then pure ()
-                        else fail "Not a pattern variable"
+      = unless (lowerFirst n || n == "_") $
+          fail "Not a pattern variable"
   validPatternVar _ = fail "Not a pattern variable"
 
   doAct : OriginDesc -> IndentInfo -> Rule (List PDo)
   doAct fname indents
-      = do b <- bounds (do n <- bounds name
+      = do b <- bounds (do n <- bounds (name <|> UN "_" <$ symbol "_")
                            -- If the name doesn't begin with a lower case letter, we should
                            -- treat this as a pattern, so fail
                            validPatternVar n.val
diff --git a/src/Libraries/Text/Parser.idr b/src/Libraries/Text/Parser.idr
index 4f6d419ae..3ace86bca 100644
--- a/src/Libraries/Text/Parser.idr
+++ b/src/Libraries/Text/Parser.idr
@@ -226,3 +226,8 @@ public export
 when : Bool -> Lazy (Grammar state token False ()) -> Grammar state token False ()
 when True y = y
 when False y = pure ()
+
+public export
+%inline
+unless : Bool -> Lazy (Grammar state token False ()) -> Grammar state token False ()
+unless = when . not
diff --git a/tests/Main.idr b/tests/Main.idr
index f5dbdebc5..d538982fc 100644
--- a/tests/Main.idr
+++ b/tests/Main.idr
@@ -41,6 +41,7 @@ idrisTestsBasic = MkTestPool "Fundamental language features" [] Nothing
        "basic046", "basic047",             "basic049", "basic050",
        "basic051", "basic052", "basic053", "basic054", "basic055",
        "basic056", "basic057", "basic058", "basic059", "basic060",
+       "basic061",
        "interpolation001", "interpolation002"]
 
 idrisTestsCoverage : TestPool
diff --git a/tests/idris2/basic061/IgnoreDo.idr b/tests/idris2/basic061/IgnoreDo.idr
new file mode 100644
index 000000000..770d606b0
--- /dev/null
+++ b/tests/idris2/basic061/IgnoreDo.idr
@@ -0,0 +1,16 @@
+module IgnoreDo
+
+bound : Maybe () -> Maybe b -> Maybe b
+bound m n = do
+  x <- m
+  n
+
+ignored : Maybe () -> Maybe b -> Maybe b
+ignored m n = do
+  _ <- m
+  n
+
+seqd : Maybe () -> Maybe b -> Maybe b
+seqd m n = do
+  m
+  n
diff --git a/tests/idris2/basic061/expected b/tests/idris2/basic061/expected
new file mode 100644
index 000000000..d779bb96f
--- /dev/null
+++ b/tests/idris2/basic061/expected
@@ -0,0 +1,8 @@
+1/1: Building IgnoreDo (IgnoreDo.idr)
+IgnoreDo> IgnoreDo.bound : Maybe () -> Maybe b -> Maybe b
+bound m n = m >>= (\x => n)
+IgnoreDo> IgnoreDo.ignored : Maybe () -> Maybe b -> Maybe b
+ignored m n = m >>= (\_ => n)
+IgnoreDo> IgnoreDo.seqd : Maybe () -> Maybe b -> Maybe b
+seqd m n = m >> Delay n
+IgnoreDo> Bye for now!
diff --git a/tests/idris2/basic061/input b/tests/idris2/basic061/input
new file mode 100644
index 000000000..83c58fa76
--- /dev/null
+++ b/tests/idris2/basic061/input
@@ -0,0 +1,4 @@
+:printdef bound
+:printdef ignored
+:printdef seqd
+:q
diff --git a/tests/idris2/basic061/run b/tests/idris2/basic061/run
new file mode 100755
index 000000000..718b7d8aa
--- /dev/null
+++ b/tests/idris2/basic061/run
@@ -0,0 +1,3 @@
+rm -rf build
+
+$1 --no-color --console-width 0 --no-banner IgnoreDo.idr < input