idris-lang/Idris-dev — pull request #1762 by bmsherman (2014-12-03 20:29:21+00:00)
Title: Improve parser errors in dependent type signatures

Partially addresses https://github.com/idris-lang/Idris-dev/issues/405. There is one change:

- 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.

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

The spurious message about implicit arguments not being allowed is now gone. Unfortunately, it's difficult to produce a much better error message than this, due to custom syntax such as that in the Effects library.