Additive inverse property for `negate` doesn't hold for `{S,U}Fixed` and `Index`

[martijnbastiaan]

In #3000 we add property tests for additive inverses. I've found that these properties don't hold for SFixed and UFixed, as well as Index.

[martijnbastiaan]

After a quick discussion:

• Additive inverse probably don't hold for signed types in any case, because of their asymmetric nature. I.e., maxBound @(Signed 8) == 127 vs minBound @(Signed 8) == -128. We can special case these in the tests though.
• For Index addition isn't always defined, so additive inverses aren't either. Should we just always return an error in this case? Maybe we already do?

[pieter-bos]

Additive inverse probably don't hold for signed types in any case

What do you mean? the negate of -128 :: Signed 8 is -128 for that reason, so (-128 :: Signed 8) + negate (-128 :: Signed 8) == 0. Similarly for haskell types: negate (minBound :: Int) == -9223372036854775808

[pieter-bos]

Incidentally it's pretty irksome that the sign doesn't change for negate (-128 :: Signed 8), but I like to think of it as: negate -128 is 128, where the representative of 128 ("0_1000_0000") in Signed 8 is -128 ("1000_0000")

[christiaanb]

So for SFixed the additive inverse is going to be difficult because addition saturates, meaning minBound + minBound :: SFixed 8 8 == minBound

[martijnbastiaan]

Gotcha, thanks @pieter-bos.

[DigitalBrains1]

For Index, I'm worried the negate implementation leads to odd results when the NegativeLiterals option is not enabled; the default is actually that this is not enabled. So we get this odd result:

clashi> -3 :: Index 7
4
clashi> :set -XNegativeLiterals
clashi> -3 :: Index 7
*** Exception: X: Clash.Sized.Index: result -3 is out of bounds: [0..6]

This means out-of-range negative literals are treated very differently from out-of-range positive literals.

For UFixed and SFixed, I think negate should satisfy x + negate x == 0 whenever ∃y : x + y == 0, and I haven't formed an opinion on what should happen when no such y exists.