Sudoku solver using SMT solver through sbv

Sudoku.hs

{-# LANGUAGE ScopedTypeVariables #-}
module Sudoku where

import Data.SBV
import Control.Monad (zipWithM_)

sudoku game = do
    vs :: [SWord8] <- mkExistVars 81
    zipWithM_ setVar game vs
    mapM_ (\x -> constrain $ x .>= 1 &&& x .<= 9) vs
    mapM_ (mapM_ (allDiff . map (vs !!)))
          [ map (take 9 . iterate (+ 9)) [0 .. 8]
          , map (take 9 . iterate (+ 1)) (take 9 [0, 9 ..])
          , map (concat . take 3 . iterate (map (+ 9)) . take 3 . iterate (+ 1)) [0,3,6,27,30,33,54,57,60]
          ]
    return (true :: SBool)
  where
    setVar 0 _ = return ()
    setVar x v = constrain $ v .== fromIntegral x

    allDiff [] = return ()
    allDiff (x:xs) = mapM_ (constrain . (x ./=)) xs >> allDiff xs

test.hs

{-# LANGUAGE ScopedTypeVariables #-}
import Data.SBV
import qualified Data.Map as M
import Control.Applicative ((<$>))
import Data.Monoid ((<>))
import Data.Function (on)
import Data.List.Split (chunksOf)
import Data.List (sortBy, intersperse)

import Sudoku

solveSudoku game = do
    res <- allSat $ sudoku game
    displayModels disp res
  where
    disp _ (_, model) = do
        printResult (model :: [Word8])
        putStrLn $ replicate 22 '='

    printResult :: [Word8] -> IO ()
    printResult ls = do
        let cols = intersperse [" "] $ chunksOf 3 $ map toString $ chunksOf 9 $ map show ls
        mapM_ (mapM_ putStrLn) cols

    readInt = read :: String -> Int
    toString =  unwords . intersperse " " . map unwords . chunksOf 3

ex = [0,0,0, 1,0,0, 0,7,0,
      0,0,8, 0,0,0, 4,0,2,
      0,3,0, 0,0,2, 0,5,0,

      4,0,0, 0,1,0, 7,0,0,
      0,0,0, 9,0,4, 0,0,0,
      0,0,2, 0,8,0, 0,0,3,

      0,5,0, 4,9,0, 0,6,0,
      1,0,9, 0,0,0, 8,0,0,
      0,4,0, 0,0,3, 0,0,0 ]

main = solveSudoku ex

{-
9 2 4   1 5 8   3 7 6
5 6 8   7 3 9   4 1 2
7 3 1   6 4 2   9 5 8

4 8 5   3 1 6   7 2 9
3 1 7   9 2 4   6 8 5
6 9 2   5 8 7   1 4 3

8 5 3   4 9 1   2 6 7
1 7 9   2 6 5   8 3 4
2 4 6   8 7 3   5 9 1
======================
-}