diff --git a/examples/WaveFunctionCollapse.hs b/examples/WaveFunctionCollapse.hs
--- a/examples/WaveFunctionCollapse.hs
+++ b/examples/WaveFunctionCollapse.hs
@@ -13,7 +13,6 @@
 import Data.List (transpose)
 import Data.List.Split (chunksOf)
 import Data.Maybe (isJust, mapMaybe)
-import Data.Propagator (lift)
 import GHC.Generics (Generic)
 import Relude ((!!?))
 import Test.Hspec (Spec, it, shouldBe)
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.3.0.1
+version:            0.3.2.0
 
 library
   exposed-modules: Control.Monad.Cell.Class
@@ -38,7 +38,7 @@
                , Data.JoinSemilattice.Class.Zipping
                , Data.CDCL
 
-  build-depends: base >= 4.12 && < 4.14
+  build-depends: base >= 4.12 && < 4.15
                , containers >= 0.6 && < 0.7
                , hashable >= 1.3 && < 1.4
                , hedgehog >= 1.0 && < 1.1
@@ -65,7 +65,7 @@
                , hspec >= 2.7 && < 2.8
                , split >= 0.2 && < 0.3
                , unordered-containers >= 0.2 && < 0.3
-               , relude >= 0.6 && < 0.7
+               , relude >= 0.6 && < 0.8
                , tasty >= 1.2 && < 1.3
                , tasty-discover
                , tasty-hspec
@@ -109,6 +109,7 @@
                , Test.Data.JoinSemilattice.Defined
                , Test.Data.JoinSemilattice.Intersect
                , Test.Data.Propagator
+               , Test.Regression.Issue7
                , Test.Util.Laws
 
   ghc-options: -Wall -Wextra -threaded
diff --git a/src/Data/Holmes.hs b/src/Data/Holmes.hs
--- a/src/Data/Holmes.hs
+++ b/src/Data/Holmes.hs
@@ -36,6 +36,7 @@
   , FlatMapping (..)
   , FractionalR (..)
   , IntegralR (..)
+  , Lifting (..)
   , Mapping (..)
   , OrdR (..), ltR, gtR, gteR
   , SumR (..), negateR, subR
@@ -48,7 +49,8 @@
   , Intersect (..)
   , using
 
-  , Prop
+  , Prop, Prop.up, Prop.down, Prop.lift, Prop.over
+  , Prop.unary, Prop.binary
 
   , (Prop..$), (Prop..>>=), Prop.zipWith'
 
@@ -79,6 +81,7 @@
 import Data.JoinSemilattice.Class.FlatMapping (FlatMapping (..))
 import Data.JoinSemilattice.Class.Fractional (FractionalR (..))
 import Data.JoinSemilattice.Class.Integral (IntegralR (..))
+import Data.JoinSemilattice.Class.Lifting (Lifting (..))
 import Data.JoinSemilattice.Class.Mapping (Mapping (..))
 import Data.JoinSemilattice.Class.Merge (Merge (..), Result (..))
 import Data.JoinSemilattice.Class.Ord (OrdR (..), ltR, gtR, gteR)
diff --git a/src/Data/JoinSemilattice/Class/Lifting.hs b/src/Data/JoinSemilattice/Class/Lifting.hs
--- a/src/Data/JoinSemilattice/Class/Lifting.hs
+++ b/src/Data/JoinSemilattice/Class/Lifting.hs
@@ -11,9 +11,8 @@
 -}
 module Data.JoinSemilattice.Class.Lifting where
 
-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.Kind (Constraint, Type)
 
@@ -21,11 +20,8 @@
 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
+instance Lifting Defined Eq where
   lift' = Exactly
 
