Consider removing Num a => Num (SBV a) instance

[LeventErkok]

As exemplified in #698 and #598, the (Old a, Num a, SymVal a) => Num (SBV a) instance creates lots of type-checking programs that actually do not work in practice.

The instance itself, however, is useful. It takes care of lifting of arithmetic operations over all basic types (Integers, signed/unsigned words, floats etc.); and it works like a charm. But when someone defines their own instance of Num for a custom type T, then they automatically get an Num (SBV T) for that type as well, which doesn't do what they'd have expected it to do. (It errors out in general; but there might be situations it silently does the "wrong" unexpected thing as well.)

We should consider removing the instance:

sbv/Data/SBV/Core/Model.hs

Lines 1322 to 1329 in 720255d

	-- Num instance for symbolic words.
	instance (Ord a, Num a, SymVal a) => Num (SBV a) where
	fromInteger = literal . fromIntegral
	SBV x + SBV y = SBV (svPlus x y)
	SBV x * SBV y = SBV (svTimes x y)
	SBV x - SBV y = SBV (svMinus x y)
	-- Abs is problematic for floating point, due to -0; case, so we carefully shuttle it down
	-- to the solver to avoid the can of worms. (Alternative would be to do an if-then-else here.)

This might lead to more boiler-plate code in the SBV code base itself, but it might things better in the long run. In particular, as Andreas pointed out, we can have more of "if it type checks it works" behavior that Haskell programmers expect, which is currently not the case for this instance.

[ocramz]

I just ran into this (or rather, my program was relying on the Num (SBV a) instance) while upgrading versions, but unfortunately removing it rules out a bunch of interesting programs. E.g. in my case I later instantiate it as a ~ Int64 but without having to commit to a concrete type too early in the library code.