Rude orphan instance for Num (SBV (Maybe a))

[drvink]

Could you please move this instance to its own module, so that users can selectively import it? I updated to sbv 9.0 from 8.17, and now I'm in overlapping instance hell.

I could rewrite my code to avoid using SMaybe entirely--before sbv had it, I'd simply made something like data Hober a = Hober { ok :: !SBool; val :: !a } with a suitable instance Mergeable a => Mergeable (Hober a), and that worked fine--but this should be fixed in sbv anyway.

[LeventErkok]

This instance is only exported from Data.SBV.Maybe, so it is in its own file. (i.e., you don't get it if you simply import Data.SBV.)

While I don't recall the exact details of how it got added, I recall it was because of a user request. So, removing it would break someone else's code.

Note that your Hober and the SBV (Maybe a) instances are qualitatively different. Your version explicitly keeps track of a "valid" bit, while the latter doesn't have that issue as it uses an algebraic data-type internally. (i.e., there's no need to check for ok whenever you use it explicitly. If ok is false, then there's no value, guaranteed.)

Anyhow. While I agree extra instances should be written with care, I don't see why you're in an overlapping instance hell. What other definition of Num (SBV (Maybe a)) can you write anyhow? If you can explain your issue more clearly, maybe we can come up with a compromise. Otherwise, I'm hesitant to break somebody else's code.

[drvink]

I am a dingus. I didn't have my own instance for Num (SBV (Maybe a)); rather, I had instance {-# OVERLAPPABLE #-} ... => MyClass (SBV a) and a few instance {-# OVERLAPPING #-} ... => MyClass (SBV Foo), and I could have sworn I tried adding Num (SBV a) to the contexts of the functions that broke. Now it's fine. Sorry for the noise.

(And thanks for SBV; it's by far the best SMT library and driver for any language!)

[LeventErkok]

Glad it all got sorted out!