-instance Lifting Intersect Hashable where
+instance Lifting Intersect Intersectable where
   lift' = Intersect.singleton
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
@@ -1,5 +1,6 @@
 {-# LANGUAGE DefaultSignatures #-}
 {-# LANGUAGE KindSignatures #-}
+{-# LANGUAGE MonoLocalBinds #-}
 
 {-|
 Module      : Data.JoinSemilattice.Class.Sum
@@ -9,10 +10,9 @@
 -}
 module Data.JoinSemilattice.Class.Sum where
 
-import Data.Hashable (Hashable)
 import Data.JoinSemilattice.Class.Merge (Merge)
 import Data.JoinSemilattice.Defined (Defined (..))
-import Data.JoinSemilattice.Intersect (Intersect)
+import Data.JoinSemilattice.Intersect (Intersect, Intersectable)
 import Data.Kind (Type)
 
 -- | A relationship between two values and their sum.
@@ -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, Ord x, Hashable x, Num x) => SumR (Intersect x)
+instance (Intersectable x, Num x) => SumR (Intersect x)
diff --git a/test/Test/Regression/Issue7.hs b/test/Test/Regression/Issue7.hs
new file mode 100644
--- /dev/null
+++ b/test/Test/Regression/Issue7.hs
@@ -0,0 +1,89 @@
+{-# OPTIONS_GHC -Wno-missing-methods #-}
+
+{-# LANGUAGE BlockArguments #-}
+{-# LANGUAGE ConstraintKinds #-}
+{-# LANGUAGE DeriveAnyClass #-}
+{-# LANGUAGE DeriveGeneric #-}
+{-# LANGUAGE DerivingStrategies #-}
+{-# LANGUAGE FlexibleContexts #-}
+{-# LANGUAGE LambdaCase #-}
+{-# LANGUAGE ViewPatterns #-}
+module Test.Regression.Issue7 where
+
+import Data.Function ((&))
+import Data.Hashable (Hashable)
+import Data.Holmes
+import GHC.Generics (Generic)
+import Test.Tasty.Hspec (Spec, describe, it, shouldBe)
+
+-------------------------------------------------------------------------------
+-- #7: stack overflow / infinite loop when solving with Intersect instead of
+-- Defined
+
+countEqual
+  :: ( Eq (f x)
+     , Lifting f c
+     , Mapping f c
+     , c x, c v
+     , Num v, Num (f v), SumR (f v)
+     , MonadCell m
+     )
+  => [(Int, x)]
+  -> [Prop m (f x)]
+  -> Prop m (f v)
+countEqual values cells = foldr (.+) (lift 0) (map f values)
+  where
+    f (index, expected) = cells !! index & over \actual ->
+      if lift' expected == actual then 1 else 0
+
+spec_17_defined :: Spec
+spec_17_defined = describe "Issue #17" do
+  it "Defined" do
+    let checks :: [( Int, Int )]
+        checks = [( 0, 3 )]
+
+        threshold :: MonadCell m => Prop m (Defined Int)
+        threshold = lift 0
+
+    example <- (1 `from` [ 1 ]) `satisfying` \cells -> do
+      countEqual checks cells .>= threshold
+
+    example `shouldBe` Just [ 1 ]
+
+  it "Intersect" do
+    let checks :: [( Int, Val4 )]
+        checks = [( 0, 3 )]
+
+        threshold :: MonadCell m => Prop m (Intersect Val4)
+        threshold = lift 0
+
+    example <- (1 `from` [ 1 ]) `satisfying` \cells -> do
+      countEqual checks cells .>= threshold
+
+    example `shouldBe` Just [ 1 ]
+
+newtype Val4 = V4 Int
+  deriving stock (Show, Eq, Ord, Generic)
+  deriving anyclass (Hashable)
+
+instance Num Val4 where
+
+  fromInteger = toEnum . fromInteger
+
+  -- this is not a valid Num instance, we just want to use
+  -- it for counting
+  V4 a + V4 b = if a + b > 4 then V4 4 else V4 (a + b)
+  V4 a - V4 b = if a - b < 0 then V4 0 else V4 (a - b)
+
+instance Enum Val4 where
+  toEnum n
+    | n < 0 || n > 4 = error $ "toEnum Val4 out of bounds: " ++ show n
+    | otherwise = V4 n
+
+  fromEnum v@(V4 m)
+    | m < 0 || m > 4 = error $ "fromEnum Val4 out of bounds: " ++ show v
+    | otherwise = m
+
+instance Bounded Val4 where
+  minBound = toEnum 0
+  maxBound = toEnum 4