Optimisation with list solution: compiler error

Question

I'm trying to solve an optimisation problem with sbv in Haskell, but get a compiler error.

The solution is a list of values, and I have a function to check the solution is valid (the constraint), and a function to calculate a number to minimize.

I get this compiler error on my minimal example:

/home/t/sbvExample/Main.hs:28:5: error:
    • No instance for (S.SymVal S.SBool)
        arising from a use of ‘Sl.length’
    • In the expression: Sl.length xs
      In an equation for ‘toNum’: toNum xs = Sl.length xs
   |
28 |     Sl.length xs
   |     ^^^^^^^^^^^^

Here's the code:

{-# LANGUAGE ScopedTypeVariables #-} 
module Main (main) where

import qualified Data.SBV.List as Sl
import qualified Data.SBV as S


main :: IO ()
main = do
    result <- S.optimize S.Lexicographic help
    print result


help :: S.SymbolicT IO ()
help = do
    xs :: S.SList S.SBool <- S.sList "xs"
    S.constrain $ isValid xs
    S.minimize "goal" $ toNum xs


isValid :: S.SList S.SBool -> S.SBool
isValid xs =
    Sl.length xs S..> 0


toNum :: S.SList S.SBool -> S.SInteger
toNum xs =
    Sl.length xs

So in this silly minimal example I would expect a list containing one item.

For convenience I put it on Github, so build it with:

git clone https://github.com/8n8/sbvExample
cd sbvExample
stack build

Answer 1

You're getting this error message because there is no instance of SymVal for SBool, only for Bool, and S.length expects a S.SList of SymVal values:

length :: SymVal a => SList a -> SInteger

You can fix this by changing toNum and isValid to accept y S.SList Bool, and changing the type of xs to S.SList Bool:

help :: S.SymbolicT IO ()
help = do
    xs :: S.SList Bool <- S.sList "xs"
    S.constrain $ isValid xs
    S.minimize "goal" $ toNum xs

isValid :: S.SList Bool -> S.SBool
isValid xs =
    Sl.length xs S..> 0

toNum :: S.SList Bool -> S.SInteger
toNum xs =
    Sl.length xs

Your isValid and toNum functions are also overly specialized, since they only require a SymVal class constraint. The following is more general and still compiles:

isValid :: S.SymVal a => S.SList a -> S.SBool
toNum :: S.SymVal a => S.SList a -> S.SInteger

EDIT

Weren't it for toNum failing to typecheck, you would have also seen that S.sList also doesn't typecheck, since its type signature has a SymVal constraint on the type parameter of the returned S.SList:

sList :: SymVal a => String -> Symbolic (SList a)

Deleting isValid and toNum, and only keeping the S.sList constructor:

help = do
    xs :: S.SList S.SBool <- S.sList "xs"
    return ()

throws this error:

• No instance for (S.SymVal S.SBool)
    arising from a use of ‘S.sList’

Which, in my opinion, tells a bit more about the actual issue. It just goes to show that a minimal example can sometimes be even more minimal, and therefore more helpful.

Answer 2

From the documentation for SList:

Note that a symbolic list is not a list of symbolic items, that is, it is not the case that SList a = [a], unlike what one might expect following haskell lists/sequences. An SList is a symbolic value of its own, of possibly arbitrary but finite length, and internally processed as one unit as opposed to a fixed-length list of items.

So if you're going to use an SList, then you need to use it with regular Bools, not SBools.