diff --git a/README.lhs b/README.lhs
--- a/README.lhs
+++ b/README.lhs
@@ -351,7 +351,7 @@
 
 `Watson` knows `Holmes`' methods, and can apply them to compute results. Unlike
 `Holmes`, however, `Watson` is built on top of `ST` rather than `IO`, and is
-thus is a much purer soul.
+thus a much purer soul.
 
 Users can import `Control.Monad.Watson` and use the equivalent `satisfying` and
 `whenever` functions to return results _without_ the `IO` wrapper, thus making
diff --git a/README.md b/README.md
--- a/README.md
+++ b/README.md
@@ -351,7 +351,7 @@
 
 `Watson` knows `Holmes`' methods, and can apply them to compute results. Unlike
 `Holmes`, however, `Watson` is built on top of `ST` rather than `IO`, and is
-thus is a much purer soul.
+thus a much purer soul.
 
 Users can import `Control.Monad.Watson` and use the equivalent `satisfying` and
 `whenever` functions to return results _without_ the `IO` wrapper, thus making
diff --git a/examples/WaveFunctionCollapse.hs b/examples/WaveFunctionCollapse.hs
--- a/examples/WaveFunctionCollapse.hs
+++ b/examples/WaveFunctionCollapse.hs
@@ -9,7 +9,7 @@
 import Data.Function ((&))
 import Data.Hashable (Hashable)
 import Data.Holmes
-import Data.JoinSemilattice.Intersect (fromList, singleton, toList)
+import Data.JoinSemilattice.Intersect (fromList, toList)
 import Data.List (transpose)
 import Data.List.Split (chunksOf)
 import Data.Maybe (isJust, mapMaybe)
