diff --git a/README.lhs b/README.lhs
--- a/README.lhs
+++ b/README.lhs
@@ -4,6 +4,8 @@
 the hood, it uses **propagator networks** and **conflict-directed clause
 learning** to optimise the search over the parameter space.
 
+Now available on [Hackage](https://hackage.haskell.org/package/holmes)!
+
 <!--
 
 ```haskell
diff --git a/README.md b/README.md
--- a/README.md
+++ b/README.md
@@ -4,6 +4,8 @@
 the hood, it uses **propagator networks** and **conflict-directed clause
 learning** to optimise the search over the parameter space.
 
+Now available on [Hackage](https://hackage.haskell.org/package/holmes)!
+
 <!--
 
 ```haskell
diff --git a/examples/Futoshiki.hs b/examples/Futoshiki.hs
--- a/examples/Futoshiki.hs
+++ b/examples/Futoshiki.hs
@@ -77,6 +77,7 @@
 -- All being well, this should be the result! Use `cabal new-test examples` to
 -- run these tests and check for correct solutions.
 
+spec_futoshiki :: Spec
 spec_futoshiki
   = it "computes the solution" do
       solution `shouldBe` Just
diff --git a/holmes.cabal b/holmes.cabal
--- a/holmes.cabal
+++ b/holmes.cabal
@@ -11,11 +11,12 @@
 name:               holmes
 description:        A reference library for constraint-solving with propagators and CDCL.
 synopsis:           Tools and combinators for solving constraint problems.
-version:            0.1.0.1
+version:            0.2.0.0
 
 library
   exposed-modules: Control.Monad.Cell.Class
                  , Control.Monad.Holmes
+                 , Control.Monad.MoriarT
                  , Control.Monad.Watson
                  , Data.Input.Config
                  , Data.JoinSemilattice.Defined
@@ -23,8 +24,7 @@
                  , Data.Propagator
                  , Data.Holmes
 
-  other-modules: Control.Monad.MoriarT
-               , Data.JoinSemilattice.Class.Abs
+  other-modules: Data.JoinSemilattice.Class.Abs
                , Data.JoinSemilattice.Class.Boolean
                , Data.JoinSemilattice.Class.Eq
                , Data.JoinSemilattice.Class.FlatMapping
@@ -38,6 +38,7 @@
                , Data.CDCL
 
   build-depends: base >= 4.12 && < 4.14
+               , containers >= 0.6 && < 0.7
                , hashable >= 1.3 && < 1.4
                , hedgehog >= 1.0 && < 1.1
                , logict >= 0.7 && < 0.8
@@ -73,6 +74,7 @@
 
   ghc-options: -Wall -Wextra -threaded
   hs-source-dirs: examples
+  build-tool-depends: tasty-discover:tasty-discover
   default-language: Haskell2010
 
 --------------------------------------------------
@@ -94,9 +96,24 @@
                , tasty-hedgehog
                , tasty-hspec
 
+  other-modules: Test.Control.Monad.Cell.Class
+               , Test.Data.Input.Config
+               , Test.Data.JoinSemilattice.Class.Abs
+               , Test.Data.JoinSemilattice.Class.Boolean
+               , Test.Data.JoinSemilattice.Class.Eq
+               , Test.Data.JoinSemilattice.Class.Fractional
+               , Test.Data.JoinSemilattice.Class.Integral
+               , Test.Data.JoinSemilattice.Class.Ord
+               , Test.Data.JoinSemilattice.Class.Sum
+               , Test.Data.JoinSemilattice.Defined
+               , Test.Data.JoinSemilattice.Intersect
+               , Test.Data.Propagator
+               , Test.Util.Laws
+
   ghc-options: -Wall -Wextra -threaded
   hs-source-dirs: test
   build-tool-depends: markdown-unlit:markdown-unlit
+                    , tasty-discover:tasty-discover
   default-language: Haskell2010
 
 --------------------------------------------------
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
@@ -26,13 +26,13 @@
   ( Holmes
   , MonadCell
 
-  , unsafeRead
   , backward
   , forward
   , runAll
   , runOne
   , satisfying
   , shuffle
+  , unsafeRead
   , whenever
   ) where
 
@@ -58,6 +58,9 @@
 newtype Holmes (x :: Type)
   = Holmes { runHolmes :: MoriarT IO x }
   deriving (Functor, Applicative, Monad)
+
+instance MonadFail Holmes where
+  fail _ = discard
 
 instance MonadCell Holmes where
   newtype Cell Holmes x = Cell { unwrap :: Cell (MoriarT IO) x }
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
@@ -21,12 +21,12 @@
   ( Watson
   , MonadCell (..)
 
-  , unsafeRead
   , backward
   , forward
   , runAll
   , runOne
   , satisfying
+  , unsafeRead
   , whenever
   ) where
 
@@ -51,6 +51,9 @@
 newtype Watson (h :: Type) (x :: Type)
   = Watson { runWatson :: MoriarT (ST h) x }
   deriving (Functor, Applicative, Monad)
+
+instance MonadFail (Watson h) where
+  fail _ = discard
 
 instance MonadCell (Watson h) where
   newtype Cell (Watson h) x = Cell { unwrap :: Cell (MoriarT (ST h)) x }
diff --git a/src/Data/JoinSemilattice/Class/Abs.hs b/src/Data/JoinSemilattice/Class/Abs.hs
--- a/src/Data/JoinSemilattice/Class/Abs.hs
+++ b/src/Data/JoinSemilattice/Class/Abs.hs
@@ -34,6 +34,6 @@
 
 instance (Eq x, Num x) => AbsR (Defined x)
 
-instance (Bounded x, Enum x, Eq x, Hashable x, Num x)
+instance (Bounded x, Enum x, Ord x, Hashable x, Num x)
     => AbsR (Intersect x) where
   absR ( x, y ) = ( Intersect.union y (negate y), abs x )
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
@@ -46,7 +46,7 @@
       , liftA2 (==) x y
       )
 
