unhelpful error message: let in do-blocks using cons

[kasrasadeghi]

Please attach complete source files that exhibit the issue in addition to quoting from them here.

Steps to Reproduce

Main.idr:

module Main

main : IO ()
main = do
   args <- getArgs
   let filename = case args of
       [] -> "default.txt"
       [x] -> x
       x:xs -> x
   putStrLn filename

Expected Behavior

A better error message, stating the use of ':' as cons instead of '::'.

Observed Behavior

 $ idris Main.idr -o main && ./main
Main.idr:7:4:
  |
7 |    let filename = case args of
  |    ^
not end of block

[jfdm]

@kasrasadeghi I agree that the error message is unhelpful, however there is one syntax error in your example that is confusing the parser, and the root of the error: In Idris, case splits, and anonymous functions, use the fat arrow: => instead of ->.

The parser has yet to report the use of : for cons :: as it's errored on the case split body.

Here, the parser is interpreting the body of the case split i.e. the splits, as a type signature. It would be better for the parser to state that the wrong arrows are being used, but OTOH, it's backtracked sufficiently to state the problem is with the let expression.