Nested calls to prove is unsound, and are thus rejected

[LeventErkok]

From a programmability perspective, it's nice to be able to embed arbitrary IO actions into a symbolic computation, and SBV allows this via the usual call to liftIO. But this is unsound if that IO action happens to create symbolic variables itself, which then gets conflated with the calling context. SBV has a dynamic check to reject such scenarios, where you'll get an error of the form:

*** Exception: Data.SBV: Mismatched contexts detected.
***
*** Current context: SBVContext 1220800691632037763
*** Mixed with     : SBVContext (-5269368573634985637)
***
*** This happens if you call a proof-function (prove/sat) etc.
*** while another one is in execution. Avoid such nested calls.
*** See https://github.com/LeventErkok/sbv/issues/71 for examples.

It would be nice if this was caught as a type-error: Alas the design for that requires a complete rewrite of how the Symbolic monad works, similar to how runST operates. Unfortunately, this is not feasible for the time being, due to backwards-compatibility concerns and making the types involved even more complicated. So, we catch such uses dynamically and error out as an "acceptable crutch."

If you run into the above message, see if your use is similar to the examples below. In general, you should never make a call to prove/sat etc. while running another SBV call. The typical case for this is the incremental use of solvers, and for that you should use the query-mode of SBV, which handles such interactions in a safe way.

Here's a few examples to demonstrate the kinds of problems that cause this issue:

{-# OPTIONS_GHC -Wall -Werror #-}

import Data.SBV
import Data.SBV.Control
import Control.Monad.Trans

bug1 :: IO ThmResult
bug1 = proveWith z3{verbose=True} $ do
  x <- free "x"
  y <- free "y"
  liftIO $ f x y
 where f :: SWord32 -> SWord32 -> IO SBool
       f x y = do
         res <- isSatisfiableWith z3{verbose=True} $ x .== y
         return $ if res then sTrue else sFalse

bug2 :: IO ThmResult
bug2 = proveWith z3{verbose=True} $ do
  x <- free "x"
  liftIO $ f x
 where f :: SWord32 -> IO SBool
       f x = do
         res <- isSatisfiableWith z3{verbose=True} $ x .== 2
         return $ if res then sTrue else sFalse

bug3 :: IO ThmResult
bug3 = proveWith z3{verbose=True} $ do
        y <- sBool "y"
        x <- lift leak        -- reach in!
        return $ y .== x
  where leak :: IO SBool
        leak = runSMTWith z3{verbose=True} $ do
                        x <- sBool "x"
                        query $ pure x

All of these behave in bad ways, compromising soundness. Thus SBV catches them at run-time and flags such uses as an error.