[ error ] Improve locality of parse errors in implicit arguments

src/Idris/Parser.idr

@@ -243,7 +243,8 @@ mutual
 
       braceArgs : OriginDesc -> IndentInfo -> Rule (List ArgType)
       braceArgs fname indents
-          = do start <- bounds (decoratedSymbol fname "{")
+        = do start <- bounds (decoratedSymbol fname "{")
+             mustWork $ do
                list <- sepBy (decoratedSymbol fname ",")
                         $ do x <- bounds (UN . Basic <$> decoratedSimpleNamedArg fname)
                              let fc = boundToFC fname x
@@ -1782,13 +1783,13 @@ topDecl fname indents
          pure [d]
   <|> do ds <- claims fname indents
          pure (forget ds)
+  <|> do d <- implDecl fname indents
+         pure [d]
   <|> do d <- definition fname indents
          pure [d]
   <|> fixDecl fname indents
   <|> do d <- ifaceDecl fname indents
          pure [d]
-  <|> do d <- implDecl fname indents
-         pure [d]
   <|> do d <- recordDecl fname indents
          pure [d]
   <|> do d <- namespaceDecl fname indents

tests/Main.idr

@@ -93,7 +93,8 @@ idrisTestsError = MkTestPool "Error messages" [] Nothing
        "perror001", "perror002", "perror003", "perror004", "perror005",
        "perror006", "perror007", "perror008", "perror009", "perror010",
        "perror011", "perror012", "perror013", "perror014", "perror015",
-       "perror016", "perror017", "perror018", "perror019", "perror020"]
+       "perror016", "perror017", "perror018", "perror019", "perror020",
+       "perror021"]
 
 idrisTestsInteractive : TestPool
 idrisTestsInteractive = MkTestPool "Interactive editing" [] Nothing

tests/idris2/perror021/Implicit.idr

@@ -0,0 +1,6 @@
+import Data.Vect
+
+myReverse : Vect n el -> Vect n el
+myReverse [] = []
+myReverse {n = S k} (x :: xs) =
+    replace {p=\n => Vect n el} (plusCommutative k 1) (myReverse xs ++ [x])

tests/idris2/perror021/expected

@@ -0,0 +1,11 @@
+1/1: Building Implicit (Implicit.idr)
+Error: Expected '}'.
+
+Implicit:6:15--6:17
+ 2 | 
+ 3 | myReverse : Vect n el -> Vect n el
+ 4 | myReverse [] = []
+ 5 | myReverse {n = S k} (x :: xs) =
+ 6 |     replace {p=\n => Vect n el} (plusCommutative k 1) (myReverse xs ++ [x])
+                   ^^
+

tests/idris2/perror021/run

@@ -0,0 +1,4 @@
+rm -rf build
+
+$1 --no-banner --no-color --console-width 0 --check Implicit.idr
+