Unary minus binds more tightly than exponentiation

[brianhuffman]

According to usual math conventions, - x ^^ y should parse as - (x ^^ y).

However, in Cryptol this is parsed instead as (- x) ^^ y, which surprising, inconsistent, and not useful, especially when used with an even exponent. It is inconsistent because the binary minus operator binds more loosely than exponentiation, so that e.g. w - x ^^ y parses as w - (x ^^ y).

[brianhuffman]

Note that ghci gets this right, unlike Cryptol:

Prelude> -2^8 :: Integer
-256

Cryptol> -2^^8 : Integer
256

[yav]

OK, this is because sometime ago we decided to treat - and ~ as normal prefix application. I guess this is a good example of why this is not always a good idea. It seems that the solution would be have a special node in the AST for prefix operator, and then when we do fixity rewrite have special rules to adjust fixity as needed (i.e., prefix operators can also have fixities)

I looked in the GHC source code, and that's what it does also, so there's a precedent that this might be the right solution here.

[jldodds]

When we fix this we should have a way to record if the behavior has changed and raise it in a warning