diff --git a/CHANGELOG.md b/CHANGELOG.md
new file mode 100644
--- /dev/null
+++ b/CHANGELOG.md
@@ -0,0 +1,4 @@
+## 0.1.0 (2024-04-30)
+Initial release.
+
+* rewrite of Nikita Volkov's refined library
diff --git a/LICENSE b/LICENSE
new file mode 100644
--- /dev/null
+++ b/LICENSE
@@ -0,0 +1,20 @@
+Copyright (c) 2024 Ben Orchard (@raehik) <thefirstmuffinman@gmail.com>
+
+Permission is hereby granted, free of charge, to any person obtaining
+a copy of this software and associated documentation files (the
+"Software"), to deal in the Software without restriction, including
+without limitation the rights to use, copy, modify, merge, publish,
+distribute, sublicense, and/or sell copies of the Software, and to
+permit persons to whom the Software is furnished to do so, subject to
+the following conditions:
+
+The above copyright notice and this permission notice shall be included
+in all copies or substantial portions of the Software.
+
+THE SOFTWARE IS PROVIDED "AS IS", WITHOUT WARRANTY OF ANY KIND,
+EXPRESS OR IMPLIED, INCLUDING BUT NOT LIMITED TO THE WARRANTIES OF
+MERCHANTABILITY, FITNESS FOR A PARTICULAR PURPOSE AND NONINFRINGEMENT.
+IN NO EVENT SHALL THE AUTHORS OR COPYRIGHT HOLDERS BE LIABLE FOR ANY
+CLAIM, DAMAGES OR OTHER LIABILITY, WHETHER IN AN ACTION OF CONTRACT,
+TORT OR OTHERWISE, ARISING FROM, OUT OF OR IN CONNECTION WITH THE
+SOFTWARE OR THE USE OR OTHER DEALINGS IN THE SOFTWARE.
diff --git a/README.md b/README.md
new file mode 100644
--- /dev/null
+++ b/README.md
@@ -0,0 +1,92 @@
+# rerefined
+[refined-nv-gh]:      https://github.com/nikita-volkov/refined
+[refined-nv-hackage]: https://hackage.haskell.org/package/refined
+[strongweak-hackage]: https://hackage.haskell.org/package/strongweak
+[binrep-hackage]:     https://hackage.haskell.org/package/binrep
+[refined1-hackage]:   https://hackage.haskell.org/package/refined1
+
+Rewrite of Nikita Volkov's [refined][refined-nv-hackage] library.
+
+* same concept
+* same performance
+* more instances
+* better ergonomics (no insidious `Typeable` constraints)
+* internals: fewer dependencies (no `aeson`), better errors, more concise
+
+## Why?
+I used the original [refined][refined-nv-hackage] library fairly extensively to
+power other libraries (see [strongweak][strongweak-hackage],
+[binrep][binrep-hackage]), though I moved to a fork [refined1][refined1-hackage]
+some time ago to provide a feature I needed. I think the library has some flaws
+and I want to contribute, but my tiny tweaks are still pending after a few
+years. A good excuse to rewrite from the ground up.
+
+All source code is original.
+
+## Major changes from original refined
+### Simplified errors
+refined encoded the logical predicates in its error type. This doesn't enable
+any further analysis, just turns a non-sum type into a sum type and complicates
+consumption. Furthermore, this error type is first transformed into another
+recursive ADT, which is then pretty printed. This is unnecessary (even mentioned
+in the code).
+
+rerefined has a single-constructor error type which can be easily and
+efficiently turned into a `String` in a single pass.
+
+### No insidious `Typeable` contexts
+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!
+
+### Cleaner design
+What do `LessThan`, `GreaterThan`, `EqualTo` etc. have in common? They're all
+relational binary operators where one value is a pre-filled `Natural`. rerefined
+packs all of these into a single predicate that takes a type-level relational
+operator. Only one instance for the same amount of code, and much easier to
+reason about.
+
+We take this even further and allow passing a type-level sign, to enable
+comparing negative values.
+
+We take this _even_ further and use the same relational operator definitions to
+define length comparisons, where the other value is taken from the input's
+length (rather than its numeric value). This does not take a sign, since length
+must be non-negative.
+
+### More instances
+You know that length comparison predicate above? It has a _single instance_ for
+each of `Refined1` and `Refined`:
+
+```haskell
+-- | 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
+    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
+    validate p = validateCompareLength p . olength
+```
+
+We get a ton more instances for a ton less code. (Note that mono-foldable has a
+surprisingly small footprint, as most of its transitive dependencies are core
+libraries.)
+
+## License
+Provided under the MIT license. See `LICENSE` for license text.
diff --git a/rerefined.cabal b/rerefined.cabal
new file mode 100644
--- /dev/null
+++ b/rerefined.cabal
@@ -0,0 +1,66 @@
+cabal-version: 1.12
+
+-- This file has been generated from package.yaml by hpack version 0.35.2.
+--
+-- see: https://github.com/sol/hpack
+
+name:           rerefined
+version:        0.1.0
+synopsis:       Refinement types, again
+description:    Please see README.md.
+category:       Types, Data
+homepage:       https://github.com/raehik/rerefined#readme
+bug-reports:    https://github.com/raehik/rerefined/issues
+author:         Ben Orchard
+maintainer:     Ben Orchard <thefirstmuffinman@gmail.com>
+license:        MIT
+license-file:   LICENSE
+build-type:     Simple
+extra-source-files:
+    README.md
+    CHANGELOG.md
+
+source-repository head
+  type: git
+  location: https://github.com/raehik/rerefined
+
+library
+  exposed-modules:
+      Rerefined.Predicate
+      Rerefined.Predicate.Common
+      Rerefined.Predicate.Fail
+      Rerefined.Predicate.Logical
+      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:
+      src
+  default-extensions:
+      LambdaCase
+      NoStarIsType
+      DerivingVia
+      DeriveAnyClass
+      GADTs
+      RoleAnnotations
+      DefaultSignatures
+      TypeFamilies
+      DataKinds
+      MagicHash
+  ghc-options: -Wall -Wno-unticked-promoted-constructors
+  build-depends:
+      base >=4.16 && <5
+    , mono-traversable >=1.0.17.0 && <1.1
+    , template-haskell
+    , typeably >=0.1.0 && <0.2
+  default-language: GHC2021
diff --git a/src/Rerefined/Predicate.hs b/src/Rerefined/Predicate.hs
new file mode 100644
--- /dev/null
+++ b/src/Rerefined/Predicate.hs
@@ -0,0 +1,63 @@
+-- | Base definitions for refinement predicates.
+
+module Rerefined.Predicate
+  ( Refine(validate)
+  , Refine1(validate1)
+  , RefineFailure(..)
+  , Predicate(predicateName)
+  ) where
+
+import GHC.Exts ( Proxy# )
+import Data.Typeable ( Typeable, typeRep )
+import Data.Typeable.Typeably
+import Data.Proxy ( Proxy(Proxy) )
+
+-- | Types which define refinements on other types.
+class Predicate p where
+    -- | The predicate name, as a 'Show'-like (for good bracketing).
+    --
+    -- 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
+
+-- | 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))
+
+-- | 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)
+
+-- | Refine functor type @f@ with functor predicate @p@.
+--
+-- By not making the contained type accessible, we ensure refinements apply
+-- @forall a. f a@. That is, refinements here apply only to the functor
+-- 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)
+
+-- | 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.
+
+  , refineFailureDetail    :: a
+  -- ^ Failure clarification.
+
+  , refineFailureInner     :: [RefineFailure a]
+  -- ^ 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
new file mode 100644
--- /dev/null
+++ b/src/Rerefined/Predicate/Common.hs
@@ -0,0 +1,50 @@
+{-# LANGUAGE AllowAmbiguousTypes #-}
+
+-- | Handy utilities for defining predicates.
+
+module Rerefined.Predicate.Common
+  (
+  -- * Re-exports
+    module Rerefined.Predicate
+  , Typeably(..), Typeable
+  , proxy#
+
+  -- * Predicate validation
+  , validateFail, validateBool
+
+  -- * Predicate name
+  , predicateName1, predicateName2
+  ) where
+
+import Rerefined.Predicate
+import GHC.Exts ( Proxy#, proxy# )
+import Data.Typeable.Typeably
+import Data.Typeable ( Typeable )
+
+-- | 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
+
+-- | Shortcut for simply validating a 'Bool'.
+validateBool
+    :: Predicate p => Proxy# p -> String -> Bool
+    -> Maybe (RefineFailure String)
+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/Fail.hs b/src/Rerefined/Predicate/Fail.hs
new file mode 100644
--- /dev/null
+++ b/src/Rerefined/Predicate/Fail.hs
@@ -0,0 +1,9 @@
+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" []
diff --git a/src/Rerefined/Predicate/Logical.hs b/src/Rerefined/Predicate/Logical.hs
new file mode 100644
--- /dev/null
+++ b/src/Rerefined/Predicate/Logical.hs
@@ -0,0 +1,138 @@
+{-# 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]
+
+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    ]
+
+data Not p
+
+instance Predicate p => Predicate (Not p) where
+    predicateName _ = predicateName1 @p "Not"
+
+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" []
+
+-- TODO principle of explosion? (p and not p -> anything)
+
+-- 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/Relational.hs b/src/Rerefined/Predicate/Relational.hs
new file mode 100644
--- /dev/null
+++ b/src/Rerefined/Predicate/Relational.hs
@@ -0,0 +1,10 @@
+module Rerefined.Predicate.Relational
+  ( CompareValue
+  , Sign(..)
+  , RelOp(..)
+  , CompareLength
+  ) where
+
+import Rerefined.Predicate.Relational.Internal
+import Rerefined.Predicate.Relational.Value
+import Rerefined.Predicate.Relational.Length
diff --git a/src/Rerefined/Predicate/Relational/Internal.hs b/src/Rerefined/Predicate/Relational/Internal.hs
new file mode 100644
--- /dev/null
+++ b/src/Rerefined/Predicate/Relational/Internal.hs
@@ -0,0 +1,75 @@
+{-# LANGUAGE AllowAmbiguousTypes #-}
+{-# LANGUAGE UndecidableInstances #-} -- for weird TODO stuff
+
+module Rerefined.Predicate.Relational.Internal where
+
+import Data.Typeable ( Typeable )
+
+import GHC.TypeNats
+import Data.Type.Ord ( OrdCond )
+
+-- | 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
+
+-- | 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
+
+    -- | Pretty operator.
+    reifyRelOpPretty :: String
+
+instance ReifyRelOp LT' where
+    reifyRelOp = (<)
+    reifyRelOpPretty = "<"
+
+instance ReifyRelOp LTE where
+    reifyRelOp = (<=)
+    reifyRelOpPretty = "<="
+
+instance ReifyRelOp EQ' where
+    reifyRelOp = (==)
+    reifyRelOpPretty = "=="
+
+instance ReifyRelOp NEQ where
+    reifyRelOp = (/=)
+    reifyRelOpPretty = "/="
+
+instance ReifyRelOp GTE where
+    reifyRelOp = (>=)
+    reifyRelOpPretty = ">="
+
+instance ReifyRelOp GT' where
+    reifyRelOp = (>)
+    reifyRelOpPretty = ">"
+
+-- | Can we widen the given 'RelOp' from @n@ to @m@?
+type family WidenRelOp (op :: RelOp) (n :: Natural) (m :: Natural) 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 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
+
+    -- can't widen (==) or (/=)
+    WidenRelOp _   _ _ = False
diff --git a/src/Rerefined/Predicate/Relational/Length.hs b/src/Rerefined/Predicate/Relational/Length.hs
new file mode 100644
--- /dev/null
+++ b/src/Rerefined/Predicate/Relational/Length.hs
@@ -0,0 +1,63 @@
+module Rerefined.Predicate.Relational.Length where
+
+import Rerefined.Predicate.Common
+import Rerefined.Predicate.Relational.Internal
+import GHC.TypeNats ( Natural, KnownNat, natVal' )
+import Data.MonoTraversable ( MonoFoldable(olength) )
+import GHC.Exts ( Proxy# )
+
+import Rerefined.Refined
+import Rerefined.Refine.Unsafe ( unsafeRerefine )
+import GHC.TypeError
+import Data.Kind ( type Constraint )
+
+-- | Compare length to a type-level 'Natural' using the given 'RelOp'.
+data CompareLength (op :: RelOp) (n :: Natural)
+    deriving Predicate via Typeably (CompareLength op 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
+    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
+    validate p = validateCompareLength p . olength
+
+validateCompareLength
+    :: forall op n. (KnownNat n, ReifyRelOp op)
+    => Proxy# (CompareLength op n) -> Int -> Maybe (RefineFailure String)
+validateCompareLength p len =
+    validateBool p ("length not "<>reifyRelOpPretty @op<>" "<>show n)
+        (reifyRelOp @op len (fromIntegral n))
+  where n = natVal' (proxy# @n)
+
+-- | 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 @Refined (CompareLength GTE 1) a@ into a @Refined
+-- (CompareLength GTE 0) a@.
+--
+-- TODO improve type error here
+widenCompareLength
+    :: forall m op n a
+    .  WROE op n m
+    => Refined (CompareLength op n) a
+    -> Refined (CompareLength op m) a
+widenCompareLength = unsafeRerefine
+
+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
+    WROE' op n m True  = ()
+    WROE' op n m False = TypeError
+      (      Text "can't widen relational equation "
+        :$$: ShowType op :<>: Text " " :<>: ShowType n
+        :$$: Text "to"
+        :$$: ShowType op :<>: Text " " :<>: ShowType m
+      )
diff --git a/src/Rerefined/Predicate/Relational/Value.hs b/src/Rerefined/Predicate/Relational/Value.hs
new file mode 100644
--- /dev/null
+++ b/src/Rerefined/Predicate/Relational/Value.hs
@@ -0,0 +1,51 @@
+{-# LANGUAGE AllowAmbiguousTypes #-}
+
+module Rerefined.Predicate.Relational.Value where
+
+import Rerefined.Predicate.Common
+import Rerefined.Predicate.Relational.Internal
+import GHC.TypeNats ( Natural, KnownNat, natVal' )
+
+-- | 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))
+-}
+
+--type LessThan n = CompareValue LT' n
+
+instance
+  ( KnownNat n, Num a, Ord a
+  , ReifyRelOp op, ReifySignedNat sign n, ReifySign sign
+  ) => 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)
+            (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 = "-"
+
+-- TODO do I add any KnownNat constraints anywhere here
+class ReifySignedNat (sign :: Sign) (n :: Natural) where
+    reifySignedNat :: (Num a, KnownNat n) => a
+
+instance ReifySignedNat Pos n where
+    reifySignedNat = fromIntegral (natVal' (proxy# @n))
+
+instance ReifySignedNat Neg n where
+    reifySignedNat = negate (fromIntegral (natVal' (proxy# @n)))
diff --git a/src/Rerefined/Predicate/Succeed.hs b/src/Rerefined/Predicate/Succeed.hs
new file mode 100644
--- /dev/null
+++ b/src/Rerefined/Predicate/Succeed.hs
@@ -0,0 +1,9 @@
+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
diff --git a/src/Rerefined/Predicates.hs b/src/Rerefined/Predicates.hs
new file mode 100644
--- /dev/null
+++ b/src/Rerefined/Predicates.hs
@@ -0,0 +1,23 @@
+-- | Predicate re-exports, for when you're heavily using refinement types.
+
+module Rerefined.Predicates
+  (
+  -- * Base
+    Succeed
+  , Fail
+
+  -- * Logical
+  , Not
+  , Logical
+
+  -- * Relational
+  , CompareValue
+  , Sign(..)
+  , RelOp(..)
+  , CompareLength
+  ) where
+
+import Rerefined.Predicate.Succeed
+import Rerefined.Predicate.Fail
+import Rerefined.Predicate.Logical
+import Rerefined.Predicate.Relational
diff --git a/src/Rerefined/Predicates/RefinedShim.hs b/src/Rerefined/Predicates/RefinedShim.hs
new file mode 100644
--- /dev/null
+++ b/src/Rerefined/Predicates/RefinedShim.hs
@@ -0,0 +1,3 @@
+module Rerefined.Predicates.RefinedShim where
+
+-- TODO cba
diff --git a/src/Rerefined/Refine.hs b/src/Rerefined/Refine.hs
new file mode 100644
--- /dev/null
+++ b/src/Rerefined/Refine.hs
@@ -0,0 +1,44 @@
+{-# LANGUAGE OverloadedStrings, AllowAmbiguousTypes #-}
+
+module Rerefined.Refine where
+
+import Rerefined.Refined
+import Rerefined.Refined1
+import Rerefined.Predicate
+import GHC.Exts ( proxy#, IsString )
+
+-- | Refine @a@ with predicate @p@.
+refine
+    :: forall p a. Refine p a
+    => a -> Either (RefineFailure String) (Refined p a)
+refine a =
+    case validate (proxy# @p) a of
+      Nothing -> Right (Refined a)
+      Just e  -> Left e
+
+-- reifyPredicate is just a weaker version of validate without proxy.
+-- Maybe the latter is useful, though...?
+
+-- | Refine @f a@ with functor predicate @p@.
+refine1
+    :: forall p f a. Refine1 p f
+    => f a -> Either (RefineFailure String) (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])
+  where
+    go n = \case
+      []     -> ""
+      (e:es) ->
+           "\n" <> indent n     <> refineFailurePredicate e
+        <> "\n" <> indent (n+2) <> refineFailureDetail    e
+        <> go (n+2) (refineFailureInner e)
+        <> go n es
+    indent = \case
+      0 -> ""
+      n -> " " <> indent (n-1)
diff --git a/src/Rerefined/Refine/TH.hs b/src/Rerefined/Refine/TH.hs
new file mode 100644
--- /dev/null
+++ b/src/Rerefined/Refine/TH.hs
@@ -0,0 +1,31 @@
+module Rerefined.Refine.TH
+  ( refineTH
+  , refine1TH
+  ) where
+
+import Rerefined.Refine
+import Rerefined.Predicate
+import Rerefined.Refined
+import Rerefined.Refined1
+import Language.Haskell.TH.Syntax qualified as TH
+
+-- | Refine @a@ with predicate @p@ at compile time via Template Haskell.
+refineTH
+    :: forall p a m
+    .  (Refine p a, TH.Lift a, TH.Quote m, MonadFail m)
+    => a
+    -> TH.Code m (Refined p a)
+refineTH = either refineTHFail TH.liftTyped . refine @p @a
+
+-- | Refine @f a@ with functor predicate @p@ at compile time via Template
+--   Haskell.
+refine1TH
+    :: forall p f a m
+    .  (Refine1 p f, TH.Lift (f a), TH.Quote m, MonadFail m)
+    => f a
+    -> TH.Code m (Refined1 p f a)
+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
diff --git a/src/Rerefined/Refine/Unsafe.hs b/src/Rerefined/Refine/Unsafe.hs
new file mode 100644
--- /dev/null
+++ b/src/Rerefined/Refine/Unsafe.hs
@@ -0,0 +1,33 @@
+{- | 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 where
+
+import Rerefined.Refined
+import Rerefined.Refined1
+
+-- | 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
+
+-- | 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 '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
diff --git a/src/Rerefined/Refined.hs b/src/Rerefined/Refined.hs
new file mode 100644
--- /dev/null
+++ b/src/Rerefined/Refined.hs
@@ -0,0 +1,13 @@
+module Rerefined.Refined 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?
+
+-- | 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
diff --git a/src/Rerefined/Refined1.hs b/src/Rerefined/Refined1.hs
new file mode 100644
--- /dev/null
+++ b/src/Rerefined/Refined1.hs
@@ -0,0 +1,13 @@
+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 (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