Eq instance for SBV

[LeventErkok]

We would really like to remove the Eq instance for SBV, since it doesn't make any sense.

However, we want Bits (SBV a). But in Haskell, Bits class has Eq as its super-class, which necessitates the Eq (SBV a). This is unfortunate. What's not clear to me is why the Bits class require Eq? This seems to be an oversight and/or historical, and perhaps might be good to take it with the proposals process to see if it can be removed.

[LeventErkok]

Historical, it seems.

[juliapath]

I think Eq is a superclass of Bits because you could implement Eq from Bits like this:

defaultEq :: Bits a => a -> a -> Bool
defaultEq x y = popCount (x `xor` y) == 0

Also there should probably be warnings in the documentation of the Eq and Bits instances that some of the functions (==/popCount/testBit) are partial. Currently the documentation of Eq just says, that equality constraints on SBV values are undesirable and there is no documentation for the Bits instance. Furthermore I think that should be equality tests not equality constraints, as constraints usually refer to the type-level constraints in Haskell and an equality test doesn't really constrain anything.

[LeventErkok]

popCount was added to the Bits class long after it first showed up, but that's a good point that it gives a default way to implement equality. Note that this is also the reason why SBV defines it's own popCount method as we cannot return a Haskell Int on a symbolic value.

Regarding documentation improvements: Pull requests are always welcome! Please submit a patch.