To Mock a Mockingbird puzzle in Haskell/SBV

Garden.hs

-- A Haskell solution to:
--
--  https://stackoverflow.com/questions/53711168/modelling-a-logic-puzzle
--

{-# LANGUAGE TemplateHaskell     #-}
{-# LANGUAGE StandaloneDeriving  #-}
{-# LANGUAGE DeriveDataTypeable  #-}
{-# LANGUAGE DeriveAnyClass      #-}

import Data.SBV
import Data.List

data Color = R | Y | B
mkSymbolicEnumeration ''Color

type Flower = SInteger

col :: Flower -> SColor
col = uninterpret "col"

validPick :: SInteger -> Flower -> Flower -> Flower -> SBool
validPick n i j k = distinct [i, j, k] .&& sAll ok [i, j, k]
  where ok x = inRange x (1, n)

count :: Color -> [Flower] -> SInteger
count c fs = sum [ite (col f .== literal c) 1 0 | f <- fs]

puzzle :: Goal
puzzle = do n <- sInteger "N"

            let valid = validPick n

            ef1 <- exists "ef1_modelIgnore"
            ef2 <- exists "ef2_modelIgnore"
            ef3 <- exists "ef3_modelIgnore"

            af1 <- forall "af1"
            af2 <- forall "af2"
            af3 <- forall "af3"

            constrain $ valid ef1 ef2 ef3
            constrain $ map col [ef1, ef2, ef3] .== map literal [R, Y, B]

            constrain $ valid af1 af2 af3 .=> count R [af1, af2, af3] .>= 1
            constrain $ valid af1 af2 af3 .=> count Y [af1, af2, af3] .>= 1
            constrain $ valid af1 af2 af3 .=> count B [af1, af2, af3] .== 1

-- *Main> main
-- Solution #1:
--   N = 3 :: Integer
-- This is the only solution. (Unique up to prefix existentials.)
main :: IO ()
main = print =<< allSatWith cfg puzzle
 where cfg = z3{satTrackUFs=False, isNonModelVar = ("_modelIgnore" `isSuffixOf`)}