diff --git a/CHANGELOG.md b/CHANGELOG.md
--- a/CHANGELOG.md
+++ b/CHANGELOG.md
@@ -1,3 +1,6 @@
+## 0.8.0 (2024-10-12)
+* tweak `Simplify` exports (should stay fairly stable now)
+
 ## 0.7.0 (2024-10-11)
 * add predicate simplifier at `Rerefined.Simplify`
   * old "normalizer" stuff removed
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.7.0
+version:        0.8.0
 synopsis:       Refinement types, again
 description:    Please see README.md.
 category:       Types, Data
@@ -54,6 +54,7 @@
       Rerefined.Refine
       Rerefined.Refine.TH
       Rerefined.Simplify
+      Rerefined.Simplify.Core
       Rerefined.Simplify.Relational
   other-modules:
       Paths_rerefined
@@ -70,7 +71,7 @@
       TypeFamilies
       DataKinds
       MagicHash
-  ghc-options: -Wall -Wno-unticked-promoted-constructors
+  ghc-options: -fhide-source-paths -Wall
   build-depends:
       QuickCheck >=2.14 && <2.16
     , base >=4.18 && <5
@@ -79,4 +80,35 @@
     , text >=2.0 && <2.2
     , text-builder-linear >=0.1.2 && <0.2
     , type-level-show >=0.2.1 && <0.4
+  default-language: GHC2021
+
+test-suite spec
+  type: exitcode-stdio-1.0
+  main-is: Main.hs
+  other-modules:
+      Paths_rerefined
+  hs-source-dirs:
+      test
+  default-extensions:
+      LambdaCase
+      NoStarIsType
+      DerivingVia
+      DeriveAnyClass
+      GADTs
+      RoleAnnotations
+      DefaultSignatures
+      TypeFamilies
+      DataKinds
+      MagicHash
+  ghc-options: -fhide-source-paths -Wall
+  build-depends:
+      QuickCheck >=2.14 && <2.16
+    , base >=4.18 && <5
+    , mono-traversable >=1.0.17.0 && <1.1
+    , rerefined
+    , template-haskell >=2.19.0.0 && <2.23
+    , text >=2.0 && <2.2
+    , text-builder-linear >=0.1.2 && <0.2
+    , type-level-show >=0.2.1 && <0.4
+    , type-spec >=0.4.0.0 && <0.5
   default-language: GHC2021
diff --git a/src/Rerefined/Simplify.hs b/src/Rerefined/Simplify.hs
--- a/src/Rerefined/Simplify.hs
+++ b/src/Rerefined/Simplify.hs
@@ -2,53 +2,30 @@
 
 {- | Primitive predicate simplifier.
 
-This is related to an NP-complete problem (see Boolean satisfiability problem).
-We focus on /immediate, operation-reducing simplifications/, and hope that the
-input is formed in such a way that our rules match.
-
-In short, the simplifier is largely contextless. It inspects (usually) a single
-layer/depth at a time. So we can consistently simplify things like logical
-identities. But don't expect simplifications hard to spot with the naked eye.
-
 The simplifier may not be expectected to consistently implement any
 transformations whatsoever. The only guarantees are
 
 * the output has the same or fewer operations
 * the output meaning is identical to the input
 
-Implementation pitfalls:
-
-* not extensible: only works for built-in logical & relational predicates
-* no protection against non-termination e.g. if a pair of transformations loop
-* very tedious to write. that's life
+See 'Rerefined.Simplify.Core' (internal module) for more details.
 -}
 
 module Rerefined.Simplify
   ( Simplify
-  , SimplifyStep
+  , TrySimplify
+  , AssertSimplified
   ) where
 
-import Rerefined.Predicate.Succeed
-import Rerefined.Predicate.Fail
-
-import Rerefined.Predicate.Logical
-
-import Rerefined.Predicate.Relational ( CompareLength, CompareValue, FlipRelOp )
-import Rerefined.Simplify.Relational
-  ( SimplifyCompareLength
-  , SimplifyCompareLengthAnd
-  , SimplifyCompareLengthOr
-  )
-
-import Data.Kind ( Type )
+import Rerefined.Simplify.Core ( SimplifyStep )
 
