idris-lang/Idris-dev — pull request #1760 by bmsherman (2014-12-03 19:41:25+00:00)
Title: Improve parser errors in dependent type signatures

Fixes https://github.com/idris-lang/Idris-dev/issues/405. There are two changes:

- Even if implicit arguments are not allowed, still try to parse them, and then fail saying that implicits are not allowed *only* after a successful parse of the implicit arguments.
- Don't use "try" to backtrack on reading implicit arguments. I *believe* that the remaining alternative (`opExpr`) must not begin with an opening brace `{`, so this should not change parsing behavior. But someone might want to check me on this.

The new error message for
```Idris
data Labelled : Type -> Type -> Type where
(:::) : {Mark Payload : Type} -> Mark -> Payload -> Labelled Mark Payload
```
is
```
./Test.idr:2:19: error: expected: ",",
":"
(:::) : {Mark Payload : Type} -> Mark -> Payload -> Labelled Mark Payload
^
```