idris-lang/Idris-dev — pull request #504 by david-christiansen (2013-09-29 01:38:32+00:00)
Title: Make parens mandatory after with - vastly improving the error message

Right now, parentheses are required around any non-atomic expressions that are
the scrutinee of a with-rule. In practice, this means that almost all
expressions require parentheses, as with is typically used to introduce more
information that was not available in the outer pattern match.

In the standard library, the only place where with rules occur without
parentheses is in Data.Bits.

Making the parentheses mandatory vastly improves parser errors in case they
are forgotten, RE #166 .

Sample of current message:
````
./WithRule.idr:4:14: error: expected: "{",
function declaration
foo x with x == 0
^
````

Sample of message with the first patch:
`````
./WithRule.idr:4:12: error: expected: "("
foo x with x == 0
^
````
Sample of message with the second patch as well:
````
./WithRule.idr:4:12: error: expected: parenthesized expression
foo x with x == 0
^
````