diff --git a/CHANGELOG.md b/CHANGELOG.md
--- a/CHANGELOG.md
+++ b/CHANGELOG.md
@@ -1,3 +1,8 @@
+## 0.4.0 (2024-05-11)
+* add `Eq`, `Ord`, `Arbitrary` instances
+* simplify modules (fewer)
+* add `reifyPredicate`, `reifyPredicate1` for reifying predicates to `a -> Bool`
+
 ## 0.3.0 (2024-05-07)
 * refactor predicate names: now handled with a sort of type-level `Show`. no
   `Typeable`, lots of custom prettiness (infix operators!)
diff --git a/rerefined.cabal b/rerefined.cabal
--- a/rerefined.cabal
+++ b/rerefined.cabal
@@ -5,7 +5,7 @@
 -- see: https://github.com/sol/hpack
 
 name:           rerefined
-version:        0.3.0
+version:        0.4.0
 synopsis:       Refinement types, again
 description:    Please see README.md.
 category:       Types, Data
@@ -53,8 +53,6 @@
       Rerefined.Predicates
       Rerefined.Refine
       Rerefined.Refine.TH
-      Rerefined.Refine.Unsafe
-      Rerefined.Refined
   other-modules:
       Paths_rerefined
   hs-source-dirs:
@@ -72,7 +70,8 @@
       MagicHash
   ghc-options: -Wall -Wno-unticked-promoted-constructors
   build-depends:
-      base >=4.17 && <5
+      QuickCheck >=2.14 && <2.16
+    , base >=4.17 && <5
     , mono-traversable >=1.0.17.0 && <1.1
     , template-haskell >=2.19.0.0 && <2.22
     , text >=2.0 && <2.2
diff --git a/src/Rerefined.hs b/src/Rerefined.hs
--- a/src/Rerefined.hs
+++ b/src/Rerefined.hs
@@ -1,7 +1,9 @@
 module Rerefined
   ( module Rerefined.Refine
+  , module Rerefined.Refine.TH
   , Predicate, Refine, Refine1
   ) where
 
 import Rerefined.Refine
+import Rerefined.Refine.TH
 import Rerefined.Predicate
diff --git a/src/Rerefined/Predicate.hs b/src/Rerefined/Predicate.hs
--- a/src/Rerefined/Predicate.hs
+++ b/src/Rerefined/Predicate.hs
@@ -7,6 +7,7 @@
   , Refine1(validate1)
   , RefineFailure(..)
   , Predicate(..)
+  , KnownPredicateName
   , predicateName
   ) where
 
@@ -21,22 +22,19 @@
     -- Predicate names should aim to communicate the meaning of the predicate as
     -- clearly and concisely as possible.
     --
-    -- Consider using @type-level-show@ to build this. However, note that GHC
-    -- cannot figure out 'KnownSymbol' when there are type families in play, so
-    -- you may need to put 'KnownSymbol' constraints in instance contexts.
+    -- Consider using the package @type-level-show@ to build this.
     type PredicateName (d :: Natural) p :: Symbol
         -- ^ TODO d: the operator precedence of the enclosing context (a number
         --   from 0 to 11). Function application has precedence 10.
 
-{- TODO
-stuffing the KnownSymbol constraint into a Predicate superclass is handy, but
-then we have to handle it in combinator predicates. probably _not_ doing so is
-better, so I'm trying that first.
--}
+-- | Constraint for reifying a predicate name.
+type KnownPredicateName p = KnownSymbol (PredicateName 0 p)
 
--- | Reify predicate name.
-predicateName
-    :: forall p. (Predicate p, KnownSymbol (PredicateName 0 p)) => String
+-- | Reify predicate name to a 'String'.
+--
+-- Using this regrettably necessitates @UndecidableInstances@, due to the type
+-- family in the constraint. It sucks, but that's life.
+predicateName :: forall p. KnownPredicateName p => String
 predicateName = symbolVal' (proxy# @(PredicateName 0 p))
 
 -- | Refine @a@ with predicate @p@.
diff --git a/src/Rerefined/Predicate/Common.hs b/src/Rerefined/Predicate/Common.hs
--- a/src/Rerefined/Predicate/Common.hs
+++ b/src/Rerefined/Predicate/Common.hs
@@ -8,20 +8,14 @@
     module Rerefined.Predicate
   , proxy#
   , TBL.Builder
