From 830e5dc12de246a0b78c6c304e637c62590abc27 Mon Sep 17 00:00:00 2001
From: Mathew Polzin <matt.polzin@gmail.com>
Date: Wed, 14 Jul 2021 00:25:02 -0700
Subject: [PATCH] Fix bug with what value was propagated from rhs of alt parse
 failure and add test case for '@' as value constructor.

---
 src/Libraries/Text/Parser/Core.idr |  4 +++-
 tests/Main.idr                     |  2 +-
 tests/idris2/perror009/Error1.idr  |  4 ++++
 tests/idris2/perror009/expected    | 19 +++++++++++++++++++
 tests/idris2/perror009/run         |  3 +++
 tests/idris2/with003/expected      | 24 ++++++++++++------------
 6 files changed, 42 insertions(+), 14 deletions(-)
 create mode 100644 tests/idris2/perror009/Error1.idr
 create mode 100644 tests/idris2/perror009/expected
 create mode 100644 tests/idris2/perror009/run

diff --git a/src/Libraries/Text/Parser/Core.idr b/src/Libraries/Text/Parser/Core.idr
index bebd049bf..e3f5232a1 100644
--- a/src/Libraries/Text/Parser/Core.idr
+++ b/src/Libraries/Text/Parser/Core.idr
@@ -317,8 +317,10 @@ doParse s com (Alt {c1} {c2} x y) xs
                    then Failure com fatal errs
                    else case (assert_total doParse s False y xs) of
                              (Failure com'' fatal' errs') => if com'' || fatal'
+                                                                     -- Only add the errors together if the second branch
+                                                                     -- is also non-committed and non-fatal.
                                                              then Failure com fatal' errs'
-                                                             else Failure com'' fatal' (errs ++ errs')
+                                                             else Failure com False (errs ++ errs')
                              (Res s _ val xs) => Res s com val xs
            -- Successfully parsed the first option, so use the outer commit flag
            Res s _ val xs => Res s com val xs
diff --git a/tests/Main.idr b/tests/Main.idr
index 33290f2c2..47ab15d94 100644
--- a/tests/Main.idr
+++ b/tests/Main.idr
@@ -66,7 +66,7 @@ idrisTestsError = MkTestPool "Error messages" [] Nothing
        "error016", "error017", "error018", "error019",
        -- Parse errors
        "perror001", "perror002", "perror003", "perror004", "perror005",
-       "perror006", "perror007", "perror008"]
+       "perror006", "perror007", "perror008", "perror009"]
 
 idrisTestsInteractive : TestPool
 idrisTestsInteractive = MkTestPool "Interactive editing" [] Nothing
diff --git a/tests/idris2/perror009/Error1.idr b/tests/idris2/perror009/Error1.idr
new file mode 100644
index 000000000..b5c32756f
--- /dev/null
+++ b/tests/idris2/perror009/Error1.idr
@@ -0,0 +1,4 @@
+
+data Foo : Type where
+  FooBase : Foo
+  (@) : Foo -> Foo -> Foo
diff --git a/tests/idris2/perror009/expected b/tests/idris2/perror009/expected
new file mode 100644
index 000000000..e18bdd7f3
--- /dev/null
+++ b/tests/idris2/perror009/expected
@@ -0,0 +1,19 @@
+1/1: Building Error1 (Error1.idr)
+Error: Couldn't parse any alternatives:
+1: Expected name.
+
+Error1:4:3--4:4
+ 1 | 
+ 2 | data Foo : Type where
+ 3 |   FooBase : Foo
+ 4 |   (@) : Foo -> Foo -> Foo
+       ^
+2: Can't use reserved symbol @.
+
+Error1:4:4--4:5
+ 1 | 
+ 2 | data Foo : Type where
+ 3 |   FooBase : Foo
+ 4 |   (@) : Foo -> Foo -> Foo
+        ^
+
diff --git a/tests/idris2/perror009/run b/tests/idris2/perror009/run
new file mode 100644
index 000000000..045b3b74f
--- /dev/null
+++ b/tests/idris2/perror009/run
@@ -0,0 +1,3 @@
+$1 --no-color --console-width 0 --no-banner -Werror --check Error1.idr
+
+rm -rf build/
diff --git a/tests/idris2/with003/expected b/tests/idris2/with003/expected
index 9122f6f8d..01a166b26 100644
--- a/tests/idris2/with003/expected
+++ b/tests/idris2/with003/expected
@@ -32,20 +32,20 @@ Mismatch between: Vect 0 ?elem and List ?a.
 
 Main> the (Maybe Integer) (pure 4) : Maybe Integer
 Main> Couldn't parse any alternatives:
-1: Expected 'case', 'if', 'do', application or operator expression.
+1: Expected namespaced name.
+
+(Interactive):1:10--1:11
+ 1 | :t with [] 4
+              ^
+2: Expected '('.
+
+(Interactive):1:10--1:11
+ 1 | :t with [] 4
+              ^
+3: Expected 'if'.
 
 (Interactive):1:4--1:5
  1 | :t with [] 4
         ^
-2: Expected '`'.
-
-(Interactive):1:4--1:5
- 1 | :t with [] 4
-        ^
-3: Expected operator.
-
-(Interactive):1:4--1:5
- 1 | :t with [] 4
-        ^
-... (42 others)
+... (8 others)
 Main> Bye for now!