--- note that we can't modularize logical simplifications because they're
--- mutually recursive with the main simplifier :(
+import Data.Kind ( type Constraint )
+import GHC.TypeError ( type TypeError, type ErrorMessage(..) )
+import Rerefined.Predicate ( type PredicateName )
 
 -- | Simplify the given predicate.
 --
 -- Returns the input predicate if we were unable to simplify.
-type Simplify :: Type -> Type
 type Simplify p = Simplify' p
 
 -- | Helper definition for reducing duplication.
@@ -62,216 +39,29 @@
     -- failed to simplify: give up, return the latest predicate
     SimplifyLoop p Nothing   = p
 
--- | Try to perform a single simplification step on the given predicate.
+-- | Try to simplify the given predicate.
 --
 -- Returns 'Nothing' if we were unable to simplify.
-type family SimplifyStep p where
-    SimplifyStep (Not  p)   = SimplifyNot  p
-
-    SimplifyStep (And  l r) = SimplifyAnd  l r
-    SimplifyStep (Or   l r) = SimplifyOr   l r
-    SimplifyStep (Nand l r) = SimplifyNand l r
-    SimplifyStep (Nor  l r) = SimplifyNor  l r
-    SimplifyStep (Iff  l r) = SimplifyIff  l r
-    SimplifyStep (Xor  l r) = SimplifyXor  l r
-    SimplifyStep (If   l r) = SimplifyIf   l r
-
-    SimplifyStep (CompareLength op n) = SimplifyCompareLength op n
-    -- Don't think we can do anything for CompareValue.
-
-    SimplifyStep p = Nothing
-
-type family SimplifyAnd l r where
-    -- identity laws
-    SimplifyAnd p       Fail    = Just Fail
-    SimplifyAnd Fail    p       = Just Fail
-    SimplifyAnd p       Succeed = Just p
-    SimplifyAnd Succeed p       = Just p
-
-    SimplifyAnd p p = Just p
-
-    -- distributivity
-    SimplifyAnd (Or x y) (Or x z) = Just (Or x (And y z))
-
-    -- special
-    SimplifyAnd (CompareLength lop ln) (CompareLength rop rn) =
-        SimplifyCompareLengthAnd lop ln rop rn
-
-    -- recurse
-    SimplifyAnd l r =
-        (OrElseAndL r (SimplifyStep l)
-            (OrElseAndR l (SimplifyStep r)
-                Nothing))
-
-type family OrElseAndL r mp cont where
-    OrElseAndL r Nothing   cont = cont
-    OrElseAndL r (Just l') cont = Just (And l' r)
-
-type family OrElseAndR l mp cont where
-    OrElseAndR l Nothing   cont = cont
-    OrElseAndR l (Just r') cont = Just (And l r')
-
-type family SimplifyOr l r where
-    -- identity laws
-    SimplifyOr Succeed p       = Just Succeed
-    SimplifyOr p       Succeed = Just Succeed
-    SimplifyOr Fail    p       = Just p
-    SimplifyOr p       Fail    = Just p
-
-    SimplifyOr p p = Just p
-
-    -- distributivity
-    SimplifyOr (And x y) (And x z) = Just (And x (Or y z))
-
-    -- special relational
-    SimplifyOr (CompareLength lop ln) (CompareLength rop rn) =
-        SimplifyCompareLengthOr lop ln rop rn
-
-    -- recurse
-    SimplifyOr l r =
-        (OrElseOrL r (SimplifyStep l)
-            (OrElseOrR l (SimplifyStep r)
-                Nothing))
-
-type family OrElseOrL r mp cont where
-    OrElseOrL r Nothing   cont = cont
-    OrElseOrL r (Just l') cont = Just (Or l' r)
-
-type family OrElseOrR l mp cont where
-    OrElseOrR l Nothing   cont = cont
-    OrElseOrR l (Just r') cont = Just (Or l r')
-
-type family SimplifyNand l r where
-    -- identity laws
-    SimplifyNand Fail    p       = Just Succeed
-    SimplifyNand p       Fail    = Just Succeed
-    SimplifyNand Succeed p       = Just (Not p)
-    SimplifyNand p       Succeed = Just (Not p)
-
-    SimplifyNand p p = Just (Not p)
-
-    -- recurse
-    SimplifyNand l r =
-        (OrElseNandL r (SimplifyStep l)
-            (OrElseNandR l (SimplifyStep r)
-                Nothing))
-
-type family OrElseNandL r mp cont where
-    OrElseNandL r Nothing   cont = cont
-    OrElseNandL r (Just l') cont = Just (Nand l' r)
-
-type family OrElseNandR l mp cont where
-    OrElseNandR l Nothing   cont = cont
-    OrElseNandR l (Just r') cont = Just (Nand l r')
-
-type family SimplifyNor l r where
-    -- identity laws
-    SimplifyNor Succeed p       = Just Fail
-    SimplifyNor p       Succeed = Just Fail
-    SimplifyNor Fail    p       = Just (Not p)
-    SimplifyNor p       Fail    = Just (Not p)
-
-    SimplifyNor p p = Just (Not p)
-
-    -- recurse
-    SimplifyNor l r =
-        (OrElseNorL r (SimplifyStep l)
-            (OrElseNorR l (SimplifyStep r)
-                Nothing))
-
-type family OrElseNorL r mp cont where
-    OrElseNorL r Nothing   cont = cont
-    OrElseNorL r (Just l') cont = Just (Nor l' r)
-
-type family OrElseNorR l mp cont where
-    OrElseNorR l Nothing   cont = cont
-    OrElseNorR l (Just r') cont = Just (Nor l r')
-
-type family SimplifyXor l r where
-    -- identity laws
-    SimplifyXor Fail    p       = Just p
-    SimplifyXor p       Fail    = Just p
-    SimplifyXor Succeed p       = Just (Not p)
-    SimplifyXor p       Succeed = Just (Not p)
-
-    SimplifyXor p p = Just Fail
-
-    -- recurse
-    SimplifyXor l r =
-        (OrElseXorL r (SimplifyStep l)
-            (OrElseXorR l (SimplifyStep r)
-                Nothing))
-
-type family OrElseXorL r mp cont where
-    OrElseXorL r Nothing   cont = cont
-    OrElseXorL r (Just l') cont = Just (Xor l' r)
-
-type family OrElseXorR l mp cont where
-    OrElseXorR l Nothing   cont = cont
-    OrElseXorR l (Just r') cont = Just (Xor l r')
-
-type family SimplifyIf l r where
-    -- identity laws
-    SimplifyIf Fail    p       = Just Succeed
-    SimplifyIf p       Fail    = Just Succeed
-    SimplifyIf Succeed p       = Just p
-    SimplifyIf p       Succeed = Just p
-
-    SimplifyIf p p = Just Succeed
-
-    -- recurse
-    SimplifyIf l r =
-        (OrElseIfL r (SimplifyStep l)
-            (OrElseIfR l (SimplifyStep r)
-                Nothing))
-
-type family OrElseIfL r mp cont where
-    OrElseIfL r Nothing   cont = cont
-    OrElseIfL r (Just l') cont = Just (If l' r)
-
-type family OrElseIfR l mp cont where
-    OrElseIfR l Nothing   cont = cont
-    OrElseIfR l (Just r') cont = Just (If l r')
-
-type family SimplifyIff l r where
-    -- identity laws
-    SimplifyIff Succeed p       = Just p
-    SimplifyIff p       Succeed = Just p
-    SimplifyIff Fail    p       = Just (Not p)
-    SimplifyIff p       Fail    = Just (Not p)
-
-    SimplifyIff p p = Just Succeed
-
-    -- recurse
-    SimplifyIff l r =
-        (OrElseIffL r (SimplifyStep l)
-            (OrElseIffR l (SimplifyStep r)
-                Nothing))
-
-type family OrElseIffL r mp cont where
-    OrElseIffL r Nothing   cont = cont
-    OrElseIffL r (Just l') cont = Just (Iff l' r)
-
-type family OrElseIffR l mp cont where
-    OrElseIffR l Nothing   cont = cont
-    OrElseIffR l (Just r') cont = Just (Iff l r')
-
-type family SimplifyNot p where
-    -- double negation
-    SimplifyNot (Not p) = Just p
+type TrySimplify p = TrySimplifyLoop p (SimplifyStep p)
 
-    SimplifyNot Succeed = Just Fail
-    SimplifyNot Fail    = Just Succeed
+-- | Simplification loop which returns 'Nothing' for 0 simplifications.
+type family TrySimplifyLoop p mp where
+    -- got a simplification: continue with the regular simplifier
+    TrySimplifyLoop p (Just p') = Just (Simplify' p')
 
-    -- special relational
-    SimplifyNot (CompareLength op      n) =
-        Just (CompareLength (FlipRelOp op)      n)
-    SimplifyNot (CompareValue  op sign n) =
-        Just (CompareValue  (FlipRelOp op) sign n)
+    -- couldn't simplify
+    TrySimplifyLoop p Nothing   = Nothing
 
-    -- recurse
-    SimplifyNot p = OrElseNot (SimplifyStep p) Nothing
+-- | Assert that a predicate may not be trivially simplified.
+--
+-- Returns the empty constraint on success, else emits a pretty type error.
+--
+-- Useful e.g. if you'd like to make sure a user isn't writing silly predicates.
+type AssertSimplified p = AssertSimplified' p (TrySimplify p)
 
-type family OrElseNot mp cont where
-    OrElseNot (Just p') cont = Just (Not p')
-    OrElseNot Nothing   cont = cont
+type family AssertSimplified' p mp' :: Constraint where
+    AssertSimplified' p Nothing   = ()
+    AssertSimplified' p (Just p') = TypeError
+        (    Text "Predicate is trivially simplifiable"
+        :$$: Text "   " :<>: Text (PredicateName 0 p)
+        :$$: Text "-> " :<>: Text (PredicateName 0 p') )
diff --git a/src/Rerefined/Simplify/Core.hs b/src/Rerefined/Simplify/Core.hs
new file mode 100644
--- /dev/null
+++ b/src/Rerefined/Simplify/Core.hs
@@ -0,0 +1,251 @@
+{-# LANGUAGE UndecidableInstances #-}
+
+{- | Core predicate simplification algorithm.
+
+This is related to an NP-complete problem (see Boolean satisfiability problem).
+We focus on /immediate, operation-reducing simplifications/, and hope that the
+input is formed in such a way that our rules match.
+
+In short, the simplifier is largely contextless. It inspects (usually) a single
+layer/depth at a time. So we can consistently simplify things like logical
+identities. But don't expect simplifications hard to spot with the naked eye.
+
+Implementation pitfalls:
+
+* not extensible: only works for built-in logical & relational predicates
+* no protection against non-termination e.g. if a pair of transformations loop
+* very tedious to write. that's life
+
+__Internal module. Exports may change without warning. Try not to use.__
+-}
+
+module Rerefined.Simplify.Core where
+
+import Rerefined.Predicate.Succeed
+import Rerefined.Predicate.Fail
+
+import Rerefined.Predicate.Logical
+
+import Rerefined.Predicate.Relational ( CompareLength, CompareValue, FlipRelOp )
+import Rerefined.Simplify.Relational
+  ( SimplifyCompareLength
+  , SimplifyCompareLengthAnd
+  , SimplifyCompareLengthOr
+  )
+
+-- note that we can't modularize logical simplifications because they're
+-- mutually recursive with the main simplifier :(
+
+-- | Try to perform a single simplification step on the given predicate.
+--
+-- Returns 'Nothing' if we were unable to simplify.
+type family SimplifyStep p where
+    SimplifyStep (Not  p)   = SimplifyNot  p
+
+    SimplifyStep (And  l r) = SimplifyAnd  l r
+    SimplifyStep (Or   l r) = SimplifyOr   l r
+    SimplifyStep (Nand l r) = SimplifyNand l r
+    SimplifyStep (Nor  l r) = SimplifyNor  l r
+    SimplifyStep (Iff  l r) = SimplifyIff  l r
+    SimplifyStep (Xor  l r) = SimplifyXor  l r
+    SimplifyStep (If   l r) = SimplifyIf   l r
+
+    SimplifyStep (CompareLength op n) = SimplifyCompareLength op n
+    -- Don't think we can do anything for CompareValue.
+
+    SimplifyStep p = Nothing
+
+type family SimplifyAnd l r where
+    -- identity laws
+    SimplifyAnd p       Fail    = Just Fail
+    SimplifyAnd Fail    p       = Just Fail
+    SimplifyAnd p       Succeed = Just p
+    SimplifyAnd Succeed p       = Just p
+
+    SimplifyAnd p p = Just p
+
+    -- distributivity
+    SimplifyAnd (Or x y) (Or x z) = Just (Or x (And y z))
+
+    -- special
+    SimplifyAnd (CompareLength lop ln) (CompareLength rop rn) =
+        SimplifyCompareLengthAnd lop ln rop rn
+
+    -- recurse
+    SimplifyAnd l r =
+        (OrElseAndL r (SimplifyStep l)
+            (OrElseAndR l (SimplifyStep r)
+                Nothing))
+
+type family OrElseAndL r mp cont where
+    OrElseAndL r Nothing   cont = cont
+    OrElseAndL r (Just l') cont = Just (And l' r)
+
+type family OrElseAndR l mp cont where
+    OrElseAndR l Nothing   cont = cont
+    OrElseAndR l (Just r') cont = Just (And l r')
+
+type family SimplifyOr l r where
+    -- identity laws
+    SimplifyOr Succeed p       = Just Succeed
+    SimplifyOr p       Succeed = Just Succeed
+    SimplifyOr Fail    p       = Just p
+    SimplifyOr p       Fail    = Just p
+
+    SimplifyOr p p = Just p
+
+    -- distributivity
+    SimplifyOr (And x y) (And x z) = Just (And x (Or y z))
+
+    -- special relational
+    SimplifyOr (CompareLength lop ln) (CompareLength rop rn) =
+        SimplifyCompareLengthOr lop ln rop rn
+
+    -- recurse
+    SimplifyOr l r =
+        (OrElseOrL r (SimplifyStep l)
+            (OrElseOrR l (SimplifyStep r)
+                Nothing))
+
+type family OrElseOrL r mp cont where
+    OrElseOrL r Nothing   cont = cont
+    OrElseOrL r (Just l') cont = Just (Or l' r)
+
+type family OrElseOrR l mp cont where
+    OrElseOrR l Nothing   cont = cont
+    OrElseOrR l (Just r') cont = Just (Or l r')
+
+type family SimplifyNand l r where
+    -- identity laws
+    SimplifyNand Fail    p       = Just Succeed
+    SimplifyNand p       Fail    = Just Succeed
+    SimplifyNand Succeed p       = Just (Not p)
+    SimplifyNand p       Succeed = Just (Not p)
+
+    SimplifyNand p p = Just (Not p)
+
+    -- recurse
+    SimplifyNand l r =
+        (OrElseNandL r (SimplifyStep l)
+            (OrElseNandR l (SimplifyStep r)
+                Nothing))
+
+type family OrElseNandL r mp cont where
+    OrElseNandL r Nothing   cont = cont
+    OrElseNandL r (Just l') cont = Just (Nand l' r)
+
+type family OrElseNandR l mp cont where
+    OrElseNandR l Nothing   cont = cont
+    OrElseNandR l (Just r') cont = Just (Nand l r')
+
+type family SimplifyNor l r where
+    -- identity laws
+    SimplifyNor Succeed p       = Just Fail
+    SimplifyNor p       Succeed = Just Fail
+    SimplifyNor Fail    p       = Just (Not p)
+    SimplifyNor p       Fail    = Just (Not p)
+
+    SimplifyNor p p = Just (Not p)
+
+    -- recurse
+    SimplifyNor l r =
+        (OrElseNorL r (SimplifyStep l)
+            (OrElseNorR l (SimplifyStep r)
+                Nothing))
+
+type family OrElseNorL r mp cont where
+    OrElseNorL r Nothing   cont = cont
+    OrElseNorL r (Just l') cont = Just (Nor l' r)
+
+type family OrElseNorR l mp cont where
+    OrElseNorR l Nothing   cont = cont
+    OrElseNorR l (Just r') cont = Just (Nor l r')
+
+type family SimplifyXor l r where
+    -- identity laws
+    SimplifyXor Fail    p       = Just p
+    SimplifyXor p       Fail    = Just p
+    SimplifyXor Succeed p       = Just (Not p)
+    SimplifyXor p       Succeed = Just (Not p)
+
+    SimplifyXor p p = Just Fail
+
+    -- recurse
+    SimplifyXor l r =
+        (OrElseXorL r (SimplifyStep l)
+            (OrElseXorR l (SimplifyStep r)
+                Nothing))
+
+type family OrElseXorL r mp cont where
+    OrElseXorL r Nothing   cont = cont
+    OrElseXorL r (Just l') cont = Just (Xor l' r)
+
+type family OrElseXorR l mp cont where
+    OrElseXorR l Nothing   cont = cont
+    OrElseXorR l (Just r') cont = Just (Xor l r')
+
+type family SimplifyIf l r where
+    -- identity laws
+    SimplifyIf Fail    p       = Just Succeed
+    SimplifyIf p       Fail    = Just Succeed
+    SimplifyIf Succeed p       = Just p
+    SimplifyIf p       Succeed = Just p
+
+    SimplifyIf p p = Just Succeed
+
+    -- recurse
+    SimplifyIf l r =
+        (OrElseIfL r (SimplifyStep l)
+            (OrElseIfR l (SimplifyStep r)
+                Nothing))
+
+type family OrElseIfL r mp cont where
+    OrElseIfL r Nothing   cont = cont
+    OrElseIfL r (Just l') cont = Just (If l' r)
+
+type family OrElseIfR l mp cont where
+    OrElseIfR l Nothing   cont = cont
+    OrElseIfR l (Just r') cont = Just (If l r')
+
+type family SimplifyIff l r where
+    -- identity laws
+    SimplifyIff Succeed p       = Just p
+    SimplifyIff p       Succeed = Just p
+    SimplifyIff Fail    p       = Just (Not p)
+    SimplifyIff p       Fail    = Just (Not p)
+
+    SimplifyIff p p = Just Succeed
+
+    -- recurse
+    SimplifyIff l r =
+        (OrElseIffL r (SimplifyStep l)
+            (OrElseIffR l (SimplifyStep r)
+                Nothing))
+
+type family OrElseIffL r mp cont where
+    OrElseIffL r Nothing   cont = cont
+    OrElseIffL r (Just l') cont = Just (Iff l' r)
+
+type family OrElseIffR l mp cont where
+    OrElseIffR l Nothing   cont = cont
+    OrElseIffR l (Just r') cont = Just (Iff l r')
+
+type family SimplifyNot p where
+    -- double negation
+    SimplifyNot (Not p) = Just p
+
+    SimplifyNot Succeed = Just Fail
+    SimplifyNot Fail    = Just Succeed
+
+    -- special relational
+    SimplifyNot (CompareLength op      n) =
+        Just (CompareLength (FlipRelOp op)      n)
+    SimplifyNot (CompareValue  op sign n) =
+        Just (CompareValue  (FlipRelOp op) sign n)
+
+    -- recurse
+    SimplifyNot p = OrElseNot (SimplifyStep p) Nothing
+
+type family OrElseNot mp cont where
+    OrElseNot (Just p') cont = Just (Not p')
+    OrElseNot Nothing   cont = cont
diff --git a/src/Rerefined/Simplify/Relational.hs b/src/Rerefined/Simplify/Relational.hs
--- a/src/Rerefined/Simplify/Relational.hs
+++ b/src/Rerefined/Simplify/Relational.hs
@@ -1,5 +1,13 @@
 {-# LANGUAGE UndecidableInstances #-}
 
+{- | Relational predicate simplification.
+
+These bits aren't mutually recursive with the main simplifier, so we can keep
+them separate for a bit of code hygiene.
+
+__Internal module. Exports may change without warning. Try not to use.__
+-}
+
 module Rerefined.Simplify.Relational where
 
 import Rerefined.Predicate.Succeed
diff --git a/test/Main.hs b/test/Main.hs
new file mode 100644
--- /dev/null
+++ b/test/Main.hs
@@ -0,0 +1,44 @@
+{-# LANGUAGE AllowAmbiguousTypes #-}
+
+module Main where
+
+import Test.TypeSpec hiding ( And )
+import Rerefined.Simplify
+import Rerefined.Predicates
+import Rerefined.Predicate
+import TypeLevelShow.Utils ( type (++) )
+
+-- | Pretty opaque predicate for simplification proofs.
+data Opaque
+instance Predicate Opaque where type PredicateName d Opaque = "p"
+
+-- | Shorthand for the pretty opaque predicate.
+type P = Opaque
+
+main :: IO ()
+main = print spec
+
+spec :: Expect
+    -- AND identity laws
+    (And Fail    P       `SimplifiesTo` Fail
+ -/- And P       Fail    `SimplifiesTo` Fail
+ -/- And Succeed P       `SimplifiesTo` P
+ -/- And P       Succeed `SimplifiesTo` P
+
+     -- OR identity laws
+ -/- Or  Succeed P       `SimplifiesTo` Succeed
+ -/- Or  P       Succeed `SimplifiesTo` Succeed
+ -/- Or  Fail    P       `SimplifiesTo` P
+ -/- Or  P       Fail    `SimplifiesTo` P
+
+     -- other
+ -/- And (CompareLength RelOpLT 3) (CompareLength RelOpGT 3)
+        `SimplifiesTo` Fail
+    )
+spec = Valid
+
+-- | TODO I'd like to write my own failure message here, but type-spec is
+--   complicated.
+type SimplifiesTo p p' = It
+    (PredicateName 0 p ++ " simplifies to " ++ PredicateName 0 p')
+    (TrySimplify p `Is` Just p')