@@ -93,16 +93,16 @@
     and'
       [ -- As we're trying to draw an island, we'll surround the whole map with
         -- water:
-        all' (.== lift (singleton Water)) (head rows)
-      , all' (.== lift (singleton Water)) (last rows)
+        all' (.== lift Water) (head rows)
+      , all' (.== lift Water) (last rows)
 
-      , all' (.== lift (singleton Water)) (head columns)
-      , all' (.== lift (singleton Water)) (last columns)
+      , all' (.== lift Water) (head columns)
+      , all' (.== lift Water) (last columns)
 
         -- To generate more interesting maps, we'll require that every valid
         -- map contains at least one tree (and thus has at least one 5 × 5
         -- island).
-      , any' (.== lift (singleton Tree)) board
+      , any' (.== lift Tree) board
 
         -- For each tile, find the valid surrounding tiles, then constraint its
         -- neighbours to those possibilities.
diff --git a/holmes.cabal b/holmes.cabal
--- a/holmes.cabal
+++ b/holmes.cabal
@@ -11,7 +11,7 @@
 name:               holmes
 description:        A reference library for constraint-solving with propagators and CDCL.
 synopsis:           Tools and combinators for solving constraint problems.
-version:            0.2.0.0
+version:            0.3.0.0
 
 library
   exposed-modules: Control.Monad.Cell.Class
@@ -30,6 +30,7 @@
                , Data.JoinSemilattice.Class.FlatMapping
                , Data.JoinSemilattice.Class.Fractional
                , Data.JoinSemilattice.Class.Integral
+               , Data.JoinSemilattice.Class.Lifting
                , Data.JoinSemilattice.Class.Mapping
                , Data.JoinSemilattice.Class.Merge
                , Data.JoinSemilattice.Class.Ord
diff --git a/src/Control/Monad/Holmes.hs b/src/Control/Monad/Holmes.hs
--- a/src/Control/Monad/Holmes.hs
+++ b/src/Control/Monad/Holmes.hs
@@ -6,6 +6,7 @@
 {-# LANGUAGE TypeApplications #-}
 {-# LANGUAGE TypeFamilies #-}
 {-# LANGUAGE ViewPatterns #-}
+{-# LANGUAGE CPP #-}
 
 {-|
 Module      : Control.Monad.Holmes
@@ -36,6 +37,9 @@
   , whenever
   ) where
 
+#if __GLASGOW_HASKELL__ == 806
+import Control.Monad.Fail (MonadFail, fail)
+#endif
 import Control.Monad.Cell.Class (MonadCell (..))
 import Control.Monad.IO.Class (MonadIO (..))
 import qualified Control.Monad.Cell.Class as Cell
@@ -43,7 +47,7 @@
 import qualified Control.Monad.MoriarT as MoriarT
 import Data.Coerce (coerce)
 import Data.Input.Config (Config (..))
-import Data.JoinSemilattice.Class.Eq (EqR)
+import Data.JoinSemilattice.Class.Eq (EqR (..))
 import Data.JoinSemilattice.Class.Merge (Merge)
 import Data.Kind (Type)
 import Data.Propagator (Prop)
@@ -117,8 +121,16 @@
 
 -- | Given an input configuration, and a predicate on those input variables,
 -- return the __first__ configuration that satisfies the predicate.
-satisfying :: (EqR x b, Typeable x) => Config Holmes x -> (forall m. MonadCell m => [ Prop m x ] -> Prop m b) -> IO (Maybe [ x ])
-satisfying (coerce -> config :: Config (MoriarT IO) x) f = MoriarT.runOne (MoriarT.solve config f)
+satisfying
+  :: ( EqC f x
+     , EqR f
+     , Typeable x
+     )
+  => Config Holmes (f x)
+  -> (forall m. MonadCell m => [ Prop m (f x) ] -> Prop m (f Bool))
+  -> IO (Maybe [ f x ])
+satisfying (coerce -> config :: Config (MoriarT IO) x) f
+  = MoriarT.runOne (MoriarT.solve config f)
 
 -- | Shuffle the refinements in a configuration. If we make a configuration
 -- like @100 `from` [1 .. 10]@, the first configuration will be one hundred @1@
@@ -137,5 +149,13 @@
 -- return __all configurations__ that satisfy the predicate. It should be noted
 -- that there's nothing lazy about this; if your problem has a lot of
 -- solutions, or your search space is very big, you'll be waiting a long time!
-whenever :: (EqR x b, Typeable x) => Config Holmes x -> (forall m. MonadCell m => [ Prop m x ] -> Prop m b) -> IO [[ x ]]
-whenever (coerce -> config :: Config (MoriarT IO) x) f = MoriarT.runAll (MoriarT.solve config f)
+whenever
+  :: ( EqC f x
+     , EqR f
+     , Typeable x
+     )
+  => Config Holmes (f x)
+  -> (forall m. MonadCell m => [ Prop m (f x) ] -> Prop m (f Bool))
+  -> IO [[ f x ]]
+whenever (coerce -> config :: Config (MoriarT IO) x) f
+  = MoriarT.runAll (MoriarT.solve config f)
diff --git a/src/Control/Monad/MoriarT.hs b/src/Control/Monad/MoriarT.hs
--- a/src/Control/Monad/MoriarT.hs
+++ b/src/Control/Monad/MoriarT.hs
@@ -186,7 +186,15 @@
 -- | Given an input configuration, and a predicate on those input variables,
 -- compute the configurations that satisfy the predicate. This result (or these
 -- results) can be extracted using 'runOne' or 'runAll'.
-solve :: (PrimMonad m, EqR x b, Merge x, Typeable x) => Config (MoriarT m) x -> (forall f. MonadCell f => [ Prop f x ] -> Prop f b) -> MoriarT m [ x ]
+solve
+  :: ( PrimMonad m
+     , EqR f
+     , Merge (f x)
+     , Typeable x
+     )
+  => Config (MoriarT m) (f x)
+  -> (forall m'. MonadCell m' => [ Prop m' (f x) ] -> Prop m' (f Bool))
+  -> MoriarT m [ f x ]
 solve Config{..} predicate = do
   inputs <- traverse Cell.fill initial
   output <- Prop.down (predicate (map Prop.up inputs))
diff --git a/src/Control/Monad/Watson.hs b/src/Control/Monad/Watson.hs
--- a/src/Control/Monad/Watson.hs
+++ b/src/Control/Monad/Watson.hs
@@ -4,6 +4,7 @@
 {-# LANGUAGE ScopedTypeVariables #-}
 {-# LANGUAGE TypeApplications #-}
 {-# LANGUAGE TypeFamilies #-}
+{-# LANGUAGE CPP #-}
 
 {-|
 Module      : Control.Monad.Watson
@@ -30,6 +31,9 @@
   , whenever
   ) where
 
+#if __GLASGOW_HASKELL__ == 806
+import Control.Monad.Fail (MonadFail, fail)
+#endif
 import Control.Monad.ST (ST, runST)
 import Control.Monad.Cell.Class (MonadCell (..))
 import qualified Control.Monad.Cell.Class as Cell
@@ -37,7 +41,7 @@
 import qualified Control.Monad.MoriarT as MoriarT
 import Data.Coerce (coerce)
 import Data.Input.Config (Config (..))
-import Data.JoinSemilattice.Class.Eq (EqR)
+import Data.JoinSemilattice.Class.Eq (EqR (..))
 import Data.JoinSemilattice.Class.Merge (Merge)
 import Data.Kind (Type)
 import Data.Propagator (Prop)
@@ -109,12 +113,28 @@
 
 -- | Given an input configuration, and a predicate on those input variables,
 -- return the __first__ configuration that satisfies the predicate.
-satisfying :: (EqR x b, Typeable x) => (forall h. Config (Watson h) x) -> (forall m. MonadCell m => [ Prop m x ] -> Prop m b) -> Maybe [ x ]
-satisfying config f = runST (MoriarT.runOne (MoriarT.solve (coerce config) f))
+satisfying
+  :: ( EqC f x
+     , EqR f
+     , Typeable x
+     )
+  => (forall h. Config (Watson h) (f x))
+  -> (forall m. MonadCell m => [ Prop m (f x) ] -> Prop m (f Bool))
+  -> Maybe [ f x ]
+satisfying config f
+  = runST (MoriarT.runOne (MoriarT.solve (coerce config) f))
 
 -- | Given an input configuration, and a predicate on those input variables,
 -- return __all configurations__ that satisfy the predicate. It should be noted
 -- that there's nothing lazy about this; if your problem has a lot of
 -- solutions, or your search space is very big, you'll be waiting a long time!
-whenever :: (EqR x b, Typeable x) => (forall h. Config (Watson h) x) -> (forall m. MonadCell m => [ Prop m x ] -> Prop m b) -> [[ x ]]
-whenever config f = runST (MoriarT.runAll (MoriarT.solve (coerce config) f))
+whenever
+  :: ( EqC f x
+     , EqR f
+     , Typeable x
+     )
+  => (forall h. Config (Watson h) (f x))
+  -> (forall m. MonadCell m => [ Prop m (f x) ] -> Prop m (f Bool))
+  -> [[ f x ]]
+whenever config f
+  = runST (MoriarT.runAll (MoriarT.solve (coerce config) f))
diff --git a/src/Data/JoinSemilattice/Class/Boolean.hs b/src/Data/JoinSemilattice/Class/Boolean.hs
--- a/src/Data/JoinSemilattice/Class/Boolean.hs
+++ b/src/Data/JoinSemilattice/Class/Boolean.hs
@@ -24,23 +24,24 @@
 -- tell you that the /output/ of @x && y@ is 'True', you can tell me what the
 -- inputs are, even if your computer can't. The implementations of 'BooleanR'
 -- should be such that all directions of inference are considered.
-class Merge x => BooleanR (x :: Type) where
+class Merge (f Bool) => BooleanR (f :: Type -> Type) where
+
   -- | An overloaded 'False' value.
-  falseR :: x
+  falseR :: f Bool
 
   -- | An overloaded 'True' value.
-  trueR :: x
+  trueR :: f Bool
 
   -- | A relationship between a boolean value and its opposite.
-  notR :: ( x, x ) -> ( x, x )
+  notR :: ( f Bool, f Bool ) -> ( f Bool, f Bool )
 
   -- | A relationship between two boolean values and their conjunction.
-  andR :: ( x, x, x ) -> ( x, x, x )
+  andR :: ( f Bool, f Bool, f Bool ) -> ( f Bool, f Bool, f Bool )
 
   -- | A relationship between two boolean values and their disjunction.
-  orR :: ( x, x, x ) -> ( x, x, x )
+  orR :: ( f Bool, f Bool, f Bool ) -> ( f Bool, f Bool, f Bool )
 
-instance BooleanR (Defined Bool) where
+instance BooleanR Defined where
   falseR = Exactly False
   trueR  = Exactly True
 
@@ -70,7 +71,7 @@
       , liftA2 (||) x y
       )
 
-instance BooleanR (Intersect Bool) where
+instance BooleanR Intersect where
   falseR = Intersect.singleton False
   trueR  = Intersect.singleton True
 
diff --git a/src/Data/JoinSemilattice/Class/Eq.hs b/src/Data/JoinSemilattice/Class/Eq.hs
--- a/src/Data/JoinSemilattice/Class/Eq.hs
+++ b/src/Data/JoinSemilattice/Class/Eq.hs
@@ -2,6 +2,10 @@
 {-# LANGUAGE KindSignatures #-}
 {-# LANGUAGE FunctionalDependencies #-}
 {-# LANGUAGE MultiWayIf #-}
+{-# LANGUAGE QuantifiedConstraints #-}
+{-# LANGUAGE TypeFamilies #-}
+{-# LANGUAGE UndecidableInstances #-}
+{-# LANGUAGE UndecidableSuperClasses #-}
 
 {-|
 Module      : Data.JoinSemilattice.Class.Eq
@@ -12,26 +16,48 @@
 module Data.JoinSemilattice.Class.Eq where
 
 import Control.Applicative (liftA2)
-import Data.Hashable (Hashable)
 import Data.JoinSemilattice.Class.Boolean (BooleanR (..))
 import Data.JoinSemilattice.Class.Merge (Merge)
 import Data.JoinSemilattice.Defined (Defined (..))
-import Data.JoinSemilattice.Intersect (Intersect (..))
+import Data.JoinSemilattice.Intersect (Intersect (..), Intersectable)
 import qualified Data.JoinSemilattice.Intersect as Intersect
-import Data.Kind (Type)
+import Data.Kind (Constraint, Type)
 
+class EqC f x => EqC' f x
+instance EqC f x => EqC' f x
+
 -- | Equality between two variables as a relationship between them and their
 -- result. The hope here is that, if we learn the output before the inputs, we
 -- can often "work backwards" to learn something about them. If we know the
 -- result is exactly /true/, for example, we can effectively then
 -- 'Control.Monad.Cell.Class.unify' the two input cells, as we know that their
 -- values will always be the same.
-class (BooleanR b, Merge x) => EqR (x :: Type) (b :: Type) | x -> b where
-  eqR :: ( x, x, b ) -> ( x, x, b )
+--
+-- The class constraints are a bit ugly here, and it's something I'm hoping I
+-- can tidy up down the line. The idea is that, previously, our class was
+-- defined as:
+--
+-- @
+--   class EqR (x :: Type) (b :: Type) | x -> b where
+--     eqR :: (x -> x -> b) -> (x -> x -> b)
+-- @
+--
+-- The problem here was that, if we said @x .== x :: Prop m (Defined Bool)@, we
+-- couldn't even infer that the type of @x@ was @Defined@-wrapped, which made
+-- the overloaded literals, for example, largely pointless.
+--
+-- To fix it, the class was rewritten to parameterise the wrapper type, which
+-- means we can always make this inference. However, the constraints got a bit
+-- grizzly when I hacked it together.
+class (forall x. EqC' f x => Merge (f x), BooleanR f)
+    => EqR (f :: Type -> Type) where
+  type EqC f :: Type -> Constraint
 
+  eqR :: EqC' f x => ( f x, f x, f Bool ) -> ( f x, f x, f Bool )
+
 -- | A relationship between two variables and the result of a not-equals
 -- comparison between them.
-neR :: EqR x b => ( x, x, b ) -> ( x, x, b )
+neR :: (EqR f, EqC' f x) => ( f x, f x, f Bool ) -> ( f x, f x, f Bool )
 neR ( x, y, z )
   = let ( notZ', _ ) = notR ( mempty, z )
         ( x', y', notZR ) = eqR ( x, y, notZ' )
@@ -39,15 +65,18 @@
 
     in ( x', y', z' )
 
-instance Eq x => EqR (Defined x) (Defined Bool) where
+instance EqR Defined where
+  type EqC Defined = Eq
+
   eqR ( x, y, z )
     = ( if z == trueR then y else mempty
       , if z == trueR then x else mempty
       , liftA2 (==) x y
       )
 
-instance (Bounded x, Enum x, Ord x, Hashable x)
-    => EqR (Intersect x) (Intersect Bool) where
+instance EqR Intersect where
+  type EqC Intersect = Intersectable
+
   eqR ( x, y, z )
     = ( if | z == trueR                           -> y
            | z == falseR && Intersect.size y == 1 -> Intersect.except y
diff --git a/src/Data/JoinSemilattice/Class/Lifting.hs b/src/Data/JoinSemilattice/Class/Lifting.hs
new file mode 100644
--- /dev/null
+++ b/src/Data/JoinSemilattice/Class/Lifting.hs
@@ -0,0 +1,31 @@
+{-# LANGUAGE ConstraintKinds #-}
+{-# LANGUAGE FlexibleInstances #-}
+{-# LANGUAGE FunctionalDependencies #-}
+{-# LANGUAGE KindSignatures #-}
+
+{-|
+Module      : Data.JoinSemilattice.Class.Lifting
+Description : Lifting values into parameter types.
+Copyright   : (c) Tom Harding, 2020
+License     : MIT
+-}
+module Data.JoinSemilattice.Class.Lifting where
+
+import Data.Hashable (Hashable)
+import Data.JoinSemilattice.Defined (Defined (..))
+import Data.JoinSemilattice.Intersect (Intersect)
+import qualified Data.JoinSemilattice.Intersect as Intersect
+import Data.Kind (Constraint, Type)
+
+-- | Embed a regular value inside a parameter type.
+class Lifting (f :: Type -> Type) (c :: Type -> Constraint) | f -> c where
+  lift' :: c x => x -> f x
+
+class Trivial (x :: Type)
+instance Trivial x
+
+instance Lifting Defined Trivial where
+  lift' = Exactly
+
+instance Lifting Intersect Hashable where
+  lift' = Intersect.singleton
diff --git a/src/Data/JoinSemilattice/Class/Ord.hs b/src/Data/JoinSemilattice/Class/Ord.hs
--- a/src/Data/JoinSemilattice/Class/Ord.hs
+++ b/src/Data/JoinSemilattice/Class/Ord.hs
@@ -1,7 +1,8 @@
 {-# LANGUAGE FlexibleInstances #-}
-{-# LANGUAGE FunctionalDependencies #-}
-{-# LANGUAGE KindSignatures #-}
 {-# LANGUAGE MultiWayIf #-}
+{-# LANGUAGE QuantifiedConstraints #-}
+{-# LANGUAGE TypeFamilies #-}
+{-# LANGUAGE UndecidableInstances #-}
 
 {-|
 Module      : Data.JoinSemilattice.Class.Ord
@@ -12,31 +13,34 @@
 module Data.JoinSemilattice.Class.Ord where
 
 import Control.Applicative (liftA2)
-import Data.Hashable (Hashable)
 import Data.JoinSemilattice.Defined (Defined (..))
-import Data.JoinSemilattice.Intersect (Intersect (..))
+import Data.JoinSemilattice.Intersect (Intersect (..), Intersectable)
 import qualified Data.JoinSemilattice.Intersect as Intersect
 import Data.JoinSemilattice.Class.Boolean (BooleanR (..))
-import Data.JoinSemilattice.Class.Eq (EqR)
-import Data.Kind (Type)
+import Data.JoinSemilattice.Class.Eq (EqR (..), EqC')
+import Data.Kind (Constraint, Type)
 
 -- | Comparison relationships between two values and their comparison result.
-class EqR x b => OrdR (x :: Type) (b :: Type) | x -> b where
+-- See 'Data.JoinSemilattice.Class.Eq.EqR' for more information on the design
+-- of this class, and a full apology for the constraints involved.
+class (EqR f, forall x. OrdC f x => EqC' f x) => OrdR (f :: Type -> Type) where
+  type OrdC f :: Type -> Constraint
+  type OrdC f = EqC f
 
   -- | A relationship between two values and whether the left is less than or
   -- equal to the right.
-  lteR :: ( x, x, b ) -> ( x, x, b )
+  lteR :: OrdC f x => ( f x, f x, f Bool ) -> ( f x, f x, f Bool )
 
 -- | Comparison between two values and their '(>)' result.
-gtR :: OrdR x b => ( x, x, b ) -> ( x, x, b )
+gtR :: (OrdR f, OrdC f x) => ( f x, f x, f Bool ) -> ( f x, f x, f Bool )
 gtR ( x, y, z ) = let ( y', x', z' ) = ltR ( y, x, z ) in ( x', y', z' )
 
 -- | Comparison between two values and their '(>=)' result.
-gteR :: OrdR x b => ( x, x, b ) -> ( x, x, b )
+gteR :: (OrdR f, OrdC f x) => ( f x, f x, f Bool ) -> ( f x, f x, f Bool )
 gteR ( x, y, z ) = let ( y', x', z' ) = lteR ( y, x, z ) in ( x', y', z' )
 
 -- | Comparison between two values and their '(<)' result.
-ltR :: OrdR x b => ( x, x, b ) -> ( x, x, b )
+ltR :: (OrdR f, OrdC f x) => ( f x, f x, f Bool ) -> ( f x, f x, f Bool )
 ltR ( x, y, z )
   = let ( notZ', _ ) = notR ( mempty, z )
         ( x', y', notZR ) = gteR ( x, y, notZ' )
@@ -44,11 +48,17 @@
 
     in ( x', y', z' )
 
-instance Ord x => OrdR (Defined x) (Defined Bool) where
+instance OrdR Defined where
+  type OrdC Defined = Ord
+
   lteR ( x, y, _ ) = ( mempty, mempty, liftA2 (<=) x y )
 
-instance (Bounded x, Enum x, Hashable x, Ord x)
-    => OrdR (Intersect x) (Intersect Bool) where
+class (Ord x, Intersectable x) => OrdIntersectable (x :: Type)
+instance (Ord x, Intersectable x) => OrdIntersectable x
+
+instance OrdR Intersect where
+  type OrdC Intersect = OrdIntersectable
+
   lteR ( x, y, z )
     = ( if | z == trueR  -> Intersect.filter (<= maximum y) x
            | z == falseR -> Intersect.filter ( > minimum y) x
diff --git a/src/Data/Propagator.hs b/src/Data/Propagator.hs
--- a/src/Data/Propagator.hs
+++ b/src/Data/Propagator.hs
@@ -30,7 +30,7 @@
 
   , (.&&), all', allWithIndex', and'
   , (.||), any', anyWithIndex', or'
-  , false, not', true
+  , false, not', true, exactly, choose
 
   , (.==), (./=), distinct
 
@@ -54,6 +54,7 @@
 import Data.JoinSemilattice.Class.FlatMapping (FlatMapping (..))
 import Data.JoinSemilattice.Class.Fractional (FractionalR (..), divideR, multiplyR, recipR)
 import Data.JoinSemilattice.Class.Integral (IntegralR (..), divR, modR, timesR)
+import Data.JoinSemilattice.Class.Lifting (Lifting (..))
 import Data.JoinSemilattice.Class.Mapping (Mapping (..))
 import Data.JoinSemilattice.Class.Merge (Merge)
 import Data.JoinSemilattice.Class.Ord (OrdR (..), gtR, gteR, ltR)
@@ -132,10 +133,8 @@
     f x y z
     pure z
 
--- | Lift a regular value into a propagator network. This is analogous to
--- 'pure' for some 'Applicative' type.
-lift :: MonadCell m => x -> Prop m x
-lift = Nullary . Cell.fill
+lift :: forall f m c x. (MonadCell m, c x) => Lifting f c => x -> Prop m (f x)
+lift = Nullary . fill . lift'
 
 -- | Lift a regular function into a propagator network. The function is lifted
 -- into a relationship with one-way information flow.
@@ -164,7 +163,7 @@
 -- values.
 --
 -- It's a lot of words, but the intuition is, "'(&&)' over propagators".
-(.&&) :: BooleanR b => Prop m b -> Prop m b -> Prop m b
+(.&&) :: BooleanR f => Prop m (f Bool) -> Prop m (f Bool) -> Prop m (f Bool)
 (.&&) = Binary (Cell.binary andR)
 
 infixr 3 .&&
@@ -174,7 +173,7 @@
 -- focus on the conjunction of all these values.
 --
 -- In other words, "'all' over propagators".
-all' :: (BooleanR b, MonadCell m) => (x -> Prop m b) -> [ x ] -> Prop m b
+all' :: (BooleanR f, MonadCell m) => (x -> Prop m (f Bool)) -> [ x ] -> Prop m (f Bool)
 all' f = and' . map f
 
 -- | The same as the 'all'' function, but with access to the index of the
@@ -182,14 +181,14 @@
 -- each element to /other/ elements within the array.
 --
 -- /For example, cells "surrounding" the current cell in a conceptual "board"./
-allWithIndex' :: (BooleanR b, MonadCell m) => (Int -> x -> Prop m b) -> [ x ] -> Prop m b
+allWithIndex' :: (BooleanR f, MonadCell m) => (Int -> x -> Prop m (f Bool)) -> [ x ] -> Prop m (f Bool)
 allWithIndex' f = all' (uncurry f) . zip [0 ..]
 
 -- | Given a list of propagator networks with a focus on boolean values, create
 -- a new network with a focus on the conjugation of all these values.
 --
 -- In other words, "'and' over propagators".
-and' :: (BooleanR b, MonadCell m) => [ Prop m b ] -> Prop m b
+and' :: (BooleanR f, MonadCell m) => [ Prop m (f Bool) ] -> Prop m (f Bool)
 and' = foldr (.&&) true
 
 -- | Run a predicate on all values in a list, producing a list of propagator
@@ -197,7 +196,7 @@
 -- focus on the disjunction of all these values.
 --
 -- In other words, "'any' over propagators".
-any' :: (BooleanR b, MonadCell m) => (x -> Prop m b) -> [ x ] -> Prop m b
+any' :: (BooleanR f, MonadCell m) => (x -> Prop m (f Bool)) -> [ x ] -> Prop m (f Bool)
 any' f = or' . map f
 
 -- | The same as the 'any'' function, but with access to the index of the
@@ -205,37 +204,59 @@
 -- each element to /other/ elements within the array.
 --
 -- /For example, cells "surrounding" the current cell in a conceptual "board"./
-anyWithIndex' :: (BooleanR b, MonadCell m) => (Int -> x -> Prop m b) -> [ x ] -> Prop m b
+anyWithIndex' :: (BooleanR f, MonadCell m) => (Int -> x -> Prop m (f Bool)) -> [ x ] -> Prop m (f Bool)
 anyWithIndex' f = any' (uncurry f) . zip [0 ..]
 
+-- | Asserts that exactly n of the elements must match the given predicate.
+exactly :: (BooleanR f, MonadCell m) => Int -> (x -> Prop m (f Bool)) -> [x] -> Prop m (f Bool)
+exactly n f xs = 
+    let l = length xs
+        choices = choose l n
+        applyChoice picks = zipWith (\pick x -> if pick then f x else not' (f x)) picks xs
+    in or' (map (and'.applyChoice) choices)
+
+-- | Utility function that calculates all possible ways to pick k values out of n.
+-- It returns a list of picks, where each pick contains a boolean indicating whether
+-- that value was picked
+choose :: Int -> Int -> [[Bool]]
+choose n k = 
+  if k<0 || k>n
+    then []
+    else
+      if n==0
+        then [[]]
+        else
+          map (False:) (choose (pred n) k) ++
+          map (True:)  (choose (pred n) (pred k))
+
 -- | Different parameter types come with different representations for 'Bool'.
 -- This value is a propagator network with a focus on a polymorphic "falsey"
 -- value.
-false :: (BooleanR b, MonadCell m) => Prop m b
+false :: (BooleanR f, MonadCell m) => Prop m (f Bool)
 false = Nullary (Cell.fill falseR)
 
 -- | Given a propagator network with a focus on a boolean value, produce a
 -- network with a focus on its negation.
 --
 -- ... It's "'not' over propagators".
-not' :: (BooleanR b, MonadCell m) => Prop m b -> Prop m b 
+not' :: (BooleanR f, MonadCell m) => Prop m (f Bool) -> Prop m (f Bool) 
 not' = Unary (Cell.unary notR)
 
 -- | Given a list of propagator networks with a focus on boolean values, create
 -- a new network with a focus on the disjunction of all these values.
 --
 -- In other words, "'or' over propagators".
-or' :: (BooleanR b, MonadCell m) => [ Prop m b ] -> Prop m b 
+or' :: (BooleanR f, MonadCell m) => [ Prop m (f Bool) ] -> Prop m (f Bool)
 or' = foldr (.||) false
 
 -- | Different parameter types come with different representations for 'Bool'.
 -- This value is a propagator network with a focus on a polymorphic "truthy"
 -- value.
-true :: (BooleanR b, MonadCell m) => Prop m b
+true :: (BooleanR f, MonadCell m) => Prop m (f Bool)
 true = Nullary (Cell.fill trueR)
 
 -- | Calculate the disjunction of two boolean propagator network values.
-(.||) :: BooleanR b => Prop m b -> Prop m b -> Prop m b
+(.||) :: BooleanR f => Prop m (f Bool) -> Prop m (f Bool) -> Prop m (f Bool)
 (.||) = Binary (Cell.binary orR)
 
 infixr 2 .||
@@ -244,7 +265,7 @@
 -- result of testing the two for equality.
 --
 -- In other words, "it's '(==)' for propagators".
-(.==) :: (EqR x b, MonadCell m) => Prop m x -> Prop m x -> Prop m b
+(.==) :: (EqR f, EqC f x, MonadCell m) => Prop m (f x) -> Prop m (f x) -> Prop m (f Bool)
 (.==) = Binary (Cell.binary eqR)
 
 infix 4 .==
@@ -253,7 +274,7 @@
 -- result of testing the two for inequality.
 --
 -- In other words, "it's '(/=)' for propagators".
-(./=) :: (EqR x b, MonadCell m) => Prop m x -> Prop m x -> Prop m b
+(./=) :: (EqR f, EqC f x, MonadCell m) => Prop m (f x) -> Prop m (f x) -> Prop m (f Bool)
 (./=) = Binary (Cell.binary neR)
 
 infix 4 ./=
@@ -263,7 +284,7 @@
 -- every propagator network's focus is different to the others.
 --
 -- /Are all the values in this list distinct?/
-distinct :: (EqR x b, MonadCell m) => [ Prop m x ] -> Prop m b
+distinct :: (EqR f, EqC f x, MonadCell m) => [ Prop m (f x) ] -> Prop m (f Bool)
 distinct = \case
   x : xs -> all' (./= x) xs .&& distinct xs
   [    ] -> Nullary (Cell.fill trueR)
@@ -272,7 +293,7 @@
 -- whether the first network's focus be greater than the second.
 --
 -- In other words, "it's '(>)' for propagators".
-(.>) :: (OrdR x b, MonadCell m) => Prop m x -> Prop m x -> Prop m b
+(.>) :: (OrdR f, OrdC f x, MonadCell m) => Prop m (f x) -> Prop m (f x) -> Prop m (f Bool)
 (.>) = Binary (Cell.binary gtR)
 
 infix 4 .>
@@ -281,7 +302,7 @@
 -- whether the first network's focus be greater than or equal to the second.
 --
 -- In other words, "it's '(>=)' for propagators".
-(.>=) :: (OrdR x b, MonadCell m) => Prop m x -> Prop m x -> Prop m b
+(.>=) :: (OrdR f, OrdC f x, MonadCell m) => Prop m (f x) -> Prop m (f x) -> Prop m (f Bool)
 (.>=) = Binary (Cell.binary gteR)
 
 infix 4 .>=
@@ -290,7 +311,7 @@
 -- whether the first network's focus be less than the second.
 --
 -- In other words, "it's '(<)' for propagators".
-(.<) :: (OrdR x b, MonadCell m) => Prop m x -> Prop m x -> Prop m b
+(.<) :: (OrdR f, OrdC f x, MonadCell m) => Prop m (f x) -> Prop m (f x) -> Prop m (f Bool)
 (.<) = Binary (Cell.binary ltR)
 
 infix 4 .<
@@ -299,7 +320,7 @@
 -- whether the first network's focus be less than or equal to the second.
 --
 -- In other words, "it's '(<=)' for propagators".
-(.<=) :: (OrdR x b, MonadCell m) => Prop m x -> Prop m x -> Prop m b
+(.<=) :: (OrdR f, OrdC f x, MonadCell m) => Prop m (f x) -> Prop m (f x) -> Prop m (f Bool)
 (.<=) = Binary (Cell.binary lteR)
 
 infix 4 .<=
diff --git a/test/Test/Data/JoinSemilattice/Class/Boolean.hs b/test/Test/Data/JoinSemilattice/Class/Boolean.hs
--- a/test/Test/Data/JoinSemilattice/Class/Boolean.hs
+++ b/test/Test/Data/JoinSemilattice/Class/Boolean.hs
@@ -9,13 +9,13 @@
 import Hedgehog
 import qualified Hedgehog.Gen as Gen
 
-bool :: BooleanR x => Gen x
+bool :: BooleanR f => Gen (f Bool)
 bool = Gen.element [ trueR, falseR ]
 
-booleanR_andR :: forall x. (BooleanR x, Eq x, Show x) => Property
+booleanR_andR :: forall f. (BooleanR f, Eq (f Bool), Show (f Bool)) => Property
 booleanR_andR = property do
-  (a :: x) <- forAll bool
-  (b :: x) <- forAll bool
+  a :: f Bool <- forAll bool
+  b :: f Bool <- forAll bool
 
   let ( _, _, c ) = andR ( a, b, mempty )
   annotateShow c
@@ -28,10 +28,10 @@
   annotateShow b'
   b' <> b === b
 
-booleanR_deMorgan_and :: forall x. (BooleanR x, Eq x, Show x) => Property
+booleanR_deMorgan_and :: forall f. (BooleanR f, Eq (f Bool), Show (f Bool)) => Property
 booleanR_deMorgan_and = property do
-  (a :: x) <- forAll bool
-  (b :: x) <- forAll bool
+  a :: f Bool <- forAll bool
+  b :: f Bool <- forAll bool
 
   let ( _, _, c ) = andR ( a, b, mempty )
       ( _, a' ) = notR ( a, mempty )
@@ -41,10 +41,10 @@
 
   c === d
 
-booleanR_deMorgan_or :: forall x. (BooleanR x, Eq x, Show x) => Property
+booleanR_deMorgan_or :: forall f. (BooleanR f, Eq (f Bool), Show (f Bool)) => Property
 booleanR_deMorgan_or = property do
-  (a :: x) <- forAll bool
-  (b :: x) <- forAll bool
+  a :: f Bool <- forAll bool
+  b :: f Bool <- forAll bool
 
   let ( _, _, c ) = orR ( a, b, mempty )
       ( _, a' ) = notR ( a, mempty )
@@ -54,10 +54,10 @@
 
   c === d
 
-booleanR_orR :: forall x. (BooleanR x, Eq x, Show x) => Property
+booleanR_orR :: forall f. (BooleanR f, Eq (f Bool), Show (f Bool)) => Property
 booleanR_orR = property do
-  (a :: x) <- forAll bool
-  (b :: x) <- forAll bool
+  a :: f Bool <- forAll bool
+  b :: f Bool <- forAll bool
 
   let ( _, _, c ) = orR ( a, b, mempty )
   annotateShow c
@@ -70,9 +70,9 @@
   annotateShow b'
   b' <> b === b
 
-booleanR_notR :: forall x. (BooleanR x, Eq x, Show x) => Property
+booleanR_notR :: forall f. (BooleanR f, Eq (f Bool), Show (f Bool)) => Property
 booleanR_notR = property do
-  (a :: x) <- forAll bool
+  a :: f Bool <- forAll bool
 
   let ( _, b ) = notR ( a, mempty )
   annotateShow b
diff --git a/test/Test/Data/JoinSemilattice/Class/Eq.hs b/test/Test/Data/JoinSemilattice/Class/Eq.hs
--- a/test/Test/Data/JoinSemilattice/Class/Eq.hs
+++ b/test/Test/Data/JoinSemilattice/Class/Eq.hs
@@ -8,7 +8,16 @@
 import Data.Holmes (BooleanR (..), EqR (..), neR)
 import Hedgehog
 
-eqR_eqR :: (EqR x b, Show b, Eq x, Show x) => Gen x -> Property
+eqR_eqR
+  :: ( EqC f x
+     , EqR f
+     , Eq (f x)
+     , Eq (f Bool)
+     , Show (f x)
+     , Show (f Bool)
+     )
+  => Gen (f x)
+  -> Property
 eqR_eqR gen = property do
   a <- forAll gen
   b <- forAll gen
@@ -24,7 +33,16 @@
   annotateShow b'
   b' <> b === b
 
-eqR_negation :: (EqR x b, Show b, Eq b, Eq x, Show x) => Gen x -> Property
+eqR_negation
+  :: ( EqC f x
+     , EqR f
+     , Eq (f x)
+     , Eq (f Bool)
+     , Show (f x)
+     , Show (f Bool)
+     )
+  => Gen (f x)
+  -> Property
 eqR_negation gen = property do
   a <- forAll gen
   b <- forAll gen
@@ -38,14 +56,32 @@
   let ( _, c' ) = notR ( c, mempty )
   c' === d
 
-eqR_reflexivity :: (EqR x b, Show b, Eq b, Show x) => Gen x -> Property
+eqR_reflexivity
+  :: ( EqC f x
+     , EqR f
+     , Eq (f x)
+     , Eq (f Bool)
+     , Show (f x)
+     , Show (f Bool)
+     )
+  => Gen (f x)
+  -> Property
 eqR_reflexivity gen = property do
   a <- forAll gen
 
   let ( _, _, c ) = eqR ( a, a, mempty )
   c <> trueR === trueR
 
-eqR_symmetry :: (EqR x b, Eq b, Show b, Show x) => Gen x -> Property
+eqR_symmetry
+  :: ( EqC f x
+     , EqR f
+     , Eq (f x)
+     , Eq (f Bool)
+     , Show (f x)
+     , Show (f Bool)
+     )
+  => Gen (f x)
+  -> Property
 eqR_symmetry gen = property do
   a <- forAll gen
   b <- forAll gen
diff --git a/test/Test/Data/JoinSemilattice/Class/Ord.hs b/test/Test/Data/JoinSemilattice/Class/Ord.hs
--- a/test/Test/Data/JoinSemilattice/Class/Ord.hs
+++ b/test/Test/Data/JoinSemilattice/Class/Ord.hs
@@ -8,7 +8,16 @@
 import Data.Holmes (BooleanR (..), OrdR (..))
 import Hedgehog
 
-ordR_lteR :: (OrdR x b, Show b, Eq x, Show x) => Gen x -> Property
+ordR_lteR
+  :: ( OrdR f
+     , OrdC f x
+     , Eq (f x)
+     , Eq (f Bool)
+     , Show (f x)
+     , Show (f Bool)
+     )
+  => Gen (f x)
+  -> Property
 ordR_lteR gen = property do
   a <- forAll gen
   b <- forAll gen
@@ -24,7 +33,15 @@
   annotateShow b'
   b' <> b === b
 
-ordR_symmetry :: (OrdR x b, Eq b, Eq x, Show x) => Gen x -> Property
+ordR_symmetry
+  :: ( OrdR f
+     , OrdC f x
+     , Eq (f x)
+     , Eq (f Bool)
+     , Show (f x)
+     )
+  => Gen (f x)
+  -> Property
 ordR_symmetry gen = property do
   a <- forAll gen
   b <- forAll gen
diff --git a/test/Test/Data/JoinSemilattice/Defined.hs b/test/Test/Data/JoinSemilattice/Defined.hs
--- a/test/Test/Data/JoinSemilattice/Defined.hs
+++ b/test/Test/Data/JoinSemilattice/Defined.hs
@@ -78,19 +78,19 @@
   z === Exactly (x && y)
 
 hprop_booleanR_andR :: Property
-hprop_booleanR_andR = BooleanR.booleanR_andR @(Defined Bool)
+hprop_booleanR_andR = BooleanR.booleanR_andR @Defined
 
 hprop_booleanR_deMorgan_and :: Property
-hprop_booleanR_deMorgan_and = BooleanR.booleanR_deMorgan_and @(Defined Bool)
+hprop_booleanR_deMorgan_and = BooleanR.booleanR_deMorgan_and @Defined
 
 hprop_booleanR_deMorgan_or :: Property
-hprop_booleanR_deMorgan_or = BooleanR.booleanR_deMorgan_or @(Defined Bool)
+hprop_booleanR_deMorgan_or = BooleanR.booleanR_deMorgan_or @Defined
 
 hprop_booleanR_notR :: Property
-hprop_booleanR_notR = BooleanR.booleanR_notR @(Defined Bool)
+hprop_booleanR_notR = BooleanR.booleanR_notR @Defined
 
 hprop_booleanR_orR :: Property
-hprop_booleanR_orR = BooleanR.booleanR_orR @(Defined Bool)
+hprop_booleanR_orR = BooleanR.booleanR_orR @Defined
 
 hprop_eqR_simple :: Property
 hprop_eqR_simple = property do
diff --git a/test/Test/Data/JoinSemilattice/Intersect.hs b/test/Test/Data/JoinSemilattice/Intersect.hs
--- a/test/Test/Data/JoinSemilattice/Intersect.hs
+++ b/test/Test/Data/JoinSemilattice/Intersect.hs
@@ -54,23 +54,23 @@
   x <- forAll Gen.bool
   y <- forAll Gen.bool
 
-  let ( _, _, z ) = andR ( Exactly x, Exactly y, mempty )
-  z === Exactly (x && y)
+  let ( _, _, z ) = andR ( Intersect.singleton x, Intersect.singleton y, mempty )
+  z === Intersect.singleton (x && y)
 
 hprop_booleanR_andR :: Property
-hprop_booleanR_andR = BooleanR.booleanR_andR @(Defined Bool)
+hprop_booleanR_andR = BooleanR.booleanR_andR @Intersect
 
 hprop_booleanR_deMorgan_and :: Property
-hprop_booleanR_deMorgan_and = BooleanR.booleanR_deMorgan_and @(Defined Bool)
+hprop_booleanR_deMorgan_and = BooleanR.booleanR_deMorgan_and @Intersect
 
 hprop_booleanR_deMorgan_or :: Property
-hprop_booleanR_deMorgan_or = BooleanR.booleanR_deMorgan_or @(Defined Bool)
+hprop_booleanR_deMorgan_or = BooleanR.booleanR_deMorgan_or @Intersect
 
 hprop_booleanR_notR :: Property
-hprop_booleanR_notR = BooleanR.booleanR_notR @(Defined Bool)
+hprop_booleanR_notR = BooleanR.booleanR_notR @Intersect
 
 hprop_booleanR_orR :: Property
-hprop_booleanR_orR = BooleanR.booleanR_orR @(Defined Bool)
+hprop_booleanR_orR = BooleanR.booleanR_orR @Intersect
 
 hprop_eqR_simple :: Property
 hprop_eqR_simple = property do
diff --git a/test/Test/Data/Propagator.hs b/test/Test/Data/Propagator.hs
--- a/test/Test/Data/Propagator.hs
+++ b/test/Test/Data/Propagator.hs
@@ -8,39 +8,41 @@
 import Hedgehog
 import qualified Hedgehog.Gen as Gen
 import qualified Hedgehog.Range as Range
+import Data.List (nub)
 import Prelude hiding (read)
 import Test.Control.Monad.Cell.Class (Lestrade, read, scotlandYardSays)
-import Test.Data.JoinSemilattice.Defined (defined_int)
 
 hprop_eqR_reflexivity :: Property
 hprop_eqR_reflexivity = property do
-  x <- forAll defined_int
+  x <- forAll (Gen.int (Range.linear 0 10))
 
   let program :: Lestrade h ()
       program = Prop.down (Prop.lift x .== Prop.lift x)
             >>= \o -> Cell.write o (Exactly True)
 
   if scotlandYardSays program == Nothing
-    then x === Conflict
+    then failure
     else success
 
 hprop_eqR_negation :: Property
 hprop_eqR_negation = property do
-  x <- forAll defined_int
-  y <- forAll defined_int
+  x <- forAll (Gen.int (Range.linear 0 10))
+  y <- forAll (Gen.int (Range.linear 0 10))
 
   let this :: Lestrade h ()
-      this = Prop.down (Prop.lift x .== Prop.lift y) >>= \o -> Cell.write o (Exactly True)
+      this = Prop.down (Prop.lift x .== Prop.lift y)
+         >>= \o -> Cell.write o (Exactly True)
 
       that :: Lestrade h ()
-      that = Prop.down (Prop.lift x ./= Prop.lift y) >>= \o -> Cell.write o (Exactly False)
+      that = Prop.down (Prop.lift x ./= Prop.lift y)
+         >>= \o -> Cell.write o (Exactly False)
 
   scotlandYardSays this === scotlandYardSays that
 
 hprop_eqR_simple :: Property
 hprop_eqR_simple = property do
-  (Exactly -> x) <- forAll (Gen.int (Range.linear 0 10))
-  (Exactly -> y) <- forAll (Gen.int (Range.linear 0 10))
+  x <- forAll (Gen.int (Range.linear 0 10))
+  y <- forAll (Gen.int (Range.linear 0 10))
 
   let program :: Lestrade h (Defined Bool)
       program = Prop.down (Prop.lift x .== Prop.lift y) >>= read
@@ -49,8 +51,8 @@
 
 hprop_eqR_symmetry :: Property
 hprop_eqR_symmetry = property do
-  x <- forAll defined_int
-  y <- forAll defined_int
+  x <- forAll (Gen.int (Range.linear 0 10))
+  y <- forAll (Gen.int (Range.linear 0 10))
 
   let this :: Lestrade h (Defined Bool)
       this = Prop.down (Prop.lift x .== Prop.lift y) >>= read
@@ -62,8 +64,8 @@
 
 hprop_ordR_negation :: Property
 hprop_ordR_negation = property do
-  x <- forAll defined_int
-  y <- forAll defined_int
+  x <- forAll (Gen.int (Range.linear 0 10))
+  y <- forAll (Gen.int (Range.linear 0 10))
 
   let this :: Lestrade h (Defined Bool)
       this = Prop.down (Prop.lift x .<= Prop.lift y) >>= read
@@ -75,8 +77,8 @@
 
 hprop_ordR_lteR_symmetry :: Property
 hprop_ordR_lteR_symmetry = property do
-  x <- forAll defined_int
-  y <- forAll defined_int
+  x <- forAll (Gen.int (Range.linear 0 10))
+  y <- forAll (Gen.int (Range.linear 0 10))
 
   let this :: Lestrade h (Defined Bool)
       this = Prop.down (Prop.lift x .<= Prop.lift y) >>= read
@@ -88,8 +90,8 @@
 
 hprop_ordR_ltR_symmetry :: Property
 hprop_ordR_ltR_symmetry = property do
-  x <- forAll defined_int
-  y <- forAll defined_int
+  x <- forAll (Gen.int (Range.linear 0 10))
+  y <- forAll (Gen.int (Range.linear 0 10))
 
   let this :: Lestrade h (Defined Bool)
       this = Prop.down (Prop.lift x .< Prop.lift y) >>= read
@@ -101,10 +103,53 @@
 
 hprop_ordR_simple :: Property
 hprop_ordR_simple = property do
-  (Exactly -> x) <- forAll (Gen.int (Range.linear 0 10))
-  (Exactly -> y) <- forAll (Gen.int (Range.linear 0 10))
+  x <- forAll (Gen.int (Range.linear 0 10))
+  y <- forAll (Gen.int (Range.linear 0 10))
 
-  let program :: Lestrade h (Defined Bool)
-      program = Prop.down (Prop.lift x .<= Prop.lift y) >>= read
+  let x', y' :: MonadCell m => Prop m (Defined Int)
+      x' = Prop.lift x
+      y' = Prop.lift y
 
+      program :: Lestrade h (Defined Bool)
+      program = Prop.down (x' .<= y') >>= read
+
   scotlandYardSays program === Just (Exactly (x <= y))
+
+hprop_choice_unique_choices :: Property
+hprop_choice_unique_choices = property do
+  n <- forAll $ Gen.int (Range.linear 0 6)
+  k <- forAll $ Gen.int (Range.linear 0 n)
+
+  let choices = Prop.choose n k
+
+  nub choices === choices
+
+hprop_choice_correct_number_of_choices :: Property
+hprop_choice_correct_number_of_choices = property do
+  n <- forAll $ Gen.int (Range.linear 0 6)
+  k <- forAll $ Gen.int (Range.linear 0 n)
+
+  let choices = Prop.choose n k
+      factorial 0 = 1
+      factorial n = n * factorial (pred n)
+
+  length choices === factorial n `div` (factorial k * factorial (n-k))
+
+hprop_exactly_simple :: Property
+hprop_exactly_simple = property do
+  xs <- forAll (Gen.list (Range.linear 0 10) (Gen.int (Range.linear 0 10)))
+  k  <- forAll (Gen.int (Range.linear 0 (length xs)))
+  x  <- forAll (Gen.int (Range.linear 0 10))
+
+  let x' :: MonadCell m => Prop m (Defined Int)
+      x' = Prop.lift x
+      
+      xs' :: MonadCell m => [Prop m (Defined Int)]
+      xs' = map Prop.lift xs
+
+      program :: Lestrade h (Defined Bool)
+      program = Prop.down (Prop.exactly k (.== x') xs') >>= read
+
+      expected = length (filter (==x) xs) == k
+
+  scotlandYardSays program === Just (Exactly expected)