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.)
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.
As exemplified in https://github.com/LeventErkok/sbv/issues/698 and https://github.com/LeventErkok/sbv/issues/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
Numfor a custom typeT, then they automatically get anNum (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: https://github.com/LeventErkok/sbv/blob/720255d2a843b146d248720036a986917ee62041/Data/SBV/Core/Model.hs#L1322-L1329
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.