diff --git a/CHANGELOG.md b/CHANGELOG.md
--- a/CHANGELOG.md
+++ b/CHANGELOG.md
@@ -1,3 +1,11 @@
+## 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!)
+* refactor logical predicates, keeping them together doesn't help
+* define relational operators using `Ordering` and logical `Or`
+* add missing `Foldable`, `Traversable` instances to `Refined1`
+* general cleanup
+
 ## 0.2.0 (2024-05-01)
 * add missing `Show` instance to `RefineFailure`
 * add missing `Functor` instance to `Refined1`
diff --git a/README.md b/README.md
--- a/README.md
+++ b/README.md
@@ -38,18 +38,11 @@
 See [refined#101](https://github.com/nikita-volkov/refined/issues/101).
 `Typeable` is useful, but the way it is used brings lots of `Typeable` contexts.
 
-rerefined has predicates declare their "predicate name" explicitly. You can
-still use `Typeable` for non-combinator predicates, where no `Typeable` contexts
-are incurred, but combinator predicates such as binary logical predicates
-require more work. However, you can use all the existing `ShowS` helpers (that's
-how `typeRep`s are printed anyway), so it's just like writing a manual `Show`
-instance! Plus, combinator predicates are fairly unusual, so library users will
-probably never see this.
-
-Note that this change also improves predicate name display, since `typeRep`
-tries to display inferred/hidden kinds for wrapped predicates in combinator
-predicates, which are uninteresting. We can ignore these in our manual
-instances!
+rerefined asks that you do a bit more work upfront, but gives you tools and
+grants much more power. Predicates declare their "predicate name" explicitly as
+a type-level `Symbol`. Precedence is supported and infix operators are welcomed.
+(For now, the logical operators primarily look like their propositional logic
+counterparts.)
 
 ### Cleaner design
 What do `LessThan`, `GreaterThan`, `EqualTo` etc. have in common? They're all
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.2.0
+version:        0.3.0
 synopsis:       Refinement types, again
 description:    Please see README.md.
 category:       Types, Data
@@ -16,6 +16,10 @@
 license:        MIT
 license-file:   LICENSE
 build-type:     Simple
+tested-with:
+    GHC==9.8
+  , GHC==9.6
+  , GHC==9.4
 extra-source-files:
     README.md
     CHANGELOG.md
@@ -29,20 +33,28 @@
       Rerefined
       Rerefined.Predicate
       Rerefined.Predicate.Common
+      Rerefined.Predicate.Common.Binary
       Rerefined.Predicate.Fail
       Rerefined.Predicate.Logical
+      Rerefined.Predicate.Logical.And
+      Rerefined.Predicate.Logical.Equivalences
+      Rerefined.Predicate.Logical.If
+      Rerefined.Predicate.Logical.Iff
+      Rerefined.Predicate.Logical.Nand
+      Rerefined.Predicate.Logical.Nor
+      Rerefined.Predicate.Logical.Not
+      Rerefined.Predicate.Logical.Or
+      Rerefined.Predicate.Logical.Xor
       Rerefined.Predicate.Relational
       Rerefined.Predicate.Relational.Internal
       Rerefined.Predicate.Relational.Length
       Rerefined.Predicate.Relational.Value
       Rerefined.Predicate.Succeed
       Rerefined.Predicates
-      Rerefined.Predicates.RefinedShim
       Rerefined.Refine
       Rerefined.Refine.TH
       Rerefined.Refine.Unsafe
       Rerefined.Refined
-      Rerefined.Refined1
   other-modules:
       Paths_rerefined
   hs-source-dirs:
@@ -60,8 +72,10 @@
       MagicHash
   ghc-options: -Wall -Wno-unticked-promoted-constructors
   build-depends:
-      base >=4.16 && <5
+      base >=4.17 && <5
     , mono-traversable >=1.0.17.0 && <1.1
-    , template-haskell
-    , typeably >=0.1.0 && <0.2
+    , template-haskell >=2.19.0.0 && <2.22
+    , text >=2.0 && <2.2
+    , text-builder-linear >=0.1.2 && <0.2
+    , type-level-show >=0.1.0 && <0.2
   default-language: GHC2021
diff --git a/src/Rerefined/Predicate.hs b/src/Rerefined/Predicate.hs
--- a/src/Rerefined/Predicate.hs
+++ b/src/Rerefined/Predicate.hs
@@ -1,40 +1,50 @@
+{-# LANGUAGE AllowAmbiguousTypes #-}
+
 -- | Base definitions for refinement predicates.
 
 module Rerefined.Predicate
   ( Refine(validate)
   , Refine1(validate1)
   , RefineFailure(..)
-  , Predicate(predicateName)
+  , Predicate(..)
+  , predicateName
   ) where
 
-import GHC.Exts ( Proxy# )
-import Data.Typeable ( Typeable, typeRep )
-import Data.Typeable.Typeably
-import Data.Proxy ( Proxy(Proxy) )
+import GHC.Exts ( Proxy#, proxy# )
+import Data.Text.Builder.Linear qualified as TBL
+import GHC.TypeLits ( Natural, Symbol, KnownSymbol, symbolVal' )
 
 -- | Types which define refinements on other types.
 class Predicate p where
-    -- | The predicate name, as a 'Show'-like (for good bracketing).
+    -- | Predicate name.
     --
-    -- Non-combinator predicates may derive this via 'Typeably'. Combinator
-    -- predicates must write a 'Show'-like instance manually, in order to avoid
-    -- incurring insidious 'Typeable' contexts for the wrapped predicate(s).
-    -- (TODO figure out some generics and/or TH to resolve that)
-    predicateName :: Proxy# p -> Int -> ShowS
+    -- 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.
+    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.
 
--- | Fill out predicate metadata using its 'Typeable' instance.
---
--- Do not use this for combinator predicates. Doing so will incur insidious
--- 'Typeable' contexts for the wrapped predicate(s).
-instance Typeable a => Predicate (Typeably a) where
-    predicateName _ d = showsPrec d (typeRep (Proxy @a))
+{- 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.
+-}
 
+-- | Reify predicate name.
+predicateName
+    :: forall p. (Predicate p, KnownSymbol (PredicateName 0 p)) => String
+predicateName = symbolVal' (proxy# @(PredicateName 0 p))
+
 -- | Refine @a@ with predicate @p@.
 class Predicate p => Refine p a where
     -- | Validate predicate @p@ for the given @a@.
     --
     -- 'Nothing' indicates success. 'Just' contains a validation failure.
-    validate :: Proxy# p -> a -> Maybe (RefineFailure String)
+    validate :: Proxy# p -> a -> Maybe RefineFailure
 
 -- | Refine functor type @f@ with functor predicate @p@.
 --
@@ -43,20 +53,20 @@
 -- structure, and not the stored elements.
 class Predicate p => Refine1 p f where
     -- | Validate predicate @p@ for the given @f a@.
-    validate1 :: Proxy# p -> f a -> Maybe (RefineFailure String)
+    validate1 :: Proxy# p -> f a -> Maybe RefineFailure
 
 -- | Predicate validation failure.
---
--- Polymorphic over the message type because I want to use 'Text', but want it
--- doesn't have the convenient 'Show' internals that 'String' does.
-data RefineFailure a = RefineFailure
-  { refineFailurePredicate :: a
-  -- ^ The predicate that failed.
+data RefineFailure = RefineFailure
+  { refineFailurePredicate :: TBL.Builder
+  -- ^ The name of the predicate that failed.
+  --
+  -- Obtained via 'predicateName'.
 
-  , refineFailureDetail    :: a
-  -- ^ Failure clarification.
+  , refineFailureDetail    :: TBL.Builder
+  -- ^ Precise failure detail e.g. which of the inner predicates of an @And@
+  --   combinator predicate failed.
 
-  , refineFailureInner     :: [RefineFailure a]
+  , refineFailureInner     :: [RefineFailure]
   -- ^ Any wrapped errors, for combinator predicates.
   --
   -- What these are, and their order, should be noted in 'refineFailureDetail'.
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
@@ -6,45 +6,38 @@
   (
   -- * Re-exports
     module Rerefined.Predicate
-  , Typeably(..), Typeable
   , proxy#
+  , TBL.Builder
+  , IsString -- TODO remove
 
   -- * Predicate validation
   , validateFail, validateBool
-
-  -- * Predicate name
-  , predicateName1, predicateName2
+  , KnownPredicateName
   ) where
 
 import Rerefined.Predicate
-import GHC.Exts ( Proxy#, proxy# )
-import Data.Typeable.Typeably
-import Data.Typeable ( Typeable )
+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
     :: forall p
-    .  Predicate p
-    => Proxy# p -> String -> [RefineFailure String]
-    -> Maybe (RefineFailure String)
-validateFail p msg es = Just $ RefineFailure (predicateName p 0 "") msg es
+    .  (Predicate p, KnownPredicateName p)
+    => Proxy# p -> TBL.Builder -> [RefineFailure]
+    -> Maybe RefineFailure
+validateFail _p msg es =
+    Just $ RefineFailure (fromString $ predicateName @p) msg es
 
 -- | Shortcut for simply validating a 'Bool'.
 validateBool
-    :: Predicate p => Proxy# p -> String -> Bool
-    -> Maybe (RefineFailure String)
+    :: forall p
+    .  (Predicate p, KnownPredicateName p)
+    => Proxy# p -> TBL.Builder -> Bool
+    -> Maybe RefineFailure
 validateBool p e = \case
   True  -> Nothing
   False -> validateFail p e []
-
-predicateName1 :: forall p. Predicate p => String -> Int -> ShowS
-predicateName1 pName d = showParen (d > 10) $
-      showString pName . showChar ' '
-    . predicateName (proxy# @p) 11
-
-predicateName2
-    :: forall l r. (Predicate l, Predicate r) => String -> Int -> ShowS
-predicateName2 pName d = showParen (d > 10) $
-      showString pName . showChar ' '
-    . predicateName (proxy# @l) 11 . showChar ' '
-    . predicateName (proxy# @r) 11
diff --git a/src/Rerefined/Predicate/Common/Binary.hs b/src/Rerefined/Predicate/Common/Binary.hs
new file mode 100644
--- /dev/null
+++ b/src/Rerefined/Predicate/Common/Binary.hs
@@ -0,0 +1,13 @@
+-- | Common utilities for binary combinator predicates.
+
+module Rerefined.Predicate.Common.Binary where
+
+import Rerefined.Predicate
+import TypeLevelShow.Utils
+import GHC.TypeNats
+
+-- | Render a binary combinator predicate with an infix operator.
+--
+-- The operator must include the left and right spaces.
+type PredicateNameBOp op prec d l r = ShowParen (d > prec)
+    (PredicateName (prec+1) l ++ op ++ PredicateName (prec+1) r)
diff --git a/src/Rerefined/Predicate/Fail.hs b/src/Rerefined/Predicate/Fail.hs
--- a/src/Rerefined/Predicate/Fail.hs
+++ b/src/Rerefined/Predicate/Fail.hs
@@ -1,9 +1,10 @@
+{-# LANGUAGE OverloadedStrings #-}
+
 module Rerefined.Predicate.Fail where
 
 import Rerefined.Predicate.Common
 
 -- | Always fails.
-data Fail deriving Predicate via Typeably Fail
-
-instance Refine Fail a where
-    validate p _ = validateFail p "fail" []
+data Fail
+instance Predicate Fail where type PredicateName d Fail = "⊥"
+instance Refine Fail a where validate p _ = validateFail p "fail" []
diff --git a/src/Rerefined/Predicate/Logical.hs b/src/Rerefined/Predicate/Logical.hs
--- a/src/Rerefined/Predicate/Logical.hs
+++ b/src/Rerefined/Predicate/Logical.hs
@@ -1,138 +1,41 @@
-{-# LANGUAGE AllowAmbiguousTypes #-}
-
-module Rerefined.Predicate.Logical where
-
-import Rerefined.Predicate.Common
-import Rerefined.Refined
-import Rerefined.Refine.Unsafe
-
--- | Logical binary operator.
---
--- No need to disambiguate that these are binary operators, because there's only
--- one logical unary operator 'Not'.
-data LogicOp = And | Or | Nand | Nor | Xor | Xnor
-
--- | A logical binary operation on two predicates.
-data Logical (op :: LogicOp) l r
-
--- TODO could do whatever we want here e.g. infix. (but idk what e.g. XNOR uses)
-instance (Predicate l, Predicate r, ReifyLogicOp op)
-  => Predicate (Logical op l r) where
-    predicateName _ d = showParen (d > 10) $
-          showString "Logical "
-        . showString (reifyLogicOpPretty @op) . showChar ' '
-        . predicateName (proxy# @l) 11 . showChar ' '
-        . predicateName (proxy# @r) 11
-
-instance (Refine l a, Refine r a, ReifyLogicOp op)
-  => Refine (Logical op l r) a where
-    validate p a =
-        reifyLogicOp @op (validateFail p)
-            (validate (proxy# @l) a)
-            (validate (proxy# @r) a)
-
--- | Reify a logical binary operator type tag.
-class ReifyLogicOp (op :: LogicOp) where
-    reifyLogicOpPretty :: String
-    reifyLogicOp
-        :: (String -> [a] -> Maybe a)
-        -> Maybe a
-        -> Maybe a
-        -> Maybe a
-
-instance ReifyLogicOp And where
-    reifyLogicOpPretty = "And"
-    reifyLogicOp fFail l r =
-        case l of
-          Nothing ->
-            case r of
-              Nothing -> Nothing
-              Just er -> fFail "AND:  right failed"    [    er]
-          Just el ->
-            case r of
-              Nothing -> fFail "AND:   left failed"    [el    ]
-              Just er -> fFail "AND:    l&r failed"    [el, er]
-
-instance ReifyLogicOp Or where
-    reifyLogicOpPretty = "Or"
-    reifyLogicOp fFail l r =
-        case l of
-          Nothing -> Nothing
-          Just el ->
-            case r of
-              Nothing -> Nothing
-              Just er -> fFail "OR:     l&r failed"    [el, er]
-
-instance ReifyLogicOp Nand where
-    reifyLogicOpPretty = "Nand"
-    reifyLogicOp fFail l r =
-        case l of
-          Just _  -> Nothing
-          Nothing ->
-            case r of
-              Just _  -> Nothing
-              Nothing -> fFail "NAND:   l&r succeeded" [      ]
-
-instance ReifyLogicOp Nor where
-    reifyLogicOpPretty = "Nor"
-    reifyLogicOp fFail l r =
-        case l of
-          Just el ->
-            case r of
-              Just _  -> Nothing
-              Nothing -> fFail "NOR:  right succeeded" [el    ]
-          Nothing ->
-            case r of
-              Just er -> fFail "NOR:   left succeeded" [    er]
-              Nothing -> fFail "NOR:    l&r succeeded" [      ]
-
-instance ReifyLogicOp Xor where
-    reifyLogicOpPretty = "Xor"
-    reifyLogicOp fFail l r =
-        case l of
-          Nothing ->
-            case r of
-              Just _  -> Nothing
-              Nothing -> fFail "XOR:    l&r succeeded" [      ]
-          Just el ->
-            case r of
-              Nothing -> Nothing
-              Just er -> fFail "XOR:    l&r failed"    [el, er]
+{-# LANGUAGE UndecidableInstances #-} -- TODO TMP
 
-instance ReifyLogicOp Xnor where
-    reifyLogicOpPretty = "Xnor"
-    reifyLogicOp fFail l r =
-        case l of
-          Nothing ->
-            case r of
-              Nothing -> Nothing
-              Just er -> fFail "XNOR: right failed"    [    er]
-          Just el ->
-            case r of
-              Just _  -> Nothing
-              Nothing -> fFail "XNOR:  left failed"    [el    ]
+module Rerefined.Predicate.Logical
+  ( And, Iff, If, Nand, Nor, Not, Or, Xor
+  , NormalizeLogicalStep
+  , NormalizeLogical1Step
+  , Result(..), Idk1'
+  ) where
 
-data Not p
+import Rerefined.Predicate.Logical.And
+import Rerefined.Predicate.Logical.Iff
+import Rerefined.Predicate.Logical.If
+import Rerefined.Predicate.Logical.Nand
+import Rerefined.Predicate.Logical.Nor
+import Rerefined.Predicate.Logical.Not
+import Rerefined.Predicate.Logical.Or
+import Rerefined.Predicate.Logical.Xor
 
-instance Predicate p => Predicate (Not p) where
-    predicateName _ = predicateName1 @p "Not"
+import Data.Kind ( Type )
+-- left = continue, right = normalized
+type NormalizeLogicalStep :: (kl -> kr -> Type) -> kl -> kr -> Result kl
+type family NormalizeLogicalStep op l r where
+    NormalizeLogicalStep Or   l l = Cont  l
+    NormalizeLogicalStep And  l l = Cont  l
+    NormalizeLogicalStep Nand l l = Cont1 (Not l)
+    NormalizeLogicalStep op   l r = Done (op l r)
 
-instance Refine p a => Refine (Not p) a where
-    validate p a =
-        case validate (proxy# @p) a of
-          Just _  -> Nothing
-          Nothing -> validateFail p "NOT: predicate succeeded" []
+data Result kl = Done Type | Cont kl | Cont1 Type
 
--- TODO principle of explosion? (p and not p -> anything)
+type NormalizeLogical1Step :: (k -> Type) -> k -> Result k
+type family NormalizeLogical1Step op p where
+    NormalizeLogical1Step Not (Not p) = Cont p
+    NormalizeLogical1Step op  p       = Done (op p)
 
--- TODO
-rerefineDeMorgans1
-    :: Refined (Not (Logical Or  l r))       a
-    -> Refined (Logical And (Not l) (Not r)) a
-rerefineDeMorgans1 = unsafeRerefine
+type family Idk1 res where
+    Idk1 (Cont p) = Idk1' p
+    Idk1 (Done p) = p
 
--- TODO
-rerefineDeMorgans2
-    :: Refined (Not (Logical And l r))       a
-    -> Refined (Logical Or  (Not l) (Not r)) a
-rerefineDeMorgans2 = unsafeRerefine
+type family Idk1' p where
+    Idk1' (Not p) = Idk1 (NormalizeLogical1Step Not p)
+    Idk1' p = p
diff --git a/src/Rerefined/Predicate/Logical/And.hs b/src/Rerefined/Predicate/Logical/And.hs
new file mode 100644
--- /dev/null
+++ b/src/Rerefined/Predicate/Logical/And.hs
@@ -0,0 +1,56 @@
+{-# LANGUAGE UndecidableInstances #-} -- for easier PredicateName
+{-# LANGUAGE OverloadedStrings #-} -- for builder
+
+module Rerefined.Predicate.Logical.And where
+
+import Rerefined.Predicate.Common.Binary
+import Rerefined.Predicate.Common
+import Rerefined.Refine.Unsafe
+import Rerefined.Refined
+
+-- | Logical conjunction. Also AND logic gate.
+data And l r
+
+-- | Precendence 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
+
+instance (Refine l a, Refine r a, KnownPredicateName (And l r))
+  => Refine (And l r) a where
+    validate p a =
+        case l of
+          Nothing ->
+            case r of
+              Nothing -> Nothing
+              Just er -> validateFail p "AND:  right failed"    [er    ]
+          Just el ->
+            case r of
+              Nothing -> validateFail p "AND:   left failed"    [    el]
+              Just er -> validateFail p "AND:    l&r failed"    [er, el]
+      where
+        l = validate (proxy# @l) a
+        r = validate (proxy# @r) a
+
+-- | Take just the left predicate from an 'And'.
+rerefineAndL :: Refined (And l r) a -> Refined l a
+rerefineAndL = unsafeRerefine
+
+-- | Take just the right predicate from an 'And'.
+rerefineAndR :: Refined (And l r) a -> Refined r a
+rerefineAndR = unsafeRerefine
+
+-- | Eliminate an 'And' by applying the left predicate, then the right.
+eliminateAndLR :: Refined (And l r) a -> Refined r (Refined l a)
+eliminateAndLR = unsafeRefine . unsafeRefine . unrefine
+
+-- | Eliminate an 'And' by applying the right predicate, then the left.
+eliminateAndRL :: Refined (And l r) a -> Refined l (Refined r a)
+eliminateAndRL = unsafeRefine . unsafeRefine . unrefine
+
+-- | Introduce an 'And' given a double-'Refined'. Inner is left.
+introduceAndLR :: Refined r (Refined l a) -> Refined (And l r) a
+introduceAndLR = unsafeRefine . unrefine . unrefine
+
+-- | Introduce an 'And' given a double-'Refined'. Inner is right.
+introduceAndRL :: Refined l (Refined r a) -> Refined (And l r) a
+introduceAndRL = unsafeRefine . unrefine . unrefine
diff --git a/src/Rerefined/Predicate/Logical/Equivalences.hs b/src/Rerefined/Predicate/Logical/Equivalences.hs
new file mode 100644
--- /dev/null
+++ b/src/Rerefined/Predicate/Logical/Equivalences.hs
@@ -0,0 +1,19 @@
+-- | Logical equivalences.
+
+module Rerefined.Predicate.Logical.Equivalences where
+
+{-
+
+-- TODO
+rerefineDeMorgans1
+    :: Refined (Not (Logical Or  l r))       a
+    -> Refined (Logical And (Not l) (Not r)) a
+rerefineDeMorgans1 = unsafeRerefine
+
+-- TODO
+rerefineDeMorgans2
+    :: Refined (Not (Logical And l r))       a
+    -> Refined (Logical Or  (Not l) (Not r)) a
+rerefineDeMorgans2 = unsafeRerefine
+
+-}
diff --git a/src/Rerefined/Predicate/Logical/If.hs b/src/Rerefined/Predicate/Logical/If.hs
new file mode 100644
--- /dev/null
+++ b/src/Rerefined/Predicate/Logical/If.hs
@@ -0,0 +1,29 @@
+{-# LANGUAGE UndecidableInstances #-} -- for easier PredicateName
+{-# LANGUAGE OverloadedStrings #-} -- for builder
+
+module Rerefined.Predicate.Logical.If where
+
+import Rerefined.Predicate.Common.Binary
+import Rerefined.Predicate.Common
+
+-- | Logical implication. "If l then r".
+data If l r
+
+-- | Precendence 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
+
+instance (Refine l a, Refine r a, KnownPredicateName (If l r))
+  => Refine (If l r) a where
+    validate p a =
+        case l of
+          Just _  -> Nothing
+          Nothing ->
+            case r of
+              Nothing -> Nothing
+              Just er ->
+                validateFail p "IF: left succeeded, but right failed" [er]
+      where
+        l = validate (proxy# @l) a
+        r = validate (proxy# @r) a
diff --git a/src/Rerefined/Predicate/Logical/Iff.hs b/src/Rerefined/Predicate/Logical/Iff.hs
new file mode 100644
--- /dev/null
+++ b/src/Rerefined/Predicate/Logical/Iff.hs
@@ -0,0 +1,33 @@
+{-# LANGUAGE UndecidableInstances #-} -- for easier PredicateName
+{-# LANGUAGE OverloadedStrings #-} -- for builder
+
+module Rerefined.Predicate.Logical.Iff where
+
+import Rerefined.Predicate.Common.Binary
+import Rerefined.Predicate.Common
+
+-- | Logical biconditional ("if and only if"). Also the XNOR logic gate, or
+--   equivalence (loosely).
+data Iff l r
+
+-- | Precendence of 4 (matching '==').
+instance (Predicate l, Predicate r) => Predicate (Iff l r) where
+    type PredicateName d (Iff l r) = PredicateNameBOp " ↔ " 4 d l r
+
+instance (Refine l a, Refine r a, KnownPredicateName (Iff l r))
+  => Refine (Iff l r) a where
+    validate p a =
+        case l of
+          Nothing ->
+            case r of
+              Nothing -> Nothing
+              Just er ->
+                validateFail p "IFF: left succeeded, but right failed" [er]
+          Just el ->
+            case r of
+              Just _  -> Nothing
+              Nothing ->
+                validateFail p "IFF: left failed, but right succeeded" [el]
+      where
+        l = validate (proxy# @l) a
+        r = validate (proxy# @r) a
diff --git a/src/Rerefined/Predicate/Logical/Nand.hs b/src/Rerefined/Predicate/Logical/Nand.hs
new file mode 100644
--- /dev/null
+++ b/src/Rerefined/Predicate/Logical/Nand.hs
@@ -0,0 +1,27 @@
+{-# LANGUAGE UndecidableInstances #-} -- for easier PredicateName
+{-# LANGUAGE OverloadedStrings #-} -- for builder
+
+module Rerefined.Predicate.Logical.Nand where
+
+import Rerefined.Predicate.Common.Binary
+import Rerefined.Predicate.Common
+
+-- | NAND logic gate. Also called the Sheffer stroke, or non-conjunction.
+data Nand l r
+
+-- | Precendence 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
+
+instance (Refine l a, Refine r a, KnownPredicateName (Nand l r))
+  => Refine (Nand l r) a where
+    validate p a =
+        case l of
+          Just _  -> Nothing
+          Nothing ->
+            case r of
+              Just _  -> Nothing
+              Nothing -> validateFail p "NAND: l&r succeeded" []
+      where
+        l = validate (proxy# @l) a
+        r = validate (proxy# @r) a
diff --git a/src/Rerefined/Predicate/Logical/Nor.hs b/src/Rerefined/Predicate/Logical/Nor.hs
new file mode 100644
--- /dev/null
+++ b/src/Rerefined/Predicate/Logical/Nor.hs
@@ -0,0 +1,30 @@
+{-# LANGUAGE UndecidableInstances #-} -- for easier PredicateName
+{-# LANGUAGE OverloadedStrings #-} -- for builder
+
+module Rerefined.Predicate.Logical.Nor where
+
+import Rerefined.Predicate.Common.Binary
+import Rerefined.Predicate.Common
+
+-- | NOR logic gate. Also called non-disjunction, or joint denial.
+data Nor l r
+
+-- | Precendence 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
+
+instance (Refine l a, Refine r a, KnownPredicateName (Nor l r))
+  => Refine (Nor l r) a where
+    validate p a =
+        case l of
+          Just _ ->
+            case r of
+              Just _  -> Nothing
+              Nothing -> validateFail p "NOR: left succeeded"  []
+          Nothing ->
+            case r of
+              Just _  -> validateFail p "NOR: right succeeded" []
+              Nothing -> validateFail p "NOR: l&r succeeded"   []
+      where
+        l = validate (proxy# @l) a
+        r = validate (proxy# @r) a
diff --git a/src/Rerefined/Predicate/Logical/Not.hs b/src/Rerefined/Predicate/Logical/Not.hs
new file mode 100644
--- /dev/null
+++ b/src/Rerefined/Predicate/Logical/Not.hs
@@ -0,0 +1,22 @@
+{-# LANGUAGE UndecidableInstances #-} -- for easier PredicateName
+{-# LANGUAGE OverloadedStrings #-} -- for builder
+
+module Rerefined.Predicate.Logical.Not where
+
+import Rerefined.Predicate.Common
+import TypeLevelShow.Utils
+
+-- | Logical negation. Also NOT logic gate, or logical complement.
+data Not p
+
+-- | Precendence of 9 (one below function application).
+instance Predicate p => Predicate (Not p) where
+    type PredicateName d (Not p) = ShowParen (d > 9)
+        ("¬ " ++ PredicateName 10 p)
+
+instance (Refine p a, KnownPredicateName (Not p))
+  => Refine (Not p) a where
+    validate p a =
+        case validate (proxy# @p) a of
+          Just _  -> Nothing
+          Nothing -> validateFail p "NOT: predicate succeeded" []
diff --git a/src/Rerefined/Predicate/Logical/Or.hs b/src/Rerefined/Predicate/Logical/Or.hs
new file mode 100644
--- /dev/null
+++ b/src/Rerefined/Predicate/Logical/Or.hs
@@ -0,0 +1,27 @@
+{-# LANGUAGE UndecidableInstances #-} -- for easier PredicateName
+{-# LANGUAGE OverloadedStrings #-} -- for builder
+
+module Rerefined.Predicate.Logical.Or where
+
+import Rerefined.Predicate.Common.Binary
+import Rerefined.Predicate.Common
+
+-- | Logical disjunction. Also OR logic gate.
+data Or l r
+
+-- | Precendence 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
+
+instance (Refine l a, Refine r a, KnownPredicateName (Or l r))
+  => Refine (Or l r) a where
+    validate p a =
+        case l of
+          Nothing -> Nothing
+          Just el ->
+            case r of
+              Nothing -> Nothing
+              Just er -> validateFail p "OR: l&r failed" [er, el]
+      where
+        l = validate (proxy# @l) a
+        r = validate (proxy# @r) a
diff --git a/src/Rerefined/Predicate/Logical/Xor.hs b/src/Rerefined/Predicate/Logical/Xor.hs
new file mode 100644
--- /dev/null
+++ b/src/Rerefined/Predicate/Logical/Xor.hs
@@ -0,0 +1,30 @@
+{-# LANGUAGE UndecidableInstances #-} -- for easier PredicateName
+{-# LANGUAGE OverloadedStrings #-} -- for builder
+
+module Rerefined.Predicate.Logical.Xor where
+
+import Rerefined.Predicate.Common.Binary
+import Rerefined.Predicate.Common
+
+-- | Logical exclusive disjunction. Also XOR logic gate.
+data Xor l r
+
+-- | Precendence of 4 (matching '==').
+instance (Predicate l, Predicate r) => Predicate (Xor l r) where
+    type PredicateName d (Xor l r) = PredicateNameBOp " ⊕ " 4 d l r
+
+instance (Refine l a, Refine r a, KnownPredicateName (Xor l r))
+  => Refine (Xor l r) a where
+    validate p a =
+        case l of
+          Nothing ->
+            case r of
+              Just _  -> Nothing
+              Nothing -> validateFail p "XOR: l&r succeeded" [      ]
+          Just el ->
+            case r of
+              Nothing -> Nothing
+              Just er -> validateFail p "XOR: l&r failed"    [er, el]
+      where
+        l = validate (proxy# @l) a
+        r = validate (proxy# @r) a
diff --git a/src/Rerefined/Predicate/Relational.hs b/src/Rerefined/Predicate/Relational.hs
--- a/src/Rerefined/Predicate/Relational.hs
+++ b/src/Rerefined/Predicate/Relational.hs
@@ -1,8 +1,8 @@
 module Rerefined.Predicate.Relational
   ( CompareValue
   , Sign(..)
-  , RelOp(..)
   , CompareLength
+  , LTE, GTE
   ) where
 
 import Rerefined.Predicate.Relational.Internal
diff --git a/src/Rerefined/Predicate/Relational/Internal.hs b/src/Rerefined/Predicate/Relational/Internal.hs
--- a/src/Rerefined/Predicate/Relational/Internal.hs
+++ b/src/Rerefined/Predicate/Relational/Internal.hs
@@ -1,75 +1,111 @@
-{-# LANGUAGE AllowAmbiguousTypes #-}
-{-# LANGUAGE UndecidableInstances #-} -- for weird TODO stuff
+{-# LANGUAGE AllowAmbiguousTypes #-}  -- for ReifyRelOp
+{-# LANGUAGE UndecidableInstances #-} -- for WidenRelOp
 
-module Rerefined.Predicate.Relational.Internal where
+{- | Relational operator definitions.
 
-import Data.Typeable ( Typeable )
+Haskell base exports the type 'Ordering', which is an enum that states the
+result of comparing two 'Ord's. We can utilize this to define /relational
+operators/:
 
+* 'LT', 'EQ' and 'GT' already map to relational operators.
+* The others can be defined by combining the above with 'Or'. e.g. @'LT' ``Or``
+  'EQ'@ -> "less than or equal" ('<=')
+
+What's the point? We save on definitions, and get to reuse well-known data types
+which most users will have intuition for. We do have to contest with
+commutativity, but this is an extremely minor concern which can only come up if
+you don't use the provided type synonyms, or do lots of type-level predicate
+manipulation. And we provide those swapped-order instances anyway!
+-}
+
+module Rerefined.Predicate.Relational.Internal where
+
+import Rerefined.Predicate.Logical.Or
 import GHC.TypeNats
 import Data.Type.Ord ( OrdCond )
+import GHC.TypeLits ( Symbol )
 
--- | Relational operator.
---
--- There are three possible outcomes from 'compare'ing two terms, defined in
--- 'Ordering'. However, we may instead compare terms using relational operators
--- such as @>=@, which are more specific comparisons that return a 'Bool'.
---
--- Constructor order is arbitrary due to @NEQ@, which obstructs ordering in a
--- meaningful way.
-data RelOp
-  = LT' -- ^ '<'  less than
-  | LTE -- ^ '<=' less than or equal to
-  | EQ' -- ^ '=='              equal to
-  | NEQ -- ^ '/=' less than or             greater than
-  | GTE -- ^ '>='              equal to or greater than
-  | GT' -- ^ '>'                           greater than
+import Data.Kind ( Type )
 
+type LTE = LT `Or` EQ
+
+-- | "not equal to" is equivalent to "strictly less than or greater than". We
+--   could use 'Rerefined.Predicate.Logical.Not.Not', but sticking with just
+--   'Or' keeps the internals simple.
+type NEQ = LT `Or` GT
+
+type GTE = GT `Or` EQ
+
 -- | Reify a relational operator type tag.
 --
--- We stuff the 'Typeable' constraint in here because we need it for easy
--- 'Rerefined.Predicate.Predicate' instances, and we don't want to expose the
--- 'Typeable' constraint elsewhere.
-class Typeable op => ReifyRelOp (op :: RelOp) where
-    -- | The term-level relational operator that @op@ describes.
-    reifyRelOp :: forall a. (Num a, Ord a) => a -> a -> Bool
+-- Permitted operators are @Ordering@ constructors 'LT', 'EQ' and 'GT'; and
+-- combinations of these using 'Or'.
+class ReifyRelOp op where
+    -- | Pretty @op@.
+    type ShowRelOp op :: Symbol
 
-    -- | Pretty operator.
-    reifyRelOpPretty :: String
+    -- | The term-level relational operator that @op@ describes.
+    reifyRelOp :: forall a. Ord a => a -> a -> Bool
 
-instance ReifyRelOp LT' where
+instance ReifyRelOp LT where
+    type ShowRelOp LT = "<"
     reifyRelOp = (<)
-    reifyRelOpPretty = "<"
 
 instance ReifyRelOp LTE where
+    type  ShowRelOp LTE = "<="
     reifyRelOp = (<=)
-    reifyRelOpPretty = "<="
 
-instance ReifyRelOp EQ' where
+-- | Hidden instance. You won't see this if you use the type synonyms.
+deriving via LTE instance ReifyRelOp (EQ `Or` LT)
+
+instance ReifyRelOp EQ where
+    type  ShowRelOp EQ = "=="
     reifyRelOp = (==)
-    reifyRelOpPretty = "=="
 
 instance ReifyRelOp NEQ where
+    type  ShowRelOp NEQ = "/="
     reifyRelOp = (/=)
-    reifyRelOpPretty = "/="
 
+-- | Hidden instance. You won't see this if you use the type synonyms.
+deriving via NEQ instance ReifyRelOp (GT `Or` LT)
+
 instance ReifyRelOp GTE where
+    type ShowRelOp GTE = ">="
     reifyRelOp = (>=)
-    reifyRelOpPretty = ">="
 
-instance ReifyRelOp GT' where
+-- | Hidden instance. You won't see this if you use the type synonyms.
+deriving via GTE instance ReifyRelOp (EQ `Or` GT)
+
+instance ReifyRelOp GT where
+    type ShowRelOp GT = ">"
     reifyRelOp = (>)
-    reifyRelOpPretty = ">"
 
--- | Can we widen the given 'RelOp' from @n@ to @m@?
-type family WidenRelOp (op :: RelOp) (n :: Natural) (m :: Natural) where
+-- | Can we widen the given 'RelOp' on the given 'Natural' from @n@ to @m@?
+type WidenRelOp :: k -> Natural -> Natural -> Bool
+type family WidenRelOp op n m where
     -- @n == m@? no problem
     WidenRelOp op  n n = True
 
     -- I'd love to simplify this, but 'CmpNat' is opaque.
-    WidenRelOp LT' n m = OrdCond (CmpNat n m) True  True False
+    WidenRelOp LT  n m = OrdCond (CmpNat n m) True  True False
     WidenRelOp LTE n m = OrdCond (CmpNat n m) True  True False
     WidenRelOp GTE n m = OrdCond (CmpNat n m) False True True
-    WidenRelOp GT' n m = OrdCond (CmpNat n m) False True True
+    WidenRelOp GT  n m = OrdCond (CmpNat n m) False True True
 
+    -- | swapped LTE, lower down in equation list because less common
+    WidenRelOp (EQ `Or` LT) n m =
+        OrdCond (CmpNat n m) True  True False
+
+    -- | swapped GTE, lower down in equation list because less common
+    WidenRelOp (EQ `Or` GT) n m =
+        OrdCond (CmpNat n m) False True True
+
     -- can't widen (==) or (/=)
     WidenRelOp _   _ _ = False
+
+-- this gets clumsier due to kinding clashes (k vs. Ordering)
+type NormalizeOrRelOp :: Type -> Type
+type family NormalizeOrRelOp op where
+    NormalizeOrRelOp (EQ `Or` LT) = LTE
+    NormalizeOrRelOp (GT `Or` LT) = NEQ
+    NormalizeOrRelOp (EQ `Or` GT) = GTE
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
@@ -1,3 +1,6 @@
+{-# LANGUAGE OverloadedStrings #-}
+{-# LANGUAGE UndecidableInstances #-} -- for GHC <= 9.4, WROE
+
 module Rerefined.Predicate.Relational.Length where
 
 import Rerefined.Predicate.Common
@@ -6,34 +9,45 @@
 import Data.MonoTraversable ( MonoFoldable(olength) )
 import GHC.Exts ( Proxy# )
 
-import Rerefined.Refined
-import Rerefined.Refine.Unsafe ( unsafeRerefine )
+import Rerefined.Refine.Unsafe
 import GHC.TypeError
 import Data.Kind ( type Constraint )
+import TypeLevelShow.Utils
+import TypeLevelShow.Natural
+import Data.Text.Builder.Linear qualified as TBL
 
 -- | Compare length to a type-level 'Natural' using the given 'RelOp'.
-data CompareLength (op :: RelOp) (n :: Natural)
-    deriving Predicate via Typeably (CompareLength op n)
+data CompareLength op (n :: Natural)
 
+-- | Precedence of 4 (matching base relational operators e.g. '>=').
+instance Predicate (CompareLength op n) where
+    type PredicateName d (CompareLength op n) = ShowParen (d > 4)
+        ("Length " ++ ShowRelOp op ++ ShowChar ' ' ++ ShowNatDec n)
+
 -- | Compare the length of a 'Foldable' to a type-level 'Natural' using the
 --   given 'RelOp'.
-instance (KnownNat n, Foldable f, ReifyRelOp op)
-  => Refine1 (CompareLength op n) f where
+instance
+  ( KnownNat n, Foldable f, ReifyRelOp op
+  , KnownPredicateName (CompareLength op n)
+  ) => Refine1 (CompareLength op n) f where
     validate1 p = validateCompareLength p . length
 
 -- | Compare the length of a 'MonoFoldable' to a type-level 'Natural' using the
 --   given 'RelOp'.
-instance (KnownNat n, MonoFoldable a, ReifyRelOp op)
-  => Refine (CompareLength op n) a where
+instance
+  ( KnownNat n, MonoFoldable a, ReifyRelOp op
+  , KnownPredicateName (CompareLength op n)
+  ) => Refine (CompareLength op n) a where
     validate p = validateCompareLength p . olength
 
 validateCompareLength
-    :: forall op n. (KnownNat n, ReifyRelOp op)
-    => Proxy# (CompareLength op n) -> Int -> Maybe (RefineFailure String)
+    :: forall op n
+    .  ( KnownNat n, ReifyRelOp op
+       , KnownPredicateName (CompareLength op n)
+    ) => Proxy# (CompareLength op n) -> Int -> Maybe RefineFailure
 validateCompareLength p len =
-    validateBool p ("length not "<>reifyRelOpPretty @op<>" "<>show n)
-        (reifyRelOp @op len (fromIntegral n))
-  where n = natVal' (proxy# @n)
+    validateBool p ("length: "<>TBL.fromDec n) (reifyRelOp @op len n)
+  where n = fromIntegral (natVal' (proxy# @n))
 
 -- | Widen a length comparison predicate.
 --
@@ -51,9 +65,25 @@
     -> Refined (CompareLength op m) a
 widenCompareLength = unsafeRerefine
 
+-- | Widen a length comparison predicate.
+--
+-- Only valid widenings are permitted, checked at compile time.
+--
+-- Example: Given a >= 1, we know also that a >= 0. Thus, this function allows
+-- you to turn a @Refined1 (CompareLength GTE 1) f a@ into a @Refined1
+-- (CompareLength GTE 0) f a@.
+--
+-- TODO improve type error here
+widenCompareLength1
+    :: forall m op n f a
+    .  WROE op n m
+    => Refined1 (CompareLength op n) f a
+    -> Refined1 (CompareLength op m) f a
+widenCompareLength1 = unsafeRerefine1
+
 type WROE op n m = WROE' op n m (WidenRelOp op n m)
-type WROE' :: RelOp -> Natural -> Natural -> Bool -> Constraint
-type family WROE' (op :: RelOp) (n :: Natural) (m :: Natural) (b :: Bool) where
+type WROE' :: k -> Natural -> Natural -> Bool -> Constraint
+type family WROE' op n m b where
     WROE' op n m True  = ()
     WROE' op n m False = TypeError
       (      Text "can't widen relational equation "
diff --git a/src/Rerefined/Predicate/Relational/Value.hs b/src/Rerefined/Predicate/Relational/Value.hs
--- a/src/Rerefined/Predicate/Relational/Value.hs
+++ b/src/Rerefined/Predicate/Relational/Value.hs
@@ -1,44 +1,42 @@
-{-# LANGUAGE AllowAmbiguousTypes #-}
+{-# LANGUAGE UndecidableInstances #-} -- for PredicateName
+{-# LANGUAGE OverloadedStrings #-}
+{-# LANGUAGE AllowAmbiguousTypes #-} -- for signPretty
 
 module Rerefined.Predicate.Relational.Value where
 
 import Rerefined.Predicate.Common
 import Rerefined.Predicate.Relational.Internal
 import GHC.TypeNats ( Natural, KnownNat, natVal' )
+import TypeLevelShow.Utils
+import TypeLevelShow.Natural
+import GHC.TypeLits ( Symbol )
 
 -- | Compare value to a type-level 'Natural' using the given 'RelOp'.
-data CompareValue (op :: RelOp) (sign :: Sign) (n :: Natural)
-    deriving Predicate via Typeably (CompareValue op sign n)
--- TODO I could write custom predicateNames here if I wanted to override how
--- they display. But I don't mind the expanded type synonyms. @CompareValue
--- 'CBOpLT 10@ still makes sense to me, especially with the extra message.
---
--- I should simplify op names, but not sure what to, since I can't use LT/EQ/GT.
-{-
-instance KnownNat n => Predicate (LessThan n) where
-    predicateName d = showParen (d > 10) $
-        showString "LessThan " . showsPrec 11 (natVal' (proxy# :: Proxy# n))
--}
+data CompareValue op (sign :: Sign) (n :: Natural)
 
---type LessThan n = CompareValue LT' n
+-- | Precedence of 4 (matching base relational operators e.g. '>=').
+instance Predicate (CompareValue op sign n) where
+    type PredicateName d (CompareValue op sign n) = ShowParen (d > 4)
+        (    "Value " ++ ShowRelOp op ++ ShowChar ' '
+          ++ ShowSign sign ++ ShowNatDec n )
 
 instance
   ( KnownNat n, Num a, Ord a
-  , ReifyRelOp op, ReifySignedNat sign n, ReifySign sign
+  , ReifyRelOp op, ReifySignedNat sign n
+  , KnownPredicateName (CompareValue op sign n)
   ) => Refine (CompareValue op sign n) a where
     -- note that we show the reified 'Natural' rather than the coerced numeric
     -- type, as otherwise we'd need a @'Show' a@
     validate p a =
         validateBool p
-            ("value not "<>reifyRelOpPretty @op<>" "<>signPretty @sign<>show n)
+            ("bad value")
             (reifyRelOp @op a (reifySignedNat @sign @n))
-      where n = natVal' (proxy# @n)
 
 data Sign = Pos | Neg
 
-class Typeable sign => ReifySign (sign :: Sign) where signPretty :: String
-instance ReifySign Pos where signPretty = ""
-instance ReifySign Neg where signPretty = "-"
+type family ShowSign (sign :: Sign) :: Symbol where
+    ShowSign Pos = ""
+    ShowSign Neg = "-"
 
 -- TODO do I add any KnownNat constraints anywhere here
 class ReifySignedNat (sign :: Sign) (n :: Natural) where
diff --git a/src/Rerefined/Predicate/Succeed.hs b/src/Rerefined/Predicate/Succeed.hs
--- a/src/Rerefined/Predicate/Succeed.hs
+++ b/src/Rerefined/Predicate/Succeed.hs
@@ -1,9 +1,10 @@
+{-# LANGUAGE OverloadedStrings #-}
+
 module Rerefined.Predicate.Succeed where
 
 import Rerefined.Predicate.Common
 
 -- | The unit predicate. Always succeeds.
-data Succeed deriving Predicate via Typeably Succeed
-
-instance Refine Succeed a where
-    validate _ _ = Nothing
+data Succeed
+instance Predicate Succeed where type PredicateName d Succeed = "⊤"
+instance Refine Succeed a where validate _ _ = Nothing
diff --git a/src/Rerefined/Predicates.hs b/src/Rerefined/Predicates.hs
--- a/src/Rerefined/Predicates.hs
+++ b/src/Rerefined/Predicates.hs
@@ -7,14 +7,13 @@
   , Fail
 
   -- * Logical
-  , Not
-  , Logical
+  , And, Iff, If, Nand, Nor, Not, Or, Xor
 
   -- * Relational
   , CompareValue
   , Sign(..)
-  , RelOp(..)
   , CompareLength
+  , LTE, GTE
   ) where
 
 import Rerefined.Predicate.Succeed
diff --git a/src/Rerefined/Predicates/RefinedShim.hs b/src/Rerefined/Predicates/RefinedShim.hs
deleted file mode 100644
--- a/src/Rerefined/Predicates/RefinedShim.hs
+++ /dev/null
@@ -1,3 +0,0 @@
-module Rerefined.Predicates.RefinedShim where
-
--- TODO cba
diff --git a/src/Rerefined/Refine.hs b/src/Rerefined/Refine.hs
--- a/src/Rerefined/Refine.hs
+++ b/src/Rerefined/Refine.hs
@@ -15,17 +15,19 @@
   -- * Errors
   , type RefineFailure
   , prettyRefineFailure
+  , prettyRefineFailure'
   ) where
 
 import Rerefined.Refined
-import Rerefined.Refined1
 import Rerefined.Predicate
-import GHC.Exts ( proxy#, IsString )
+import GHC.Exts ( proxy# )
+import Data.Text ( Text )
+import Data.Text.Builder.Linear qualified as TBL
 
 -- | Refine @a@ with predicate @p@.
 refine
     :: forall p a. Refine p a
-    => a -> Either (RefineFailure String) (Refined p a)
+    => a -> Either RefineFailure (Refined p a)
 refine a =
     case validate (proxy# @p) a of
       Nothing -> Right (Refined a)
@@ -37,23 +39,48 @@
 -- | Refine @f a@ with functor predicate @p@.
 refine1
     :: forall p f a. Refine1 p f
-    => f a -> Either (RefineFailure String) (Refined1 p f a)
+    => f a -> Either RefineFailure (Refined1 p f a)
 refine1 fa =
     case validate1 (proxy# @p) fa of
       Nothing -> Right (Refined1 fa)
       Just e  -> Left e
 
--- TODO needs work. boring & idk how to format nicely. and extra \n at start
-prettyRefineFailure :: (Semigroup a, IsString a) => RefineFailure a -> a
-prettyRefineFailure = go (0 :: Int) . (\e -> [e])
+{- TODO
+* got an extra \n at start oops
+* make it look better lol
+* make tail-call recursive? need to ferry more indents around though
+-}
+prettyRefineFailure :: RefineFailure -> Text
+prettyRefineFailure = TBL.runBuilder . go (0 :: Int) . (\e -> [e])
   where
     go n = \case
-      []     -> ""
+      []     -> mempty
       (e:es) ->
-           "\n" <> indent n     <> refineFailurePredicate e
-        <> "\n" <> indent (n+2) <> refineFailureDetail    e
-        <> go (n+2) (refineFailureInner e)
-        <> go n es
+        let bPred   = TBL.fromChar '\n' <> indent n <> refineFailurePredicate e
+            bDetail = TBL.fromChar '\n' <> indent (n+2) <> refineFailureDetail e
+         in bPred <> bDetail <> go (n+2) (refineFailureInner e) <> go n es
     indent = \case
-      0 -> ""
-      n -> " " <> indent (n-1)
+      0 -> mempty
+      n -> TBL.fromChar ' ' <> indent (n-1)
+
+-- TODO this requires switching inner errors so that last is first lol x)
+-- also we only <> right. maybe that's useful for perf
+-- to remove newline at start we need to start in a special mode so we know not
+-- to add the first newline at bPred. but I cba it will be messier and I want to
+-- replace this ASAP when someone comes up with a good pretty error format
+prettyRefineFailure' :: RefineFailure -> Text
+prettyRefineFailure' = \e -> TBL.runBuilder $ go mempty [(0 :: Int, e)]
+  where
+    go b = \case
+      []            -> b
+      ((n, e) : es) ->
+        let bPred   = TBL.fromChar '\n' <> indent n <> refineFailurePredicate e
+            bDetail = TBL.fromChar '\n' <> indent (n+2) <> refineFailureDetail e
+            b'      = b <> bPred <> bDetail
+         in go b' (idk (n+2) es (refineFailureInner e))
+    indent = \case
+      0 -> mempty
+      n -> TBL.fromChar ' ' <> indent (n-1)
+    idk n rs = \case
+      []   -> rs
+      l:ls -> idk n ((n, l):rs) ls
diff --git a/src/Rerefined/Refine/TH.hs b/src/Rerefined/Refine/TH.hs
--- a/src/Rerefined/Refine/TH.hs
+++ b/src/Rerefined/Refine/TH.hs
@@ -6,6 +6,7 @@
 import Rerefined.Refine
 import Rerefined.Predicate
 import Language.Haskell.TH.Syntax qualified as TH
+import Data.Text qualified as Text
 
 -- | Refine @a@ with predicate @p@ at compile time via Template Haskell.
 refineTH
@@ -25,5 +26,6 @@
 refine1TH = either refineTHFail TH.liftTyped . refine1 @p @f
 
 -- | Template Haskell refinement failure helper.
-refineTHFail :: forall a m. MonadFail m => RefineFailure String -> TH.Code m a
-refineTHFail = TH.liftCode . fail . prettyRefineFailure
+refineTHFail
+    :: forall a m. MonadFail m => RefineFailure -> TH.Code m a
+refineTHFail = TH.liftCode . fail . Text.unpack . prettyRefineFailure
diff --git a/src/Rerefined/Refine/Unsafe.hs b/src/Rerefined/Refine/Unsafe.hs
--- a/src/Rerefined/Refine/Unsafe.hs
+++ b/src/Rerefined/Refine/Unsafe.hs
@@ -23,7 +23,6 @@
   ) where
 
 import Rerefined.Refined
-import Rerefined.Refined1
 
 -- | Construct a 'Refined' without validating the predicate @p@.
 --
diff --git a/src/Rerefined/Refined.hs b/src/Rerefined/Refined.hs
--- a/src/Rerefined/Refined.hs
+++ b/src/Rerefined/Refined.hs
@@ -1,18 +1,48 @@
--- | 'Refined' definition.
+-- | 'Refined' and 'Refined1' definitions for refined values.
 --
--- Not intended for external use. For unsafe refines, use
+-- Not intended for external use. For unsafe refining, use
 -- 'Rerefined.Refine.Unsafe'.
 
-module Rerefined.Refined where
+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) -- TODO Show? useful but meh?
+    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
diff --git a/src/Rerefined/Refined1.hs b/src/Rerefined/Refined1.hs
deleted file mode 100644
--- a/src/Rerefined/Refined1.hs
+++ /dev/null
@@ -1,18 +0,0 @@
--- | 'Refined1' definition.
---
--- Not intended for external use. For unsafe refines, use
--- 'Rerefined.Refine.Unsafe'.
-
-module Rerefined.Refined1 where
-
-import Language.Haskell.TH.Syntax ( Lift )
-
--- | @f a@ refined with predicate @p@.
-newtype Refined1 p f a = Refined1 (f a)
-    deriving stock (Functor, Lift, Show) -- TODO Show? useful but meh?
-
--- | 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