[ error ] Improve error messages for Delay &co

idris-lang · Aug 3, 2023 · bc4176d · bc4176d
1 parent b7bda5e
commit bc4176d
Show file tree

Hide file tree

Showing 6 changed files with 43 additions and 5 deletions.
diff --git a/src/Idris/Parser.idr b/src/Idris/Parser.idr
@@ -946,16 +946,20 @@ mutual
   lazy : OriginDesc -> IndentInfo -> Rule PTerm
   lazy fname indents
       = do tm <- bounds (decorate fname Typ (exactIdent "Lazy")
-                         *> simpleExpr fname indents)
+                         *> simpleExpr fname indents
+                         <* mustFailBecause "Lazy only takes one argument" (continue indents >> simpleExpr fname indents))
            pure (PDelayed (boundToFC fname tm) LLazy tm.val)
     <|> do tm <- bounds (decorate fname Typ (exactIdent "Inf")
-                         *> simpleExpr fname indents)
+                         *> simpleExpr fname indents
+                         <* mustFailBecause "Inf only takes one argument" (continue indents >> simpleExpr fname indents))
            pure (PDelayed (boundToFC fname tm) LInf tm.val)
     <|> do tm <- bounds (decorate fname Data (exactIdent "Delay")
-                         *> simpleExpr fname indents)
+                         *> simpleExpr fname indents
+                         <* mustFailBecause "Delay only takes one argument" (continue indents >> simpleExpr fname indents))
            pure (PDelay (boundToFC fname tm) tm.val)
     <|> do tm <- bounds (decorate fname Data (exactIdent "Force")
-                         *> simpleExpr fname indents)
+                         *> simpleExpr fname indents
+                         <* mustFailBecause "Force only takes one argument" (continue indents >> simpleExpr fname indents))
            pure (PForce (boundToFC fname tm) tm.val)
 
   binder : OriginDesc -> IndentInfo -> Rule PTerm

diff --git a/src/Libraries/Text/Parser/Core.idr b/src/Libraries/Text/Parser/Core.idr
@@ -278,6 +278,13 @@ export %inline
 bounds : Grammar state tok c ty -> Grammar state tok c (WithBounds ty)
 bounds = Bounds
 
+export
+mustFailBecause :
+  String ->
+  Grammar state tok True ty -> Grammar state tok False Unit
+mustFailBecause msg p
+  = (bounds p >>= \res => fatalLoc {c=False} res.bounds msg) <|> pure ()
+
 export %inline
 position : Grammar state tok False Bounds
 position = Position

diff --git a/tests/Main.idr b/tests/Main.idr
@@ -96,7 +96,7 @@ idrisTestsError = MkTestPool "Error messages" [] Nothing
        "perror011", "perror012", "perror013", "perror014", "perror015",
        "perror016", "perror017", "perror018", "perror019", "perror020",
        "perror021", "perror022", "perror023", "perror024", "perror025",
-       "perror026", "perror027", "perror028"]
+       "perror026", "perror027", "perror028", "perror029"]
 
 idrisTestsInteractive : TestPool
 idrisTestsInteractive = MkTestPool "Interactive editing" [] Nothing

diff --git a/tests/idris2/perror029/DelayParse.idr b/tests/idris2/perror029/DelayParse.idr
@@ -0,0 +1,13 @@
+module DelayParse
+
+public export
+data MyStream : Type where
+  (::) :  (anA : a)
+       -> (nextA : a -> a)
+       -> Inf MyStream
+       -> MyStream
+
+public export
+go : a -> (a -> a) -> MyStream
+go initA fn =
+  MyStream.(::) initA fn (Delay (fn initA) fn)
diff --git a/tests/idris2/perror029/expected b/tests/idris2/perror029/expected
@@ -0,0 +1,11 @@
+1/1: Building DelayParse (DelayParse.idr)
+Error: Delay only takes one argument.
+
+DelayParse:13:44--13:46
+ 09 | 
+ 10 | public export
+ 11 | go : a -> (a -> a) -> MyStream
+ 12 | go initA fn =
+ 13 |   MyStream.(::) initA fn (Delay (fn initA) fn)
+                                                 ^^
+
diff --git a/tests/idris2/perror029/run b/tests/idris2/perror029/run
@@ -0,0 +1,3 @@
+rm -rf build
+
+$1 --no-color --console-width 0 --check DelayParse.idr