why MonadPlus in result of decode and solveWith?

[jwaldmann]

This declaration

decode :: MonadPlus f => Solution -> a -> f (Decoded a)

vaguely suggests a generality that isn't really there.

If the variable in a literal is unconstrained, we can get a list of possible values

let s = Solution (const Nothing) (const Nothing)
decode s (Literal 8) :: [ Bool]
[False,True]

but this already breaks when the unconstrained literal is wrapped in a Bit:

decode s (Var $ Literal 8) :: [ Bool]
[False]

The reason is that the code at https://github.com/ekmett/ersatz/blob/master/src/Ersatz/Bit.hs#L126 will evaluate the literal not in [Bool], but in Maybe Bool, where the Alternative instance will pick the first value. This is then lifted to a singleton list, via pure in the second argument of maybe here

instance Codec Bit where
  decode sol b
      = maybe (pure False <|> pure True) pure $ 
                ... -- now we are in Maybe

This would be much easier to understand if the result type of decode was fixed to Maybe _. Same critique for n in

solveWith ::   (Monad m, MonadPlus n ...) => ...  -> m (Result, n (Decoded a))

What is the use case for MonadPlus here? All examples I know, do use Maybe.

[jwaldmann]

slightly related: this is ambiguous

ghci> print =<< ( solveWith minisat $ return $ Bits [false,true])

<interactive>:5:1: error:
    • Ambiguous type variable ‘n0’ arising from a use of ‘print’

but this works:

ghci> print =<< ( solveWith @IO @Maybe minisat $ return $ Bits [false,true])
(Satisfied,Just 2)