Crash on sat \(a :: SMaybe Word8) (b :: SMaybe Word8) -> a + b .>= 10

[yaitskov]

Hi,

import Data.SBV

 r <- sat $ do { 
   x :: SMaybe Word8 <- exists "x" 
   y :: SMaybe Word8 <- exists "y"; 
   pure (x + y .>= 10)
}

<interactive>:59:108: error:
    • No instance for (Num (Maybe Word8)) arising from a use of ‘+’
    • In the first argument of ‘(.>=)’, namely ‘x + y’

I added:

instance Num a => Num (Maybe a) where
  x + y = (+) <$> x <*> y
  x - y = (-) <$> x <*> y
  x * y = (*) <$> x <*> y
  negate = fmap negate
  abs = fmap abs
  signum = fmap signum
  fromInteger = pure . fromInteger

Type error disappeared, but ghci started getting exception:

r <- sat $ do { 
  x :: SMaybe Word8 <- Data.SBV.exists "x"
  y :: SMaybe Word8 <- Data.SBV.exists "y"
  pure (x + y .>= 10) 
}

*** Exception: SBV.SMT.SMTLib2.cvtExp.sh: impossible happened; can't translate: s0 + s1
CallStack (from HasCallStack):
error, called at ./Data/SBV/SMT/SMTLib2.hs:996:18 in sbv-8.14-be341a06b763cd4a2cbdf74551cb63b06d28a1b5f0f9630d2a3fd28fcbb1f9fd:Data.SBV.SMT.SMTLib2

[LeventErkok]

You're breaking internal invariants by adding that Num (Maybe a) type. For symbolic computation, internal definitions crucially rely on how the symbolic expressions get computed. Instead, be explicit in your intention. You should write something like:

{-# LANGUAGE ScopedTypeVariables #-}

import Data.SBV
import Data.SBV.Maybe as SM

test = sat $ do
   mx :: SMaybe Word8 <- free "mx"
   my :: SMaybe Word8 <- free "my"

   constrain $ SM.isJust mx
   constrain $ SM.isJust my

   let x = SM.fromJust mx
       y = SM.fromJust my

   pure $ x + y .>= 10

I get:

*Main> test
Satisfiable. Model:
  mx = Just 16 :: Maybe Word8
  my =  Just 0 :: Maybe Word8

Does this address your problem?

[yaitskov]

Thanks, kind of it is solves, because I got a new view on the problem.
Bad news is that abstraction leaks here and there is runtime error instead of compile time one.

[LeventErkok]

If you want to do it the right way, you can code it as follows:

{-# LANGUAGE FlexibleInstances    #-}
{-# LANGUAGE ScopedTypeVariables  #-}
{-# OPTIONS_GHC -fno-warn-orphans #-}

import Data.SBV
import qualified Data.SBV.Maybe as SM

lift2 :: (SymVal a, SymVal b, SymVal c) => (SBV a -> SBV b -> SBV c) -> SMaybe a -> SMaybe b -> SMaybe c
lift2 op mx my = ite (SM.isJust mx .&& SM.isJust my)
                     (SM.sJust (SM.fromJust mx `op` SM.fromJust my))
                     SM.sNothing

instance {-# OVERLAPPING #-} (Ord a, SymVal a, Num a) => Num (SBV (Maybe a)) where
  (+)         = lift2 (+)
  (-)         = lift2 (-)
  (*)         = lift2 (*)
  abs         = SM.map abs
  signum      = SM.map signum
  fromInteger = SM.sJust . fromInteger

test :: IO SatResult
test = sat $ do
   x :: SMaybe Word8 <- exists "x"
   y :: SMaybe Word8 <- exists "y"
   pure (x + y .>= 10)

Now I get:

*Main> test
Satisfiable. Model:
  x = Just 21 :: Maybe Word8
  y =  Just 0 :: Maybe Word8

Having said that, I think the "explicit" version is preferable in this case. Too much type-class hackery like this hardly every pays off. But your mileage might vary.

[LeventErkok]

@yaitskov

On second thought, I think you have a point that SBV can make this easier for end users. As of e9706c3, you can now say:

{-# LANGUAGE ScopedTypeVariables #-}

import Data.SBV
import Data.SBV.Maybe () -- instances only

test :: IO SatResult
test = sat $ do
   x :: SMaybe Word8 <- exists "x"
   y :: SMaybe Word8 <- exists "y"
   pure (x + y .>= 10)

And get:

*Main> test
Satisfiable. Model:
  x = Just 21 :: Maybe Word8
  y =  Just 0 :: Maybe Word8

Note that the import Data.SBV.Maybe is required as otherwise you wouldn't have the necessary instance declaration. This is a bit unfortunate, but it avoids pollution of the instance space unless you really mean to have this particular case available.

[yaitskov]

I owe SBV premium support ;)
Thanks.