[ parser ] Improve errors on incorrect list of determining parameters

src/Idris/Parser.idr

@@ -1359,8 +1359,10 @@ dataOpt : OriginDesc -> Rule DataOpt
 dataOpt fname
     = (decorate fname Keyword (exactIdent "noHints") $> NoHints)
   <|> (decorate fname Keyword (exactIdent "uniqueSearch") $> UniqueSearch)
-  <|> (do decorate fname Keyword (exactIdent "search")
-          SearchBy <$> some (decorate fname Bound name))
+  <|> (do b   <- bounds $ decorate fname Keyword (exactIdent "search")
+          det <- mustWorkBecause b.bounds "Expected list of determining parameters" $
+                   some (decorate fname Bound name)
+          pure $ SearchBy det)
   <|> (decorate fname Keyword (exactIdent "external") $> External)
   <|> (decorate fname Keyword (exactIdent "noNewtype") $> NoNewtype)
 
@@ -1766,7 +1768,10 @@ parameters {auto fname : OriginDesc} {auto indents : IndentInfo}
             cons   <- constraints fname indents
             n      <- decorate fname Typ name
             params <- many ifaceParam
-            det    <- optional $ decoratedSymbol fname "|" *> sepBy1 (decoratedSymbol fname ",") (decorate fname Bound name)
+            det    <- optional $ do
+              b <- bounds $ decoratedSymbol fname "|"
+              mustWorkBecause b.bounds "Expected list of determining parameters" $
+                sepBy1 (decoratedSymbol fname ",") (decorate fname Bound name)
             decoratedKeyword fname "where"
             dc <- optional (recordConstructor fname)
             body <- blockAfter col (topDecl fname)

tests/idris2/data/data004/EmptySearch.idr

@@ -0,0 +1,2 @@
+data X : Type where
+  [search]

tests/idris2/data/data004/expected

@@ -0,0 +1,8 @@
+1/1: Building EmptySearch (EmptySearch.idr)
+Error: Expected list of determining parameters.
+
+EmptySearch:2:4--2:10
+ 1 | data X : Type where
+ 2 |   [search]
+        ^^^^^^
+

tests/idris2/data/data004/run

@@ -0,0 +1,3 @@
+. ../../../testutils.sh
+
+check EmptySearch.idr

tests/idris2/data/record022/EmptySearch.idr

@@ -0,0 +1,2 @@
+record R where
+  [search]

tests/idris2/data/record022/expected

@@ -0,0 +1,8 @@
+1/1: Building EmptySearch (EmptySearch.idr)
+Error: Expected list of determining parameters.
+
+EmptySearch:2:4--2:10
+ 1 | record R where
+ 2 |   [search]
+        ^^^^^^
+

tests/idris2/data/record022/run

@@ -0,0 +1,3 @@
+. ../../../testutils.sh
+
+check EmptySearch.idr

tests/idris2/interface/interface034/expected

@@ -1,7 +1,7 @@
 1/1: Building Main (Main.idr)
-Error: Expected end of input.
+Error: Expected list of determining parameters.
 
-Main:1:1--1:10
+Main:1:17--1:18
  1 | interface Iface | where
-     ^^^^^^^^^
+                     ^