-instance (Bounded x, Enum x, Eq x, Hashable x)
+instance (Bounded x, Enum x, Ord x, Hashable x)
     => EqR (Intersect x) (Intersect Bool) where
   eqR ( x, y, z )
     = ( if | z == trueR                           -> y
diff --git a/src/Data/JoinSemilattice/Class/FlatMapping.hs b/src/Data/JoinSemilattice/Class/FlatMapping.hs
--- a/src/Data/JoinSemilattice/Class/FlatMapping.hs
+++ b/src/Data/JoinSemilattice/Class/FlatMapping.hs
@@ -1,4 +1,3 @@
-{-# LANGUAGE BlockArguments #-}
 {-# LANGUAGE ConstraintKinds #-}
 {-# LANGUAGE FunctionalDependencies #-}
 {-# LANGUAGE KindSignatures #-}
@@ -14,6 +13,7 @@
 import Data.JoinSemilattice.Class.Zipping (Zipping)
 import Data.JoinSemilattice.Defined (Defined (..))
 import Data.JoinSemilattice.Intersect (Intersect (..), Intersectable)
+import qualified Data.JoinSemilattice.Intersect as Intersect
 import Data.Kind (Constraint, Type)
 import Prelude hiding (unzip)
 
@@ -29,19 +29,25 @@
 -- implementing the reverse flow for 'Defined' or 'Intersect', and see what
 -- happens.
 class Zipping f c => FlatMapping (f :: Type -> Type) (c :: Type -> Constraint) | f -> c where
-  flatMapR :: (c x, c y) => ((x, f y) -> (x, f y)) -> ((f x, f y) -> (f x, f y))
+  flatMapR :: (c x, c y) => (Maybe (x -> f y), Maybe (f y -> x)) -> ((f x, f y) -> (f x, f y))
 
 instance FlatMapping Defined Eq where
-  flatMapR f ( xs, _ )
-    = ( mempty -- Unless you have 'Monoid x'
-      , case xs of Exactly x -> let ( _, ys' ) = f (x, mempty) in ys'
-                   _         -> mempty
+  flatMapR ( fs, gs ) ( xs, ys )
+    = ( case gs of Just g  -> Exactly (g ys)
+                   Nothing -> mempty
+
+      , case xs of
+          Unknown   -> Unknown
+          Conflict  -> Conflict
+          Exactly x -> case fs of Just f  -> f x
+                                  Nothing -> mempty
       )
 
 instance FlatMapping Intersect Intersectable where
-  flatMapR f ( Intersect xs, _ )
-    = ( mempty -- Unless you have 'Monoid x'
-        
-        -- Take the union of all generated 'Intersect' values.
-      , Intersect (foldMap (\x -> let (_, Intersect ys') = f (x, mempty) in ys') xs)
+  flatMapR ( fs, gs ) ( xs, ys )
+    = ( case gs of Just g  -> Intersect.map g (Intersect.powerSet ys)
+                   Nothing -> mempty
+
+      , case fs of Just f  -> foldr (Intersect.union . f) (Intersect mempty) xs
+                   Nothing -> mempty
       )
diff --git a/src/Data/JoinSemilattice/Class/Fractional.hs b/src/Data/JoinSemilattice/Class/Fractional.hs
--- a/src/Data/JoinSemilattice/Class/Fractional.hs
+++ b/src/Data/JoinSemilattice/Class/Fractional.hs
@@ -36,5 +36,5 @@
 
 instance (Eq x, Fractional x) => FractionalR (Defined x)
 
-instance (Bounded x, Enum x, Eq x, Fractional x, Hashable x)
+instance (Bounded x, Enum x, Ord x, Fractional x, Hashable x)
   => FractionalR (Intersect x)
diff --git a/src/Data/JoinSemilattice/Class/Integral.hs b/src/Data/JoinSemilattice/Class/Integral.hs
--- a/src/Data/JoinSemilattice/Class/Integral.hs
+++ b/src/Data/JoinSemilattice/Class/Integral.hs
@@ -42,7 +42,7 @@
       ,  x - (y * z)
       )
 
-instance (Bounded x, Enum x, Eq x, Hashable x, Integral x)
+instance (Bounded x, Enum x, Ord x, Hashable x, Integral x)
     => IntegralR (Intersect x) where
   divModR ( x, y, z, w )
     = ( y * z + w
diff --git a/src/Data/JoinSemilattice/Class/Mapping.hs b/src/Data/JoinSemilattice/Class/Mapping.hs
--- a/src/Data/JoinSemilattice/Class/Mapping.hs
+++ b/src/Data/JoinSemilattice/Class/Mapping.hs
@@ -1,10 +1,8 @@
 {-# LANGUAGE ConstraintKinds #-}
-{-# LANGUAGE DefaultSignatures #-}
 {-# LANGUAGE FunctionalDependencies #-}
 {-# LANGUAGE PolyKinds #-}
 {-# LANGUAGE QuantifiedConstraints #-}
 {-# LANGUAGE UndecidableInstances #-}
-{-# LANGUAGE ViewPatterns #-}
 
 {-|
 Module      : Data.JoinSemilattice.Class.Mapping
@@ -14,28 +12,38 @@
 -}
 module Data.JoinSemilattice.Class.Mapping where
 
-import Control.Applicative (liftA2)
 import Data.JoinSemilattice.Class.Merge (Merge)
-import Data.JoinSemilattice.Defined (Defined)
+import Data.JoinSemilattice.Defined (Defined (..))
 import Data.JoinSemilattice.Intersect (Intersect, Intersectable)
 import qualified Data.JoinSemilattice.Intersect as Intersect
 import Data.Kind (Constraint, Type)
-import Data.List.NonEmpty (unzip)
-import Prelude hiding (unzip)
 
 -- | Lift a relationship between two values over some type constructor.
 -- Typically, this type constructor will be the parameter type.
 class (forall x. c x => Merge (f x))
     => Mapping (f :: Type -> Type) (c :: Type -> Constraint) | f -> c where
-  mapR :: (c x, c y) => ((x, y) -> (x, y)) -> ((f x, f y) -> (f x, f y))
+  mapR :: (c x, c y) => (Maybe (x -> y), Maybe (y -> x)) -> ((f x, f y) -> (f x, f y))
 
-  default mapR :: Applicative f => ((x, y) -> (x, y)) -> ((f x, f y) -> (f x, f y))
-  mapR f (xs, ys) = unzip (liftA2 (curry f) xs ys)
+instance Mapping Defined Eq where
+  mapR ( fs, gs ) ( xs, ys )
+    = ( case ys of
+          Unknown   -> Unknown
+          Conflict  -> Conflict
+          Exactly y -> case gs of Just g  -> Exactly (g y)
+                                  Nothing -> Unknown
 
-instance Mapping Defined Eq
+      , case xs of
+          Unknown   -> Unknown
+          Conflict  -> Conflict
+          Exactly x -> case fs of Just f  -> Exactly (f x)
+                                  Nothing -> Unknown
+      )
 
 instance Mapping Intersect Intersectable where
-  mapR f (Intersect.toList -> xs, Intersect.toList -> ys) = do
-    let ( xs', ys' ) = unzip (liftA2 (curry f) xs ys)
+  mapR ( fs, gs ) ( xs, ys )
+    = ( case gs of Just g  -> Intersect.map g ys
+                   Nothing -> mempty
 
-    ( Intersect.fromList xs', Intersect.fromList ys' )
+      , case fs of Just f  -> Intersect.map f xs
+                   Nothing -> mempty
+      )
diff --git a/src/Data/JoinSemilattice/Class/Merge.hs b/src/Data/JoinSemilattice/Class/Merge.hs
--- a/src/Data/JoinSemilattice/Class/Merge.hs
+++ b/src/Data/JoinSemilattice/Class/Merge.hs
@@ -94,6 +94,17 @@
 instance Semigroup x => Monoid (Result x) where
   mempty = Unchanged
 
+instance Applicative Result where
+  pure = Changed
+
+  Failure <*> _ = Failure
+  _ <*> Failure = Failure
+
+  Unchanged <*> _ = Unchanged
+  _ <*> Unchanged = Unchanged
+
+  Changed f <*> Changed x = Changed (f x)
+
 -- | Join semilattice '(<>)' specialised for propagator network needs. Allows
 -- types to implement the notion of "knowledge combination".
 class Monoid x => Merge (x :: Type) where
@@ -113,7 +124,7 @@
     | this == that = Unchanged
     | otherwise    = Failure
 
-instance (Bounded x, Enum x, Eq x, Hashable x)
+instance (Bounded x, Enum x, Ord x, Hashable x)
     => Merge (Intersect x) where
   before <<- news = case before <> news of
     joined | Intersect.size joined < 1                     -> Failure
diff --git a/src/Data/JoinSemilattice/Class/Sum.hs b/src/Data/JoinSemilattice/Class/Sum.hs
--- a/src/Data/JoinSemilattice/Class/Sum.hs
+++ b/src/Data/JoinSemilattice/Class/Sum.hs
@@ -31,4 +31,4 @@
 negateR ( x, y ) = let ( x', y', _ ) = addR ( x, y, 0 ) in ( x', y' )
 
 instance (Eq x, Num x) => SumR (Defined x)
-instance (Bounded x, Enum x, Eq x, Hashable x, Num x) => SumR (Intersect x)
+instance (Bounded x, Enum x, Ord x, Hashable x, Num x) => SumR (Intersect x)
diff --git a/src/Data/JoinSemilattice/Class/Zipping.hs b/src/Data/JoinSemilattice/Class/Zipping.hs
--- a/src/Data/JoinSemilattice/Class/Zipping.hs
+++ b/src/Data/JoinSemilattice/Class/Zipping.hs
@@ -1,9 +1,6 @@
-{-# LANGUAGE BlockArguments #-}
 {-# LANGUAGE ConstraintKinds #-}
-{-# LANGUAGE DefaultSignatures #-}
 {-# LANGUAGE FunctionalDependencies #-}
 {-# LANGUAGE KindSignatures #-}
-{-# LANGUAGE ViewPatterns #-}
 
 {-|
 Module      : Data.JoinSemilattice.Class.Zipping
@@ -13,33 +10,44 @@
 -}
 module Data.JoinSemilattice.Class.Zipping (Zipping (..)) where
 
-import Control.Applicative (liftA3)
-import Data.Function ((&))
+import Control.Applicative (liftA2)
 import Data.JoinSemilattice.Class.Mapping (Mapping)
 import Data.JoinSemilattice.Defined (Defined)
 import Data.JoinSemilattice.Intersect (Intersect, Intersectable)
 import qualified Data.JoinSemilattice.Intersect as Intersect
 import Data.Kind (Constraint, Type)
-import Prelude hiding (unzip3)
 
 -- | Lift a relationship between three values over some @f@ (usually a
 -- parameter type).
 class Mapping f c => Zipping (f :: Type -> Type) (c :: Type -> Constraint) | f -> c where
-  zipWithR :: (c x, c y, c z) => ((x, y, z) -> (x, y, z)) -> ((f x, f y, f z) -> (f x, f y, f z))
+  zipWithR
+    :: (c x, c y, c z)
+    => ( Maybe ((x, y) -> z)
+       , Maybe ((x, z) -> y)
+       , Maybe ((y, z) -> x)
+       )
+    -> ((f x, f y, f z) -> (f x, f y, f z))
 
-  default zipWithR :: Applicative f => ((x, y, z) -> (x, y, z)) -> ((f x, f y, f z) -> (f x, f y, f z))
-  zipWithR f (xs, ys, zs) = unzip3 (liftA3 (\x y z -> f (x, y, z)) xs ys zs)
+instance Zipping Defined Eq where
+  zipWithR (fs, gs, hs) (x, y, z)
+    = ( case hs of Just h  -> liftA2 (curry h) y z
+                   Nothing -> mempty
 
-instance Zipping Defined Eq
+      , case gs of Just g  -> liftA2 (curry g) x z
+                   Nothing -> mempty
 
+      , case fs of Just f  -> liftA2 (curry f) x y
+                   Nothing -> mempty
+      )
+
 instance Zipping Intersect Intersectable where
-  zipWithR f (Intersect.toList -> xs, Intersect.toList -> ys, Intersect.toList -> zs) = do
-    let ( xs', ys', zs' ) = unzip3 (liftA3 (\x y z -> f (x, y, z)) xs ys zs)
-    ( Intersect.fromList xs', Intersect.fromList ys', Intersect.fromList zs' )
+  zipWithR (fs, gs, hs) (x, y, z)
+    = ( case hs of Just h  -> Intersect.lift2 (curry h) y z
+                   Nothing -> mempty
 
-unzip3 :: Functor f => f (x, y, z) -> (f x, f y, f z)
-unzip3 xyz
-  = ( xyz & fmap \(x, _, _) -> x
-    , xyz & fmap \(_, y, _) -> y
-    , xyz & fmap \(_, _, z) -> z
-    )
+      , case gs of Just g  -> Intersect.lift2 (curry g) x z
+                   Nothing -> mempty
+
+      , case fs of Just f  -> Intersect.lift2 (curry f) x y
+                   Nothing -> mempty
+      )
diff --git a/src/Data/JoinSemilattice/Intersect.hs b/src/Data/JoinSemilattice/Intersect.hs
--- a/src/Data/JoinSemilattice/Intersect.hs
+++ b/src/Data/JoinSemilattice/Intersect.hs
@@ -30,6 +30,8 @@
 import Data.Hashable (Hashable)
 import Data.Input.Config (Config (..), Input (..))
 import Data.Kind (Type)
+import Data.Set (Set)
+import qualified Data.Set as Set
 import Prelude hiding (filter, map, unzip)
 
 -- | A set type with intersection as the '(<>)' operation.
@@ -38,10 +40,10 @@
   deriving stock (Eq, Ord, Show, Foldable)
   deriving newtype (Hashable)
 
-class (Bounded content, Enum content, Eq content, Hashable content)
+class (Bounded content, Enum content, Ord content, Hashable content)
   => Intersectable content
 
-instance (Bounded content, Enum content, Eq content, Hashable content)
+instance (Bounded content, Enum content, Ord content, Hashable content)
   => Intersectable content
 
 instance (Eq content, Hashable content) => Semigroup (Intersect content) where
@@ -108,10 +110,17 @@
 filter :: (x -> Bool) -> Intersect x -> Intersect x
 filter = coerce HashSet.filter
 
+-- | Convert a 'Set' to an 'Intersect'.
+fromSet :: (Eq x, Hashable x) => Set x -> Intersect x
+fromSet = Intersect . foldr HashSet.insert mempty
+
 -- | Map over an 'Intersect' with a given function.
 map :: (Eq y, Hashable y) => (x -> y) -> Intersect x -> Intersect y
 map = coerce HashSet.map
 
+powerSet :: (Bounded x, Enum x, Hashable x, Ord x) => Intersect x -> Intersect (Intersect x)
+powerSet = fromSet . Set.map fromSet . Set.powerSet . toSet
+
 -- | Create a singleton 'Intersect'.
 singleton :: Hashable x => x -> Intersect x
 singleton = coerce HashSet.singleton
@@ -119,6 +128,10 @@
 -- | Count the candidates in an 'Intersect'.
 size :: Intersectable x => Intersect x -> Int
 size = coerce HashSet.size
+
+-- | Convert an 'Intersect' to a 'Set'.
+toSet :: Ord x => Intersect x -> Set x
+toSet = foldr Set.insert mempty
 
 -- | Merge two 'Intersect' values with set __union__.
 union :: Intersectable x => Intersect x -> Intersect x -> Intersect x 
diff --git a/src/Data/Propagator.hs b/src/Data/Propagator.hs
--- a/src/Data/Propagator.hs
+++ b/src/Data/Propagator.hs
@@ -395,18 +395,18 @@
 -- type. Unlike 'over', this function abstracts away the specific behaviour of
 -- the parameter type (such as 'Data.JoinSemilattice.Defined.Defined').
 (.$) :: (Mapping f c, c x, c y) => (x -> y) -> Prop m (f x) -> Prop m (f y)
-(.$) f = Unary (Cell.unary (mapR \( x, _ ) -> ( x, f x )))
+(.$) f = Unary (Cell.unary (mapR (Just f, Nothing)))
 
 -- | Lift a three-way relationship over two propagator networks' foci to
 -- produce a third propagator network with a focus on the third value in the
 -- relationship.
 --
 -- /... It's 'Control.Applicative.liftA2' for propagators./
-zipWith' :: (Zipping f c, c x, c y, c z) => ((x, y, z) -> (x, y, z)) -> Prop m (f x) -> Prop m (f y) -> Prop m (f z)
-zipWith' f = Binary (Cell.binary (zipWithR f))
+zipWith' :: (Zipping f c, c x, c y, c z) => (x -> y -> z) -> Prop m (f x) -> Prop m (f y) -> Prop m (f z)
+zipWith' f = Binary (Cell.binary (zipWithR (Just (uncurry f), Nothing, Nothing)))
 
 -- | Produce a network in which the raw values of a given network are used to
 -- produce new parameter types. See the "wave function collapse" demo for an
 -- example usage.
 (.>>=) :: (FlatMapping f c, c x, c y) => Prop m (f x) -> (x -> f y) -> Prop m (f y)
-(.>>=) xs f = Unary (Cell.unary (flatMapR \( x, _ ) -> ( x, f x ))) xs
+(.>>=) xs f = Unary (Cell.unary (flatMapR (Just f, Nothing))) xs
diff --git a/test/Test/Control/Monad/Cell/Class.hs b/test/Test/Control/Monad/Cell/Class.hs
new file mode 100644
--- /dev/null
+++ b/test/Test/Control/Monad/Cell/Class.hs
@@ -0,0 +1,74 @@
+{-# LANGUAGE DataKinds #-}
+{-# LANGUAGE DerivingVia #-}
+{-# LANGUAGE GeneralisedNewtypeDeriving #-}
+{-# LANGUAGE KindSignatures #-}
+{-# LANGUAGE PolyKinds #-}
+{-# LANGUAGE RankNTypes #-}
+{-# LANGUAGE TypeFamilies #-}
+{-# LANGUAGE UnboxedTuples #-}
+{-# LANGUAGE UndecidableInstances #-}
+module Test.Control.Monad.Cell.Class where
+
+import Control.Applicative (Alternative (..))
+import Control.Monad (MonadPlus)
+import Control.Monad.Cell.Class (MonadCell (..))
+import Control.Monad.Primitive (PrimMonad (..))
+import Control.Monad.ST (ST, runST)
+import Control.Monad.Trans.Maybe (MaybeT (..))
+import Data.Holmes (Merge (..), Result (..))
+import Data.Kind (Type)
+import Data.Monoid (Ap (..))
+import Data.Primitive.MutVar (MutVar)
+import qualified Data.Primitive.MutVar as MutVar
+import Prelude hiding (read)
+
+-- | A monad for testing. 'Lestrade' is only capable of single computation
+-- branches, and can't backtrack.
+newtype Lestrade (h :: Type) (x :: Type)
+  = Lestrade { unwrap :: MaybeT (ST h) x }
+  deriving newtype
+    ( Functor
+    , Applicative
+    , Alternative
+    , Monad
+    , MonadPlus
+    , PrimMonad
+    )
+  deriving (Semigroup, Monoid)
+    via (Ap (Lestrade h) x)
+
+scotlandYardSays :: (forall h. Lestrade h x) -> Maybe x
+scotlandYardSays xs = runST (runMaybeT (unwrap xs))
+
+instance MonadCell (Lestrade h) where
+  data Cell (Lestrade h) x = Cell
+    ( MutVar (PrimState (Lestrade h)) (x, Lestrade h ())
+    )
+
+  discard = empty
+
+  fill x = do
+    ref <- MutVar.newMutVar (x, mempty)
+    pure (Cell ref)
+
+  watch cell@(Cell ref) f = do
+    (content, callback) <- MutVar.readMutVar ref
+
+    MutVar.writeMutVar ref (content, callback *> with cell f)
+    with cell f
+
+  with cell f = read cell >>= f
+
+  write (Cell ref) news = do
+    (content, callback) <- MutVar.readMutVar ref
+
+    case content <<- news of
+      Unchanged -> pure ()
+      Changed x -> MutVar.writeMutVar ref (x, callback) *> callback
+      Failure   -> discard
+
+read :: Cell (Lestrade h) x -> Lestrade h x
+read (Cell ref) = do
+  (content, _) <- MutVar.readMutVar ref
+
+  pure content
diff --git a/test/Test/Data/Input/Config.hs b/test/Test/Data/Input/Config.hs
new file mode 100644
--- /dev/null
+++ b/test/Test/Data/Input/Config.hs
@@ -0,0 +1,35 @@
+{-# LANGUAGE AllowAmbiguousTypes #-}
+{-# LANGUAGE BlockArguments #-}
+{-# LANGUAGE ScopedTypeVariables #-}
+{-# LANGUAGE TypeFamilies #-}
+module Test.Data.Input.Config where
+
+import Control.Monad.Holmes (Holmes, runOne)
+import Control.Monad.IO.Class (MonadIO (..))
+import Data.Hashable (Hashable)
+import Data.Input.Config (Input (..), Config (..), permute)
+import qualified Data.Set as Set
+import Hedgehog
+import qualified Hedgehog.Gen as Gen
+import qualified Hedgehog.Range as Range
+
+possibilities :: Gen [Int]
+possibilities = do
+  let values = Gen.int (Range.linear 0 100)
+  set <- Gen.set (Range.linear 1 5) values
+
+  pure (Set.toList set)
+
+from_fill :: forall x. (Eq x, Hashable x, Input x, Show x, Raw x ~ Int) => Property
+from_fill = property do
+  count  <- forAll (Gen.int (Range.linear 1 10))
+  inputs <- forAll possibilities
+
+  let config :: Config Holmes x
+      config = count `from` inputs
+  annotateShow (initial config)
+
+  Just permutations <- liftIO (runOne (permute config))
+  annotateShow permutations
+
+  length permutations === length inputs ^ count
diff --git a/test/Test/Data/JoinSemilattice/Class/Abs.hs b/test/Test/Data/JoinSemilattice/Class/Abs.hs
new file mode 100644
--- /dev/null
+++ b/test/Test/Data/JoinSemilattice/Class/Abs.hs
@@ -0,0 +1,17 @@
+{-# LANGUAGE BlockArguments #-}
+module Test.Data.JoinSemilattice.Class.Abs where
+
+import Data.Holmes (AbsR (..))
+import Hedgehog
+
+absR_absR :: (AbsR x, Eq x, Num x, Show x) => Gen x -> Property
+absR_absR gen = property do
+  a <- forAll gen
+
+  let ( _, b ) = absR ( a, mempty )
+  annotateShow b
+  b === abs a
+
+  let ( a', _ ) = absR ( mempty, b )
+  annotateShow a'
+  a' <> a === a
diff --git a/test/Test/Data/JoinSemilattice/Class/Boolean.hs b/test/Test/Data/JoinSemilattice/Class/Boolean.hs
new file mode 100644
--- /dev/null
+++ b/test/Test/Data/JoinSemilattice/Class/Boolean.hs
@@ -0,0 +1,82 @@
+{-# LANGUAGE AllowAmbiguousTypes #-}
+{-# LANGUAGE BlockArguments #-}
+{-# LANGUAGE RankNTypes #-}
+{-# LANGUAGE ScopedTypeVariables #-}
+{-# LANGUAGE ViewPatterns #-}
+module Test.Data.JoinSemilattice.Class.Boolean where
+
+import Data.Holmes (BooleanR (..))
+import Hedgehog
+import qualified Hedgehog.Gen as Gen
+
+bool :: BooleanR x => Gen x
+bool = Gen.element [ trueR, falseR ]
+
+booleanR_andR :: forall x. (BooleanR x, Eq x, Show x) => Property
+booleanR_andR = property do
+  (a :: x) <- forAll bool
+  (b :: x) <- forAll bool
+
+  let ( _, _, c ) = andR ( a, b, mempty )
+  annotateShow c
+
+  let ( a', _, _ ) = andR ( mempty, b, c )
+  annotateShow a'
+  a' <> a === a
+
+  let ( _, b', _ ) = andR ( a, mempty, c )
+  annotateShow b'
+  b' <> b === b
+
+booleanR_deMorgan_and :: forall x. (BooleanR x, Eq x, Show x) => Property
+booleanR_deMorgan_and = property do
+  (a :: x) <- forAll bool
+  (b :: x) <- forAll bool
+
+  let ( _, _, c ) = andR ( a, b, mempty )
+      ( _, a' ) = notR ( a, mempty )
+      ( _, b' ) = notR ( b, mempty )
+      ( _, _, d' ) = orR ( a', b', mempty )
+      ( _, d ) = notR ( d', mempty )
+
+  c === d
+
+booleanR_deMorgan_or :: forall x. (BooleanR x, Eq x, Show x) => Property
+booleanR_deMorgan_or = property do
+  (a :: x) <- forAll bool
+  (b :: x) <- forAll bool
+
+  let ( _, _, c ) = orR ( a, b, mempty )
+      ( _, a' ) = notR ( a, mempty )
+      ( _, b' ) = notR ( b, mempty )
+      ( _, _, d' ) = andR ( a', b', mempty )
+      ( _, d ) = notR ( d', mempty )
+
+  c === d
+
+booleanR_orR :: forall x. (BooleanR x, Eq x, Show x) => Property
+booleanR_orR = property do
+  (a :: x) <- forAll bool
+  (b :: x) <- forAll bool
+
+  let ( _, _, c ) = orR ( a, b, mempty )
+  annotateShow c
+
+  let ( a', _, _ ) = orR ( mempty, b, c )
+  annotateShow a'
+  a' <> a === a
+
+  let ( _, b', _ ) = orR ( a, mempty, c )
+  annotateShow b'
+  b' <> b === b
+
+booleanR_notR :: forall x. (BooleanR x, Eq x, Show x) => Property
+booleanR_notR = property do
+  (a :: x) <- forAll bool
+
+  let ( _, b ) = notR ( a, mempty )
+  annotateShow b
+
+  let ( a', _ ) = notR ( mempty, b )
+  annotateShow a'
+  a' === a
diff --git a/test/Test/Data/JoinSemilattice/Class/Eq.hs b/test/Test/Data/JoinSemilattice/Class/Eq.hs
new file mode 100644
--- /dev/null
+++ b/test/Test/Data/JoinSemilattice/Class/Eq.hs
@@ -0,0 +1,56 @@
+{-# LANGUAGE AllowAmbiguousTypes #-}
+{-# LANGUAGE BlockArguments #-}
+{-# LANGUAGE RankNTypes #-}
+{-# LANGUAGE ScopedTypeVariables #-}
+{-# LANGUAGE ViewPatterns #-}
+module Test.Data.JoinSemilattice.Class.Eq where
+
+import Data.Holmes (BooleanR (..), EqR (..), neR)
+import Hedgehog
+
+eqR_eqR :: (EqR x b, Show b, Eq x, Show x) => Gen x -> Property
+eqR_eqR gen = property do
+  a <- forAll gen
+  b <- forAll gen
+
+  let ( _, _, c ) = eqR ( a, b, mempty )
+  annotateShow c
+
+  let ( a', _, _ ) = eqR ( mempty, b, c )
+  annotateShow a'
+  a' <> a === a
+
+  let ( _, b', _ ) = eqR ( a, mempty, c )
+  annotateShow b'
+  b' <> b === b
+
+eqR_negation :: (EqR x b, Show b, Eq b, Eq x, Show x) => Gen x -> Property
+eqR_negation gen = property do
+  a <- forAll gen
+  b <- forAll gen
+
+  let ( _, _, c ) = eqR ( a, b, mempty )
+  annotateShow c
+
+  let ( _, _, d ) = neR ( a, b, mempty )
+  annotateShow d
+
+  let ( _, c' ) = notR ( c, mempty )
+  c' === d
+
+eqR_reflexivity :: (EqR x b, Show b, Eq b, Show x) => Gen 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 gen = property do
+  a <- forAll gen
+  b <- forAll gen
+
+  let ( _, _, x ) = eqR ( a, b, mempty )
+      ( _, _, y ) = eqR ( b, a, mempty )
+
+  x === y
diff --git a/test/Test/Data/JoinSemilattice/Class/Fractional.hs b/test/Test/Data/JoinSemilattice/Class/Fractional.hs
new file mode 100644
--- /dev/null
+++ b/test/Test/Data/JoinSemilattice/Class/Fractional.hs
@@ -0,0 +1,20 @@
+{-# LANGUAGE BlockArguments #-}
+module Test.Data.JoinSemilattice.Class.Fractional where
+
+import Data.Holmes (FractionalR (..))
+import Hedgehog
+
+fractionalR_multiplyR :: (FractionalR x, Eq x, Fractional x, Show x) => Gen x -> Property
+fractionalR_multiplyR gen = property do
+  a <- forAll gen
+  b <- forAll gen
+  let c = a * b
+
+  let ( _, _, c' ) = multiplyR ( a, b, mempty )
+  c' === a * b
+
+  let ( a', _, _ ) = multiplyR ( mempty, b, c )
+  a' === c / b
+
+  let ( _, b', _ ) = multiplyR ( a, mempty, c )
+  b' === c / a
diff --git a/test/Test/Data/JoinSemilattice/Class/Integral.hs b/test/Test/Data/JoinSemilattice/Class/Integral.hs
new file mode 100644
--- /dev/null
+++ b/test/Test/Data/JoinSemilattice/Class/Integral.hs
@@ -0,0 +1,24 @@
+{-# LANGUAGE BlockArguments #-}
+module Test.Data.JoinSemilattice.Class.Integral where
+
+import Data.Holmes (IntegralR (..))
+import Hedgehog
+
+integralR_divModR :: (IntegralR x, Eq x, Integral x, Show x) => Gen x -> Property
+integralR_divModR gen = property do
+  b <- forAll gen
+  c <- forAll gen
+  d <- fmap (`mod` b) (forAll gen)
+  let a = b * c + d
+
+  let ( a', _, _, _ ) = divModR ( mempty, b, c, d )
+  a' === b * c + d
+
+  let ( _, b', _, _ ) = divModR ( a, mempty, c, d )
+  b' === ((a - d) `div` c)
+
+  let ( _, _, c', _ ) = divModR ( a, b, mempty, d )
+  c' === a `div` b
+
+  let ( _, _, _, d' ) = divModR ( a, b, c, mempty )
+  d' === a `mod` b
diff --git a/test/Test/Data/JoinSemilattice/Class/Ord.hs b/test/Test/Data/JoinSemilattice/Class/Ord.hs
new file mode 100644
--- /dev/null
+++ b/test/Test/Data/JoinSemilattice/Class/Ord.hs
@@ -0,0 +1,37 @@
+{-# LANGUAGE AllowAmbiguousTypes #-}
+{-# LANGUAGE BlockArguments #-}
+{-# LANGUAGE RankNTypes #-}
+{-# LANGUAGE ScopedTypeVariables #-}
+{-# LANGUAGE ViewPatterns #-}
+module Test.Data.JoinSemilattice.Class.Ord where
+
+import Data.Holmes (BooleanR (..), OrdR (..))
+import Hedgehog
+
+ordR_lteR :: (OrdR x b, Show b, Eq x, Show x) => Gen x -> Property
+ordR_lteR gen = property do
+  a <- forAll gen
+  b <- forAll gen
+
+  let ( _, _, c ) = lteR ( a, b, mempty )
+  annotateShow c
+
+  let ( a', _, _ ) = lteR ( mempty, b, c )
+  annotateShow a'
+  a' <> a === a
+
+  let ( _, b', _ ) = lteR ( a, mempty, c )
+  annotateShow b'
+  b' <> b === b
+
+ordR_symmetry :: (OrdR x b, Eq b, Eq x, Show x) => Gen x -> Property
+ordR_symmetry gen = property do
+  a <- forAll gen
+  b <- forAll gen
+
+  let ( _, _, x ) = lteR ( a, b, mempty )
+      ( _, _, y ) = lteR ( b, a, mempty )
+
+  if x == trueR && y == trueR
+    then a === b
+    else success
diff --git a/test/Test/Data/JoinSemilattice/Class/Sum.hs b/test/Test/Data/JoinSemilattice/Class/Sum.hs
new file mode 100644
--- /dev/null
+++ b/test/Test/Data/JoinSemilattice/Class/Sum.hs
@@ -0,0 +1,20 @@
+{-# LANGUAGE BlockArguments #-}
+module Test.Data.JoinSemilattice.Class.Sum where
+
+import Data.Holmes (SumR (..))
+import Hedgehog
+
+sumR_addR :: (SumR x, Eq x, Num x, Show x) => Gen x -> Property
+sumR_addR gen = property do
+  a <- forAll gen
+  b <- forAll gen
+  let c = a + b
+
+  let ( _, _, c' ) = addR ( a, b, mempty )
+  c' === a + b
+
+  let ( a', _, _ ) = addR ( mempty, b, c )
+  a' === c - b
+
+  let ( _, b', _ ) = addR ( a, mempty, c )
+  b' === c - a
diff --git a/test/Test/Data/JoinSemilattice/Defined.hs b/test/Test/Data/JoinSemilattice/Defined.hs
new file mode 100644
--- /dev/null
+++ b/test/Test/Data/JoinSemilattice/Defined.hs
@@ -0,0 +1,191 @@
+{-# LANGUAGE BlockArguments #-}
+{-# LANGUAGE TypeApplications #-}
+{-# LANGUAGE ViewPatterns #-}
+module Test.Data.JoinSemilattice.Defined where
+
+import Data.Holmes
+import Hedgehog
+import qualified Hedgehog.Gen as Gen
+import qualified Hedgehog.Range as Range
+import qualified Test.Data.Input.Config as Input
+import qualified Test.Data.JoinSemilattice.Class.Abs as AbsR
+import qualified Test.Data.JoinSemilattice.Class.Boolean as BooleanR
+import qualified Test.Data.JoinSemilattice.Class.Eq as EqR
+import qualified Test.Data.JoinSemilattice.Class.Fractional as FractionalR
+import qualified Test.Data.JoinSemilattice.Class.Integral as IntegralR
+import qualified Test.Data.JoinSemilattice.Class.Ord as OrdR
+import qualified Test.Data.JoinSemilattice.Class.Sum as SumR
+import Test.Tasty.Hspec (Spec, it, shouldBe)
+import qualified Test.Util.Laws as Laws
+
+defined_double :: Gen (Defined Double)
+defined_double = do
+  content <- Gen.double (Range.linearFrac 1 100)
+  Gen.element [ Unknown, Exactly content, Conflict ]
+
+defined_int :: Gen (Defined Int)
+defined_int = do
+  content <- Gen.int (Range.linear 1 100)
+  Gen.element [ Unknown, Exactly content, Conflict ]
+
+defined_int_unconflicted :: Gen (Defined Int)
+defined_int_unconflicted = do
+  content <- Gen.int (Range.linear 1 100)
+  Gen.element [ Unknown, Exactly content ]
+
+hprop_from_fill :: Property
+hprop_from_fill = Input.from_fill @(Defined Int)
+
+hprop_semigroup_associativity :: Property
+hprop_semigroup_associativity = Laws.semigroup_associativity defined_int
+
+hprop_monoid_identity :: Property
+hprop_monoid_identity = Laws.monoid_identity defined_int
+
+hprop_join_semilattice_commutativity :: Property
+hprop_join_semilattice_commutativity = Laws.semigroup_commutativity defined_int
+
+hprop_join_semilattice_idempotence :: Property
+hprop_join_semilattice_idempotence = Laws.semigroup_idempotence defined_int
+
+hprop_functor_identity :: Property
+hprop_functor_identity = Laws.functor_identity defined_int
+
+hprop_functor_composition :: Property
+hprop_functor_composition = Laws.functor_composition defined_int
+
+hprop_applicative_identity :: Property
+hprop_applicative_identity = Laws.applicative_identity defined_int
+
+hprop_applicative_composition :: Property
+hprop_applicative_composition = Laws.applicative_composition defined_int
+
+hprop_applicative_homomorphism :: Property
+hprop_applicative_homomorphism = Laws.applicative_homomorphism @Defined
+
+hprop_applicative_interchange :: Property
+hprop_applicative_interchange = Laws.applicative_interchange defined_int
+
+hprop_absR :: Property
+hprop_absR = AbsR.absR_absR defined_int
+
+hprop_booleanR_andR_simple :: Property
+hprop_booleanR_andR_simple = property do
+  x <- forAll Gen.bool
+  y <- forAll Gen.bool
+
+  let ( _, _, z ) = andR ( Exactly x, Exactly y, mempty )
+  z === Exactly (x && y)
+
+hprop_booleanR_andR :: Property
+hprop_booleanR_andR = BooleanR.booleanR_andR @(Defined Bool)
+
+hprop_booleanR_deMorgan_and :: Property
+hprop_booleanR_deMorgan_and = BooleanR.booleanR_deMorgan_and @(Defined Bool)
+
+hprop_booleanR_deMorgan_or :: Property
+hprop_booleanR_deMorgan_or = BooleanR.booleanR_deMorgan_or @(Defined Bool)
+
+hprop_booleanR_notR :: Property
+hprop_booleanR_notR = BooleanR.booleanR_notR @(Defined Bool)
+
+hprop_booleanR_orR :: Property
+hprop_booleanR_orR = BooleanR.booleanR_orR @(Defined Bool)
+
+hprop_eqR_simple :: Property
+hprop_eqR_simple = property do
+  (Exactly -> x) <- forAll (Gen.int (Range.linear 0 20))
+  (Exactly -> y) <- forAll (Gen.int (Range.linear 0 20))
+
+  let ( _, _, z ) = eqR ( x, y, mempty )
+  z === Exactly (x == y)
+
+hprop_eqR_eqR :: Property
+hprop_eqR_eqR = EqR.eqR_eqR defined_int
+
+hprop_eqR_reflexivity :: Property
+hprop_eqR_reflexivity = EqR.eqR_reflexivity defined_int_unconflicted
+
+hprop_eqR_symmetry :: Property
+hprop_eqR_symmetry = EqR.eqR_symmetry defined_int
+
+hprop_eqR_negation :: Property
+hprop_eqR_negation = EqR.eqR_negation defined_int
+
+hprop_fractionalR_mulR :: Property
+hprop_fractionalR_mulR = FractionalR.fractionalR_multiplyR defined_double
+
+hprop_integralR_divMod :: Property
+hprop_integralR_divMod = IntegralR.integralR_divModR defined_int
+
+hprop_ordR_lteR :: Property
+hprop_ordR_lteR = OrdR.ordR_lteR defined_int
+
+hprop_ordR_lteR_simple :: Property
+hprop_ordR_lteR_simple = property do
+  (Exactly -> x) <- forAll (Gen.int (Range.linear 0 20))
+  (Exactly -> y) <- forAll (Gen.int (Range.linear 0 20))
+
+  let ( _, _, z ) = lteR ( x, y, mempty )
+  z === Exactly (x <= y)
+
+hprop_ordR_symmetry :: Property
+hprop_ordR_symmetry = OrdR.ordR_symmetry defined_int
+
+hprop_ordR_reflexivity :: Property
+hprop_ordR_reflexivity = property do
+  x <- forAll defined_int
+
+  let ( _, _, c ) = lteR ( x, x, mempty )
+  assert (x == Conflict || c <> trueR == trueR)
+
+hprop_sumR_addR :: Property
+hprop_sumR_addR = SumR.sumR_addR defined_int
+
+hprop_sumR_addR_simple :: Property
+hprop_sumR_addR_simple = property do
+  (Exactly -> x) <- forAll (Gen.int (Range.linear 0 10))
+  (Exactly -> y) <- forAll (Gen.int (Range.linear 0 10))
+
+  let ( _, _, z ) = addR ( x, y, mempty )
+  z === x + y
+
+hprop_sumR_negateR_simple :: Property
+hprop_sumR_negateR_simple = property do
+  (Exactly -> x) <- forAll (Gen.int (Range.linear 0 10))
+
+  let ( _, y ) = negateR ( x, mempty )
+  y === negate x
+
+hprop_sumR_subR_simple :: Property
+hprop_sumR_subR_simple = property do
+  (Exactly -> x) <- forAll (Gen.int (Range.linear 0 10))
+  (Exactly -> y) <- forAll (Gen.int (Range.linear 0 10))
+
+  let ( _, _, z ) = subR ( x, y, mempty )
+  z === x - y
+
+spec_dinesman :: Spec
+spec_dinesman = it "dinesman" do
+  let baker, cooper, fletcher, miller, smith :: Defined Int
+      baker    = 3
+      cooper   = 2
+      fletcher = 4
+      miller   = 5
+      smith    = 1
+
+  let ( _, _, a ) = neR  ( baker, 5, mempty ) -- *
+      ( _, _, b ) = neR  ( cooper, 1, mempty ) -- *
+      ( _, _, c ) = neR  ( fletcher, 1, mempty )
+      ( _, _, d ) = neR  ( fletcher, 5, mempty )
+      ( _, _, e ) = andR ( c, d, mempty ) -- *
+      ( _, _, f ) = gtR  ( miller, cooper, mempty ) -- *
+      ( _, _, g ) = subR ( smith, fletcher, mempty )
+      ( _,    h ) = absR ( g, mempty )
+      ( _, _, i ) = neR  ( h, 1, mempty) -- *
+      ( _, _, j ) = subR ( fletcher, cooper, mempty )
+      ( _,    k ) = absR ( j, mempty )
+      ( _, _, l ) = neR  ( k, 1, mempty) -- *
+
+  ( a, b, e, f, i, l ) `shouldBe`
+    ( trueR, trueR, trueR, trueR, trueR, trueR )
diff --git a/test/Test/Data/JoinSemilattice/Intersect.hs b/test/Test/Data/JoinSemilattice/Intersect.hs
new file mode 100644
--- /dev/null
+++ b/test/Test/Data/JoinSemilattice/Intersect.hs
@@ -0,0 +1,104 @@
+{-# LANGUAGE BlockArguments #-}
+{-# LANGUAGE DeriveAnyClass #-}
+{-# LANGUAGE DeriveGeneric #-}
+{-# LANGUAGE DerivingStrategies #-}
+{-# LANGUAGE TypeApplications #-}
+{-# LANGUAGE ViewPatterns #-}
+module Test.Data.JoinSemilattice.Intersect where
+
+import Data.Hashable (Hashable)
+import Data.Holmes
+import qualified Data.JoinSemilattice.Intersect as Intersect
+import GHC.Generics (Generic)
+import Hedgehog
+import qualified Hedgehog.Gen as Gen
+import qualified Hedgehog.Range as Range
+import qualified Test.Data.Input.Config as Input
+import qualified Test.Data.JoinSemilattice.Class.Boolean as BooleanR
+import qualified Test.Data.JoinSemilattice.Class.Eq as EqR
+import qualified Test.Data.JoinSemilattice.Class.Ord as OrdR
+import qualified Test.Util.Laws as Laws
+
+data Weekday
+  = Monday | Tuesday | Wednesday | Thursday | Friday | Saturday | Sunday
+  deriving (Bounded, Enum, Eq, Generic, Ord, Show)
+  deriving anyclass (Hashable)
+
+intersect_weekday :: Gen (Intersect Weekday)
+intersect_weekday = do
+  list <- Gen.list (Range.linear 0 4) Gen.enumBounded
+  pure (Intersect.fromList list)
+
+intersect_weekday_unconflicted :: Gen (Intersect Weekday)
+intersect_weekday_unconflicted = do
+  list <- Gen.list (Range.linear 1 4) Gen.enumBounded
+  pure (Intersect.fromList list)
+
+hprop_from_fill :: Property
+hprop_from_fill = Input.from_fill @(Intersect Int)
+
+hprop_semigroup_associativity :: Property
+hprop_semigroup_associativity = Laws.semigroup_associativity intersect_weekday
+
+hprop_monoid_identity :: Property
+hprop_monoid_identity = Laws.monoid_identity intersect_weekday
+
+hprop_join_semilattice_commutativity :: Property
+hprop_join_semilattice_commutativity = Laws.semigroup_commutativity intersect_weekday
+
+hprop_join_semilattice_idempotence :: Property
+hprop_join_semilattice_idempotence = Laws.semigroup_idempotence intersect_weekday
+
+hprop_booleanR_andR_simple :: Property
+hprop_booleanR_andR_simple = property do
+  x <- forAll Gen.bool
+  y <- forAll Gen.bool
+
+  let ( _, _, z ) = andR ( Exactly x, Exactly y, mempty )
+  z === Exactly (x && y)
+
+hprop_booleanR_andR :: Property
+hprop_booleanR_andR = BooleanR.booleanR_andR @(Defined Bool)
+
+hprop_booleanR_deMorgan_and :: Property
+hprop_booleanR_deMorgan_and = BooleanR.booleanR_deMorgan_and @(Defined Bool)
+
+hprop_booleanR_deMorgan_or :: Property
+hprop_booleanR_deMorgan_or = BooleanR.booleanR_deMorgan_or @(Defined Bool)
+
+hprop_booleanR_notR :: Property
+hprop_booleanR_notR = BooleanR.booleanR_notR @(Defined Bool)
+
+hprop_booleanR_orR :: Property
+hprop_booleanR_orR = BooleanR.booleanR_orR @(Defined Bool)
+
+hprop_eqR_simple :: Property
+hprop_eqR_simple = property do
+  (Exactly -> x) <- forAll (Gen.int (Range.linear 0 20))
+  (Exactly -> y) <- forAll (Gen.int (Range.linear 0 20))
+
+  let ( _, _, z ) = eqR ( x, y, mempty )
+  z === Exactly (x == y)
+
+hprop_eqR_eqR :: Property
+hprop_eqR_eqR = EqR.eqR_eqR intersect_weekday
+
+hprop_eqR_reflexivity :: Property
+hprop_eqR_reflexivity = EqR.eqR_reflexivity intersect_weekday_unconflicted
+
+hprop_eqR_symmetry :: Property
+hprop_eqR_symmetry = EqR.eqR_symmetry intersect_weekday
+
+hprop_eqR_negation :: Property
+hprop_eqR_negation = EqR.eqR_negation intersect_weekday
+
+hprop_ordR_lteR :: Property
+hprop_ordR_lteR = OrdR.ordR_lteR intersect_weekday
+
+hprop_ordR_lteR_simple :: Property
+hprop_ordR_lteR_simple = property do
+  (Exactly -> x) <- forAll (Gen.int (Range.linear 0 20))
+  (Exactly -> y) <- forAll (Gen.int (Range.linear 0 20))
+
+  let ( _, _, z ) = lteR ( x, y, mempty )
+  z === Exactly (x <= y)
diff --git a/test/Test/Data/Propagator.hs b/test/Test/Data/Propagator.hs
new file mode 100644
--- /dev/null
+++ b/test/Test/Data/Propagator.hs
@@ -0,0 +1,110 @@
+{-# LANGUAGE BlockArguments #-}
+{-# LANGUAGE ViewPatterns #-}
+module Test.Data.Propagator where
+
+import qualified Control.Monad.Cell.Class as Cell
+import Data.Holmes
+import qualified Data.Propagator as Prop
+import Hedgehog
+import qualified Hedgehog.Gen as Gen
+import qualified Hedgehog.Range as Range
+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
+
+  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
+    else success
+
+hprop_eqR_negation :: Property
+hprop_eqR_negation = property do
+  x <- forAll defined_int
+  y <- forAll defined_int
+
+  let this :: Lestrade h ()
+      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)
+
+  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))
+
+  let program :: Lestrade h (Defined Bool)
+      program = Prop.down (Prop.lift x .== Prop.lift y) >>= read
+
+  scotlandYardSays program === Just (Exactly (x == y))
+
+hprop_eqR_symmetry :: Property
+hprop_eqR_symmetry = property do
+  x <- forAll defined_int
+  y <- forAll defined_int
+
+  let this :: Lestrade h (Defined Bool)
+      this = Prop.down (Prop.lift x .== Prop.lift y) >>= read
+
+      that :: Lestrade h (Defined Bool)
+      that = Prop.down (Prop.lift y .== Prop.lift x) >>= read
+
+  scotlandYardSays this === scotlandYardSays that
+
+hprop_ordR_negation :: Property
+hprop_ordR_negation = property do
+  x <- forAll defined_int
+  y <- forAll defined_int
+
+  let this :: Lestrade h (Defined Bool)
+      this = Prop.down (Prop.lift x .<= Prop.lift y) >>= read
+
+      that :: Lestrade h (Defined Bool)
+      that = Prop.down (Prop.lift x .> Prop.lift y) >>= read
+
+  scotlandYardSays this === fmap (fmap not) (scotlandYardSays that)
+
+hprop_ordR_lteR_symmetry :: Property
+hprop_ordR_lteR_symmetry = property do
+  x <- forAll defined_int
+  y <- forAll defined_int
+
+  let this :: Lestrade h (Defined Bool)
+      this = Prop.down (Prop.lift x .<= Prop.lift y) >>= read
+
+      that :: Lestrade h (Defined Bool)
+      that = Prop.down (Prop.lift y .>= Prop.lift x) >>= read
+
+  scotlandYardSays this === scotlandYardSays that
+
+hprop_ordR_ltR_symmetry :: Property
+hprop_ordR_ltR_symmetry = property do
+  x <- forAll defined_int
+  y <- forAll defined_int
+
+  let this :: Lestrade h (Defined Bool)
+      this = Prop.down (Prop.lift x .< Prop.lift y) >>= read
+
+      that :: Lestrade h (Defined Bool)
+      that = Prop.down (Prop.lift y .> Prop.lift x) >>= read
+
+  scotlandYardSays this === scotlandYardSays that
+
+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))
+
+  let program :: Lestrade h (Defined Bool)
+      program = Prop.down (Prop.lift x .<= Prop.lift y) >>= read
+
+  scotlandYardSays program === Just (Exactly (x <= y))
diff --git a/test/Test/Util/Laws.hs b/test/Test/Util/Laws.hs
new file mode 100644
--- /dev/null
+++ b/test/Test/Util/Laws.hs
@@ -0,0 +1,81 @@
+{-# LANGUAGE AllowAmbiguousTypes #-}
+{-# LANGUAGE BlockArguments #-}
+{-# LANGUAGE RankNTypes #-}
+{-# LANGUAGE ScopedTypeVariables #-}
+{-# LANGUAGE TypeApplications #-}
+module Test.Util.Laws where
+
+import Control.Applicative (liftA2)
+import Hedgehog
+import qualified Hedgehog.Gen as Gen
+import qualified Hedgehog.Range as Range
+
+semigroup_associativity :: (Eq x, Semigroup x, Show x) => Gen x -> Property
+semigroup_associativity gen = property do
+  x <- forAll gen
+  y <- forAll gen
+  z <- forAll gen
+
+  x <> (y <> z) === (x <> y) <> z
+
+monoid_identity :: (Eq x, Monoid x, Show x) => Gen x -> Property
+monoid_identity gen = property do
+  x <- forAll gen
+  mempty <> x === x
+
+semigroup_commutativity :: (Eq x, Semigroup x, Show x) => Gen x -> Property
+semigroup_commutativity gen = property do
+  x <- forAll gen
+  y <- forAll gen
+
+  x <> y === y <> x
+
+semigroup_idempotence :: (Eq x, Semigroup x, Show x) => Gen x -> Property
+semigroup_idempotence gen = property do
+  x <- forAll gen
+
+  x <> x === x
+
+functor_identity :: (Eq (f x), Functor f, Show (f x)) => Gen (f x) -> Property
+functor_identity gen = property do
+  x <- forAll gen
+
+  fmap id x === x
+
+functor_composition :: (Eq (f Int), Functor f, Show (f Int)) => Gen (f Int) -> Property
+functor_composition gen = property do
+  x <- forAll gen
+  y <- forAll $ Gen.int (Range.linear 0 100)
+  z <- forAll $ Gen.int (Range.linear 0 100)
+
+  fmap (+ y) (fmap (* z) x) === fmap ((+ y) . (* z)) x
+
+applicative_identity :: (Applicative f, Eq (f x), Show (f x)) => Gen (f x) -> Property
+applicative_identity gen = property do
+  x <- forAll gen
+
+  (pure id <*> x) === x
+
+applicative_composition :: (Applicative f, Eq (f Int), Show (f Int)) => Gen (f Int) -> Property
+applicative_composition gen = property do
+  x <- forAll gen
+  y <- forAll gen
+  z <- forAll gen
+
+  liftA2 (+) x (liftA2 (+) y z) === liftA2 (+) (liftA2 (+) x y) z
+
+applicative_homomorphism :: forall f. (Applicative f, Eq (f Int), Show (f Int)) => Property
+applicative_homomorphism = property do
+  x <- forAll (Gen.int (Range.linear 0 10))
+  y <- forAll (Gen.int (Range.linear 0 10))
+
+  (pure (+) <*> pure x <*> pure y)
+    === pure @f (x + y)
+
+applicative_interchange :: (Applicative f, Eq (f Int), Show (f Int)) => Gen (f Int) -> Property
+applicative_interchange gen = property do
+  x <- forAll (Gen.int (Range.linear 0 10))
+  y <- forAll gen
+
+  let f = fmap (+) y
+  (f <*> pure x) === (pure ($ x) <*> f)