-  , IsString -- TODO remove
 
   -- * Predicate validation
   , validateFail, validateBool
-  , KnownPredicateName
   ) where
 
 import Rerefined.Predicate
 import GHC.Exts ( Proxy#, proxy#, IsString(fromString) )
-import GHC.TypeLits ( KnownSymbol )
 import Data.Text.Builder.Linear qualified as TBL
-
--- TODO maybe move to main 'Rerefined.Predicate' module
-type KnownPredicateName p = KnownSymbol (PredicateName 0 p)
 
 -- | Shortcut for returning a predicate validation failure.
 validateFail
diff --git a/src/Rerefined/Predicate/Logical/And.hs b/src/Rerefined/Predicate/Logical/And.hs
--- a/src/Rerefined/Predicate/Logical/And.hs
+++ b/src/Rerefined/Predicate/Logical/And.hs
@@ -5,13 +5,12 @@
 
 import Rerefined.Predicate.Common.Binary
 import Rerefined.Predicate.Common
-import Rerefined.Refine.Unsafe
-import Rerefined.Refined
+import Rerefined.Refine
 
 -- | Logical conjunction. Also AND logic gate.
 data And l r
 
--- | Precendence of 3 (matching 'Data.Bool.&&').
+-- | Precedence of 3 (matching 'Data.Bool.&&').
 instance (Predicate l, Predicate r) => Predicate (And l r) where
     type PredicateName d (And l r) = PredicateNameBOp " ∧ " 3 d l r
 
diff --git a/src/Rerefined/Predicate/Logical/If.hs b/src/Rerefined/Predicate/Logical/If.hs
--- a/src/Rerefined/Predicate/Logical/If.hs
+++ b/src/Rerefined/Predicate/Logical/If.hs
@@ -9,7 +9,7 @@
 -- | Logical implication. "If l then r".
 data If l r
 
--- | Precendence of 4 (matching '==').
+-- | Precedence of 4 (matching '==').
 instance (Predicate l, Predicate r) => Predicate (If l r) where
     -- TODO double arrow? idk
     type PredicateName d (If l r) = PredicateNameBOp " → " 4 d l r
diff --git a/src/Rerefined/Predicate/Logical/Iff.hs b/src/Rerefined/Predicate/Logical/Iff.hs
--- a/src/Rerefined/Predicate/Logical/Iff.hs
+++ b/src/Rerefined/Predicate/Logical/Iff.hs
@@ -10,7 +10,7 @@
 --   equivalence (loosely).
 data Iff l r
 
--- | Precendence of 4 (matching '==').
+-- | Precedence of 4 (matching '==').
 instance (Predicate l, Predicate r) => Predicate (Iff l r) where
     type PredicateName d (Iff l r) = PredicateNameBOp " ↔ " 4 d l r
 
diff --git a/src/Rerefined/Predicate/Logical/Nand.hs b/src/Rerefined/Predicate/Logical/Nand.hs
--- a/src/Rerefined/Predicate/Logical/Nand.hs
+++ b/src/Rerefined/Predicate/Logical/Nand.hs
@@ -9,7 +9,7 @@
 -- | NAND logic gate. Also called the Sheffer stroke, or non-conjunction.
 data Nand l r
 
--- | Precendence of 3 (matching 'Data.Bool.&&').
+-- | Precedence of 3 (matching 'Data.Bool.&&').
 instance (Predicate l, Predicate r) => Predicate (Nand l r) where
     type PredicateName d (Nand l r) = PredicateNameBOp " ⊼ " 3 d l r
 
diff --git a/src/Rerefined/Predicate/Logical/Nor.hs b/src/Rerefined/Predicate/Logical/Nor.hs
--- a/src/Rerefined/Predicate/Logical/Nor.hs
+++ b/src/Rerefined/Predicate/Logical/Nor.hs
@@ -9,7 +9,7 @@
 -- | NOR logic gate. Also called non-disjunction, or joint denial.
 data Nor l r
 
--- | Precendence of 2 (matching 'Data.Bool.||').
+-- | Precedence of 2 (matching 'Data.Bool.||').
 instance (Predicate l, Predicate r) => Predicate (Nor l r) where
     type PredicateName d (Nor l r) = PredicateNameBOp " ⊽ " 2 d l r
 
diff --git a/src/Rerefined/Predicate/Logical/Not.hs b/src/Rerefined/Predicate/Logical/Not.hs
--- a/src/Rerefined/Predicate/Logical/Not.hs
+++ b/src/Rerefined/Predicate/Logical/Not.hs
@@ -9,7 +9,7 @@
 -- | Logical negation. Also NOT logic gate, or logical complement.
 data Not p
 
--- | Precendence of 9 (one below function application).
+-- | Precedence of 9 (one below function application).
 instance Predicate p => Predicate (Not p) where
     type PredicateName d (Not p) = ShowParen (d > 9)
         ("¬ " ++ PredicateName 10 p)
diff --git a/src/Rerefined/Predicate/Logical/Or.hs b/src/Rerefined/Predicate/Logical/Or.hs
--- a/src/Rerefined/Predicate/Logical/Or.hs
+++ b/src/Rerefined/Predicate/Logical/Or.hs
@@ -9,7 +9,7 @@
 -- | Logical disjunction. Also OR logic gate.
 data Or l r
 
--- | Precendence of 2 (matching 'Data.Bool.||').
+-- | Precedence of 2 (matching 'Data.Bool.||').
 instance (Predicate l, Predicate r) => Predicate (Or l r) where
     type PredicateName d (Or l r) = PredicateNameBOp " ∨ " 2 d l r
 
diff --git a/src/Rerefined/Predicate/Logical/Xor.hs b/src/Rerefined/Predicate/Logical/Xor.hs
--- a/src/Rerefined/Predicate/Logical/Xor.hs
+++ b/src/Rerefined/Predicate/Logical/Xor.hs
@@ -9,7 +9,7 @@
 -- | Logical exclusive disjunction. Also XOR logic gate.
 data Xor l r
 
--- | Precendence of 4 (matching '==').
+-- | Precedence of 4 (matching '==').
 instance (Predicate l, Predicate r) => Predicate (Xor l r) where
     type PredicateName d (Xor l r) = PredicateNameBOp " ⊕ " 4 d l r
 
diff --git a/src/Rerefined/Predicate/Relational/Length.hs b/src/Rerefined/Predicate/Relational/Length.hs
--- a/src/Rerefined/Predicate/Relational/Length.hs
+++ b/src/Rerefined/Predicate/Relational/Length.hs
@@ -9,7 +9,7 @@
 import Data.MonoTraversable ( MonoFoldable(olength) )
 import GHC.Exts ( Proxy# )
 
-import Rerefined.Refine.Unsafe
+import Rerefined.Refine
 import GHC.TypeError
 import Data.Kind ( type Constraint )
 import TypeLevelShow.Utils
diff --git a/src/Rerefined/Refine.hs b/src/Rerefined/Refine.hs
--- a/src/Rerefined/Refine.hs
+++ b/src/Rerefined/Refine.hs
@@ -1,4 +1,6 @@
 {-# LANGUAGE OverloadedStrings #-}
+{-# LANGUAGE AllowAmbiguousTypes #-} -- for predicate reification
+{-# LANGUAGE UndecidableInstances #-} -- for KnownPredicateName in Arbitrary
 
 module Rerefined.Refine
   (
@@ -6,11 +8,18 @@
     type Refined
   , refine
   , unrefine
+  , reifyPredicate
+  , unsafeRefine
+  , unsafeRerefine
 
   -- * @Refined1@
   , type Refined1
   , refine1
   , unrefine1
+  , reifyPredicate1
+  , squashRefined1
+  , unsafeRefine1
+  , unsafeRerefine1
 
   -- * Errors
   , type RefineFailure
@@ -18,12 +27,45 @@
   , prettyRefineFailure'
   ) where
 
-import Rerefined.Refined
 import Rerefined.Predicate
+import Language.Haskell.TH.Syntax ( Lift )
 import GHC.Exts ( proxy# )
 import Data.Text ( Text )
 import Data.Text.Builder.Linear qualified as TBL
 
+import Test.QuickCheck ( Arbitrary(arbitrary) )
+import Test.QuickCheck.Gen qualified as QC
+
+-- | @a@ refined with predicate @p@.
+newtype Refined p a = Refined a
+    deriving stock (Lift, Eq, Ord, Show)
+
+-- | Strip the refinement from a 'Refined'.
+--
+-- This is kept as a separate function for prettier @'Show' 'Refined'@ output.
+unrefine :: Refined p a -> a
+unrefine (Refined a) = a
+
+-- | @f a@ refined with predicate @p@.
+--
+-- We may derive legal 'Functor', 'Traversable' instances for this as
+-- 'Rerefined.Predicate.Refine1' guarantees that the predicate only applies to
+-- the functor structure. That is, you _may_ alter a 'Refined1' without
+-- re-asserting its predicate, provided your changes are made without altering
+-- the structure/shape of @f@ (e.g. 'fmap', 'traverse').
+newtype Refined1 p f a = Refined1 (f a)
+    deriving stock (Functor, Foldable, Traversable, Lift, Eq, Ord, Show)
+
+-- | Strip the refinement from a 'Refined1'.
+--
+-- This is kept as a separate function for prettier @'Show' 'Refined1'@ output.
+unrefine1 :: Refined1 p f a -> f a
+unrefine1 (Refined1 fa) = fa
+
+-- | Squash a 'Refined1' into a 'Refined'. Essentially forget the @f@.
+squashRefined1 :: Refined1 p f a -> Refined p (f a)
+squashRefined1 = Refined . unrefine1
+
 -- | Refine @a@ with predicate @p@.
 refine
     :: forall p a. Refine p a
@@ -33,9 +75,22 @@
       Nothing -> Right (Refined a)
       Just e  -> Left e
 
--- reifyPredicate is just a weaker version of validate without proxy.
--- Maybe the latter is useful, though...?
+-- | Construct a 'Refined' without validating the predicate @p@.
+--
+-- Unsafe. Use only when you can manually prove that the predicate holds.
+unsafeRefine :: a -> Refined p a
+unsafeRefine = Refined
 
+-- | Replace a 'Refined''s predicate without validating the new prdicate @pNew@.
+--
+-- Unsafe. Use only when you can manually prove that the new predicate holds.
+unsafeRerefine :: forall pNew pOld a. Refined pOld a -> Refined pNew a
+unsafeRerefine = Refined . unrefine
+
+-- | Reify a predicate.
+reifyPredicate :: forall p a. Refine p a => a -> Bool
+reifyPredicate a = case refine @p a of Right{} -> True; Left{} -> False
+
 -- | Refine @f a@ with functor predicate @p@.
 refine1
     :: forall p f a. Refine1 p f
@@ -45,6 +100,23 @@
       Nothing -> Right (Refined1 fa)
       Just e  -> Left e
 
+-- | Construct a 'Refined1' without validating the predicate @p@.
+--
+-- Unsafe. Use only when you can manually prove that the predicate holds.
+unsafeRefine1 :: f a -> Refined1 p f a
+unsafeRefine1 = Refined1
+
+-- | Replace a 'Refined1''s predicate without validating the new prdicate
+--   @pNew@.
+--
+-- Unsafe. Use only when you can manually prove that the new predicate holds.
+unsafeRerefine1 :: forall pNew pOld f a. Refined1 pOld f a -> Refined1 pNew f a
+unsafeRerefine1 = Refined1 . unrefine1
+
+-- | Reify a functor predicate.
+reifyPredicate1 :: forall p f a. Refine1 p f => f a -> Bool
+reifyPredicate1 fa = case refine1 @p fa of Right{} -> True; Left{} -> False
+
 {- TODO
 * got an extra \n at start oops
 * make it look better lol
@@ -84,3 +156,27 @@
     idk n rs = \case
       []   -> rs
       l:ls -> idk n ((n, l):rs) ls
+
+-- | Generate a refined term by generating an unrefined term and asserting the
+--   predicate.
+--
+-- Will runtime error if it fails to find a satisfying term (based on size).
+instance (Arbitrary a, Refine p a, KnownPredicateName p)
+  => Arbitrary (Refined p a) where
+    arbitrary = QC.suchThatMaybe arbitrary (reifyPredicate @p) >>= \case
+      Just a  -> pure $ Refined a
+      Nothing -> error $
+           "rerefined: couldn't generate a value satisfying predicate: "
+        <> predicateName @p
+
+-- | Generate a refined term by generating an unrefined term and asserting the
+--   functor predicate.
+--
+-- Will runtime error if it fails to find a satisfying term (based on size).
+instance (Arbitrary (f a), Refine1 p f, KnownPredicateName p)
+  => Arbitrary (Refined1 p f a) where
+    arbitrary = QC.suchThatMaybe arbitrary (reifyPredicate1 @p) >>= \case
+      Just fa -> pure $ Refined1 fa
+      Nothing -> error $
+           "rerefined: couldn't generate a value satisfying predicate: "
+        <> predicateName @p
diff --git a/src/Rerefined/Refine/Unsafe.hs b/src/Rerefined/Refine/Unsafe.hs
deleted file mode 100644
--- a/src/Rerefined/Refine/Unsafe.hs
+++ /dev/null
@@ -1,50 +0,0 @@
-{- | Unsafe refining.
-
-Sometimes, you know that your value satisfies some predicate before validating.
-For those cases, we permit skipping validation and obtaining a refined value
-"for free".
-
-You should be certain that your value cannot possibly fail the predicate you are
-skipping. A good practice is to annotate all call sites with an explanation of
-why the usage is safe.
--}
-
-module Rerefined.Refine.Unsafe
-  (
-  -- * @Refined@
-    type Refined
-  , unsafeRefine
-  , unsafeRerefine
-
-  -- * @Refined1@
-  , type Refined1
-  , unsafeRefine1
-  , unsafeRerefine1
-  ) where
-
-import Rerefined.Refined
-
--- | Construct a 'Refined' without validating the predicate @p@.
---
--- Unsafe. Use only when you can manually prove that the predicate holds.
-unsafeRefine :: a -> Refined p a
-unsafeRefine = Refined
-
--- | Replace a 'Refined''s predicate without validating the new prdicate @pNew@.
---
--- Unsafe. Use only when you can manually prove that the new predicate holds.
-unsafeRerefine :: forall pNew pOld a. Refined pOld a -> Refined pNew a
-unsafeRerefine = Refined . unrefine
-
--- | Construct a 'Refined1' without validating the predicate @p@.
---
--- Unsafe. Use only when you can manually prove that the predicate holds.
-unsafeRefine1 :: f a -> Refined1 p f a
-unsafeRefine1 = Refined1
-
--- | Replace a 'Refined1''s predicate without validating the new prdicate
---   @pNew@.
---
--- Unsafe. Use only when you can manually prove that the new predicate holds.
-unsafeRerefine1 :: forall pNew pOld f a. Refined1 pOld f a -> Refined1 pNew f a
-unsafeRerefine1 = Refined1 . unrefine1
diff --git a/src/Rerefined/Refined.hs b/src/Rerefined/Refined.hs
deleted file mode 100644
--- a/src/Rerefined/Refined.hs
+++ /dev/null
@@ -1,48 +0,0 @@
--- | 'Refined' and 'Refined1' definitions for refined values.
---
--- Not intended for external use. For unsafe refining, use
--- 'Rerefined.Refine.Unsafe'.
-
-module Rerefined.Refined
-  (
-  -- * @Refined@
-    Refined(..)
-  , unrefine
-
-  -- * @Refined1@
-  , Refined1(..)
-  , unrefine1
-  , squashRefined1
-  ) where
-
-import Language.Haskell.TH.Syntax ( Lift )
-
--- | @a@ refined with predicate @p@.
-newtype Refined p a = Refined a
-    deriving stock (Lift, Show)
-
--- | Strip the refinement from a 'Refined'.
---
--- This is kept as a separate function for prettier @'Show' 'Refined'@ output.
-unrefine :: Refined p a -> a
-unrefine (Refined a) = a
-
--- | @f a@ refined with predicate @p@.
---
--- We may derive legal 'Functor', 'Traversable' instances for this as
--- 'Rerefined.Predicate.Refine1' guarantees that the predicate only applies to
--- the functor structure. That is, you _may_ alter a 'Refined1' without
--- re-asserting its predicate, provided your changes are made without altering
--- the structure/shape of @f@ (e.g. 'fmap', 'traverse').
-newtype Refined1 p f a = Refined1 (f a)
-    deriving stock (Functor, Foldable, Traversable, Lift, Show)
-
--- | Strip the refinement from a 'Refined1'.
---
--- This is kept as a separate function for prettier @'Show' 'Refined1'@ output.
-unrefine1 :: Refined1 p f a -> f a
-unrefine1 (Refined1 fa) = fa
-
--- | Squash a 'Refined1' into a 'Refined'. Essentially forget the @f@.
-squashRefined1 :: Refined1 p f a -> Refined p (f a)
-squashRefined1 = Refined . unrefine1