Couldn't match expected type sbv-8.8:Data.SBV.Core.Symbolic.VarContext' with actual type Maybe Quantifier'

[yurivict]

2.9.1 fails to build:

src/Cryptol/Eval/SBV.hs:71:52: error:
    * Couldn't match expected type `sbv-8.8:Data.SBV.Core.Symbolic.VarContext'
                  with actual type `Maybe Quantifier'
    * In the first argument of `svMkSymVar', namely `(Just ALL)'
      In the second argument of `(.)', namely
        `svMkSymVar (Just ALL) (KBounded False w) Nothing'
      In the second argument of `(>>=)', namely
        `liftIO . svMkSymVar (Just ALL) (KBounded False w) Nothing'
   |
71 | forallBV_ w = symbolicEnv >>= liftIO . svMkSymVar (Just ALL) (KBounded False w) Nothing
   |                                                    ^^^^^^^^

src/Cryptol/Eval/SBV.hs:74:52: error:
    * Couldn't match expected type `sbv-8.8:Data.SBV.Core.Symbolic.VarContext'
                  with actual type `Maybe Quantifier'
    * In the first argument of `svMkSymVar', namely `(Just EX)'
      In the second argument of `(.)', namely
        `svMkSymVar (Just EX) (KBounded False w) Nothing'
      In the second argument of `(>>=)', namely
        `liftIO . svMkSymVar (Just EX) (KBounded False w) Nothing'
   |
74 | existsBV_ w = symbolicEnv >>= liftIO . svMkSymVar (Just EX) (KBounded False w) Nothing
   |                                                    ^^^^^^^

src/Cryptol/Eval/SBV.hs:77:53: error:
    * Couldn't match expected type `sbv-8.8:Data.SBV.Core.Symbolic.VarContext'
                  with actual type `Maybe Quantifier'
    * In the first argument of `svMkSymVar', namely `(Just ALL)'
      In the second argument of `(.)', namely
        `svMkSymVar (Just ALL) KBool Nothing'
      In the second argument of `(>>=)', namely
        `liftIO . svMkSymVar (Just ALL) KBool Nothing'
   |
77 | forallSBool_ = symbolicEnv >>= liftIO . svMkSymVar (Just ALL) KBool Nothing
   |                                                     ^^^^^^^^

FreeBSD 12.1
ghc-8.10.2

[brianhuffman]

I think our test builds are using sbv 8.7. Perhaps we need to set an appropriate upper bound for sbv?

[atomb]

Yeah, and in the meantime you can build with cabal v2-build --constraint="sbv==8.6" (or 8.7, though it has slightly pickier requirements about the version of CVC4, if you're using that) or by setting that constraint in a cabal.project.freeze file.