diff --git a/changelog.md b/changelog.md
new file mode 100644
--- /dev/null
+++ b/changelog.md
@@ -0,0 +1,4 @@
+# trace-embrace changelog
+
+## Version 0.0.1 2025-06-01
+  * init
diff --git a/conduit-find/Data/Cond.hs b/conduit-find/Data/Cond.hs
new file mode 100644
--- /dev/null
+++ b/conduit-find/Data/Cond.hs
@@ -0,0 +1,569 @@
+{-# LANGUAGE TupleSections #-}
+{-# LANGUAGE FlexibleInstances #-}
+{-# LANGUAGE UndecidableInstances #-}
+{-# LANGUAGE RankNTypes #-}
+{-# LANGUAGE MultiParamTypeClasses #-}
+{-# LANGUAGE TypeFamilies #-}
+{-# LANGUAGE InstanceSigs #-}
+{-# LANGUAGE CPP #-}
+
+module Data.Cond
+    ( CondT(..), Cond
+
+    -- * Executing CondT
+    , runCondT, runCond, applyCondT, applyCond
+
+    -- * Promotions
+    , guardM, guard_, guardM_, apply, consider
+
+    -- * Boolean logic
+    , matches, if_, when_, unless_, or_, and_, not_
+
+    -- * Basic conditionals
+    , ignore, norecurse, prune
+
+    -- * Helper functions
+    , recurse, test
+
+    -- * Isomorphism with a stateful EitherT
+    , CondEitherT(..), fromCondT, toCondT
+    ) where
+
+import Control.Applicative (Alternative (..), optional)
+import Control.Arrow (first)
+import GHC.Stack
+import Control.Monad hiding (mapM_, sequence_)
+import Control.Monad.Base (MonadBase (..))
+import Control.Monad.Catch (MonadCatch (..), MonadMask (..), MonadThrow (..), ExitCase (..))
+import Control.Monad.Morph (MFunctor, hoist)
+import Control.Monad.Reader.Class (MonadReader (..), asks)
+import Control.Monad.State.Class (MonadState (..), gets)
+import Control.Monad.IO.Class (MonadIO (..))
+import Control.Monad.Trans (MonadTrans (..))
+import Control.Monad.Trans.Control (MonadBaseControl (..))
+import Control.Monad.Trans.Either (EitherT, left, runEitherT)
+import Control.Monad.Trans.State (StateT (..), withStateT, evalStateT)
+import Data.Foldable (asum)
+import Data.Functor.Identity (Identity (..))
+import Data.Maybe (fromMaybe, isJust)
+
+
+-- | 'Result' is an enriched 'Maybe' type which also specifies whether
+--   recursion should occur from the given input, and if so, how such
+--   recursion should be performed.
+data Result a m b = Ignore
+                  | Keep b
+                  | RecurseOnly (Maybe (CondT a m b))
+                  | KeepAndRecurse b (Maybe (CondT a m b))
+
+instance Show b => Show (Result a m b) where
+    show Ignore               = "Ignore"
+    show (Keep a)             = "Keep " ++ show a
+    show (RecurseOnly _)      = "RecurseOnly"
+    show (KeepAndRecurse a _) = "KeepAndRecurse " ++ show a
+
+instance Monad m => Functor (Result a m) where
+    fmap _ Ignore               = Ignore
+    fmap f (Keep a)             = Keep (f a)
+    fmap f (RecurseOnly l)      = RecurseOnly (liftM (fmap f) l)
+    fmap f (KeepAndRecurse a l) = KeepAndRecurse (f a) (liftM (fmap f) l)
+    {-# INLINE fmap #-}
+
+instance MFunctor (Result a) where
+    hoist _ Ignore                 = Ignore
+    hoist _ (Keep a)               = Keep a
+    hoist nat (RecurseOnly l)      = RecurseOnly (fmap (hoist nat) l)
+    hoist nat (KeepAndRecurse a l) = KeepAndRecurse a (fmap (hoist nat) l)
+    {-# INLINE hoist #-}
+
+instance Semigroup (Result a m b) where
+    Ignore        <> _                  = Ignore
+    _             <> Ignore             = Ignore
+    RecurseOnly _ <> Keep _             = Ignore
+    RecurseOnly _ <> KeepAndRecurse _ m = RecurseOnly m
+    RecurseOnly m <> _                  = RecurseOnly m
+    Keep _        <> RecurseOnly _      = Ignore
+    _             <> RecurseOnly m      = RecurseOnly m
+    _             <> Keep b             = Keep b
+    Keep _        <> KeepAndRecurse b _ = Keep b
+    _             <> KeepAndRecurse b m = KeepAndRecurse b m
+    {-# INLINE (<>) #-}
+
+instance Monoid b => Monoid (Result a m b) where
+    mempty  = KeepAndRecurse mempty Nothing
+    {-# INLINE mempty #-}
+    mappend = (<>)
+    {-# INLINE mappend #-}
+
+getResult :: Result a m b -> (Maybe b, Maybe (CondT a m b))
+getResult Ignore               = (Nothing, Nothing)
+getResult (Keep b)             = (Just b, Nothing)
+getResult (RecurseOnly c)      = (Nothing, c)
+getResult (KeepAndRecurse b c) = (Just b, c)
+
+setRecursion :: CondT a m b -> Result a m b -> Result a m b
+setRecursion _ Ignore               = Ignore
+setRecursion _ (Keep b)             = Keep b
+setRecursion c (RecurseOnly _)      = RecurseOnly (Just c)
+setRecursion c (KeepAndRecurse b _) = KeepAndRecurse b (Just c)
+
+accept' :: b -> Result a m b
+accept' = flip KeepAndRecurse Nothing
+
+recurse' :: Result a m b
+recurse' = RecurseOnly Nothing
+
+-- | Convert from a 'Maybe' value to its corresponding 'Result'.
+--
+-- >>> maybeToResult Nothing :: Result () Identity ()
+-- RecurseOnly
+-- >>> maybeToResult (Just ()) :: Result () Identity ()
+-- KeepAndRecurse ()
+maybeToResult :: Maybe a -> Result r m a
+maybeToResult Nothing  = recurse'
+maybeToResult (Just a) = accept' a
+
+maybeFromResult :: Result r m a -> Maybe a
+maybeFromResult Ignore               = Nothing
+maybeFromResult (Keep a)             = Just a
+maybeFromResult (RecurseOnly _)      = Nothing
+maybeFromResult (KeepAndRecurse a _) = Just a
+
+-- | 'CondT' is a kind of @StateT a (MaybeT m) b@, which uses a special
+--   'Result' type instead of 'Maybe' to express whether recursion should be
+--   performed from the item under consideration.  This is used to build
+--   predicates that can guide recursive traversals.
+--
+-- Several different types may be promoted to 'CondT':
+--
+--   [@Bool@]                  Using 'guard'
+--
+--   [@m Bool@]                Using 'guardM'
+--
+--   [@a -> Bool@]              Using 'guard_'
+--
+--   [@a -> m Bool@]            Using 'guardM_'
+--
+--   [@a -> m (Maybe b)@]       Using 'apply'
+--
+--   [@a -> m (Maybe (b, a))@]  Using 'consider'
+--
+-- Here is a trivial example:
+--
+-- @
+-- flip runCondT 42 $ do
+--   guard_ even
+--   liftIO $ putStrLn "42 must be even to reach here"
+--   guard_ odd \<|\> guard_ even
+--   guard_ (== 42)
+-- @
+--
+-- If 'CondT' is executed using 'runCondT', it return a @Maybe b@ if the
+-- predicate matched.  It can also be run with 'applyCondT', which does case
+-- analysis on the 'Result', specifying how recursion should be performed from
+-- the given 'a' value.
+newtype CondT a m b = CondT { getCondT :: StateT a m (Result a m b) }
+
+type Cond a = CondT a Identity
+
+instance Show (CondT a m b) where
+    show _ = "CondT"
+
+instance (Monad m, Semigroup b) => Semigroup (CondT a m b) where
+    (<>) = liftM2 (<>)
+    {-# INLINE (<>) #-}
+
+instance (Monad m, Monoid b) => Monoid (CondT a m b) where
+    mempty  = CondT $ return $ accept' mempty
+    {-# INLINE mempty #-}
+    -- mappend = liftM2 mappend
+    -- {-# INLINE mappend #-}
+
+instance Monad m => Functor (CondT a m) where
+#if __GLASGOW_HASKELL__ < 710
+    -- GHC 8.0.1 seems to go into some sort of optimiser loop with -O1 and above
+    -- if this is `liftM`, but for GHC 7.8 `Applicative` is not a super class
+    -- of `Monad` so we still need this.
+    -- See: https://ghc.haskell.org/trac/ghc/ticket/12425
+    fmap f (CondT g) = CondT (fmap (fmap f) g)
+#else
+    fmap f (CondT g) = CondT (fmap (fmap f) g)
+#endif
+    {-# INLINE fmap #-}
+
+instance Monad m => Applicative (CondT a m) where
+    pure  = CondT . pure . accept' -- pure
+    {-# INLINE pure #-}
+    (<*>) = ap
+    {-# INLINE (<*>) #-}
+
+instance MonadFail m => MonadFail (CondT a m) where
+    fail _ = mzero
+    {-# INLINE fail #-}
+
+instance Monad m => Monad (CondT a m) where
+    -- return = CondT . pure . accept'
+    -- {-# INLINE return #-}
+    CondT f >>= k = CondT $ do
+        r <- f
+        case r of
+            Ignore -> return Ignore
+            Keep b -> do
+                n <- getCondT (k b)
+                return $ case n of
+                    RecurseOnly _      -> Ignore
+                    KeepAndRecurse c _ -> Keep c
+                    _                  -> n
+            RecurseOnly l -> return $ RecurseOnly (fmap (>>= k) l)
+            KeepAndRecurse b _ -> getCondT (k b)
+
+instance Monad m => MonadReader a (CondT a m) where
+    ask               = CondT $ gets accept'
+    {-# INLINE ask #-}
+    local f (CondT m) = CondT $ withStateT f m
+    {-# INLINE local #-}
+    reader f          = liftM f ask
+    {-# INLINE reader #-}
+
+instance Monad m => MonadState a (CondT a m) where
+    get     = CondT $ gets accept'
+    {-# INLINE get #-}
+    put s   = CondT $ liftM accept' $ put s
+    {-# INLINE put #-}
+    state f = CondT $ state (fmap (first accept') f)
+    {-# INLINE state #-}
+
+instance Monad m => Alternative (CondT a m) where
+    empty = CondT $ return recurse'
+    {-# INLINE empty #-}
+    CondT f <|> CondT g = CondT $ do
+        r <- f
+        case r of
+            x@(Keep _) -> return x
+            x@(KeepAndRecurse _ _) -> return x
+            _ -> g
+    {-# INLINE (<|>) #-}
+
+instance Monad m => MonadPlus (CondT a m) where
+    mzero = empty
+    {-# INLINE mzero #-}
+    mplus = (<|>)
+    {-# INLINE mplus #-}
+
+instance MonadThrow m => MonadThrow (CondT a m) where
+    throwM = CondT . throwM
+    {-# INLINE throwM #-}
+
+instance MonadCatch m => MonadCatch (CondT a m) where
+    catch (CondT m) c = CondT $ m `catch` \e -> getCondT (c e)
+
+instance MonadMask m => MonadMask (CondT aa m) where
+    mask a = CondT $ mask $ \u -> getCondT (a $ q u)
+      where q u = CondT . u . getCondT
+    uninterruptibleMask a =
+        CondT $ uninterruptibleMask $ \u -> getCondT (a $ q u)
+      where q u = CondT . u . getCondT
+    generalBracket :: forall a b c. HasCallStack =>
+      CondT aa m a ->
+      (a -> ExitCase b -> CondT aa m c) ->
+      (a -> CondT aa m b) ->
+      CondT aa m (b, c)
+    generalBracket acquire release use = CondT go
+      where
+        arg1 :: StateT aa m (Result aa m a)
+        arg1 = getCondT acquire
+        arg2 :: (Result aa m a) -> ExitCase (Result aa m b) -> StateT aa m (Result aa m c)
+        arg2 a b = case a of
+          Ignore -> pure Ignore
+          Keep a' ->
+            case b of
+              ExitCaseSuccess b' ->
+                case b' of
+                  Ignore -> getCondT $ release a' ExitCaseAbort
+                  Keep b'' -> getCondT $ release a' (ExitCaseSuccess b'')
+                  RecurseOnly _mb -> getCondT $ release a' ExitCaseAbort -- set mb?
+                  KeepAndRecurse b'' _mb -> getCondT $ release a' (ExitCaseSuccess b'') -- set mb?
+              ExitCaseException se -> getCondT $ release a' (ExitCaseException se)
+              ExitCaseAbort -> getCondT $ release a' ExitCaseAbort
+          RecurseOnly _ma ->
+            pure Ignore
+          KeepAndRecurse a' _ma ->
+            case b of
+              ExitCaseSuccess b' ->
+                case b' of
+                  Ignore -> getCondT $ release a' ExitCaseAbort
+                  Keep b'' -> getCondT $ release a' (ExitCaseSuccess b'')
+                  RecurseOnly _mb -> getCondT $ release a' ExitCaseAbort -- set mb?
+                  KeepAndRecurse b'' _mb -> getCondT $ release a' (ExitCaseSuccess b'') -- set mb?
+              ExitCaseException se -> getCondT $ release a' (ExitCaseException se)
+              ExitCaseAbort -> getCondT $ release a' ExitCaseAbort
+
+        arg3 :: (Result aa m a) -> StateT aa m (Result aa m b)
+        arg3 a = getCondT (CondT (pure a) >>= use)
+        gb = generalBracket
+        go :: HasCallStack => StateT aa m (Result aa m (b, c))
+        go = do
+          gb arg1 arg2 arg3 >>= \case
+            -- anyway looks like a total nonsense - i give up
+            (Keep b, Keep c) -> pure $ Keep (b, c)
+            (RecurseOnly mb, RecurseOnly mc) -> pure $ RecurseOnly (liftA2 (,) <$> mb <*> mc)
+            (KeepAndRecurse b mb, KeepAndRecurse c mc) ->
+              pure $ KeepAndRecurse (b, c) (liftA2 (,) <$> mb <*> mc)
+            (Keep b, KeepAndRecurse c _) -> pure $ Keep (b, c)
+            (KeepAndRecurse b _, Keep c) -> pure $ Keep (b, c)
+            (KeepAndRecurse _ mb, RecurseOnly mc) -> pure $ RecurseOnly (liftA2 (,) <$> mb <*> mc)
+            (RecurseOnly mb, KeepAndRecurse _ mc) -> pure $ RecurseOnly (liftA2 (,) <$> mb <*> mc)
+            _ -> pure Ignore
+
+instance MonadBase b m => MonadBase b (CondT a m) where
+    liftBase m = CondT $ liftM accept' $ liftBase m
+    {-# INLINE liftBase #-}
+
+instance MonadIO m => MonadIO (CondT a m) where
+    liftIO m = CondT $ liftM accept' $ liftIO m
+    {-# INLINE liftIO #-}
+
+instance MonadTrans (CondT a) where
+    lift m = CondT $ liftM accept' $ lift m
+    {-# INLINE lift #-}
+
+instance MonadBaseControl b m => MonadBaseControl b (CondT r m) where
+    type StM (CondT r m) a = StM m (Result r m a, r)
+    liftBaseWith f = CondT $ StateT $ \s ->
+        liftM (\x -> (accept' x, s)) $ liftBaseWith $ \runInBase -> f $ \k ->
+            runInBase $ runStateT (getCondT k) s
+    restoreM = CondT . StateT . const . restoreM
+    {-# INLINE liftBaseWith #-}
+    {-# INLINE restoreM #-}
+
+instance MFunctor (CondT a) where
+    hoist nat (CondT m) = CondT $ hoist nat (liftM (hoist nat) m)
+    {-# INLINE hoist #-}
+
+runCondT :: Monad m => CondT a m b -> a -> m (Maybe b)
+runCondT (CondT f) a = maybeFromResult `liftM` evalStateT f a
+{-# INLINE runCondT #-}
+
+runCond :: Cond a b -> a -> Maybe b
+runCond = (runIdentity .) . runCondT
+{-# INLINE runCond #-}
+
+-- | Case analysis of applying a condition to an input value.  The result is a
+--   pair whose first part is a pair of Maybes specifying if the input matched
+--   and if recursion is expected from this value, and whose second part is
+--   the (possibly) mutated input value.
+applyCondT :: Monad m
+           => a
+           -> CondT a m b
+           -> m ((Maybe b, Maybe (CondT a m b)), a)
+applyCondT a cond = do
+    -- Apply a condition to the input value, determining the result and the
+    -- mutated value.
+    (r, a') <- runStateT (getCondT cond) a
+
+    -- Convert from the 'Result' to a pair of Maybes: one to specify if the
+    -- predicate succeeded, and the other to specify if recursion should be
+    -- performed.  If there is no sub-recursion specified, return 'cond'.
+    return (fmap (Just . fromMaybe cond) (getResult r), a')
+{-# INLINE applyCondT #-}
+
+-- | Case analysis of applying a pure condition to an input value.  The result
+--   is a pair whose first part is a pair of Maybes specifying if the input
+--   matched and if recursion is expected from this value, and whose second
+--   part is the (possibly) mutated input value.
+applyCond :: a -> Cond a b -> ((Maybe b, Maybe (Cond a b)), a)
+applyCond a cond = first (fmap (Just . fromMaybe cond) . getResult)
+                       (runIdentity (runStateT (getCondT cond) a))
+{-# INLINE applyCond #-}
+
+guardM :: Monad m => m Bool -> CondT a m ()
+guardM m = lift m >>= guard
+{-# INLINE guardM #-}
+
+guard_ :: Monad m => (a -> Bool) -> CondT a m ()
+guard_ f = asks f >>= guard
+{-# INLINE guard_ #-}
+
+guardM_ :: Monad m => (a -> m Bool) -> CondT a m ()
+guardM_ f = ask >>= lift . f >>= guard
+{-# INLINE guardM_ #-}
+
+apply :: Monad m => (a -> m (Maybe b)) -> CondT a m b
+apply f = CondT $ get >>= liftM maybeToResult . lift . f
+{-# INLINE apply #-}
+
+consider :: Monad m => (a -> m (Maybe (b, a))) -> CondT a m b
+consider f = CondT $ do
+    mres <- lift . f =<< get
+    case mres of
+        Nothing      -> return Ignore
+        Just (b, a') -> put a' >> return (accept' b)
+{-# INLINE consider #-}
+
+-- | Return True or False depending on whether the given condition matches or
+--   not.  This differs from simply stating the condition in that it itself
+--   always succeeds.
+--
+-- >>> flip runCond "foo.hs" $ matches (guard =<< asks (== "foo.hs"))
+-- Just True
+-- >>> flip runCond "foo.hs" $ matches (guard =<< asks (== "foo.hi"))
+-- Just False
+matches :: Monad m => CondT a m b -> CondT a m Bool
+matches = fmap isJust . optional
+{-# INLINE matches #-}
+
+-- | A variant of ifM which branches on whether the condition succeeds or not.
+--   Note that @if_ x@ is equivalent to @ifM (matches x)@, and is provided
+--   solely for convenience.
+--
+-- >>> let good = guard_ (== "foo.hs") :: Cond String ()
+-- >>> let bad  = guard_ (== "foo.hi") :: Cond String ()
+-- >>> flip runCond "foo.hs" $ if_ good (return "Success") (return "Failure")
+-- Just "Success"
+-- >>> flip runCond "foo.hs" $ if_ bad (return "Success") (return "Failure")
+-- Just "Failure"
+if_ :: Monad m => CondT a m r -> CondT a m b -> CondT a m b -> CondT a m b
+if_ c x y =
+    CondT $ getCondT . maybe y (const x) . maybeFromResult =<< getCondT c
+{-# INLINE if_ #-}
+
+-- | 'when_' is just like 'when', except that it executes the body if the
+--   condition passes, rather than based on a Bool value.
+--
+-- >>> let good = guard_ (== "foo.hs") :: Cond String ()
+-- >>> let bad  = guard_ (== "foo.hi") :: Cond String ()
+-- >>> flip runCond "foo.hs" $ when_ good ignore
+-- Nothing
+-- >>> flip runCond "foo.hs" $ when_ bad ignore
+-- Just ()
+when_ :: Monad m => CondT a m r -> CondT a m () -> CondT a m ()
+when_ c x = if_ c (void x) (return ())
+{-# INLINE when_ #-}
+
+-- | 'when_' is just like 'when', except that it executes the body if the
+--   condition fails, rather than based on a Bool value.
+--
+-- >>> let good = guard_ (== "foo.hs") :: Cond String ()
+-- >>> let bad  = guard_ (== "foo.hi") :: Cond String ()
+-- >>> flip runCond "foo.hs" $ unless_ bad ignore
+-- Nothing
+-- >>> flip runCond "foo.hs" $ unless_ good ignore
+-- Just ()
+unless_ :: Monad m => CondT a m r -> CondT a m () -> CondT a m ()
+unless_ c = if_ c (return ()) . void
+{-# INLINE unless_ #-}
+
+-- | Check whether at least one of the given conditions is true.  This is a
+--   synonym for 'Data.Foldable.asum'.
+--
+-- >>> let good = guard_ (== "foo.hs") :: Cond String ()
+-- >>> let bad  = guard_ (== "foo.hi") :: Cond String ()
+-- >>> flip runCond "foo.hs" $ or_ [bad, good]
+-- Just ()
+-- >>> flip runCond "foo.hs" $ or_ [bad]
+-- Nothing
+or_ :: Monad m => [CondT a m b] -> CondT a m b
+or_ = asum
+{-# INLINE or_ #-}
+
+-- | Check that all of the given conditions are true.  This is a synonym for
+--   'Data.Foldable.sequence_'.
+--
+-- >>> let good = guard_ (== "foo.hs") :: Cond String ()
+-- >>> let bad  = guard_ (== "foo.hi") :: Cond String ()
+-- >>> flip runCond "foo.hs" $ and_ [bad, good]
+-- Nothing
+-- >>> flip runCond "foo.hs" $ and_ [good]
+-- Just ()
+and_ :: Monad m => [CondT a m b] -> CondT a m ()
+and_ = sequence_
+{-# INLINE and_ #-}
+
+-- | 'not_' inverts the meaning of the given predicate.
+--
+-- >>> let good = guard_ (== "foo.hs") :: Cond String ()
+-- >>> let bad  = guard_ (== "foo.hi") :: Cond String ()
+-- >>> flip runCond "foo.hs" $ not_ bad >> return "Success"
+-- Just "Success"
+-- >>> flip runCond "foo.hs" $ not_ good >> return "Shouldn't reach here"
+-- Nothing
+not_ :: Monad m => CondT a m b -> CondT a m ()
+not_ c = when_ c ignore
+{-# INLINE not_ #-}
+
+-- | 'ignore' ignores the current entry, but allows recursion into its
+--   descendents.  This is the same as 'mzero'.
+ignore :: Monad m => CondT a m b
+ignore = mzero
+{-# INLINE ignore #-}
+
+-- | 'norecurse' prevents recursion into the current entry's descendents, but
+--   does not ignore the entry itself.
+norecurse :: Monad m => CondT a m ()
+norecurse = CondT $ return $ Keep ()
+{-# INLINE norecurse #-}
+
+-- | 'prune' is a synonym for both ignoring an entry and its descendents. It
+--   is the same as @ignore >> norecurse@.
+prune :: Monad m => CondT a m b
+prune = CondT $ return Ignore
+{-# INLINE prune #-}
+
+-- | 'recurse' changes the recursion predicate for any child elements.  For
+--   example, the following file-finding predicate looks for all @*.hs@ files,
+--   but under any @.git@ directory looks only for a file named @config@:
+--
+-- @
+-- if_ (name_ \".git\" \>\> directory)
+--     (ignore \>\> recurse (name_ \"config\"))
+--     (glob \"*.hs\")
+-- @
+--
+-- NOTE: If this code had used @recurse (glob \"*.hs\"))@ instead in the else
+-- case, it would have meant that @.git@ is only looked for at the top-level
+-- of the search (i.e., the top-most element).
+recurse :: Monad m => CondT a m b -> CondT a m b
+recurse c = CondT $ setRecursion c `liftM` getCondT c
+{-# INLINE recurse #-}
+
+-- | A specialized variant of 'runCondT' that simply returns True or False.
+--
+-- >>> let good = guard_ (== "foo.hs") :: Cond String ()
+-- >>> let bad  = guard_ (== "foo.hi") :: Cond String ()
+-- >>> runIdentity $ test "foo.hs" $ not_ bad >> return "Success"
+-- True
+-- >>> runIdentity $ test "foo.hs" $ not_ good >> return "Shouldn't reach here"
+-- False
+test :: Monad m => a -> CondT a m b -> m Bool
+test = (liftM isJust .) . flip runCondT
+{-# INLINE test #-}
+
+-- | This type is for documentation only, and shows the isomorphism between
+--   'CondT' and 'CondEitherT'.  The reason for using 'Result' is that it
+--   makes meaning of the constructors more explicit.
+newtype CondEitherT a m b = CondEitherT
+    (StateT a (EitherT (Maybe (Maybe (CondEitherT a m b))) m)
+         (b, Maybe (Maybe (CondEitherT a m b))))
+
+-- | Witness one half of the isomorphism from 'CondT' to 'CondEitherT'.
+fromCondT :: Monad m => CondT a m b -> CondEitherT a m b
+fromCondT (CondT f) = CondEitherT $ do
+    s <- get
+    (r, s') <- lift $ lift $ runStateT f s
+    case r of
+        Ignore             -> lift $ left Nothing
+        Keep a             -> put s' >> return (a, Nothing)
+        RecurseOnly m      -> lift $ left (Just (fmap fromCondT m))
+        KeepAndRecurse a m -> put s' >> return (a, Just (fmap fromCondT m))
+
+-- | Witness the other half of the isomorphism from 'CondEitherT' to 'CondT'.
+toCondT :: Monad m => CondEitherT a m b -> CondT a m b
+toCondT (CondEitherT f) = CondT $ do
+    s <- get
+    eres <- lift $ runEitherT $ runStateT f s
+    case eres of
+        Left Nothing             -> return Ignore
+        Right ((a, Nothing), s') -> put s' >> return (Keep a)
+        Left (Just m)            -> return $ RecurseOnly (fmap toCondT m)
+        Right ((a, Just m), s')  ->
+            put s' >> return (KeepAndRecurse a (fmap toCondT m))
diff --git a/conduit-find/Data/Conduit/Find.hs b/conduit-find/Data/Conduit/Find.hs
new file mode 100644
--- /dev/null
+++ b/conduit-find/Data/Conduit/Find.hs
@@ -0,0 +1,618 @@
+{-# LANGUAGE BangPatterns #-}
+{-# LANGUAGE CPP #-}
+{-# LANGUAGE FlexibleContexts #-}
+{-# LANGUAGE OverloadedStrings #-}
+{-# LANGUAGE RankNTypes #-}
+{-# LANGUAGE TupleSections #-}
+{-# LANGUAGE ScopedTypeVariables #-}
+
+module Data.Conduit.Find
+    (
+    -- * Introduction
+    -- $intro
+
+    -- ** Basic comparison with GNU find
+    -- $gnufind
+
+    -- ** Performance
+    -- $performance
+
+    -- ** Other notes
+    -- $notes
+
+    -- * Finding functions
+      sourceFindFiles
+    , find
+    , findFiles
+    , findFilePaths
+    , FindOptions(..)
+    , defaultFindOptions
+    , test
+    , ltest
+    , stat
+    , lstat
+    , hasStatus
+
+      -- * File path predicates
+    , glob
+    , regex
+    , ignoreVcs
+
+      -- * GNU find compatibility predicates
+    , depth_
+    , follow_
+    , noleaf_
+    , prune_
+    , maxdepth_
+    , mindepth_
+    , ignoreErrors_
+    , noIgnoreErrors_
+    , amin_
+    , atime_
+    , anewer_
+    , empty_
+    , executable_
+    , gid_
+    , name_
+    , getDepth
+    , filename_
+    , pathname_
+    , getFilePath
+
+    -- * File entry predicates (uses stat information)
+    , regular
+    , directory
+    , hasMode
+    , executable
+    , lastAccessed_
+    , lastModified_
+
+    -- * Predicate combinators
+    , module Cond
+    , (=~)
+
+    -- * Types and type classes
+    , FileEntry(..)
+    ) where
+
+import           Control.Applicative (Alternative (..))
+import           Control.Exception (IOException, catch, throwIO)
+import           Control.Monad hiding (forM_, forM)
+import           Control.Monad.Catch (MonadThrow)
+import           Control.Monad.IO.Class (MonadIO, liftIO)
+import           Control.Monad.IO.Unlift (MonadUnliftIO)
+import           Control.Monad.Morph (hoist, lift)
+import           Control.Monad.State.Class (get, gets, modify, put)
+import           Control.Monad.Trans.Control (MonadBaseControl)
+import           Control.Monad.Trans.Resource (MonadResource)
+
+import           Data.Attoparsec.Text as A
+import           Data.Bits ((.&.))
+import           Data.Conduit (ConduitT, runConduitRes, (.|))
+import qualified Data.Conduit as DC
+import qualified Data.Conduit.List as DCL
+import qualified Data.Cond as Cond
+import           Data.Cond hiding (test)
+import qualified Data.Conduit.Filesystem as CF
+#if LEAFOPT
+import           Data.IORef (IORef, newIORef, modifyIORef, readIORef)
+#endif
+import           Data.Maybe (fromMaybe)
+import           Data.Text (Text, unpack, pack)
+import           Data.Time (UTCTime,  diffUTCTime)
+import           Data.Time.Clock.POSIX (getCurrentTime, posixSecondsToUTCTime)
+import qualified System.FilePath as FP
+import           System.PosixCompat.Files (FileStatus, linkCount)
+import qualified System.PosixCompat.Files as Files
+import           System.PosixCompat.Types (EpochTime, FileMode)
+import           Text.Regex.Posix ((=~))
+
+{- $intro
+
+**find-conduit** is essentially a souped version of GNU find for Haskell,
+using a DSL to provide both ease of us, and extensive flexbility.
+
+In its simplest form, let's compare some uses of find to find-conduit.  Bear
+in mind that the result of the find function is a conduit, so you're expected
+to either sink it to a list, or operate on the file paths as they are yielded.
+-}
+
+{- $gnufind
+
+A typical find command:
+
+@
+find src -name '*.hs' -type f -print
+@
+
+Would in find-conduit be:
+
+@
+find "src" (glob \"*.hs\" \<\> regular) $$ mapM_C (liftIO . print)
+@
+
+The 'glob' predicate matches the file basename against the globbing pattern,
+while the 'regular' predicate matches plain files.
+
+A more complicated example:
+
+@
+find . -size +100M -perm 644 -mtime 1
+@
+
+Now in find-conduit:
+
+@
+let megs = 1024 * 1024
+    days = 86400
+now <- liftIO getCurrentTime
+find \".\" ( fileSize (> 100*megs)
+        \<\> hasMode 0o644
+        \<\> lastModified (> addUTCTime now (-(1*days)))
+         )
+@
+
+Appending predicates like this expressing an "and" relationship.  Use '<|>' to
+express "or".  You can also negate any predicate:
+
+@
+find \".\" (not_ (hasMode 0o644))
+@
+
+By default, predicates, whether matching or not, will allow recursion into
+directories.  In order to express that matching predicate should disallow
+recursion, use 'prune':
+
+@
+find \".\" (prune (depth (> 2)))
+@
+
+This is the same as using '-maxdepth 2' in find.
+
+@
+find \".\" (prune (filename_ (== \"dist\")))
+@
+
+This is the same as:
+
+@
+find . \\( -name dist -prune \\) -o -print
+@
+-}
+
+{- $performance
+
+find-conduit strives to make file-finding a well performing operation.  To
+this end, a composed Predicate will only call stat once per entry being
+considered; and if you prune a directory, it is not traversed at all.
+
+By default, 'find' calls stat for every file before it applies the predicate,
+in order to ensure that only one such call is needed.  Sometimes, however, you
+know just from the FilePath that you don't want to consider a certain file, or
+you want to prune a directory tree.
+
+To support these types of optimized queries, a variant of find is provided
+called 'findWithPreFilter'.  This takes two predicates: one that is applied to
+only the FilePath, before stat (or lstat) is called; and one that is applied
+to the full file information after the stat.
+-}
+
+{- $notes
+
+See 'Data.Cond' for more details on the Monad used to build predicates.
+-}
+
+data FindOptions = FindOptions
+    { findFollowSymlinks   :: !Bool
+    , findContentsFirst    :: !Bool
+    , findIgnoreErrors     :: !Bool
+    , findIgnoreResults    :: !Bool
+    , findLeafOptimization :: !Bool
+    }
+
+defaultFindOptions :: FindOptions
+defaultFindOptions = FindOptions
+    { findFollowSymlinks   = True
+    , findContentsFirst    = False
+    , findIgnoreErrors     = False
+    , findIgnoreResults    = False
+    , findLeafOptimization = True
+    }
+
+data FileEntry = FileEntry
+    { entryPath        :: !FP.FilePath
+    , entryDepth       :: !Int
+    , entryFindOptions :: !FindOptions
+    , entryStatus      :: !(Maybe FileStatus)
+      -- ^ This is Nothing until we determine stat should be called.
+    }
+
+newFileEntry :: FP.FilePath -> Int -> FindOptions -> FileEntry
+newFileEntry fp d f = FileEntry fp d f Nothing
+
+instance Show FileEntry where
+    show entry = "FileEntry "
+              ++ show (entryPath entry)
+              ++ " " ++ show (entryDepth entry)
+
+getFilePath :: Monad m => CondT FileEntry m FP.FilePath
+getFilePath = gets entryPath
+
+pathname_ :: Monad m => (FP.FilePath -> Bool) -> CondT FileEntry m ()
+pathname_ f = guard . f =<< getFilePath
+
+filename_ :: Monad m => (FP.FilePath -> Bool) -> CondT FileEntry m ()
+filename_ f = pathname_ (f . FP.takeFileName)
+
+getDepth :: Monad m => CondT FileEntry m Int
+getDepth = gets entryDepth
+
+modifyFindOptions :: Monad m
+                  => (FindOptions -> FindOptions)
+                  -> CondT FileEntry m ()
+modifyFindOptions f =
+    modify $ \e -> e { entryFindOptions = f (entryFindOptions e) }
+
+------------------------------------------------------------------------
+-- Workalike options for emulating GNU find.
+------------------------------------------------------------------------
+
+depth_ :: Monad m => CondT FileEntry m ()
+depth_ = modifyFindOptions $ \opts -> opts { findContentsFirst = True }
+
+follow_ :: Monad m => CondT FileEntry m ()
+follow_ = modifyFindOptions $ \opts -> opts { findFollowSymlinks = True }
+
+noleaf_ :: Monad m => CondT FileEntry m ()
+noleaf_ = modifyFindOptions $ \opts -> opts { findLeafOptimization = False }
+
+prune_ :: Monad m => CondT a m ()
+prune_ = prune
+
+ignoreErrors_ :: Monad m => CondT FileEntry m ()
+ignoreErrors_ =
+    modifyFindOptions $ \opts -> opts { findIgnoreErrors = True }
+
+noIgnoreErrors_ :: Monad m => CondT FileEntry m ()
+noIgnoreErrors_ =
+    modifyFindOptions $ \opts -> opts { findIgnoreErrors = False }
+
+maxdepth_ :: Monad m => Int -> CondT FileEntry m ()
+maxdepth_ l = getDepth >>= guard . (<= l)
+
+mindepth_ :: Monad m => Int -> CondT FileEntry m ()
+mindepth_ l = getDepth >>= guard . (>= l)
+
+-- xdev_ = error "NYI"
+
+timeComp :: MonadIO m
+         => ((UTCTime -> Bool) -> CondT FileEntry m ()) -> Int
+         -> CondT FileEntry m ()
+timeComp f n = do
+    now <- liftIO getCurrentTime
+    f (\t -> diffUTCTime now t > fromIntegral n)
+
+amin_ :: MonadIO m => Int -> CondT FileEntry m ()
+amin_ n = timeComp lastAccessed_ (n * 60)
+
+atime_ :: MonadIO m => Int -> CondT FileEntry m ()
+atime_ n = timeComp lastAccessed_ (n * 24 * 3600)
+
+anewer_ :: MonadIO m => FP.FilePath -> CondT FileEntry m ()
+anewer_ path = do
+    e  <- get
+    es <- applyStat Nothing
+    ms <- getStat Nothing e { entryPath   = path
+                            , entryStatus = Nothing
+                            }
+    case ms of
+        Nothing     -> prune >> error "This is never reached"
+        Just (s, _) -> guard $ diffUTCTime (f s) (f es) > 0
+  where
+    f = posixSecondsToUTCTime . realToFrac . Files.accessTime
+
+-- cmin_ = error "NYI"
+-- cnewer_ = error "NYI"
+-- ctime_ = error "NYI"
+
+empty_ :: MonadIO m => CondT FileEntry m ()
+empty_ = (regular   >> hasStatus ((== 0) . Files.fileSize))
+     <|> (directory >> hasStatus ((== 2) . linkCount))
+
+executable_ :: MonadIO m => CondT FileEntry m ()
+executable_ = executable
+
+gid_ :: MonadIO m => Int -> CondT FileEntry m ()
+gid_ n = hasStatus ((== n) . fromIntegral . Files.fileGroup)
+
+{-
+group_ name
+ilname_ pat
+iname_ pat
+inum_ n
+ipath_ pat
+iregex_ pat
+iwholename_ pat
+links_ n
+lname_ pat
+mmin_
+mtime_
+-}
+
+name_ :: Monad m => FP.FilePath -> CondT FileEntry m ()
+name_ = filename_ . (==)
+
+{-
+newer_ path
+newerXY_ ref
+nogroup_
+nouser_
+path_ pat
+perm_ mode :: Perm
+readable_
+regex_ pat
+samefile_ path
+size_ n :: Size
+type_ c
+uid_ n
+used_ n
+user_ name
+wholename_ pat
+writable_
+xtype_ c
+-}
+
+------------------------------------------------------------------------
+
+statFilePath :: Bool -> Bool -> FP.FilePath -> IO (Maybe FileStatus)
+statFilePath follow ignoreErrors path = do
+    let doStat = (if follow
+                  then Files.getFileStatus
+                  else Files.getSymbolicLinkStatus) path
+    catch (Just <$> doStat) $ \e ->
+        if ignoreErrors
+        then return Nothing
+        else throwIO (e :: IOException)
+
+-- | Get the current status for the file.  If the status being requested is
+--   already cached in the entry information, simply return it from there.
+getStat :: MonadIO m
+        => Maybe Bool
+        -> FileEntry
+        -> m (Maybe (FileStatus, FileEntry))
+getStat mfollow entry = case entryStatus entry of
+    Just s
+        | maybe True (== follow entry) mfollow ->
+            return $ Just (s, entry)
+        | otherwise -> fmap (, entry) `liftM` wrapStat
+    Nothing -> do
+        ms <- wrapStat
+        return $ case ms of
+            Just s  -> Just (s, entry { entryStatus = Just s })
+            Nothing -> Nothing
+  where
+    follow   = findFollowSymlinks . entryFindOptions
+    wrapStat = liftIO $ statFilePath
+        (fromMaybe (findFollowSymlinks opts) mfollow)
+        (findIgnoreErrors opts)
+        (entryPath entry)
+      where
+        opts = entryFindOptions entry
+
+applyStat :: MonadIO m => Maybe Bool -> CondT FileEntry m FileStatus
+applyStat mfollow = do
+    ms <- lift . getStat mfollow =<< get
+    case ms of
+        Nothing      -> prune >> error "This is never reached"
+        Just (s, e') -> s <$ put e'
+
+lstat :: MonadIO m => CondT FileEntry m FileStatus
+lstat = applyStat (Just False)
+
+stat :: MonadIO m => CondT FileEntry m FileStatus
+stat = applyStat (Just True)
+
+hasStatus :: MonadIO m => (FileStatus -> Bool) -> CondT FileEntry m ()
+hasStatus f = guard . f =<< applyStat Nothing
+
+regular :: MonadIO m => CondT FileEntry m ()
+regular = hasStatus Files.isRegularFile
+
+executable :: MonadIO m => CondT FileEntry m ()
+executable = hasMode Files.ownerExecuteMode
+
+directory :: MonadIO m => CondT FileEntry m ()
+directory = hasStatus Files.isDirectory
+
+hasMode :: MonadIO m => FileMode -> CondT FileEntry m ()
+hasMode m = hasStatus (\s -> Files.fileMode s .&. m /= 0)
+
+withStatusTime :: MonadIO m
+               => (FileStatus -> EpochTime) -> (UTCTime -> Bool)
+               -> CondT FileEntry m ()
+withStatusTime g f = hasStatus (f . posixSecondsToUTCTime . realToFrac . g)
+
+lastAccessed_ :: MonadIO m => (UTCTime -> Bool) -> CondT FileEntry m ()
+lastAccessed_ = withStatusTime Files.accessTime
+
+lastModified_ :: MonadIO m => (UTCTime -> Bool) -> CondT FileEntry m ()
+lastModified_ = withStatusTime Files.modificationTime
+
+regex :: Monad m => String -> CondT FileEntry m ()
+regex pat = filename_ (=~ pat)
+
+-- | Return all entries, except for those within version-control metadata
+--   directories (and not including the version control directory itself either).
+ignoreVcs :: Monad m => CondT FileEntry m ()
+ignoreVcs = when_ (filename_ (`elem` vcsDirs)) prune
+  where
+    vcsDirs = [ ".git", "CVS", "RCS", "SCCS", ".svn", ".hg", "_darcs" ]
+
+-- | Find every entry whose filename part matching the given filename globbing
+--   expression.  For example: @glob "*.hs"@.
+glob :: Monad m => String -> CondT FileEntry m ()
+glob g = case parseOnly globParser (pack g) of
+    Left e  -> error $ "Failed to parse glob: " ++ e
+    Right x -> regex ("^" <> unpack x <> "$")
+  where
+    globParser :: Parser Text
+    globParser = fmap mconcat $ many $
+            char '*' *> return ".*"
+        <|> char '?' *> return "."
+        <|> string "[]]" *> return "[]]"
+        <|> (\x y z -> pack ((x:y) ++ [z]))
+                <$> char '['
+                <*> manyTill anyChar (A.try (char ']'))
+                <*> char ']'
+        <|> do
+            x <- anyChar
+            return . pack $ if x `elem` (".()^$" :: String)
+                            then ['\\', x]
+                            else [x]
+
+#if LEAFOPT
+type DirCounter = IORef Word
+
+newDirCounter :: MonadIO m => m DirCounter
+newDirCounter = liftIO $ newIORef 1
+#else
+type DirCounter = ()
+
+newDirCounter :: MonadIO m => m DirCounter
+newDirCounter = return ()
+#endif
+
+-- | Find file entries in a directory tree, recursively, applying the given
+--   recursion predicate to the search.  This conduit yields pairs of type
+--   @(FileEntry, a)@, where is the return value from the predicate at each
+--   step.
+sourceFindFiles :: MonadResource m
+                => FindOptions
+                -> FilePath
+                -> CondT FileEntry m a
+                -> ConduitT i (FileEntry, a) m ()
+sourceFindFiles findOptions startPath predicate = do
+    startDc <- newDirCounter
+    walk startDc
+        (newFileEntry startPath 0 findOptions)
+        startPath
+        predicate
+  where
+    walk :: MonadResource m
+         => DirCounter
+         -> FileEntry
+         -> FP.FilePath
+         -> CondT FileEntry m a
+         -> ConduitT i (FileEntry, a) m ()
+    walk !dc !entry !path !cond = do
+        ((!mres, !mcond), !entry') <- lift $ applyCondT entry cond
+        let opts' = entryFindOptions entry
+            this  = unless (findIgnoreResults opts') $
+                        yieldEntry entry' mres
+            next  = walkChildren dc entry' path mcond
+        if findContentsFirst opts'
+            then next >> this
+            else this >> next
+      where
+        yieldEntry _      Nothing    = return ()
+        yieldEntry entry' (Just res) = DC.yield (entry', res)
+
+    walkChildren :: MonadResource m
+                 => DirCounter
+                 -> FileEntry
+                 -> FP.FilePath
+                 -> Maybe (CondT FileEntry m a)
+                 -> ConduitT i (FileEntry, a) m ()
+    walkChildren _ _ _ Nothing = return ()
+    -- If the conditional matched, we are requested to recurse if this is a
+    -- directory
+    walkChildren !dc !entry !path (Just !cond) = do
+        st <- lift $ checkIfDirectory dc entry path
+        when (fmap Files.isDirectory st == Just True) $ do
+#if LEAFOPT
+            -- Update directory count for the parent directory.
+            liftIO $ modifyIORef dc pred
+            -- Track the directory count for this child path.
+            let leafOpt = findLeafOptimization (entryFindOptions entry)
+            let lc = linkCount (fromJust st) - 2
+                opts' = (entryFindOptions entry)
+                    { findLeafOptimization = leafOpt && lc >= 0
+                    }
+            dc' <- liftIO $ newIORef (fromIntegral lc :: Word)
+#else
+            let dc'   = dc
+                opts' = entryFindOptions entry
+#endif
+            CF.sourceDirectory path .| DC.awaitForever (go dc' opts')
+      where
+        go dc' opts' fp =
+            let entry' = newFileEntry fp (succ (entryDepth entry)) opts'
+            in walk dc' entry' fp cond
+
+    -- Return True if the given entry is a directory.  We can sometimes use
+    -- "leaf optimization" on Linux to answer this question without performing
+    -- a stat call.  This is possible because the link count of a directory is
+    -- two more than the number of sub-directories it contains, so we've seen
+    -- that many sub-directories, the remaining entries must be files.
+    checkIfDirectory :: MonadResource m
+                     => DirCounter
+                     -> FileEntry
+                     -> FP.FilePath
+                     -> m (Maybe FileStatus)
+    checkIfDirectory !dc !entry !path = do
+#if LEAFOPT
+        let leafOpt = findLeafOptimization (entryFindOptions entry)
+        doStat <- if leafOpt
+                  then (> 0) <$> liftIO (readIORef dc)
+                  else return True
+#else
+        let doStat = dc == () -- to quiet hlint warnings
+#endif
+        let opts = entryFindOptions entry
+        if doStat
+            then liftIO $ statFilePath
+                (findFollowSymlinks opts)
+                (findIgnoreErrors opts)
+                path
+            else return Nothing
+
+findFiles :: (MonadIO m, MonadBaseControl IO m, MonadThrow m, MonadUnliftIO m)
+          => FindOptions
+          -> FilePath
+          -> CondT FileEntry m a
+          -> m ()
+findFiles opts path predicate =
+    runConduitRes $
+        sourceFindFiles opts { findIgnoreResults = True } path
+            (hoist lift predicate) .| DCL.sinkNull
+
+-- | A simpler version of 'findFiles', which yields only 'FilePath' values,
+--   and ignores any values returned by the predicate action.
+findFilePaths :: (MonadIO m, MonadResource m)
+              => FindOptions
+              -> FilePath
+              -> CondT FileEntry m a
+              -> ConduitT i FilePath m ()
+findFilePaths opts path predicate =
+    sourceFindFiles opts path predicate .| DCL.map (entryPath . fst)
+
+-- | Calls 'findFilePaths' with the default set of finding options.
+--   Equivalent to @findFilePaths defaultFindOptions@.
+find :: MonadResource m
+     => FilePath -> CondT FileEntry m a -> DC.ConduitT i FilePath m ()
+find = findFilePaths defaultFindOptions
+
+-- | Test a file path using the same type of predicate that is accepted by
+--   'findFiles'.
+test :: MonadIO m => CondT FileEntry m () -> FilePath -> m Bool
+test matcher path =
+    Cond.test (newFileEntry path 0 defaultFindOptions) matcher
+
+-- | Test a file path using the same type of predicate that is accepted by
+--   'findFiles', but do not follow symlinks.
+ltest :: MonadIO m => CondT FileEntry m () -> FilePath -> m Bool
+ltest matcher path =
+    Cond.test
+        (newFileEntry path 0 defaultFindOptions
+            { findFollowSymlinks = False })
+        matcher
diff --git a/quick-process.cabal b/quick-process.cabal
new file mode 100644
--- /dev/null
+++ b/quick-process.cabal
@@ -0,0 +1,417 @@
+cabal-version: 3.0
+name:          quick-process
+version:       0.0.1
+synopsis:      Run external processes verified at compilation/installation
+description:
+    The library checks program name during compilation, generates exec spec
+    to be verified in tests, before installation or before launch.
+    
+    == Motivation
+    #motivation#
+    
+    The strongest trait of Haskell language is its type system. This
+    powerful type system gives infinite opportunities for experimenting with
+    mapping relational entities onto application values in safer, more
+    comprehensible and maintainable ways.
+    
+    Compare popularity of Java and Haskell languagues and number of SOL
+    libraries in them:
+    
+    > > length $ words "Hasql Beam Reigh8 postgresql-typed persistent esqueleto Opaleye Rel8 Squeal Selda Groundhog"
+    > 11
+    > > length $ words "JPA Hibernate JOOQ EJB"
+    > 4
+    
+    Haskell ecosystem counts 2.75 times more SQL libraries nonetheless
+    according to <https://www.tiobe.com/tiobe-index/ TIOBE index> in 2025
+    Java is 20 times more popular than Haskell and by
+    <https://pypl.github.io/PYPL.html PYPL> 126 times!
+    
+    As far as I remember only <https://www.jooq.org/ JOOQ> resembles a type
+    safe library. Other libraries require runtime environment to check
+    compatibility of codebase with SQL queries.
+    
+    RDBMSs talk SQL and it are inherently text oriented for extenal clients.
+    All these Haskell libraries first of all are trying to hide plain string
+    manipulation behind type fence as deep as possible.
+    
+    Once I tried had to launch an external process in a Haskell program.
+    Keeping in mind the 50-200x slope on SQL arena in Haskell, I expected to
+    find at least a few libraries on <https://hackage.haskell.org/ hackage>
+    providing some type safety layer between my application and execv
+    syscall interface accepting a bare strings.
+    
+    The observation above motivated me experimenting with a type safe
+    wrapper for <https://hackage.haskell.org/package/process process>
+    library.
+    
+    Structure of command line arguments is way simpler than SQL. An external
+    program can be modelled as a function with a side effect. Haskell has an
+    amazing library for testing functions -
+    <hackage.haskell.org/package/QuickCheck QuickCheck> including impure
+    ones.
+    
+    Main concern of external programs - they are not shipped with the
+    application. Recall
+    <https://en.wikipedia.org/wiki/Dependency_hell PRM hell> phrase. These
+    days situation with external explicit dependency resolution during
+    software installation and upgrade improved by nix and bazel. Nix and
+    bazel are powerful, because they can pack\/isolate\/unpack the whole
+    dependency universe of a single app, but they are complicated systems
+    with a steep learning curve. Plus nix is not supported on Windows.
+    That’s why they’ve got limited popularity and lot of software is still
+    distributed as a self-extracting archive assuming some dependencies are
+    compatible and preinstalled manually.
+    
+    Explicit list of dependencies is manually currated.
+    
+    Language does not provide out of the box solution to build such list.
+    Taking into account human factor explicit list of dependencies always
+    has a chance to diverge from the full (effective) one. E.g. host system
+    got newer version of dependency which behaves differently.
+    
+    Software installation out of prebuilt executables usually don’t run
+    tests.
+    
+    == Goals
+    #goals#
+    
+    quick-process defines following goals:
+    
+    -   provide DSL for describing a call spec of an external program
+    -   generate types, from the call spec, compatible with application
+        domain and arguments of an external program
+    -   automatic discovery of call specs in code base
+    -   check call spec compatibility during app development, testing and
+        installation
+    -   process launch and mapping call spec to CreadeProcess
+    
+    == Call spec verification
+    #call-spec-verification#
+    
+    Often call spec can be verified with @--help@ key terminating command
+    line arguments. It’s way easier than running the program in sandbox,
+    because no files gerenration is required and validating after effects
+    either. Help key validation support can be checked.
+    
+    == Examples
+    #examples#
+    
+    === Constant argument
+    #constant-argument#
+    
+    > {-# LANGUAGE TemplateHaskell #-}
+    > module CallSpecs where
+    > import System.Process.Quick
+    >
+    > $(genCallSpec [TrailingHelpValidate, SandboxValidate] "date" (ConstArg "+%Y" .*. HNil))
+    
+    > {-# LANGUAGE TemplateHaskell #-}
+    > module CallSpecTest where
+    >
+    > import CallSpecs
+    > import System.Process.Quick
+    >
+    > main :: IO ()
+    > main = $(discoverAndVerifyCallSpecs
+    >           (fromList [ TrailingHelpValidate
+    >                     , SandboxValidate
+    >                     ])
+    >           3)
+    
+    > {-# LANGUAGE TemplateHaskell #-}
+    > module Main where
+    >
+    > import CallSpecs
+    > import System.Process.Quick
+    >
+    > main :: IO ()
+    > main = callProcess Date
+    
+    @genCallSpec@ defines type @Date@ with nullary constructor and
+    @CallSpec@ instance for it.
+    
+    @discoverAndVerifyCallSpecs@ discovers all types with @CallSpec@
+    instances, generates 3 values per type ande executes help key check.
+    There is not much to check besides exit code in Date spec.
+    
+    @callProcess@ is similar to
+    <https://hackage.haskell.org/package/process/docs/System-Process.html#v:callProcess callProcess>
+    from process library, but accepts typed input instead of strings.
+    
+    === Variable argument
+    #variable-argument#
+    
+    > {-# LANGUAGE TemplateHaskell #-}
+    > module CallSpecs where
+    > import System.Process.Quick
+    >
+    > $(genCallSpec
+    >   [TrailingHelpValidate, SandboxValidate]
+    >   "/bin/cp"
+    >   (   VarArg @(Refined (InFile "hs") FilePath) "source"
+    >   .*. VarArg @(Refined (OutFile "*") FilePath) "destination"
+    >   .*. HNil
+    >   )
+    >  )
+    
+    > {-# LANGUAGE TemplateHaskell #-}
+    > module CallSpecTest where
+    >
+    > import CallSpecs
+    > import System.Process.Quick
+    >
+    > main :: IO ()
+    > main = $(discoverAndVerifyCallSpecs
+    >           (fromList [ TrailingHelpValidate
+    >                     , SandboxValidate
+    >                     ])
+    >           100)
+    
+    > {-# LANGUAGE TemplateHaskell #-}
+    > module Main where
+    >
+    > import CallSpecs
+    > import System.Process.Quick
+    >
+    > main :: IO ()
+    > main =
+    >   callProcess $ BinCp $(refinedTH "app.hs") $(refinedTH "app.bak")
+    
+    @CallSpec@ of cp command requires 2 parameters and here quick-process
+    power start to show up. Refined constraint InFile ensures that first
+    string is a valid file path to a Haskell source file. This part is
+    delegated to <https://hackage.haskell.org/package/refined refined>
+    library. HelpKey mode generates appropriate values, but they don’t point
+    to real files on disk. Use Sandbox mode to actually launch process in a
+    temporary dir with real files. In Sandbox @OutFile@ cause to check that
+    the file appears on the path once process terminates.
+    
+    === Subcases
+    #subcases#
+    
+    Call spec can be composed of sum types.
+    
+    > {-# LANGUAGE TemplateHaskell #-}
+    > module CallSpecs where
+    > import System.Process.Quick
+    >
+    > $(genCallSpec
+    >   [TrailingHelpValidate, SandboxValidate]
+    >   "find"
+    >   (   ConstArg "."
+    >   .*. Subcases
+    >         "FindCases"
+    >         [ Subcase "FindPrintf"
+    >           (KeyArg @(Refined (Regex "^[%][fpactbnM%]$") String) "-printf" .*. HNil)
+    >         , Subcase "FindExec"
+    >           (KeyArg @(Refined (Regex "^(ls|file|du)$") String) "-exec" .*. ConstArg "{}" .*. ConstArg ";" .*. HNil)
+    >         ]
+    >   .*. HNil
+    >   )
+    >  )
+    
+    Note usage of @Regex@ predicate - thanks to
+    <https://hackage.haskell.org/package/refined sbv> and z3 SMT solver
+    values satisfing arbitrary TDFA regex can be generated.
+
+homepage:      http://github.com/yaitskov/quick-process
+license:       BSD-3-Clause
+author:        Daniil Iaitskov
+maintainer:    dyaitskov@gmail.com
+copyright:     Daniil Iaitkov 2025
+category:      System
+build-type:    Simple
+bug-reports:   https://github.com/yaitskov/quick-process/issues
+extra-doc-files:
+  changelog.md
+tested-with:
+  GHC == 9.10.1
+
+source-repository head
+  type:
+    git
+  location:
+    https://github.com/yaitskov/quick-process.git
+
+Flag leafopt
+  Description: Enable leaf optimization
+  Default: False
+
+common base
+  default-language: GHC2024
+  ghc-options: -Wall
+  default-extensions:
+    DefaultSignatures
+    NoImplicitPrelude
+    OverloadedStrings
+    TemplateHaskell
+  build-depends:
+      HList >= 0.5.4.0 && < 1
+    , QuickCheck >= 2.14.3 && < 3
+    , base >=4 && < 5
+    , bytestring >= 0.12.1 && < 1
+    , generic-lens >= 2.2.2 && < 3
+    , lens >= 5.3.2 && < 6
+    , relude >= 1.2.2 && < 2
+
+-- https://github.com/erikd/conduit-find/pull/17
+library conduit-find-internal
+  import: base
+  hs-source-dirs: conduit-find
+  ghc-options: -Wall -funbox-strict-fields
+  if os(linux) && flag(leafopt)
+     cpp-options: -DLEAFOPT=1
+  default-extensions:
+    ImplicitPrelude
+  exposed-modules:
+      Data.Cond, Data.Conduit.Find
+  build-depends:
+      attoparsec           >= 0.14.4 && < 1
+    , conduit              >= 1.2 && < 2
+    , conduit-combinators  >= 1.3.0 && < 2
+    , conduit-extra        >= 1.3.6 && < 2
+    , either               >= 5.0.2 && < 6
+    , exceptions           >= 0.6 && < 1
+    , filepath             >= 1.5.2 && < 2
+    , mmorph               >= 1.2.0 && < 2
+    , monad-control        >= 1.0 && < 2
+    , mtl                  >= 2.3.1 && < 3
+    , regex-posix          >= 0.96.0 && < 1
+    , resourcet            >= 1.1 && < 2
+    , semigroups           >= 0.20 && < 1
+    , streaming-commons    >= 0.2.2 && < 1
+    , text                 >= 2.0 && < 3
+    , time                 >= 1.12.2 && < 2
+    , transformers         >= 0.6.1 && < 1
+    , transformers-base    >= 0.4.6 && < 1
+    , transformers-either  >= 0.1.4 && < 1
+    , unix-compat          >= 0.4.1.1 && < 1
+    , unliftio-core        >= 0.2.1 && < 1
+
+-- https://github.com/nikita-volkov/refined/pull/112
+library refined-internal
+  import: base
+  hs-source-dirs: refined
+  default-extensions:
+    ImplicitPrelude
+  cpp-options: -DHAVE_QUICKCHECK
+  exposed-modules:
+    Refined
+  other-modules:
+    Refined.Unsafe
+    Refined.Unsafe.Type
+  build-depends:
+      deepseq          >= 1.4 && < 2
+    , exceptions       < 1
+    , hashable         >= 1.0 && < 2
+    , mtl              < 3
+    , template-haskell < 3
+    , text             < 3
+    , these-skinny     < 1
+
+library
+  import: base
+  hs-source-dirs: src
+  exposed-modules:
+    System.Process.Quick
+    System.Process.Quick.CallEffect
+    System.Process.Quick.CallArgument
+    System.Process.Quick.CallSpec
+    System.Process.Quick.CallSpec.Run
+    System.Process.Quick.CallSpec.Subcases
+    System.Process.Quick.CallSpec.Type
+    System.Process.Quick.CallSpec.Verify
+    System.Process.Quick.OrphanArbitrary
+    System.Process.Quick.Predicate
+    System.Process.Quick.Predicate.ImplDir
+    System.Process.Quick.Predicate.InDir
+    System.Process.Quick.Predicate.InFile
+    System.Process.Quick.Predicate.LowerCase
+    System.Process.Quick.Predicate.Regex
+    System.Process.Quick.Prelude
+    System.Process.Quick.Pretty
+    System.Process.Quick.Sbv.Arbitrary
+    System.Process.Quick.TdfaToSbvRegex
+  build-depends:
+      casing                  < 1
+    , conduit                 < 2
+    , conduit-find-internal
+    , containers              < 1
+    , directory               < 2
+    , filepath                < 2
+    , generic-random          < 2
+    , mtl                     < 3
+    , pretty                  < 2
+    , process                 < 2
+    , refined-internal
+    , regex-compat            < 1
+    , regex-tdfa              < 2
+    , safe-exceptions         < 1
+    , sbv                     < 12
+    , template-haskell        < 3
+    , temporary               < 2
+    , th-utilities            < 1
+    , trace-embrace           < 2
+    , unix                    < 3
+
+test-suite verify-call-specs
+  import: base
+  type: exitcode-stdio-1.0
+  main-is: VerifyCallSpecs.hs
+  other-modules:
+    CallSpecs.Find
+    CallSpecs.Find.Type
+  hs-source-dirs:
+    verify-call-specs
+  ghc-options: -Wall -rtsopts -threaded -main-is VerifyCallSpecs
+  build-depends: quick-process
+
+test-suite sandbox-effect
+  import: base
+  type: exitcode-stdio-1.0
+  main-is: SandBoxEffect.hs
+  other-modules:
+    CallSpecs.CpOne
+    CallSpecs.CpManyToDir
+    CallSpecs.Date
+    CallSpecs.FindCases
+  hs-source-dirs:
+    sandbox-effect
+  ghc-options: -Wall -rtsopts -threaded -main-is SandBoxEffect
+  build-depends:
+      quick-process
+    , refined-internal
+
+test-suite test
+  import: base
+  type: exitcode-stdio-1.0
+  main-is: Driver.hs
+  other-modules:
+    Discovery
+    System.Process.Quick.Test.CallSpec
+    System.Process.Quick.Test.CallSpec.Const
+    System.Process.Quick.Test.CallSpec.VarArg
+    System.Process.Quick.Test.CallSpec.VarArg.Refined
+    System.Process.Quick.Test.Prelude
+    System.Process.Quick.Test.Th
+    Paths_quick_process
+  autogen-modules:
+    Paths_quick_process
+  hs-source-dirs:
+    test
+  ghc-options: -Wall -rtsopts -threaded -main-is Driver
+  build-depends:
+      directory
+    , quickcheck-instances
+    , refined-internal
+    , th-utilities
+    , tasty
+    , tasty-discover
+    , tasty-hunit
+    , tasty-quickcheck
+    , template-haskell
+    , temporary
+    , th-lift-instances
+    , quick-process
+    , unliftio
diff --git a/refined/Refined.hs b/refined/Refined.hs
new file mode 100644
--- /dev/null
+++ b/refined/Refined.hs
@@ -0,0 +1,1888 @@
+--------------------------------------------------------------------------------
+
+-- Copyright © 2015 Nikita Volkov
+-- Copyright © 2018 Remy Goldschmidt
+-- Copyright © 2020 chessai
+--
+-- 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.
+
+--------------------------------------------------------------------------------
+
+{-# OPTIONS_GHC -Wall                        #-}
+{-# OPTIONS_GHC -fno-warn-orphans            #-}
+{-# OPTIONS_GHC -funbox-strict-fields        #-}
+
+--------------------------------------------------------------------------------
+
+{-# LANGUAGE AllowAmbiguousTypes        #-}
+{-# LANGUAGE BangPatterns               #-}
+{-# LANGUAGE CPP                        #-}
+{-# LANGUAGE DataKinds                  #-}
+{-# LANGUAGE DeriveDataTypeable         #-}
+{-# LANGUAGE DeriveGeneric              #-}
+{-# LANGUAGE FlexibleContexts           #-}
+{-# LANGUAGE FlexibleInstances          #-}
+{-# LANGUAGE LambdaCase                 #-}
+{-# LANGUAGE MagicHash                  #-}
+{-# LANGUAGE MultiParamTypeClasses      #-}
+{-# LANGUAGE OverloadedStrings          #-}
+{-# LANGUAGE PackageImports             #-}
+{-# LANGUAGE PolyKinds                  #-}
+{-# LANGUAGE RoleAnnotations            #-}
+{-# LANGUAGE ScopedTypeVariables        #-}
+{-# LANGUAGE TemplateHaskellQuotes      #-}
+{-# LANGUAGE TypeApplications           #-}
+{-# LANGUAGE TypeFamilies               #-}
+{-# LANGUAGE TypeOperators              #-}
+{-# LANGUAGE UndecidableInstances       #-}
+
+--------------------------------------------------------------------------------
+
+-- | In type theory, a refinement type is a type endowed
+--   with a predicate which is assumed to hold for any element
+--   of the refined type.
+--
+--   This library allows one to capture the idea of a refinement type
+--   using the 'Refined' type. A 'Refined' @p@ @x@ wraps a value
+--   of type @x@, ensuring that it satisfies a type-level predicate @p@.
+--
+--   A simple introduction to this library can be found here: http://nikita-volkov.github.io/refined/
+--
+module Refined
+  ( -- * 'Refined' type
+    Refined
+
+    -- ** Creation
+  , refine
+  , refine_
+  , refineThrow
+  , refineFail
+  , refineError
+  , refineEither
+  , refineTH
+  , refineTH_
+
+    -- ** Consumption
+  , unrefine
+
+    -- * 'Refined1' type
+  , Refined1
+
+    -- ** Creation
+  , refine1
+
+    -- ** Consumption
+  , unrefine1
+
+    -- * 'Predicate'
+  , Predicate (validate), validate'
+  , reifyPredicate
+
+    -- * 'Predicate1'
+  , Predicate1 (validate1), validate1'
+
+    -- * Logical predicates
+  , Not(..)
+  , And(..)
+  , type (&&)
+  , Or(..)
+  , type (||)
+  , Xor(..)
+
+    -- * Identity predicate
+  , IdPred(..)
+
+    -- * Numeric predicates
+  , LessThan(..)
+  , GreaterThan(..)
+  , From(..)
+  , To(..)
+  , FromTo(..)
+  , NegativeFromTo(..)
+  , EqualTo(..)
+  , NotEqualTo(..)
+  , Odd(..)
+  , Even(..)
+  , DivisibleBy(..)
+  , NaN(..)
+  , Infinite(..)
+  , Positive
+  , NonPositive
+  , Negative
+  , NonNegative
+  , ZeroToOne
+  , NonZero
+
+    -- * Foldable predicates
+    -- ** Size predicates
+  , SizeLessThan(..)
+  , SizeGreaterThan(..)
+  , SizeEqualTo(..)
+  , Empty
+  , NonEmpty
+    -- ** Ordering predicates
+  , Ascending(..)
+  , Descending(..)
+
+    -- * Weakening
+  , Weaken (weaken)
+  , andLeft
+  , andRight
+  , leftOr
+  , rightOr
+  , weakenAndLeft
+  , weakenAndRight
+  , weakenOrLeft
+  , weakenOrRight
+
+    -- * Strengthening
+  , strengthen
+
+    -- * Error handling
+
+    -- ** 'RefineException'
+  , RefineException
+    ( RefineNotException
+    , RefineAndException
+    , RefineOrException
+    , RefineXorException
+    , RefineOtherException
+    , RefineSomeException
+    )
+  , displayRefineException
+
+    -- ** 'validate' helpers
+  , throwRefineOtherException
+  , throwRefineSomeException
+  , success
+ ) where
+
+--------------------------------------------------------------------------------
+
+import           Control.Exception            (Exception (displayException))
+import           Data.Coerce                  (coerce)
+import           Data.Data                    (Data)
+import           Data.Either                  (isRight, rights)
+import           Data.Proxy                   (Proxy(Proxy))
+import           Data.Text                    (Text)
+import qualified Data.Text                    as Text
+import qualified Data.Text.Lazy               as TextLazy
+import qualified Data.Text.Lazy.Builder       as TextBuilder
+import qualified Data.Text.Lazy.Builder.Int   as TextBuilder
+import qualified Data.ByteString              as BS
+import qualified Data.ByteString.Lazy         as BL
+import           Data.Typeable                (TypeRep, Typeable, typeRep)
+
+import           Control.Monad.Catch          (MonadThrow, SomeException)
+import qualified Control.Monad.Catch          as MonadThrow
+import           Control.Monad.Error.Class    (MonadError)
+import qualified Control.Monad.Error.Class    as MonadError
+#if !MIN_VERSION_base(4,13,0)
+import           Control.Monad.Fail           (MonadFail, fail)
+import           Prelude                      hiding (fail)
+#endif
+
+import           GHC.Exts                     (Proxy#, proxy#)
+import           GHC.Generics                 (Generic, Generic1)
+import           GHC.TypeLits                 (type (<=), KnownNat, Nat, natVal')
+
+import           Refined.Unsafe.Type          (Refined(Refined), Refined1(Refined1))
+
+import qualified Language.Haskell.TH.Syntax   as TH
+
+#if HAVE_AESON
+import           Control.Monad    ((<=<))
+import           Data.Aeson       (FromJSON, FromJSONKey, ToJSON, ToJSONKey)
+import qualified Data.Aeson    as Aeson
+#endif
+
+#if HAVE_QUICKCHECK
+import           Test.QuickCheck  (Arbitrary, Gen)
+import qualified Test.QuickCheck  as QC
+import           Data.Typeable    (showsTypeRep)
+#endif
+
+import "these-skinny" Data.These                   (These(This,That,These))
+
+--------------------------------------------------------------------------------
+
+-- $setup
+--
+-- Doctest imports
+--
+-- >>> :set -XDataKinds
+-- >>> :set -XOverloadedStrings
+-- >>> :set -XTypeApplications
+-- >>> import Data.Int
+-- >>> import Data.Either (isLeft)
+--
+
+--------------------------------------------------------------------------------
+
+infixl 0 |>
+infixl 9 .>
+
+-- | Helper function, stolen from the flow package.
+(|>) :: a -> (a -> b) -> b
+x |> f = apply x f
+{-# INLINE (|>) #-}
+
+-- | Helper function, stolen from the flow package.
+(.>) :: (a -> b) -> (b -> c) -> a -> c
+f .> g = compose f g
+{-# INLINE (.>) #-}
+
+-- | Helper function, stolen from the flow package.
+apply :: a -> (a -> b) -> b
+apply x f = f x
+
+-- | Helper function, stolen from the flow package.
+compose :: (a -> b) -> (b -> c) -> (a -> c)
+compose f g x = g (f x)
+
+-- | FIXME: doc
+data Ordered a = Empty | Decreasing a | Increasing a
+
+-- | FIXME: doc
+inc :: Ordered a -> Bool
+inc (Decreasing _) = False
+inc _              = True
+{-# INLINE inc #-}
+
+-- | FIXME: doc
+dec :: Ordered a -> Bool
+dec (Increasing _) = False
+dec _              = True
+{-# INLINE dec #-}
+
+increasing :: (Foldable t, Ord a) => t a -> Bool
+increasing = inc . foldl' go Empty where
+  go Empty y = Increasing y
+  go (Decreasing x) _ = Decreasing x
+  go (Increasing x) y
+    | x <= y = Increasing y
+    | otherwise = Decreasing y
+{-# INLINABLE increasing #-}
+
+decreasing :: (Foldable t, Ord a) => t a -> Bool
+decreasing = dec . foldl' go Empty where
+  go Empty y = Decreasing y
+  go (Increasing x) _ = Increasing x
+  go (Decreasing x) y
+    | x >= y = Decreasing y
+    | otherwise = Increasing y
+{-# INLINABLE decreasing #-}
+
+--------------------------------------------------------------------------------
+
+-- | This instance makes sure to check the refinement.
+--
+--   @since 0.1.0.0
+instance (Read x, Predicate p x) => Read (Refined p x) where
+  readsPrec d = readParen (d > 10) $ \r1 -> do
+    ("Refined", r2) <- lex r1
+    (raw,       r3) <- readsPrec 11 r2
+    case refine raw of
+      Right val -> [(val, r3)]
+      Left  _   -> []
+
+#if HAVE_AESON
+-- | @since 0.4
+instance (FromJSON a, Predicate p a) => FromJSON (Refined p a) where
+  parseJSON = refineFail <=< Aeson.parseJSON
+
+instance (FromJSONKey a, Predicate p a) => FromJSONKey (Refined p a) where
+  fromJSONKey = case Aeson.fromJSONKey @a of
+    Aeson.FromJSONKeyCoerce -> Aeson.FromJSONKeyTextParser $ refineFail . coerce
+    Aeson.FromJSONKeyText f -> Aeson.FromJSONKeyTextParser $ refineFail . f
+    Aeson.FromJSONKeyTextParser f -> Aeson.FromJSONKeyTextParser $ refineFail <=< f
+    Aeson.FromJSONKeyValue f -> Aeson.FromJSONKeyValue $ refineFail <=< f
+
+  fromJSONKeyList = case Aeson.fromJSONKeyList @a of
+    Aeson.FromJSONKeyText f -> Aeson.FromJSONKeyTextParser $ traverse refineFail . f
+    Aeson.FromJSONKeyTextParser f -> Aeson.FromJSONKeyTextParser $ traverse refineFail <=< f
+    Aeson.FromJSONKeyValue f -> Aeson.FromJSONKeyValue $ traverse refineFail <=< f
+
+-- | @since 0.4
+instance (ToJSON a) => ToJSON (Refined p a) where
+  toJSON = Aeson.toJSON . unrefine
+
+-- | @since 0.6.3
+instance (ToJSONKey a) => ToJSONKey (Refined p a) where
+  toJSONKey = unrefine >$< Aeson.toJSONKey
+  toJSONKeyList = map unrefine >$< Aeson.toJSONKeyList
+#endif /* HAVE_AESON */
+
+#if HAVE_QUICKCHECK
+-- | @since 0.4
+instance forall p a. (Arbitrary a, Typeable a, Typeable p, Predicate p a) => Arbitrary (Refined p a) where
+  arbitrary = loop 0 QC.arbitrary
+    where
+      loop :: Int -> Gen a -> Gen (Refined p a)
+      loop !runs gen
+        | runs < 100 = do
+            m <- suchThatRefined gen
+            case m of
+              Just x -> do
+                pure x
+              Nothing -> do
+                loop (runs + 1) gen
+        | otherwise = error (refinedGenError (Proxy @p) (Proxy @a))
+  shrink = rights . map refine . QC.shrink . unrefine
+
+refinedGenError :: (Typeable p, Typeable a)
+  => Proxy p -> Proxy a -> String
+refinedGenError p a = "arbitrary :: Refined ("
+  ++ typeName p
+  ++ ") ("
+  ++ typeName a
+  ++ "): Failed to generate a value that satisfied"
+  ++ " the predicate after 100 tries."
+
+suchThatRefined :: forall p a. (Predicate p a)
+  => Gen a -> Gen (Maybe (Refined p a))
+suchThatRefined gen = do
+  m <- QC.suchThatMaybe gen (reifyPredicate @p @a)
+  case m of
+    Nothing -> pure Nothing
+    Just x -> pure (Just (Refined x))
+
+typeName :: Typeable a => Proxy a -> String
+typeName = flip showsTypeRep "" . typeRep
+#endif /* HAVE_QUICKCHECK */
+
+--------------------------------------------------------------------------------
+
+-- | A smart constructor of a 'Refined' value.
+--   Checks the input value at runtime.
+--
+--   @since 0.1.0.0
+refine :: forall p x. (Predicate p x) => x -> Either RefineException (Refined p x)
+refine x = maybe (Right (Refined x)) Left (validate (Proxy @p) x)
+{-# INLINABLE refine #-}
+
+-- | Like 'refine', but discards the refinement.
+--   This _can_ be useful when you only need to validate
+--   that some value at runtime satisfies some predicate.
+--   See also 'reifyPredicate'.
+--
+--   @since 0.4.4
+refine_ :: forall p x. (Predicate p x) => x -> Either RefineException x
+refine_ = refine @p @x .> coerce
+{-# INLINABLE refine_ #-}
+
+-- | Constructs a 'Refined' value at run-time,
+--   calling 'Control.Monad.Catch.throwM' if the value
+--   does not satisfy the predicate.
+--
+--   @since 0.2.0.0
+refineThrow :: (Predicate p x, MonadThrow m) => x -> m (Refined p x)
+refineThrow = refine .> either MonadThrow.throwM pure
+{-# INLINABLE refineThrow #-}
+
+-- | Constructs a 'Refined' value at run-time,
+--   calling 'Control.Monad.Fail.fail' if the value
+--   does not satisfy the predicate.
+--
+--   @since 0.2.0.0
+refineFail :: (Predicate p x, MonadFail m) => x -> m (Refined p x)
+refineFail = refine .> either (displayException .> fail) pure
+{-# INLINABLE refineFail #-}
+
+-- | Constructs a 'Refined' value at run-time,
+--   calling 'Control.Monad.Error.throwError' if the value
+--   does not satisfy the predicate.
+--
+--   @since 0.2.0.0
+refineError :: (Predicate p x, MonadError RefineException m)
+            => x -> m (Refined p x)
+refineError = refine .> either MonadError.throwError pure
+{-# INLINABLE refineError #-}
+
+-- | Like 'refine', but, when the value doesn't satisfy the predicate, returns
+--   a 'Refined' value with the predicate negated, instead of returning
+--   'RefineException'.
+--
+--   >>> isRight (refineEither @Even @Int 42)
+--   True
+--
+--   >>> isLeft (refineEither @Even @Int 43)
+--   True
+--
+refineEither :: forall p x. (Predicate p x) => x -> Either (Refined (Not p) x) (Refined p x)
+refineEither x =
+  case validate (Proxy @p) x of
+    Nothing -> Right $ Refined x
+    Just _  -> Left  $ Refined x
+{-# INLINABLE refineEither #-}
+
+--------------------------------------------------------------------------------
+
+-- | A smart constructor of a 'Refined1' value.
+--   Checks the input value at runtime.
+--
+--   @since 0.1.0.0
+refine1
+    :: forall p f x. Predicate1 p f
+    => f x -> Either RefineException (Refined1 p f x)
+refine1 x = maybe (Right (Refined1 x)) Left (validate1 (Proxy @p) x)
+{-# INLINABLE refine1 #-}
+
+--------------------------------------------------------------------------------
+
+-- | Constructs a 'Refined' value at compile-time using @-XTemplateHaskell@.
+--
+--   For example:
+--
+--   > $$(refineTH 23) :: Refined Positive Int
+--   > Refined 23
+--
+--   Here's an example of an invalid value:
+--
+--   > $$(refineTH 0) :: Refined Positive Int
+--   > <interactive>:6:4:
+--   >     Value is not greater than 0
+--   >     In the Template Haskell splice $$(refineTH 0)
+--   >     In the expression: $$(refineTH 0) :: Refined Positive Int
+--   >     In an equation for ‘it’:
+--   >         it = $$(refineTH 0) :: Refined Positive Int
+--
+--   The example above indicates a compile-time failure,
+--   which means that the checking was done at compile-time,
+--   thus introducing a zero-runtime overhead compared to
+--   a plain value construction.
+--
+--   /Note/: It may be useful to use this function with the
+--   <https://hackage.haskell.org/package/th-lift-instances/ th-lift-instances package>.
+--
+--   @since 0.1.0.0
+#if MIN_VERSION_template_haskell(2,17,0)
+refineTH :: forall p x m. (Predicate p x, TH.Lift x, TH.Quote m, MonadFail m)
+  => x
+  -> TH.Code m (Refined p x)
+refineTH =
+  let showException = refineExceptionToTree
+        .> showTree True
+        .> fail
+        .> TH.liftCode
+  in refine @p @x
+     .> either showException TH.liftTyped
+#else
+refineTH :: forall p x. (Predicate p x, TH.Lift x)
+  => x
+  -> TH.Q (TH.TExp (Refined p x))
+refineTH =
+  let showException = refineExceptionToTree
+        .> showTree True
+        .> fail
+  in refine @p @x
+     .> either showException TH.lift
+     .> fmap TH.TExp
+#endif
+
+-- | Like 'refineTH', but immediately unrefines the value.
+--   This is useful when some value need only be refined
+--   at compile-time.
+--
+--   @since 0.4.4
+#if MIN_VERSION_template_haskell(2,17,0)
+refineTH_ :: forall p x m. (Predicate p x, TH.Lift x, TH.Quote m, MonadFail m)
+  => x
+  -> TH.Code m x
+refineTH_ =
+  refineTH @p @x
+  .> TH.examineCode
+  .> fmap unsafeUnrefineTExp
+  .> TH.liftCode
+#else
+refineTH_ :: forall p x. (Predicate p x, TH.Lift x)
+  => x
+  -> TH.Q (TH.TExp x)
+refineTH_ = refineTH @p @x .> fmap unsafeUnrefineTExp
+#endif
+
+unsafeUnrefineTExp :: TH.TExp (Refined p x) -> TH.TExp x
+unsafeUnrefineTExp (TH.TExp e) = TH.TExp
+  (TH.VarE 'unrefine `TH.AppE` e)
+
+--------------------------------------------------------------------------------
+
+-- | Extracts the refined value.
+--
+--   @since 0.1.0.0
+unrefine :: Refined p x -> x
+unrefine = coerce
+{-# INLINE unrefine #-}
+
+-- | Extracts the refined value.
+unrefine1 :: Refined1 p f x -> f x
+unrefine1 = coerce
+{-# INLINE unrefine1 #-}
+
+--------------------------------------------------------------------------------
+
+-- | A typeclass which defines a runtime interpretation of
+--   a type-level predicate @p@ for type @x@.
+--
+--   @since 0.1.0.0
+class (Typeable p, Typeable k) => Predicate (p :: k) x where
+  {-# MINIMAL validate #-}
+  -- | Check the value @x@ according to the predicate @p@,
+  --   producing an error 'RefineException' if the value
+  --   does not satisfy.
+  --
+  --   /Note/: 'validate' is not intended to be used
+  --   directly; instead, it is intended to provide the minimal
+  --   means necessary for other utilities to be derived. As
+  --   such, the 'Maybe' here should be interpreted to mean
+  --   the presence or absence of a 'RefineException', and
+  --   nothing else.
+  --
+  --   Note that due to GHC's type variable order rules, this function has an
+  --   implicit kind in position 1, which makes TypeApplications awkward. Use
+  --   'validate'' for nicer behaviour.
+  validate :: Proxy p -> x -> Maybe RefineException
+
+-- | Check the value @x@ according to the predicate @p@,
+--   producing an error 'RefineException' if the value
+--   does not satisfy.
+--
+-- Same as 'validate' but with more convenient type variable order for a better
+-- TypeApplications experience.
+validate'
+    :: forall {k} p x
+    .  Predicate (p :: k) x => Proxy p -> x -> Maybe RefineException
+validate' = validate
+{-# INLINE validate' #-}
+
+-- | A typeclass which defines a runtime interpretation of
+--   a type-level predicate @p@ for type @forall a. f a@.
+--
+-- The inner type may not be inspected. If you find yourself needing to add
+-- constraints to it, you want 'Predicate'.
+class (Typeable p, Typeable k) => Predicate1 (p :: k) f where
+  {-# MINIMAL validate1 #-}
+  -- | Check the value @f a@ according to the predicate @p@,
+  --   producing an error 'RefineException' if the value
+  --   does not satisfy.
+  --
+  --   /Note/: 'validate1' is not intended to be used
+  --   directly; instead, it is intended to provide the minimal
+  --   means necessary for other utilities to be derived. As
+  --   such, the 'Maybe' here should be interpreted to mean
+  --   the presence or absence of a 'RefineException', and
+  --   nothing else.
+  --
+  --   Note that due to GHC's type variable order rules, this function has an
+  --   implicit kind in position 1, which makes TypeApplications awkward. Use
+  --   'validate1'' for nicer behaviour.
+  validate1 :: Proxy p -> f a -> Maybe RefineException
+
+-- | Check the value @f a@ according to the predicate @p@,
+--   producing an error 'RefineException' if the value
+--   does not satisfy.
+--
+-- Same as 'validate1' but with more convenient type variable order for a better
+-- TypeApplications experience.
+validate1'
+    :: forall {k} p f a
+    .  Predicate1 (p :: k) f => Proxy p -> f a -> Maybe RefineException
+validate1' = validate1
+{-# INLINE validate1' #-}
+
+--------------------------------------------------------------------------------
+
+-- | Reify a 'Predicate' by turning it into a value-level predicate.
+--
+--   @since 0.4.2.3
+reifyPredicate :: forall p a. Predicate p a => a -> Bool
+reifyPredicate = refine @p @a .> isRight
+{-# INLINABLE reifyPredicate #-}
+
+--------------------------------------------------------------------------------
+
+-- | A predicate which is satisfied for all types.
+--   Arguments passed to @'validate'@ in @'validate' 'IdPred' x@
+--   are not evaluated.
+--
+--   >>> isRight (refine @IdPred @Int undefined)
+--   True
+--
+--   >>> isLeft (refine @IdPred @Int undefined)
+--   False
+--
+--   @since 0.3.0.0
+data IdPred
+  = IdPred -- ^ @since 0.4.2
+  deriving
+    ( Generic -- ^ @since 0.3.0.0
+    , Data -- ^ @since 0.8.3
+    )
+
+-- | @since 0.3.0.0
+instance Predicate IdPred x where
+  validate _ _ = Nothing
+  {-# INLINE validate #-}
+
+--------------------------------------------------------------------------------
+
+-- | The negation of a predicate.
+--
+--   >>> isRight (refine @(Not NonEmpty) @[Int] [])
+--   True
+--
+--   >>> isLeft (refine @(Not NonEmpty) @[Int] [1,2])
+--   True
+--
+--   @since 0.1.0.0
+data Not p
+  = Not -- ^ @since 0.4.2
+  deriving
+    ( Generic -- ^ @since 0.3.0.0
+    , Generic1 -- ^ @since 0.3.0.0
+    , Data -- ^ @since 0.8.3
+    )
+
+
+-- | @since 0.1.0.0
+instance Predicate p x => Predicate (Not p) x where
+  validate p x = do
+    maybe (Just (RefineNotException (typeRep p)))
+          (const Nothing)
+          (validate' @p undefined x)
+
+--------------------------------------------------------------------------------
+
+-- | The conjunction of two predicates.
+--
+--   >>> isLeft (refine @(And Positive Negative) @Int 3)
+--   True
+--
+--   >>> isRight (refine @(And Positive Odd) @Int 203)
+--   True
+--
+--   @since 0.1.0.0
+data And l r
+  = And -- ^ @since 0.4.2
+  deriving
+    ( Generic -- ^ @since 0.3.0.0
+    , Generic1 -- ^ @since 0.3.0.0
+    , Data -- ^ @since 0.8.3
+    )
+
+infixr 3 &&
+-- | The conjunction of two predicates.
+--
+--   @since 0.2.0.0
+type (&&) = And
+
+-- | @since 0.1.0.0
+instance ( Predicate l x, Predicate r x ) => Predicate (And l r) x where
+  validate p x = do
+    let a = validate' @l undefined x
+    let b = validate' @r undefined x
+    let throw err = Just (RefineAndException (typeRep p) err)
+    case (a, b) of
+      (Just  e, Just e1) -> throw (These e e1)
+      (Just  e,       _) -> throw (This e)
+      (Nothing, Just  e) -> throw (That e)
+      (Nothing, Nothing) -> Nothing
+
+--------------------------------------------------------------------------------
+
+-- | The disjunction of two predicates.
+--
+--   >>> isRight (refine @(Or Even Odd) @Int 3)
+--   True
+--
+--   >>> isRight (refine @(Or (LessThan 3) (GreaterThan 3)) @Int 2)
+--   True
+--
+--   >>> isRight (refine @(Or Even Even) @Int 4)
+--   True
+--
+--   @since 0.1.0.0
+data Or l r
+  = Or -- ^ @since 0.4.2
+  deriving
+    ( Generic -- ^ @since 0.3.0.0
+    , Generic1 -- ^ @since 0.3.0.0
+    , Data -- ^ @since 0.8.3
+    )
+
+infixr 2 ||
+-- | The disjunction of two predicates.
+--
+--   @since 0.2.0.0
+type (||) = Or
+
+-- | @since 0.2.0.0
+instance ( Predicate l x, Predicate r x ) => Predicate (Or l r) x where
+  validate p x = do
+    let left  = validate' @l undefined x
+    let right = validate' @r undefined x
+    case (left, right) of
+      (Just l, Just r) -> Just (RefineOrException (typeRep p) l r)
+      _                -> Nothing
+
+--------------------------------------------------------------------------------
+
+-- | The exclusive disjunction of two predicates.
+--
+--
+--   >>> isRight (refine @(Xor Even Odd) @Int 3)
+--   True
+--
+--   >>> isLeft (refine @(Xor (LessThan 3) (EqualTo 2)) @Int 2)
+--   True
+--
+--   >>> isLeft (refine @(Xor Even Even) @Int 2)
+--   True
+--
+--   @since 0.5
+data Xor l r
+  = Xor -- ^ @since 0.5
+  deriving
+    ( Generic -- ^ @since 0.5
+    , Generic1 -- ^ @since 0.5
+    , Data -- ^ @since 0.8.3
+    )
+
+-- not provided because it clashes with GHC.TypeLits.^
+-- infixr 8 ^
+-- The exclusive disjunction of two predicates.
+-- type (^) = Xor
+
+-- | @since 0.5
+instance ( Predicate l x, Predicate r x ) => Predicate (Xor l r) x where
+  validate p x = do
+    let left = validate' @l undefined x
+    let right = validate' @r undefined x
+    case (left, right) of
+      (Nothing, Nothing) -> Just (RefineXorException (typeRep p) Nothing)
+      (Just  l, Just  r) -> Just (RefineXorException (typeRep p) (Just (l, r)))
+      _ -> Nothing
+
+--------------------------------------------------------------------------------
+
+-- | A 'Predicate' ensuring that the value has a length
+-- which is less than the specified type-level number.
+--
+--   >>> isRight (refine @(SizeLessThan 4) @[Int] [1,2,3])
+--   True
+--
+--   >>> isLeft (refine @(SizeLessThan 5) @[Int] [1,2,3,4,5])
+--   True
+--
+--   >>> isRight (refine @(SizeLessThan 4) @Text "Hi")
+--   True
+--
+--   >>> isLeft (refine @(SizeLessThan 4) @Text "Hello")
+--   True
+--
+--   @since 0.2.0.0
+data SizeLessThan (n :: Nat)
+  = SizeLessThan -- ^ @since 0.4.2
+  deriving
+    ( Generic -- ^ @since 0.3.0.0
+    , Data -- ^ @since 0.8.3
+    )
+
+instance (Foldable t, KnownNat n) => Predicate1 (SizeLessThan n) t where
+  validate1 p x = sized p (x, "Foldable") length ((<), "less than")
+
+instance (Foldable t, KnownNat n) => Predicate (SizeLessThan n) (t a) where
+  validate = validate1
+
+-- | @since 0.5
+instance (KnownNat n) => Predicate (SizeLessThan n) Text where
+  validate p x = sized p (x, "Text") Text.length ((<), "less than")
+
+-- | @since 0.5
+instance (KnownNat n) => Predicate (SizeLessThan n) BS.ByteString where
+  validate p x = sized p (x, "ByteString") BS.length ((<), "less than")
+
+-- | @since 0.5
+instance (KnownNat n) => Predicate (SizeLessThan n) BL.ByteString where
+  validate p x = sized p (x, "ByteString") (fromIntegral . BL.length) ((<), "less than")
+
+--------------------------------------------------------------------------------
+
+-- | A 'Predicate' ensuring that the value has a length
+-- which is greater than the specified type-level number.
+--
+--   >>> isLeft (refine  @(SizeGreaterThan 3) @[Int] [1,2,3])
+--   True
+--
+--   >>> isRight (refine @(SizeGreaterThan 3) @[Int] [1,2,3,4,5])
+--   True
+--
+--   >>> isLeft (refine @(SizeGreaterThan 4) @Text "Hi")
+--   True
+--
+--   >>> isRight (refine @(SizeGreaterThan 4) @Text "Hello")
+--   True
+--
+--   @since 0.2.0.0
+data SizeGreaterThan (n :: Nat)
+  = SizeGreaterThan -- ^ @since 0.4.2
+  deriving
+    ( Generic -- ^ @since 0.3.0.0
+    , Data -- ^ @since 0.8.3
+    )
+
+instance (Foldable t, KnownNat n) => Predicate1 (SizeGreaterThan n) t where
+  validate1 p x = sized p (x, "Foldable") length ((>), "greater than")
+
+-- | @since 0.2.0.0
+instance (Foldable t, KnownNat n) => Predicate (SizeGreaterThan n) (t a) where
+  validate = validate1
+
+-- | @since 0.5
+instance (KnownNat n) => Predicate (SizeGreaterThan n) Text where
+  validate p x = sized p (x, "Text") Text.length ((>), "greater than")
+
+-- | @since 0.5
+instance (KnownNat n) => Predicate (SizeGreaterThan n) BS.ByteString where
+  validate p x = sized p (x, "ByteString") BS.length ((>), "greater than")
+
+-- | @since 0.5
+instance (KnownNat n) => Predicate (SizeGreaterThan n) BL.ByteString where
+  validate p x = sized p (x, "ByteString") (fromIntegral . BL.length) ((>), "greater than")
+
+--------------------------------------------------------------------------------
+
+-- | A 'Predicate' ensuring that the value has a length
+-- which is equal to the specified type-level number.
+--
+--   >>> isRight (refine @(SizeEqualTo 4) @[Int] [1,2,3,4])
+--   True
+--
+--   >>> isLeft (refine @(SizeEqualTo 35) @[Int] [1,2,3,4])
+--   True
+--
+--   >>> isRight (refine @(SizeEqualTo 4) @Text "four")
+--   True
+--
+--   >>> isLeft (refine @(SizeEqualTo 35) @Text "four")
+--   True
+--
+--   @since 0.2.0.0
+data SizeEqualTo (n :: Nat)
+  = SizeEqualTo -- ^ @since 0.4.2
+  deriving
+    ( Generic -- ^ @since 0.3.0.0
+    , Data -- ^ @since 0.8.3
+    )
+
+instance (Foldable t, KnownNat n) => Predicate1 (SizeEqualTo n) t where
+  validate1 p x = sized p (x, "Foldable") length ((==), "equal to")
+
+-- | @since 0.2.0.0
+instance (Foldable t, KnownNat n) => Predicate (SizeEqualTo n) (t a) where
+  validate = validate1
+
+-- | @since 0.5
+instance (KnownNat n) => Predicate (SizeEqualTo n) Text where
+  validate p x = sized p (x, "Text") Text.length ((==), "equal to")
+
+-- | @since 0.5
+instance (KnownNat n) => Predicate (SizeEqualTo n) BS.ByteString where
+  validate p x = sized p (x, "ByteString") BS.length ((==), "equal to")
+
+-- | @since 0.5
+instance (KnownNat n) => Predicate (SizeEqualTo n) BL.ByteString where
+  validate p x = sized p (x, "ByteString") (fromIntegral . BL.length) ((==), "equal to")
+
+--------------------------------------------------------------------------------
+
+-- | A 'Predicate' ensuring that the 'Foldable' contains elements
+-- in a strictly ascending order.
+--
+--   >>> isRight (refine @Ascending @[Int] [5, 8, 13, 21, 34])
+--   True
+--
+--   >>> isLeft (refine @Ascending @[Int] [34, 21, 13, 8, 5])
+--   True
+--
+--   @since 0.2.0.0
+data Ascending
+  = Ascending -- ^ @since 0.4.2
+  deriving
+    ( Generic -- ^ @since 0.3.0.0
+    , Data -- ^ @since 0.8.3
+    )
+
+-- | @since 0.2.0.0
+instance (Foldable t, Ord a) => Predicate Ascending (t a) where
+  validate p x = do
+    if increasing x
+    then Nothing
+    else throwRefineOtherException
+         (typeRep p)
+         "Foldable is not in ascending order."
+
+--------------------------------------------------------------------------------
+
+-- | A 'Predicate' ensuring that the 'Foldable' contains elements
+-- in a strictly descending order.
+--
+--   >>> isRight (refine @Descending @[Int] [34, 21, 13, 8, 5])
+--   True
+--
+--   >>> isLeft (refine @Descending @[Int] [5, 8, 13, 21, 34])
+--   True
+--
+--   @since 0.2.0.0
+data Descending
+  = Descending -- ^ @since 0.4.2
+  deriving
+    ( Generic -- ^ @since 0.3.0.0
+    , Data -- ^ @since 0.8.3
+    )
+
+-- | @since 0.2.0.0
+instance (Foldable t, Ord a) => Predicate Descending (t a) where
+  validate p x = do
+    if decreasing x
+    then Nothing
+    else throwRefineOtherException
+        (typeRep p)
+        "Foldable is not in descending order."
+
+--------------------------------------------------------------------------------
+
+-- | A 'Predicate' ensuring that the value is less than the
+--   specified type-level number.
+--
+--   >>> isRight (refine @(LessThan 12) @Int 11)
+--   True
+--
+--   >>> isLeft (refine @(LessThan 12) @Int 12)
+--   True
+--
+--   @since 0.1.0.0
+data LessThan (n :: Nat)
+  = LessThan -- ^ @since 0.4.2
+  deriving
+    ( Generic -- ^ @since 0.3.0.0
+    , Data -- ^ @since 0.8.3
+    )
+
+-- | @since 0.1.0.0
+instance (Ord x, Num x, KnownNat n) => Predicate (LessThan n) x where
+  validate p x = do
+    let n = nv @n
+    let x' = fromIntegral n
+    if x < x'
+    then Nothing
+    else throwRefineOtherException
+         (typeRep p)
+         ("Value is not less than " <> i2text n)
+
+--------------------------------------------------------------------------------
+
+-- | A 'Predicate' ensuring that the value is greater than the
+--   specified type-level number.
+--
+--   >>> isRight (refine @(GreaterThan 65) @Int 67)
+--   True
+--
+--   >>> isLeft (refine @(GreaterThan 65) @Int 65)
+--   True
+--
+--   @since 0.1.0.0
+data GreaterThan (n :: Nat)
+  = GreaterThan -- ^ @since 0.4.2
+  deriving
+    ( Generic -- ^ @since 0.3.0.0
+    , Data -- ^ @since 0.8.3
+    )
+
+-- | @since 0.1.0.0
+instance (Ord x, Num x, KnownNat n) => Predicate (GreaterThan n) x where
+  validate p x = do
+    let n = nv @n
+    let x' = fromIntegral n
+    if x > x'
+    then Nothing
+    else throwRefineOtherException
+         (typeRep p)
+         ("Value is not greater than " <> i2text n)
+
+--------------------------------------------------------------------------------
+
+-- | A 'Predicate' ensuring that the value is greater than or equal to the
+--   specified type-level number.
+--
+--   >>> isRight (refine @(From 9) @Int 10)
+--   True
+--
+--   >>> isRight (refine @(From 10) @Int 10)
+--   True
+--
+--   >>> isLeft (refine @(From 11) @Int 10)
+--   True
+--
+--   @since 0.1.2
+data From (n :: Nat)
+  = From -- ^ @since 0.4.2
+  deriving
+    ( Generic -- ^ @since 0.3.0.0
+    , Data -- ^ @since 0.8.3
+    )
+
+-- | @since 0.1.2
+instance (Ord x, Num x, KnownNat n) => Predicate (From n) x where
+  validate p x = do
+    let n = nv @n
+    let x' = fromIntegral n
+    if x >= x'
+    then Nothing
+    else throwRefineOtherException
+         (typeRep p)
+         ("Value is less than " <> i2text n)
+
+--------------------------------------------------------------------------------
+
+-- | A 'Predicate' ensuring that the value is less than or equal to the
+--   specified type-level number.
+--
+--   >>> isRight (refine @(To 23) @Int 17)
+--   True
+--
+--   >>> isLeft (refine @(To 17) @Int 23)
+--   True
+--
+--   @since 0.1.2
+data To (n :: Nat)
+  = To -- ^ @since 0.4.2
+  deriving
+    ( Generic -- ^ @since 0.3.0.0
+    , Data -- ^ @since 0.8.3
+    )
+
+-- | @since 0.1.2
+instance (Ord x, Num x, KnownNat n) => Predicate (To n) x where
+  validate p x = do
+    let n = nv @n
+    let x' = fromIntegral n
+    if x <= x'
+    then Nothing
+    else throwRefineOtherException
+         (typeRep p)
+         ("Value is greater than " <> i2text n)
+
+--------------------------------------------------------------------------------
+
+-- | A 'Predicate' ensuring that the value is within an inclusive range.
+--
+--   >>> isRight (refine @(FromTo 0 16) @Int 13)
+--   True
+--
+--   >>> isRight (refine @(FromTo 13 15) @Int 13)
+--   True
+--
+--   >>> isRight (refine @(FromTo 13 15) @Int 15)
+--   True
+--
+--   >>> isLeft (refine @(FromTo 13 15) @Int 12)
+--   True
+--
+--   @since 0.1.2
+data FromTo (mn :: Nat) (mx :: Nat)
+  = FromTo -- ^ @since 0.4.2
+  deriving
+    ( Generic-- ^ @since 0.3.0.0
+    , Data -- ^ @since 0.8.3
+    )
+
+-- | @since 0.1.2
+instance ( Ord x, Num x, KnownNat mn, KnownNat mx, mn <= mx
+         ) => Predicate (FromTo mn mx) x where
+  validate p x = do
+    let mn' = nv @mn
+    let mx' = nv @mx
+    if x >= fromIntegral mn' && x <= fromIntegral mx'
+    then Nothing
+    else
+      let msg = [ "Value is out of range (minimum: "
+                , i2text mn'
+                , ", maximum: "
+                , i2text mx'
+                , ")"
+                ] |> mconcat
+      in throwRefineOtherException (typeRep p) msg
+
+--------------------------------------------------------------------------------
+
+-- | A 'Predicate' ensuring that the value is equal to the specified
+--   type-level number @n@.
+--
+--   >>> isRight (refine @(EqualTo 5) @Int 5)
+--   True
+--
+--   >>> isLeft (refine @(EqualTo 6) @Int 5)
+--   True
+--
+--   @since 0.1.0.0
+data EqualTo (n :: Nat)
+  = EqualTo -- ^ @since 0.4.2
+  deriving
+    ( Generic -- ^ @since 0.3.0.0
+    , Data -- ^ @since 0.8.3
+    )
+
+-- | @since 0.1.0.0
+instance (Eq x, Num x, KnownNat n) => Predicate (EqualTo n) x where
+  validate p x = do
+    let n = nv @n
+    let x' = fromIntegral n
+    if x == x'
+    then Nothing
+    else throwRefineOtherException
+         (typeRep p)
+         ("Value does not equal " <> i2text n)
+
+--------------------------------------------------------------------------------
+
+-- | A 'Predicate' ensuring that the value is not equal to the specified
+--   type-level number @n@.
+--
+--   >>> isRight (refine @(NotEqualTo 6) @Int 5)
+--   True
+--
+--   >>> isLeft (refine @(NotEqualTo 5) @Int 5)
+--   True
+--
+--   @since 0.2.0.0
+data NotEqualTo (n :: Nat)
+  = NotEqualTo -- ^ @since 0.4.2
+  deriving
+    ( Generic -- ^ @since 0.3.0.0
+    , Data -- ^ @since 0.8.3
+    )
+
+-- | @since 0.2.0.0
+instance (Eq x, Num x, KnownNat n) => Predicate (NotEqualTo n) x where
+  validate p x = do
+    let n = nv @n
+    let x' = fromIntegral n
+    if x /= x'
+    then Nothing
+    else throwRefineOtherException
+         (typeRep p)
+         ("Value does equal " <> i2text n)
+
+--------------------------------------------------------------------------------
+
+-- | A 'Predicate' ensuring that the value is greater or equal than a negative
+--   number specified as a type-level (positive) number @n@ and less than a
+--   type-level (positive) number @m@.
+--
+--   >>> isRight (refine @(NegativeFromTo 5 12) @Int (-3))
+--   True
+--
+--   >>> isLeft (refine @(NegativeFromTo 4 3) @Int (-5))
+--   True
+--
+--   @since 0.4
+data NegativeFromTo (n :: Nat) (m :: Nat)
+  = NegativeFromTo -- ^ @since 0.4.2
+  deriving
+    ( Generic -- ^ @since 0.3.0.0
+    , Data -- ^ @since 0.8.3
+    )
+
+-- | @since 0.4
+instance (Ord x, Num x, KnownNat n, KnownNat m) => Predicate (NegativeFromTo n m) x where
+  validate p x = do
+    let n' = nv @n
+    let m' = nv @m
+    if x >= fromIntegral (negate n') && x <= fromIntegral m'
+    then Nothing
+    else
+      let msg = [ "Value is out of range (minimum: "
+                , i2text (negate n')
+                , ", maximum: "
+                , i2text m'
+                , ")"
+                ] |> mconcat
+      in throwRefineOtherException (typeRep p) msg
+
+--------------------------------------------------------------------------------
+
+-- | A 'Predicate' ensuring that the value is divisible by @n@.
+--
+--   >>> isRight (refine @(DivisibleBy 3) @Int 12)
+--   True
+--
+--   >>> isLeft (refine @(DivisibleBy 2) @Int 37)
+--   True
+--
+--   @since 0.4.2
+data DivisibleBy (n :: Nat)
+  = DivisibleBy -- ^ @since 0.4.2
+  deriving
+    ( Generic -- ^ @since 0.3.0.0
+    , Data -- ^ @since 0.8.3
+    )
+
+-- | @since 0.4.2
+instance (Integral x, KnownNat n) => Predicate (DivisibleBy n) x where
+  validate p x = do
+    let n = nv @n
+    let x' = fromIntegral n
+    if x `mod` x' == 0
+    then Nothing
+    else throwRefineOtherException
+         (typeRep p)
+         ("Value is not divisible by " <> i2text n)
+
+--------------------------------------------------------------------------------
+
+-- | A 'Predicate' ensuring that the value is odd.
+--
+--   >>> isRight (refine @Odd @Int 33)
+--   True
+--
+--   >>> isLeft (refine @Odd @Int 32)
+--   True
+--
+--   @since 0.4.2
+data Odd
+  = Odd -- ^ @since 0.4.2
+  deriving
+    ( Generic -- ^ @since 0.3.0.0
+    , Data -- ^ @since 0.8.3
+    )
+
+-- | @since 0.4.2
+instance (Integral x) => Predicate Odd x where
+  validate p x = do
+    if odd x
+    then Nothing
+    else throwRefineOtherException
+         (typeRep p)
+         "Value is not odd."
+
+--------------------------------------------------------------------------------
+
+-- | A 'Predicate' ensuring that the value is IEEE "not-a-number" (NaN).
+--
+--   >>> isRight (refine @NaN @Double (0/0))
+--   True
+--
+--   >>> isLeft (refine @NaN @Double 13.9)
+--   True
+--
+--   @since 0.5
+data NaN
+  = NaN -- ^ @since 0.5
+  deriving
+    ( Generic -- ^ @since 0.5
+    , Data -- ^ @since 0.8.3
+    )
+
+-- | @since 0.5
+instance (RealFloat x) => Predicate NaN x where
+  validate p x = do
+    if isNaN x
+    then Nothing
+    else throwRefineOtherException
+         (typeRep p)
+         "Value is not IEEE \"not-a-number\" (NaN)."
+
+--------------------------------------------------------------------------------
+
+-- | A 'Predicate' ensuring that the value is IEEE infinity or negative infinity.
+--
+--   >>> isRight (refine @Infinite @Double (1/0))
+--   True
+--
+--   >>> isRight (refine @Infinite @Double (-1/0))
+--   True
+--
+--   >>> isLeft (refine @Infinite @Double 13.20)
+--   True
+--
+--   @since 0.5
+data Infinite
+  = Infinite -- ^ @since 0.5
+  deriving
+    ( Generic -- ^ @since 0.5
+    , Data -- ^ @since 0.8.3
+    )
+
+-- | @since 0.5
+instance (RealFloat x) => Predicate Infinite x where
+  validate p x = do
+    if isInfinite x
+    then Nothing
+    else throwRefineOtherException
+         (typeRep p)
+         "Value is not IEEE infinity or negative infinity."
+
+--------------------------------------------------------------------------------
+
+-- | A 'Predicate' ensuring that the value is even.
+--
+--   >>> isRight (refine @Even @Int 32)
+--   True
+--
+--   >>> isLeft (refine @Even @Int 33)
+--   True
+--
+--   @since 0.4.2
+data Even
+  = Even -- ^ @since 0.4.2
+  deriving
+    ( Generic -- ^ @since 0.4.2
+    , Data -- ^ @since 0.8.3
+    )
+
+-- | @since 0.4.2
+instance (Integral x) => Predicate Even x where
+  validate p x = do
+    if even x
+    then Nothing
+    else throwRefineOtherException
+         (typeRep p)
+         "Value is not even."
+
+--------------------------------------------------------------------------------
+
+-- | A 'Predicate' ensuring that the value is greater than zero.
+--
+--   @since 0.1.0.0
+type Positive = GreaterThan 0
+
+-- | A 'Predicate' ensuring that the value is less than or equal to zero.
+--
+--   @since 0.1.2
+type NonPositive = To 0
+
+-- | A 'Predicate' ensuring that the value is less than zero.
+--
+--   @since 0.1.0.0
+type Negative = LessThan 0
+
+-- | A 'Predicate' ensuring that the value is greater than or equal to zero.
+--
+--   @since 0.1.2
+type NonNegative = From 0
+
+-- | An inclusive range of values from zero to one.
+--
+--   @since 0.1.0.0
+type ZeroToOne = FromTo 0 1
+
+-- | A 'Predicate' ensuring that the value is not equal to zero.
+--
+--   @since 0.2.0.0
+type NonZero = NotEqualTo 0
+
+-- | A 'Predicate' ensuring that the type is empty.
+--
+--   @since 0.5
+type Empty = SizeEqualTo 0
+
+-- | A 'Predicate' ensuring that the type is non-empty.
+--
+--   @since 0.2.0.0
+type NonEmpty = SizeGreaterThan 0
+
+--------------------------------------------------------------------------------
+
+-- | A typeclass containing "safe" conversions between refined
+--   predicates where the target is /weaker/ than the source:
+--   that is, all values that satisfy the first predicate will
+--   be guaranteed to satisfy the second.
+--
+--   Take care: writing an instance declaration for your custom
+--   predicates is the same as an assertion that 'weaken' is
+--   safe to use:
+--
+--   @
+--   instance 'Weaken' Pred1 Pred2
+--   @
+--
+--   For most of the instances, explicit type annotations for
+--   the result value's type might be required.
+--
+-- @since 0.2.0.0
+class Weaken from to where
+  -- | @since 0.2.0.0
+  weaken :: Refined from x -> Refined to x
+  weaken = coerce
+
+-- | @since 0.2.0.0
+instance (n <= m)         => Weaken (LessThan n)        (LessThan m)
+-- | @since 0.2.0.0
+instance (n <= m)         => Weaken (LessThan n)        (To m)
+-- | @since 0.2.0.0
+instance (n <= m)         => Weaken (To n)              (To m)
+-- | @since 0.2.0.0
+instance (m <= n)         => Weaken (GreaterThan n)     (GreaterThan m)
+-- | @since 0.2.0.0
+instance (m <= n)         => Weaken (GreaterThan n)     (From m)
+-- | @since 0.2.0.0
+instance (m <= n)         => Weaken (From n)            (From m)
+-- | @since 0.2.0.0
+instance (p <= n, m <= q) => Weaken (FromTo n m)        (FromTo p q)
+-- | @since 0.2.0.0
+instance (p <= n)         => Weaken (FromTo n m)        (From p)
+-- | @since 0.2.0.0
+instance (m <= q)         => Weaken (FromTo n m)        (To q)
+-- | @since 0.8.1
+instance (n <= m)         => Weaken (SizeLessThan n)    (SizeLessThan m)
+-- | @since 0.8.1
+instance (m <= n)         => Weaken (SizeGreaterThan n) (SizeGreaterThan m)
+
+-- | This function helps type inference.
+--   It is equivalent to the following:
+--
+-- @
+-- instance Weaken (And l r) l
+-- @
+--
+--   @since 0.2.0.0
+andLeft :: Refined (And l r) x -> Refined l x
+andLeft = coerce
+
+-- | This function helps type inference.
+--   It is equivalent to the following:
+--
+-- @
+-- instance Weaken (And l r) r
+-- @
+--
+--   @since 0.2.0.0
+andRight :: Refined (And l r) x -> Refined r x
+andRight = coerce
+
+-- | This function helps type inference.
+--   It is equivalent to the following:
+--
+-- @
+-- instance Weaken l (Or l r)
+-- @
+--
+--   @since 0.2.0.0
+leftOr :: Refined l x -> Refined (Or l r) x
+leftOr = coerce
+
+-- | This function helps type inference.
+--   It is equivalent to the following:
+--
+-- @
+-- instance Weaken r (Or l r)
+-- @
+--
+--   @since 0.2.0.0
+rightOr :: Refined r x -> Refined (Or l r) x
+rightOr = coerce
+
+-- | This function helps type inference.
+--   It is equivalent to the following:
+--
+-- @
+-- instance Weaken from to => Weaken (And from x) (And to x)
+-- @
+--
+--   @since 0.8.1.0
+weakenAndLeft :: Weaken from to => Refined (And from x) a -> Refined (And to x) a
+weakenAndLeft = coerce
+
+-- | This function helps type inference.
+--   It is equivalent to the following:
+--
+-- @
+-- instance Weaken from to => Weaken (And x from) (And x to)
+-- @
+--
+--   @since 0.8.1.0
+weakenAndRight :: Weaken from to => Refined (And x from) a -> Refined (And x to) a
+weakenAndRight = coerce
+
+-- | This function helps type inference.
+--   It is equivalent to the following:
+--
+-- @
+-- instance Weaken from to => Weaken (Or from x) (Or to x)
+-- @
+--
+--   @since 0.9.0.0
+weakenOrLeft :: Weaken from to => Refined (Or from x) a -> Refined (Or to x) a
+weakenOrLeft = coerce
+
+-- | This function helps type inference.
+--   It is equivalent to the following:
+--
+-- @
+-- instance Weaken from to => Weaken (Or x from) (Or x to)
+-- @
+--
+--   @since 0.9.0.0
+weakenOrRight :: Weaken from to => Refined (Or x from) a -> Refined (Or x to) a
+weakenOrRight = coerce
+
+-- | Strengthen a refinement by composing it with another.
+--
+--   @since 0.4.2.2
+strengthen :: forall p p' x. (Predicate p x, Predicate p' x)
+  => Refined p x
+  -> Either RefineException (Refined (p && p') x)
+strengthen r = do
+  Refined x <- refine @p' @x (unrefine r)
+  pure (Refined x)
+{-# inlineable strengthen #-}
+
+--------------------------------------------------------------------------------
+
+-- | An exception encoding the way in which a 'Predicate' failed.
+--
+--   @since 0.2.0.0
+data RefineException
+  = -- | A 'RefineException' for failures involving the 'Not' predicate.
+    --
+    --   @since 0.2.0.0
+    RefineNotException
+    { _RefineException_typeRep   :: !TypeRep
+      -- ^ The 'TypeRep' of the @'Not' p@ type.
+    }
+
+  | -- | A 'RefineException' for failures involving the 'And' predicate.
+    --
+    --   @since 0.2.0.0
+    RefineAndException
+    { _RefineException_typeRep   :: !TypeRep
+      -- ^ The 'TypeRep' of the @'And' l r@ type.
+    , _RefineException_andChild  :: !(These RefineException RefineException)
+      -- ^ A 'These' encoding which branch(es) of the 'And' failed:
+      --   if the 'RefineException' came from the @l@ predicate, then
+      --   this will be 'This', if it came from the @r@ predicate, this
+      --   will be 'That', and if it came from both @l@ and @r@, this
+      --   will be 'These'.
+
+      -- note to self: what am I, Dr. Seuss?
+    }
+
+  | -- | A 'RefineException' for failures involving the 'Or' predicate.
+    --
+    --   @since 0.2.0.0
+    RefineOrException
+    { _RefineException_typeRep   :: !TypeRep
+      -- ^ The 'TypeRep' of the @'Or' l r@ type.
+    , _RefineException_orLChild  :: !RefineException
+      -- ^ The 'RefineException' for the @l@ failure.
+    , _RefineException_orRChild  :: !RefineException
+      -- ^ The 'RefineException' for the @l@ failure.
+    }
+
+  | -- | A 'RefineException' for failures involving the 'Xor' predicate.
+    --
+    --   @since 0.5
+    RefineXorException
+    { _RefineException_typeRep   :: !TypeRep
+    , _RefineException_children  :: !(Maybe (RefineException, RefineException))
+    }
+
+  | -- | A 'RefineException' for failures involving all other predicates with custom exception.
+    --
+    --   @since 0.5
+    RefineSomeException
+    { _RefineException_typeRep   :: !TypeRep
+      -- ^ The 'TypeRep' of the predicate that failed.
+    , _RefineException_Exception :: !SomeException
+      -- ^ A custom exception.
+    }
+
+  | -- | A 'RefineException' for failures involving all other predicates.
+    --
+    --   @since 0.2.0.0
+    RefineOtherException
+    { _RefineException_typeRep   :: !TypeRep
+      -- ^ The 'TypeRep' of the predicate that failed.
+    , _RefineException_message   :: !Text
+      -- ^ A custom message to display.
+    }
+  deriving
+    ( Generic -- ^ @since 0.3.0.0
+    )
+
+-- | /Note/: Equivalent to @'displayRefineException'@.
+--
+--   @since 0.2.0.0
+instance Show RefineException where
+  show = displayRefineException
+
+-- | A Tree which is a bit easier to pretty-print
+--   TODO: get rid of this
+data ExceptionTree a
+  = NodeNone
+  | NodeSome !TypeRep SomeException
+  | NodeOther !TypeRep !Text
+  | NodeNot !TypeRep
+  | NodeOr !TypeRep [ExceptionTree a]
+  | NodeAnd !TypeRep [ExceptionTree a]
+  | NodeXor !TypeRep [ExceptionTree a]
+
+-- | pretty-print an 'ExceptionTree', contains a hack to
+--   work differently whether or not you are "inGhc", i.e.
+--   inside of refineTH/refineTH_ (because GHC messes with
+--   the indentation)
+showTree :: Bool -> ExceptionTree RefineException -> String
+showTree inGhc
+  | inGhc = showOne "" "" ""
+      .> mapOnTail (indent 6)
+      .> unlines
+  | otherwise = showOne "  " "" "" .> unlines
+  where
+    mapOnTail :: (a -> a) -> [a] -> [a]
+    mapOnTail f = \case
+      [] -> []
+      (a : as) -> a : map f as
+
+    indent :: Int -> String -> String
+    indent n s = replicate n ' ' ++ s
+
+    showOne :: String -> String -> String -> ExceptionTree RefineException -> [String]
+    showOne leader tie arm = \case
+      NodeNone ->
+        [
+        ]
+      NodeSome tr e ->
+        [ leader
+          <> arm
+          <> tie
+          <> "The predicate ("
+          <> show tr
+          <> ") failed with the exception: "
+          <> displayException e
+        ]
+      NodeOther tr p ->
+        [ leader
+          <> arm
+          <> tie
+          <> "The predicate ("
+          <> show tr
+          <> ") failed with the message: "
+          <> Text.unpack p
+        ]
+      NodeNot tr ->
+        [ leader
+          <> arm
+          <> tie
+          <> "The predicate ("
+          <> show tr
+          <> ") does not hold"
+        ]
+      NodeOr tr rest -> nodeRep tr : showChildren rest (leader <> extension)
+      NodeAnd tr rest -> nodeRep tr : showChildren rest (leader <> extension)
+      -- can be empty since both can be satisfied
+      NodeXor tr [] ->
+        [ leader
+          <> arm
+          <> tie
+          <> "The predicate ("
+          <> show tr
+          <> ") does not hold, because both predicates were satisfied"
+        ]
+      NodeXor tr rest -> nodeRep tr : showChildren rest (leader <> extension)
+      where
+        nodeRep :: TypeRep -> String
+        -- TODO: make tr bold
+        nodeRep tr = leader <> arm <> tie <> show tr
+
+        extension :: String
+        extension = case arm of
+          ""  -> ""
+          "└" -> "    "
+          _   -> "│   "
+
+    showChildren :: [ExceptionTree RefineException] -> String -> [String]
+    showChildren children leader =
+      let arms = replicate (length children - 1) "├" <> ["└"]
+      in concat (zipWith (showOne leader "── ") arms children)
+
+refineExceptionToTree :: RefineException -> ExceptionTree RefineException
+refineExceptionToTree = go
+  where
+    go = \case
+      RefineSomeException tr e -> NodeSome tr e
+      RefineOtherException tr p -> NodeOther tr p
+      RefineNotException tr -> NodeNot tr
+      RefineOrException tr l r -> NodeOr tr [go l, go r]
+      RefineAndException tr (This l) -> NodeAnd tr [go l]
+      RefineAndException tr (That r) -> NodeAnd tr [go r]
+      RefineAndException tr (These l r) -> NodeAnd tr [go l, go r]
+      RefineXorException tr Nothing -> NodeXor tr []
+      RefineXorException tr (Just (l, r)) -> NodeXor tr [go l, go r]
+
+-- | Display a 'RefineException' as @'String'@
+--
+--   This function can be extremely useful for debugging
+--   @'RefineException's@, especially deeply nested ones.
+--
+--   Consider:
+--
+--   @
+--   myRefinement = refine
+--     \@(And
+--         (Not (LessThan 5))
+--         (Xor
+--           (DivisibleBy 10)
+--           (And
+--             (EqualTo 4)
+--             (EqualTo 3)
+--           )
+--         )
+--      )
+--     \@Int
+--     3
+--   @
+--
+--   This function will show the following tree structure, recursively breaking down
+--   every issue:
+--
+--   @
+--   And (Not (LessThan 5)) (Xor (EqualTo 4) (And (EqualTo 4) (EqualTo 3)))
+--   ├── The predicate (Not (LessThan 5)) does not hold.
+--   └── Xor (DivisibleBy 10) (And (EqualTo 4) (EqualTo 3))
+--       ├── The predicate (DivisibleBy 10) failed with the message: Value is not divisible by 10
+--       └── And (EqualTo 4) (EqualTo 3)
+--           └── The predicate (EqualTo 4) failed with the message: Value does not equal 4
+--   @
+--
+--   /Note/: Equivalent to @'show' \@'RefineException'@
+--
+--   @since 0.2.0.0
+displayRefineException :: RefineException -> String
+displayRefineException = refineExceptionToTree .> showTree False
+
+-- | Encode a 'RefineException' for use with \Control.Exception\.
+--
+--   /Note/: Equivalent to @'displayRefineException'@.
+--
+--   @since 0.2.0.0
+instance Exception RefineException where
+  displayException = show
+
+--------------------------------------------------------------------------------
+
+-- | A handler for a @'RefineException'@.
+--
+--   'throwRefineOtherException' is useful for defining what
+--   behaviour 'validate' should have in the event of a predicate failure.
+--
+--   Typically the first argument passed to this function
+--   will be the result of applying 'typeRep' to the first
+--   argument of 'validate'.
+--
+--   @since 0.2.0.0
+throwRefineOtherException
+  :: TypeRep
+  -- ^ The 'TypeRep' of the 'Predicate'. This can usually be given by using 'typeRep'.
+  -> Text
+  -- ^ A 'PP.Doc' 'Void' encoding a custom error message to be pretty-printed.
+  -> Maybe RefineException
+throwRefineOtherException rep
+  = RefineOtherException rep .> Just
+
+-- | A handler for a @'RefineException'@.
+--
+--   'throwRefineSomeException' is useful for defining what
+--   behaviour 'validate' should have in the event of a predicate failure
+--   with a specific exception.
+--
+--   @since 0.5
+throwRefineSomeException
+  :: TypeRep
+  -- ^ The 'TypeRep' of the 'Predicate'. This can usually be given by using 'typeRep'.
+  -> SomeException
+  -- ^ A custom exception.
+  -> Maybe RefineException
+throwRefineSomeException rep
+  = RefineSomeException rep .> Just
+
+-- | An implementation of 'validate' that always succeeds.
+--
+--   ==== __Examples__
+--
+--   @
+--   data ContainsLetterE = ContainsLetterE
+--
+--   instance Predicate ContainsLetterE 'Text' where
+--     validate p t
+--       | 'Data.Text.any' (== \'e\') t = 'success'
+--       | otherwise = Just $ 'throwRefineException' (typeRep p) "Text doesn't contain letter \'e\'".
+--   @
+--
+--   @since 0.5
+success
+  :: Maybe RefineException
+success
+  = Nothing
+
+--------------------------------------------------------------------------------
+
+-- | Helper function for sized predicates.
+sized :: forall p n a. (Typeable (p n), KnownNat n)
+  => Proxy (p n)
+     -- ^ predicate
+  -> (a, Text)
+     -- ^ (value, type)
+  -> (a -> Int)
+     -- ^ length of value
+  -> (Int -> Int -> Bool, Text)
+     -- ^ (compare :: Length -> KnownNat -> Bool, comparison string)
+  -> Maybe RefineException
+sized p (x, typ) lenF (cmp, cmpDesc) = do
+  let x' = fromIntegral (nv @n)
+  let sz = lenF x
+  if cmp sz x'
+  then Nothing
+  else
+    let msg =
+          [ "Size of ", typ, " is not ", cmpDesc, " "
+          , i2text x'
+          , ". "
+          , "Size is: "
+          , i2text sz
+          ] |> mconcat
+    in throwRefineOtherException (typeRep p) msg
+
+-- helper function to make sure natVal calls are
+-- zero runtime overhead
+nv :: forall n. KnownNat n => Integer
+nv = natVal' (proxy# :: Proxy# n)
+
+-- convert an Integral number to Text
+--
+-- todo: use toLazyTextWith, providing a tiny buffer size
+i2text :: Integral a => a -> Text
+i2text = TextBuilder.decimal
+  .> TextBuilder.toLazyText
+  .> TextLazy.toStrict
+{-# SPECIALISE i2text :: Int -> Text #-}
+{-# SPECIALISE i2text :: Integer -> Text #-}
diff --git a/refined/Refined/Unsafe.hs b/refined/Refined/Unsafe.hs
new file mode 100644
--- /dev/null
+++ b/refined/Refined/Unsafe.hs
@@ -0,0 +1,138 @@
+--------------------------------------------------------------------------------
+
+-- Copyright © 2015 Nikita Volkov
+-- Copyright © 2018 Remy Goldschmidt
+-- Copyright © 2020 chessai
+--
+-- 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.
+
+--------------------------------------------------------------------------------
+
+{-# LANGUAGE CPP #-}
+{-# LANGUAGE FlexibleContexts #-}
+{-# LANGUAGE PolyKinds #-}
+#if __GLASGOW_HASKELL__ >= 805
+{-# LANGUAGE QuantifiedConstraints #-}
+{-# LANGUAGE RankNTypes #-}
+#endif
+{-# OPTIONS_GHC -Wall #-}
+
+--------------------------------------------------------------------------------
+
+-- | This module exposes /unsafe/ refinements. An /unsafe/ refinement
+--   is one which either does not make the guarantee of totality in construction
+--   of the 'Refined' value or does not perform a check of the refinement
+--   predicate. It is recommended only to use this when you can manually prove
+--   that the refinement predicate holds.
+module Refined.Unsafe
+  ( -- * 'Refined'
+    Refined
+  , Refined1
+
+    -- ** Creation
+  , reallyUnsafeRefine
+  , reallyUnsafeRefine1
+  , unsafeRefine
+
+    -- ** Coercion
+  , reallyUnsafeUnderlyingRefined
+#if __GLASGOW_HASKELL__ >= 805
+  , reallyUnsafeAllUnderlyingRefined
+#endif
+  , reallyUnsafePredEquiv
+  ) where
+
+--------------------------------------------------------------------------------
+
+import           Control.Exception            (displayException)
+import           Data.Coerce                  (coerce)
+
+import           Refined                      (Predicate, refine)
+import           Refined.Unsafe.Type          (Refined(Refined), Refined1(Refined1))
+import           Data.Type.Coercion           (Coercion (..))
+#if __GLASGOW_HASKELL__ >= 805
+import           Data.Coerce                  (Coercible)
+#endif
+
+--------------------------------------------------------------------------------
+
+-- | Constructs a 'Refined' value at run-time,
+--   calling 'Prelude.error' if the value
+--   does not satisfy the predicate.
+--
+--   WARNING: this function is not total!
+--
+--   @since 0.2.0.0
+unsafeRefine :: (Predicate p x) => x -> Refined p x
+unsafeRefine = either (error . displayException) id . refine
+{-# INLINABLE unsafeRefine #-}
+
+-- | Constructs a 'Refined' value, completely
+--   ignoring any refinements! Use this only
+--   when you can manually prove that the refinement
+--   holds.
+--
+--   @since 0.3.0.0
+reallyUnsafeRefine :: x -> Refined p x
+reallyUnsafeRefine = coerce
+{-# INLINE reallyUnsafeRefine #-}
+
+reallyUnsafeRefine1 :: f x -> Refined1 p f x
+reallyUnsafeRefine1 = coerce
+{-# INLINE reallyUnsafeRefine1 #-}
+
+-- | A coercion between a type and any refinement of that type.
+--   See "Data.Type.Coercion" for functions manipulating
+--   coercions.
+--
+--   @since 0.3.0.0
+reallyUnsafeUnderlyingRefined :: Coercion x (Refined p x)
+reallyUnsafeUnderlyingRefined = Coercion
+
+-- | A coercion between two 'Refined' types, magicking up the
+--   claim that one predicate is entirely equivalent to another.
+--
+--   @since 0.3.0.0
+reallyUnsafePredEquiv :: Coercion (Refined p x) (Refined q x)
+reallyUnsafePredEquiv = Coercion
+-- Note: reallyUnsafePredEquiv =
+-- sym 'reallyUnsafeUnderlyingRefined' `trans` 'reallyUnsafeUnderlyingRefined'
+
+#if __GLASGOW_HASKELL__ >= 805
+-- | Reveal that @x@ and @'Refined' p x@ are 'Coercible' for
+-- /all/ @x@ and @p@ simultaneously.
+--
+-- === Example
+--
+-- @
+-- reallyUnsafePredEquiv :: Coercion (Refined p x) (Refined q x)
+-- reallyUnsafePredEquiv = reallyUnsafeAllUnderlyingRefined Coercion
+-- @
+--
+--   @since 0.3.0.0
+reallyUnsafeAllUnderlyingRefined
+  :: ((forall x y p. (Coercible x y => Coercible y (Refined p x))) => r) -> r
+-- Why is this constraint so convoluted? Because otherwise the constraint
+-- solver doesn't handle transitivity properly. See "Safe Zero-cost Coercions
+-- for Haskell" by Breitner et al.
+reallyUnsafeAllUnderlyingRefined r = r
+#endif
diff --git a/refined/Refined/Unsafe/Type.hs b/refined/Refined/Unsafe/Type.hs
new file mode 100644
--- /dev/null
+++ b/refined/Refined/Unsafe/Type.hs
@@ -0,0 +1,114 @@
+--------------------------------------------------------------------------------
+
+-- Copyright © 2015 Nikita Volkov
+-- Copyright © 2018 Remy Goldschmidt
+-- Copyright © 2020 chessai
+--
+-- 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.
+
+--------------------------------------------------------------------------------
+
+{-# LANGUAGE CPP                        #-}
+{-# LANGUAGE DeriveDataTypeable         #-}
+{-# LANGUAGE DeriveFoldable             #-}
+{-# LANGUAGE DeriveTraversable          #-}
+{-# LANGUAGE DerivingStrategies         #-}
+{-# LANGUAGE GeneralizedNewtypeDeriving #-}
+{-# LANGUAGE PolyKinds                  #-}
+{-# LANGUAGE RoleAnnotations            #-}
+{-# LANGUAGE TemplateHaskell            #-}
+
+--------------------------------------------------------------------------------
+
+-- | This module exports the 'Refined' type with its
+--   constructor. This is very risky! In particular, the 'Data.Coerce.Coercible'
+--   instances will be visible throughout the importing module.
+--   It is usually better to build the necessary coercions locally
+--   using the utilities in "Refined.Unsafe", but in some cases
+--   it may be more convenient to write a separate module that
+--   imports this one and exports some large coercion.
+module Refined.Unsafe.Type
+  ( Refined(Refined)
+  , Refined1(Refined1)
+  ) where
+
+import           Data.Data                    (Data)
+import           Control.DeepSeq              (NFData)
+import           Data.Hashable (Hashable)
+import qualified Language.Haskell.TH.Syntax   as TH
+
+-- | A refinement type, which wraps a value of type @x@.
+--
+--   @since 0.1.0.0
+newtype Refined (p :: k) x
+  = Refined x -- ^ @since 0.1.0.0
+  deriving newtype
+    ( Eq -- ^ @since 0.1.0.0
+    , Ord -- ^ @since 0.1.0.0
+    , Hashable -- ^ @since 0.6.3
+    , NFData -- ^ @since 0.5
+    )
+  deriving stock
+    ( Show -- ^ @since 0.1.0.0
+    )
+  deriving stock
+    ( Foldable -- ^ @since 0.2
+    , Data -- ^ @since 0.8.3
+    )
+
+-- | @since 0.3.0.0
+type role Refined nominal nominal
+
+-- | @since 0.1.0.0
+instance (TH.Lift x) => TH.Lift (Refined p x) where
+  lift (Refined a) = [|Refined a|]
+#if MIN_VERSION_template_haskell(2,16,0)
+  liftTyped (Refined a) = [||Refined a||]
+#endif
+
+-- | A refinement type, which wraps a value of type @f x@.
+--
+-- The predicate is applied over the functor @f@. Thus, we may safely recover
+-- various 'Functor'y instances, because no matter what you do to the
+-- values inside the functor, the predicate may not be invalidated.
+newtype Refined1 (p :: k) f x
+  = Refined1 (f x)
+  deriving newtype
+    ( Eq
+    , Ord
+    , Hashable
+    , NFData
+    , Functor
+    , Foldable
+    )
+  deriving stock
+    ( Show
+    , Traversable
+    )
+
+type role Refined1 nominal nominal nominal
+
+instance TH.Lift (f a) => TH.Lift (Refined1 p f a) where
+  lift (Refined1 fa) = [|Refined1 fa|]
+#if MIN_VERSION_template_haskell(2,16,0)
+  liftTyped (Refined1 fa) = [||Refined1 fa||]
+#endif
diff --git a/sandbox-effect/CallSpecs/CpManyToDir.hs b/sandbox-effect/CallSpecs/CpManyToDir.hs
new file mode 100644
--- /dev/null
+++ b/sandbox-effect/CallSpecs/CpManyToDir.hs
@@ -0,0 +1,15 @@
+-- {-# OPTIONS_GHC -ddump-splices #-}
+{-# LANGUAGE TemplateHaskell #-}
+module CallSpecs.CpManyToDir where
+
+import System.Process.Quick
+import System.Process.Quick.Prelude
+
+$(genCallSpec
+  [TrailingHelpValidate, SandboxValidate]
+  "cp"
+  (   VarArg @(Refined (InFile "hs") (NeList FilePath)) "source"
+  .*. VarArg @(Refined InDir FilePath) "destination"
+  .*. HNil
+  )
+ )
diff --git a/sandbox-effect/CallSpecs/CpOne.hs b/sandbox-effect/CallSpecs/CpOne.hs
new file mode 100644
--- /dev/null
+++ b/sandbox-effect/CallSpecs/CpOne.hs
@@ -0,0 +1,15 @@
+-- {-# OPTIONS_GHC -ddump-splices #-}
+{-# LANGUAGE TemplateHaskell #-}
+module CallSpecs.CpOne where
+
+import System.Process.Quick
+import System.Process.Quick.Prelude
+
+$(genCallSpec
+  [TrailingHelpValidate, SandboxValidate]
+  "cp"
+  (   VarArg @(Refined (InFile "hs") FilePath) "source"
+  .*. VarArg @(Refined (OutFile "*") FilePath) "destination"
+  .*. HNil
+  )
+ )
diff --git a/sandbox-effect/CallSpecs/Date.hs b/sandbox-effect/CallSpecs/Date.hs
new file mode 100644
--- /dev/null
+++ b/sandbox-effect/CallSpecs/Date.hs
@@ -0,0 +1,13 @@
+{-# LANGUAGE TemplateHaskell #-}
+module CallSpecs.Date where
+
+import System.Process.Quick
+import System.Process.Quick.Prelude
+
+$(genCallSpec
+  [TrailingHelpValidate, SandboxValidate]
+  "date"
+  (   VarArg @(Refined (Regex "^[+][%][YmHdZ]$") String) "format"
+  .*. HNil
+  )
+ )
diff --git a/sandbox-effect/CallSpecs/FindCases.hs b/sandbox-effect/CallSpecs/FindCases.hs
new file mode 100644
--- /dev/null
+++ b/sandbox-effect/CallSpecs/FindCases.hs
@@ -0,0 +1,22 @@
+{-# LANGUAGE OverloadedStrings #-}
+{-# LANGUAGE TemplateHaskell #-}
+module CallSpecs.FindCases where
+
+import System.Process.Quick
+import System.Process.Quick.Prelude
+
+
+$(genCallSpec
+  [TrailingHelpValidate, SandboxValidate]
+  "find"
+  (   ConstArg "."
+  .*. Subcases
+        "FindCases"
+        [ Subcase "FindPrintf"
+          (KeyArg @(Refined (Regex "^[%][fpactbnM%]$") String) "-printf" .*. HNil)
+        , Subcase "FindExec"
+          (KeyArg @(Refined (Regex "^(ls|file|du)$") String) "-exec" .*. ConstArg "{}" .*. ConstArg ";" .*. HNil)
+        ]
+  .*. HNil
+  )
+ )
diff --git a/sandbox-effect/SandBoxEffect.hs b/sandbox-effect/SandBoxEffect.hs
new file mode 100644
--- /dev/null
+++ b/sandbox-effect/SandBoxEffect.hs
@@ -0,0 +1,14 @@
+{-# LANGUAGE NoOverloadedStrings #-}
+module SandBoxEffect where
+
+import CallSpecs.CpOne ()
+import CallSpecs.CpManyToDir ()
+import CallSpecs.Date
+import CallSpecs.FindCases ()
+import System.Process.Quick
+import System.Process.Quick.Prelude
+
+main :: IO ()
+main = do
+  $(discoverAndVerifyCallSpecs (fromList [SandboxValidate]) 1)
+  callProcess $ Date $$(refineTH "+%Y")
diff --git a/src/System/Process/Quick.hs b/src/System/Process/Quick.hs
new file mode 100644
--- /dev/null
+++ b/src/System/Process/Quick.hs
@@ -0,0 +1,14 @@
+module System.Process.Quick (module M) where
+
+import Data.HList as M (HList(..), (.*.))
+import Refined as M
+import System.Process.Quick.CallArgument as M
+import System.Process.Quick.CallSpec as M
+import System.Process.Quick.CallSpec.Run as M
+import System.Process.Quick.CallSpec.Subcases as M
+import System.Process.Quick.CallSpec.Verify as M
+import System.Process.Quick.Predicate as M
+import System.Process.Quick.Predicate.InDir as M (InDir)
+import System.Process.Quick.Predicate.InFile as M (OutFile, InFile)
+import System.Process.Quick.Predicate.LowerCase as M
+import System.Process.Quick.Predicate.Regex as M
diff --git a/src/System/Process/Quick/CallArgument.hs b/src/System/Process/Quick/CallArgument.hs
new file mode 100644
--- /dev/null
+++ b/src/System/Process/Quick/CallArgument.hs
@@ -0,0 +1,116 @@
+module System.Process.Quick.CallArgument where
+
+import Control.Monad.Writer.Strict
+import Data.HList
+import Language.Haskell.TH as TH
+import Refined as M hiding (NonEmpty)
+import System.Process.Quick.OrphanArbitrary ()
+import System.Process.Quick.Prelude hiding (Text)
+import TH.Utilities qualified as TU
+
+class Arbitrary a => CallArgument a where
+  toExecString :: a -> [String]
+  default toExecString :: Show a => a -> [String]
+  toExecString = (:[]) . show
+
+instance CallArgument a => CallArgument (Maybe a) where
+  toExecString = maybe [] toExecString
+instance (CallArgument a, CallArgument b) => CallArgument (Either a b) where
+  toExecString = \case
+    Left x -> toExecString x
+    Right x -> toExecString x
+instance CallArgument Int
+instance CallArgument Integer
+instance CallArgument Double
+instance CallArgument Float
+instance CallArgument Word
+instance CallArgument Bool
+instance CallArgument () where
+  toExecString _ = []
+
+-- | Disambiguate 'Refined.NonEmpty'
+type NeList = NonEmpty
+
+instance CallArgument a => CallArgument (NonEmpty a) where
+  toExecString = concatMap toExecString
+
+instance CallArgument a => CallArgument [a] where
+  toExecString = concatMap toExecString
+instance {-# OVERLAPPING #-} CallArgument String where
+  toExecString = (:[])
+
+instance (Typeable a, Predicate c a, CallArgument a) => CallArgument (Refined c a) where
+  toExecString = toExecString . unrefine
+
+newtype QR a
+  = QR { unQR :: WriterT [Dec] Q a }
+  deriving (Functor, Applicative, Monad, MonadFail, MonadWriter [Dec])
+
+instance Quote QR where
+  newName n = QR $ lift (newName n)
+
+class (Typeable a) => CallArgumentGen a where
+  -- | field name in the record; constant value does not have a field
+  cArgName :: a -> Maybe String
+  -- | lambda expression projecting a call argument in CallSpec record to a list of strings
+  -- Exp type is '\v -> [String]'
+  progArgExpr :: a -> QR Exp
+  -- | TH field definition of call argument in CallSpec record
+  fieldExpr :: a -> QR (Maybe VarBangType)
+
+newtype ConstArg = ConstArg String deriving (Eq, Show, Typeable)
+instance CallArgumentGen ConstArg where
+  cArgName _ = Nothing
+  progArgExpr (ConstArg c) = [| const [ $(stringE c)] |]
+  fieldExpr _ = pure Nothing
+
+defaultBang :: Bang
+defaultBang = Bang NoSourceUnpackedness NoSourceStrictness
+
+nameE :: String -> Q Exp
+nameE = varE . mkName . escapeFieldName
+
+isValidFirstFieldLetter :: Char -> Bool
+isValidFirstFieldLetter c = isLetter c || c == '_'
+
+isValidFieldLetter :: Char -> Bool
+isValidFieldLetter c = isAlphaNum c || c == '_' || c == '\''
+
+haskellKeyword :: Set String
+haskellKeyword = fromList [ "type", "module", "import", "where", "class", "case", "in", "of" ]
+
+mapFirst :: (a -> a) -> [a] -> [a]
+mapFirst _ [] = []
+mapFirst f (h:t) = f h : t
+
+escapeFieldName :: String -> String
+escapeFieldName = \case
+  [] -> error "Empty field name"
+  (h:t) ->
+    case filter isValidFirstFieldLetter [h] ++ filter isValidFieldLetter t of
+      [] -> error "Field name " <> show (h:t) <> " is empty after filtration"
+      "type" -> "type'"
+      "mo" -> "type'"
+      filteredFieldName
+        | filteredFieldName `member` haskellKeyword -> filteredFieldName <> "'"
+        | otherwise -> filteredFieldName
+
+-- | Command line argument without preceeding key
+newtype VarArg a = VarArg String deriving (Eq, Show, Typeable)
+instance (Typeable a, CallArgument a) => CallArgumentGen (VarArg a) where
+  cArgName (VarArg n) = Just n
+  progArgExpr (VarArg fieldName) =
+    QR $ lift [| toExecString . $(nameE fieldName) |]
+
+  fieldExpr (VarArg fieldName) =
+    Just . (mkName $ escapeFieldName fieldName, defaultBang,) <$> atRep
+    where
+      atRep = QR . lift $ TU.typeRepToType (typeRep (Proxy @a))
+
+-- | Command line argument prefixed with a key
+newtype KeyArg a = KeyArg String deriving (Eq, Show, Typeable)
+instance (Typeable a, CallArgument a) => CallArgumentGen (KeyArg a) where
+  cArgName (KeyArg n) = cArgName (VarArg @a n)
+  progArgExpr (KeyArg fieldName) =
+    [| \x -> $(progArgExpr (ConstArg fieldName)) x <> $(progArgExpr (VarArg @a fieldName)) x |]
+  fieldExpr (KeyArg fieldName) = fieldExpr (VarArg @a fieldName)
diff --git a/src/System/Process/Quick/CallEffect.hs b/src/System/Process/Quick/CallEffect.hs
new file mode 100644
--- /dev/null
+++ b/src/System/Process/Quick/CallEffect.hs
@@ -0,0 +1,59 @@
+module System.Process.Quick.CallEffect where
+
+import System.Posix
+import System.Process.Quick.Prelude
+import Text.Regex.TDFA
+import Prelude (Show (..))
+
+data TimeReference
+  = LaunchTime
+  | BootTime
+  | ExitTime
+  | Now
+  deriving (Show, Eq, Ord)
+
+data FsPredicate
+  = FsExists
+  | DirStructMatches FsEffect
+  | FsPathHasPerm FileMode -- ^ AND
+  | FsTime Ordering TimeReference
+  deriving (Show, Eq)
+
+data FsEffect
+  = FsPathPredicate FilePath [FsPredicate]
+  | FsNot FsEffect
+  | FsAnd [FsEffect]
+  | FsOr [FsEffect]
+  deriving (Show, Eq)
+
+data ViRex = ViRex ByteString Regex
+
+instance Show ViRex where
+  show (ViRex bs _) = Prelude.show bs
+
+instance Eq ViRex where
+  (ViRex a _) == (ViRex b _) = a == b
+
+data OutMatcher
+  = ExactMatching ByteString
+  | WholeMatching ViRex -- read all input
+  | LineMatching ViRex -- consume file line by line - at least one line match
+  deriving (Show, Eq)
+
+data CallEffect
+  = SleepFor Integer -- call lasts at least N microseconds
+  | ExitCode Int -- expected exit code
+  | FsEffect FsEffect
+  | OrCe [CallEffect]
+  | AndCe [CallEffect]
+  | NotCe [CallEffect]
+  | StdOutputCe OutMatcher
+  | StdErrorCe OutMatcher
+  deriving (Show, Eq)
+
+-- | instances are generated for types with CallSpec and Subcases
+-- The class is introduced because,
+-- expected effects don't have fields in a CallSpec record
+class CallSpecEffect cse where
+  -- call after callSpec in the same directory
+  unsatisfiedEffects :: MonadIO m => cse -> m [CallEffect]
diff --git a/src/System/Process/Quick/CallSpec.hs b/src/System/Process/Quick/CallSpec.hs
new file mode 100644
--- /dev/null
+++ b/src/System/Process/Quick/CallSpec.hs
@@ -0,0 +1,82 @@
+module System.Process.Quick.CallSpec
+  ( FoldrConstr
+  , genCallSpec
+  , genArbitraryInstance
+  , dataD'
+  , seqA
+  , programNameToHsIdentifier
+  , module E
+  ) where
+
+import Control.Monad.Writer.Strict
+import Data.HList
+import Language.Haskell.TH as TH
+import Language.Haskell.TH.Syntax qualified as THS
+import System.Directory
+import System.Process.Quick.CallArgument
+import System.Process.Quick.CallSpec.Type as E
+import System.Process.Quick.Prelude
+import Text.Casing
+import Text.Regex
+
+type FoldrConstr l a = (HFoldr (Mapcar (Fun CallArgumentGen (QR a))) [QR a] l [QR a])
+
+dataD' :: Quote m => Name -> [m Con] -> [m DerivClause] -> m Dec
+dataD' name = dataD (pure []) name [] Nothing
+
+genCallArgsRecord :: (Show (HList l), FoldrConstr l (Maybe VarBangType)) => Name -> HList l -> QR Dec
+genCallArgsRecord recordName l = do
+  fields <- seqA $ catMaybes <$> sequence (hMapM fieldDef l)
+  dataD' recordName [recC recordName fields]
+    [derivClause Nothing [[t|Data|], [t|Generic|], [t|Show|], [t|Eq|]]]
+  where
+    fieldDef = Fun fieldExpr :: Fun CallArgumentGen (QR (Maybe VarBangType))
+
+funD' :: Quote m => Name -> [m Pat] -> m Exp -> m Dec
+funD' fname fparams fbody =
+  funD fname [clause fparams (normalB fbody) []]
+
+type NonEmptyStr = NonEmpty Char
+
+programNameToHsIdentifier :: String -> Maybe (NonEmpty Char)
+programNameToHsIdentifier = nonEmpty . toPascal . fromSnake . underbarred
+  where
+    underbarred s = subRegex (mkRegex "[^A-Za-z0-9_]") s "_"
+
+seqA :: Monad m => m [a] -> m [m a]
+seqA = (fmap pure <$>)
+
+genArbitraryInstance :: Name -> QR Dec
+genArbitraryInstance recordName =
+  instanceD (pure []) [t| Arbitrary $(conT recordName) |]
+    [ funD' 'arbitrary [] [| genericArbitraryU |]
+    ]
+
+genCallSpecInstance :: FoldrConstr l Exp => [VerificationMethod] -> Name -> String -> HList l -> QR Dec
+genCallSpecInstance verMethods recordName progName l =
+  instanceD (pure []) [t| CallSpec $(conT recordName) |]
+  [ funD' 'programName [ [p|_|] ] [| $(stringE progName) |]
+  , funD' 'programArgs []
+      [| concat . flap $(listE (hMapM (Fun progArgExpr :: Fun CallArgumentGen (QR Exp)) l)) |]
+  , funD' 'verificationMethods [ [p|_|] ] (THS.lift $ sort verMethods)
+  ]
+
+mkName' :: NonEmptyStr -> Name
+mkName' = mkName . toList
+
+-- | gen declaration of CallSpec record with CallSpec instance
+genCallSpec ::
+  (FoldrConstr l (Maybe VarBangType), FoldrConstr l Exp, Show (HList l)) =>
+  [VerificationMethod] -> String -> HList l -> Q [Dec]
+genCallSpec verMethods progName l = do
+  runIO . whenNothingM_ (findExecutable progName) . fail $ "Program " <> show progName <> " is not found"
+  maybe err (g . mkName') (programNameToHsIdentifier progName)
+  where
+    err = fail $ "Call spec name is bad: " <> show progName <> " " <> show l
+    g recName = do
+      (a, w) <- runWriterT . unQR $ sequence
+        [ genCallArgsRecord recName l
+        , genCallSpecInstance verMethods recName progName l
+        , genArbitraryInstance recName
+        ]
+      pure $ w <> a
diff --git a/src/System/Process/Quick/CallSpec/Run.hs b/src/System/Process/Quick/CallSpec/Run.hs
new file mode 100644
--- /dev/null
+++ b/src/System/Process/Quick/CallSpec/Run.hs
@@ -0,0 +1,25 @@
+module System.Process.Quick.CallSpec.Run where
+
+import System.Process.Quick.Prelude
+import System.Process.Quick.CallSpec.Type
+import System.Process qualified as SP
+
+-- | See 'SP.callProcess'
+callProcess :: (MonadIO m, CallSpec cs) => cs -> m ()
+callProcess cs = liftIO $ SP.callProcess (programName $ pure cs) (programArgs cs)
+
+-- | See 'SP.spawnProcess'
+spawnProcess :: (MonadIO m, CallSpec cs) => cs -> m SP.ProcessHandle
+spawnProcess cs = liftIO $ SP.spawnProcess (programName $ pure cs) (programArgs cs)
+
+-- | See 'SP.readProcess'
+readProcess :: (MonadIO m, CallSpec cs) => cs -> String -> m String
+readProcess cs input = liftIO $ SP.readProcess (programName $ pure cs) (programArgs cs) input
+
+-- | See 'SP.readProcessWithExitCode'
+readProcessWithExitCode :: (MonadIO m, CallSpec cs) => cs -> String -> m (ExitCode, String, String)
+readProcessWithExitCode cs input = liftIO $ SP.readProcessWithExitCode (programName $ pure cs) (programArgs cs) input
+
+-- | See 'SP.proc'
+proc :: CallSpec cs => cs -> CreateProcess
+proc cs = SP.proc (programName $ pure cs) (programArgs cs)
diff --git a/src/System/Process/Quick/CallSpec/Subcases.hs b/src/System/Process/Quick/CallSpec/Subcases.hs
new file mode 100644
--- /dev/null
+++ b/src/System/Process/Quick/CallSpec/Subcases.hs
@@ -0,0 +1,68 @@
+module System.Process.Quick.CallSpec.Subcases where
+
+import Control.Monad.Writer.Strict
+import System.Process.Quick.CallArgument
+import System.Process.Quick.CallSpec
+import Data.HList
+import Language.Haskell.TH as TH
+import System.Process.Quick.Prelude hiding (show)
+import Text.Show (Show (show))
+
+newtype DcName = DcName { unDcName :: String } deriving (Show, Eq, Ord, Data, IsString)
+
+data Subcase where
+  Subcase ::
+    forall l.
+    ( FoldrConstr l (Maybe VarBangType)
+    , FoldrConstr l Exp
+    , Show (HList l)
+    ) => DcName -> HList l -> Subcase
+
+instance Show Subcase where
+  show (Subcase dc l) = show $ "Subcase (" <> show dc <> ") " <> show l
+
+newtype TcName = TcName { unTcName :: String } deriving (Show, Eq, Ord, Data, IsString)
+
+data Subcases
+  = Subcases
+    { tcName :: TcName
+    , subcases :: [Subcase]
+    } deriving (Show)
+
+subcaseToRecC :: Subcase -> QR TH.Con
+subcaseToRecC (Subcase (DcName dcName) l) = do
+  fields <- seqA $ catMaybes <$> sequence (hMapM fieldDef l)
+  recC (mkName dcName) fields
+  where
+    fieldDef = Fun fieldExpr :: Fun CallArgumentGen (QR (Maybe VarBangType))
+
+subcasesToDec :: Name -> [Subcase] -> QR Dec
+subcasesToDec tyCon cases = do
+  dataD'
+    tyCon
+    (fmap subcaseToRecC cases)
+    [derivClause Nothing [[t|Data|], [t|Generic|], [t|Show|], [t|Eq|]]]
+
+subcaseToClause :: Subcase -> QR Clause
+subcaseToClause (Subcase (DcName dcName) l) = do
+  x <- newName "x"
+  f <- [| concat . flap $(listE (hMapM (Fun progArgExpr :: Fun CallArgumentGen (QR Exp)) l)) |]
+  pure $ Clause
+    [AsP x (RecP (mkName dcName) [])]
+    (NormalB (AppE f (VarE x)))
+    []
+
+instance CallArgumentGen Subcases where
+  cArgName = Just . mapFirst toLower . unTcName . tcName
+  progArgExpr (Subcases (TcName tyCon) cases) = do
+    tell =<< sequence [ subcasesToDec (mkName tyCon) cases
+                      , genArbitraryInstance (mkName tyCon)
+                      ]
+    [| $(lamCasesE (subcaseToClause <$> cases)) . $(varE . mkName $ mapFirst toLower tyCon) |]
+
+
+  fieldExpr (Subcases (TcName tyCon) _) =
+    pure $ Just ( mkName $ mapFirst toLower tyCon
+                , defaultBang
+                , ConT $ mkName tyCon
+                )
diff --git a/src/System/Process/Quick/CallSpec/Type.hs b/src/System/Process/Quick/CallSpec/Type.hs
new file mode 100644
--- /dev/null
+++ b/src/System/Process/Quick/CallSpec/Type.hs
@@ -0,0 +1,15 @@
+module System.Process.Quick.CallSpec.Type where
+
+import System.Process.Quick.Prelude
+import Language.Haskell.TH.Syntax
+
+-- | DC definition order defines validation order
+data VerificationMethod
+  = TrailingHelpValidate
+  | SandboxValidate
+  deriving (Show, Ord, Eq, Typeable, Data, Generic, Lift)
+
+class (Arbitrary cs, Data cs) => CallSpec cs where
+  programName :: Proxy cs -> String
+  programArgs :: cs -> [String]
+  verificationMethods :: Proxy cs -> [VerificationMethod]
diff --git a/src/System/Process/Quick/CallSpec/Verify.hs b/src/System/Process/Quick/CallSpec/Verify.hs
new file mode 100644
--- /dev/null
+++ b/src/System/Process/Quick/CallSpec/Verify.hs
@@ -0,0 +1,230 @@
+module System.Process.Quick.CallSpec.Verify where
+
+import Control.Monad.Writer.Strict hiding (lift)
+import Data.Conduit ( runConduitRes, (.|) )
+import Data.Conduit.Find as F
+import Data.Conduit.List qualified as DCL
+import Debug.TraceEmbrace
+import Language.Haskell.TH.Syntax
+import System.Directory
+import System.Exit hiding (exitFailure)
+import System.FilePath (getSearchPath, takeDirectory, takeExtension)
+import System.IO.Temp (withSystemTempDirectory)
+import System.Process (readProcessWithExitCode)
+import System.Process.Quick.CallEffect
+import System.Process.Quick.CallSpec
+import System.Process.Quick.Predicate
+import System.Process.Quick.Predicate.InFile ()
+import System.Process.Quick.Predicate.InDir ()
+import System.Process.Quick.Prelude hiding (Type, lift)
+
+
+type FailureReport = Doc
+
+data CallSpecViolation
+  = HelpKeyIgnored
+  | HelpKeyNotSupported FailureReport
+  | ProgramNotFound FailureReport [FilePath]
+  | HelpKeyExitNonZero FailureReport
+  | SandboxLaunchFailed FailureReport
+  | UnexpectedCallEffect [CallEffect]
+  deriving (Show, Eq)
+
+data CsViolationWithCtx
+  = forall cs. CallSpec cs
+  => CsViolationWithCtx
+     { csContext :: cs
+     , csViolation :: CallSpecViolation
+     }
+
+type M m = (MonadMask m, MonadCatch m, MonadIO m)
+
+
+callProcessSilently :: M m => FilePath -> [String] -> m (Maybe Doc)
+callProcessSilently p args =
+  tryIO (liftIO (readProcessWithExitCode p args "")) >>= \case
+    Left e ->
+      pure . Just $ "Command: [" <> doc p <> " " <> hsep (escArg <$> args) <> "]" $$
+      "Failed due:" $$ tab e
+
+    Right (ExitSuccess, _, _) -> pure Nothing
+    Right (ExitFailure ec, out, err) ->
+      pure . Just $ "Command: [" <> doc p <> " " <> hsep (escArg <$> args) <> "]" $$
+      (if ec > 1 then "Exited with: " <> show ec $$ "" else "")
+      <> out &! (("Output: " <+>) . tab) <> err &! (("StdErr: " <+>) . tab)
+
+verifyWithActiveMethods ::
+  forall w m cs. (M m, CallSpec cs, WriterT [FilePath] m ~ w) =>
+  ArgCollector w ->
+  ArgCollector w ->
+  Set VerificationMethod ->
+  Proxy cs ->
+  Int ->
+  m [CsViolationWithCtx]
+verifyWithActiveMethods inArgLocators outArgLocators activeVerMethods pcs iterations =
+  catMaybes <$> mapM go  (filter (`member` activeVerMethods) (verificationMethods pcs))
+  where
+    go = \case
+      TrailingHelpValidate -> verifyTrailingHelp pcs iterations
+      SandboxValidate -> validateInSandbox inArgLocators outArgLocators pcs iterations
+
+-- |Compose a list of monadic actions into one action.  Composes using
+-- ('>=>') - that is, the output of each action is fed to the input of
+-- the one after it in the list.
+concatM :: (Monad m) => [a -> m a] -> (a -> m a)
+concatM fs = foldr (>=>) return fs
+
+validateInSandbox ::
+  forall w m cs. (M m, CallSpec cs, WriterT [FilePath] m ~ w) =>
+  ArgCollector w ->
+  ArgCollector w ->
+  Proxy cs ->
+  Int ->
+  m (Maybe CsViolationWithCtx)
+validateInSandbox inArgLocators outArgLocators pcs !iterations
+  | iterations <= 0 = pure Nothing
+  | otherwise =
+    withSystemTempDirectory "quick-process" go >>= \case
+      Nothing -> validateInSandbox inArgLocators outArgLocators pcs $ iterations - 1
+      Just e -> pure $ Just e
+  where
+    checkFilesExist cs outFiles = do
+      filterM (pure . not <=< doesFileExist) outFiles >>= \case
+        [] -> pure Nothing
+        ne -> pure . Just . CsViolationWithCtx cs $
+          UnexpectedCallEffect
+          [ FsEffect . FsAnd $ fmap (FsNot . flip FsPathPredicate [FsExists]) ne
+          ]
+
+    findOriginFor projectDir inFile = do
+      xs :: [FilePath] <- runConduitRes $
+        F.find projectDir (do ignoreVcs
+                              glob $ "*" <> takeExtension inFile
+                              regular
+                              not_ F.executable) .| DCL.consume
+      case xs of
+        [] -> pure Nothing
+        neXs -> Just <$> generate (elements neXs)
+
+    genInputFile projectDir inFile = (fromMaybe "/etc/hosts" <$> findOriginFor projectDir inFile) >>=
+      \origin -> createDirectoryIfMissing True (takeDirectory inFile) >>
+                 copyFile origin inFile
+                 -- putStrLn ("File "  <> show origin <> " => " <> show inFile)
+
+    doIn projectDir () = do
+      cs <- liftIO (generate (arbitrary @cs))
+      inFiles <- execWriterT (gmapM inArgLocators cs)
+      -- absolute path is an issue for generator
+      -- though process in docker is run under root - high chance to pass ;)
+      -- quick hack is to use  odd size in Gen to avoid absolute path it Sandbox mode
+      mapM_ (liftIO1 (genInputFile projectDir)) inFiles
+      callProcessSilently (programName (pure cs)) (programArgs cs) >>= \case
+        Nothing -> do
+          outFiles <- execWriterT (gmapM outArgLocators cs)
+          liftIO (checkFilesExist cs outFiles)
+        Just e -> pure . Just . CsViolationWithCtx cs $ SandboxLaunchFailed e
+    go tdp = do
+      projectDir <- liftIO getCurrentDirectory
+      bracket
+        (liftIO $ setCurrentDirectory tdp)
+        (\() -> liftIO $ setCurrentDirectory projectDir)
+        (doIn projectDir)
+
+verifyTrailingHelp ::
+  forall m cs. (M m, CallSpec cs) =>
+  Proxy cs ->
+  Int ->
+  m (Maybe CsViolationWithCtx)
+verifyTrailingHelp pcs iterations =
+  liftIO (findExecutable progName) >>= \case
+    Nothing -> do
+      cs <- genCs
+      Just . CsViolationWithCtx cs . ProgramNotFound (text progName) <$> liftIO getSearchPath
+    Just _ -> do
+      spCmd progName helpKey
+        (spCmd progName ("--hheellppaoesnthqkxsth" : helpKey)
+           (do cs <- genCs
+               pure . Just $ CsViolationWithCtx cs HelpKeyIgnored)
+           (\_ -> go iterations))
+        (\rep -> do
+            cs <- genCs
+            pure . Just . CsViolationWithCtx cs $ HelpKeyNotSupported rep)
+  where
+    progName = programName pcs
+    genCs = liftIO (generate (arbitrary @cs))
+    helpKey = ["--help"]
+    spCmd pn args onSuccess onFailure = do
+      liftIO $(trIo "spawn process/pn args")
+      callProcessSilently pn args >>= \case
+        Nothing -> onSuccess
+        Just rep -> onFailure rep
+    go n
+      | n <= 0 = pure Nothing
+      | otherwise = do
+          cs <- liftIO (generate (arbitrary @cs))
+          spCmd (programName pcs) (programArgs cs <> helpKey)
+            (go $ n - 1)
+            (\rep -> pure . Just . CsViolationWithCtx cs $ HelpKeyExitNonZero rep)
+
+
+consumeViolations :: MonadIO m => [CsViolationWithCtx] -> m ()
+consumeViolations = \case
+  [] ->
+    putStrLn "CallSpecs are valid"
+  vis -> do
+    let dashes = "-------------------------------------------------------------"
+    -- good case for hetftio ??
+    printDoc $ "Error: quick-process found " <> doc (length vis) <> " failed call specs:"
+      $$ (vcat $ zipWith (\i v -> tab ("-- [" <> doc i <> "] " <> dashes $$ printViolation v))
+                 [1::Int ..] (sortByProgamName vis))
+      <> "---------" <> dashes $$ "End of quick-process violation report"
+    exitFailure
+  where
+    sortByProgamName = sortWith (\(CsViolationWithCtx x _) -> programName $ pure x)
+    printViolation (CsViolationWithCtx cs v) =
+      case v of
+        HelpKeyIgnored -> (text . programName $ pure cs) <> ": help key ignored"
+        ProgramNotFound report' pathCopy ->
+          "[" <> (text . programName $ pure cs) <> "] is not found on PATH:" $$ tab (vsep pathCopy)
+           $$ "Report:" $$ tab report' $$ ""
+        HelpKeyNotSupported report' ->
+          "--help key is not supported by [" <> (text . programName $ pure cs) <> "]"
+          $$ "Report:" $$ tab report'
+        HelpKeyExitNonZero rep ->
+          (text . programName $ pure cs) <> " - non zero exit code:" $$ tab rep
+        SandboxLaunchFailed rep ->
+          (text . programName $ pure cs) <> " - non zero exit code:" $$ tab rep
+        UnexpectedCallEffect uce -> do
+          (text . programName $ pure cs) <> ": has unsafisfied effects:" $$ (text $ show uce)
+           $$ "With arguments: " <> tab (programArgs cs)
+
+discoverAndVerifyCallSpecs :: Set VerificationMethod -> Int -> Q Exp
+discoverAndVerifyCallSpecs activeVerMethods iterations = do
+  inArgLocators <- extractInstanceType <$> reifyInstances ''RefinedInArgLocator [VarT (mkName "b")]
+  when (inArgLocators == []) $ putStrLn "Discovered 0 InArg locators!!!"
+  outArgLocators <- extractInstanceType <$> reifyInstances ''RefinedOutArgLocator [VarT (mkName "c")]
+  when (outArgLocators == []) $ putStrLn "Discovered 0 OutArg locators!!!"
+  ts <- extractInstanceType <$> reifyInstances ''CallSpec [VarT (mkName "a")]
+  when (ts == []) $ putStrLn "Discovered 0 types with CallSpec instance!!!"
+  [| fmap concat (sequence $(ListE <$> (mapM (genCsVerification inArgLocators outArgLocators) ts))) >>= consumeViolations |]
+  where
+    getLocator n t = AppE (VarE n) (SigE (ConE 'Proxy) (AppT (ConT ''Proxy) t))
+
+    pipeLocators :: Name -> [Type] -> Q Exp
+    pipeLocators locName ts =
+      [| concatM $(pure . ListE $ getLocator locName <$> ts) |]
+
+    genCsVerification :: [Type] -> [Type] -> Type -> Q Exp
+    genCsVerification inArL outArL t =
+      [| verifyWithActiveMethods
+           $(pipeLocators 'locateRefinedInArg inArL)
+           $(pipeLocators 'locateRefinedOutArg outArL)
+           $(lift activeVerMethods)
+           $(pure $ SigE (ConE 'Proxy) (AppT (ConT ''Proxy) t))
+           $(lift iterations)
+       |]
+    extractInstanceType :: [Dec] -> [Type]
+    extractInstanceType = mapMaybe $ \case
+      InstanceD _ _ (AppT _ t) _ ->
+        Just t
+      _ -> Nothing
diff --git a/src/System/Process/Quick/OrphanArbitrary.hs b/src/System/Process/Quick/OrphanArbitrary.hs
new file mode 100644
--- /dev/null
+++ b/src/System/Process/Quick/OrphanArbitrary.hs
@@ -0,0 +1,7 @@
+{-# OPTIONS_GHC -Wno-orphans #-}
+module System.Process.Quick.OrphanArbitrary where
+
+import System.Process.Quick.Prelude
+
+instance Arbitrary a => Arbitrary (NonEmpty a) where
+  arbitrary = liftA2 (:|) (arbitrary :: Gen a) (listOf (arbitrary :: Gen a))
diff --git a/src/System/Process/Quick/Predicate.hs b/src/System/Process/Quick/Predicate.hs
new file mode 100644
--- /dev/null
+++ b/src/System/Process/Quick/Predicate.hs
@@ -0,0 +1,19 @@
+module System.Process.Quick.Predicate where
+
+import Control.Monad.Writer.Strict
+import System.Process.Quick.Prelude
+
+refinErr :: (Predicate p a, Show a) => a -> Refined p a
+refinErr v =
+  case refine v of
+    Left e -> error $ "Satisfing value [" <> show v <> "] is no valid: " <> show e
+    Right vv -> vv
+
+type ArgCollector m =
+  (MonadIO m, MonadWriter [FilePath] m) => forall v. Data v => v -> m v
+
+class RefinedInArgLocator x where
+  locateRefinedInArg :: Proxy x -> ArgCollector m
+
+class RefinedOutArgLocator x where
+  locateRefinedOutArg :: Proxy x -> ArgCollector m
diff --git a/src/System/Process/Quick/Predicate/ImplDir.hs b/src/System/Process/Quick/Predicate/ImplDir.hs
new file mode 100644
--- /dev/null
+++ b/src/System/Process/Quick/Predicate/ImplDir.hs
@@ -0,0 +1,6 @@
+module System.Process.Quick.Predicate.ImplDir where
+
+import System.Process.Quick.Prelude
+
+
+data ImplDir (localDirPath :: Symbol) deriving (Data, Show, Eq, Generic)
diff --git a/src/System/Process/Quick/Predicate/InDir.hs b/src/System/Process/Quick/Predicate/InDir.hs
new file mode 100644
--- /dev/null
+++ b/src/System/Process/Quick/Predicate/InDir.hs
@@ -0,0 +1,34 @@
+module System.Process.Quick.Predicate.InDir where
+
+import Data.Typeable (eqT)
+import System.Directory
+import System.Process.Quick.Predicate
+import System.Process.Quick.Predicate.InFile ( genFilePathBy )
+import System.Process.Quick.Prelude
+import Text.Regex.TDFA ((=~))
+import Type.Reflection ((:~:)(Refl))
+
+data InDir deriving (Data, Show, Eq, Generic)
+
+instance Predicate InDir FilePath where
+  validate p x
+    | x =~ ("^([.~]?[/])?[^/\x0000-\x001F]+([/][^/\x0000-\x001F]+)*[/]?$" :: String)
+    = Nothing
+    | otherwise
+    = throwRefineOtherException (typeRep p) $ "Bad FilePath " <> toText x <> "]"
+
+instance {-# OVERLAPPING #-} Arbitrary (Refined InDir FilePath) where
+  arbitrary =
+    genFilePathBy (Proxy @"*") >>= pure . refinErr
+
+findRefinedDirs :: forall m x. (MonadIO m, Data x) => x -> m x
+findRefinedDirs x
+  | Just Refl <- eqT @x @(Refined InDir FilePath) =
+      let fp = unrefine x in do
+        liftIO (createDirectoryIfMissing True fp)
+        pure x
+  | otherwise =
+      pure x
+
+instance RefinedInArgLocator (Refined InDir FilePath) where
+  locateRefinedInArg _ = findRefinedDirs
diff --git a/src/System/Process/Quick/Predicate/InFile.hs b/src/System/Process/Quick/Predicate/InFile.hs
new file mode 100644
--- /dev/null
+++ b/src/System/Process/Quick/Predicate/InFile.hs
@@ -0,0 +1,109 @@
+module System.Process.Quick.Predicate.InFile where
+
+import Control.Monad.Writer.Strict
+import System.Process.Quick.Predicate
+import System.Process.Quick.Prelude
+import System.Process.Quick.TdfaToSbvRegex as P
+import System.Process.Quick.Sbv.Arbitrary
+import System.Process.Quick.CallArgument (NeList)
+import Text.Regex.TDFA ((=~))
+import Type.Reflection qualified as R
+import Type.Reflection ((:~:)(Refl))
+import Data.Typeable (eqT)
+
+
+data InFile (ext :: Symbol) deriving (Data, Show, Eq, Generic)
+
+instance KnownSymbol e => Predicate (InFile e) String where
+  validate p x =
+    let ext = symbolVal (Proxy @e) in
+      if ext == "*"
+      then
+        if x =~  ("^([.~]?[/])?[^/\x0000-\x001F]+([/][^/\x0000-\x001F]+)*$" :: String)
+        then Nothing
+        else throwRefineOtherException (typeRep p) $ "Bad FilePath " <> toText x <> "]"
+      else
+        if x =~ ("^([.~]?[/])?[^/\x0000-\x001F]+([/][^/\x0000-\x001F]+)*[.]" <> ext <> "$")
+        then Nothing
+        else throwRefineOtherException (typeRep p) $ "Bad FilePath " <> toText x <> "]"
+
+instance Predicate (InFile e) String => Predicate (InFile e) [String] where
+  validate p = listToMaybe . mapMaybe (validate p)
+instance Predicate (InFile e) String => Predicate (InFile e) (NeList String) where
+  validate p = listToMaybe . mapMaybe (validate p) . toList
+
+genFilePathBy :: forall e. KnownSymbol e => Proxy e -> Gen FilePath
+genFilePathBy _ =
+  let ext = symbolVal (Proxy @e) in
+    findStringByRegex
+      (parse $ if ext == "*"
+        then "^[^/\x0000-\x001F]+([.][a-z]{1,4})?$"
+        else "^[^/\x0000-\x001F]+[.]" <> ext <> "$")
+
+instance {-# OVERLAPPING #-}
+  KnownSymbol e => Arbitrary (Refined (InFile e) FilePath) where
+  arbitrary =
+    genFilePathBy (Proxy @e) >>= pure . refinErr
+
+instance {-# OVERLAPPING #-}
+  KnownSymbol e => Arbitrary (Refined (InFile e) [FilePath]) where
+  arbitrary =
+    sized $ \n -> refinErr <$> mapM (\_ -> genFilePathBy $ Proxy @e) (take n [1::Int ..])
+
+instance {-# OVERLAPPING #-}
+  KnownSymbol e => Arbitrary (Refined (InFile e) (NeList FilePath)) where
+  arbitrary =
+    sized $ \n -> refinErr <$> mapM (\_ -> genFilePathBy $ Proxy @e) (0 :| take n [1::Int ..])
+
+data OutFile (ext :: Symbol)
+
+instance KnownSymbol e => Predicate (OutFile e) String where
+  validate p x =
+    let ext = symbolVal (Proxy @e) in
+      if ext == "*"
+      then
+        if x =~  ("^([.~]?[/])?[^/\x0000-\x001F]+([/][^/\x0000-\x001F]+)*$" :: String)
+        then Nothing
+        else throwRefineOtherException (typeRep p) $ "Bad FilePath " <> toText x <> "]"
+      else
+        if x =~ ("^([.~]?[/])?[^/\x0000-\x001F]+([/][^/\x0000-\x001F]+)*[.]" <> ext <> "$")
+        then Nothing
+        else throwRefineOtherException (typeRep p) $ "Bad FilePath " <> toText x <> "]"
+
+instance {-# OVERLAPPING #-}
+  KnownSymbol e => Arbitrary (Refined (OutFile e) FilePath) where
+  arbitrary =
+    let ext = symbolVal (Proxy @e) in do
+      sv <- findStringByRegex
+        (parse $ if ext == "*"
+          then "^[^/\x0000-\x001F]+([.][a-z]{1,4})?$"
+          else "^[^/\x0000-\x001F]+[.]" <> ext <> "$")
+      case refine sv of
+        Left e -> error $ "Satisfing value [" <> show sv <> "] is no valid: " <> show e
+        Right vv -> pure vv
+
+findRefinedStrings :: forall v p m x.
+  ( Typeable p
+  , MonadWriter [FilePath] m
+  , MonadIO m
+  , Typeable x
+  , Typeable v
+  , Data x
+  ) => Proxy p -> (v -> [String]) -> x -> m x
+findRefinedStrings _ f x
+  | _rRefined `R.App` rif@(R.TypeRep @tif) `R.App` _rString <- R.TypeRep @x
+  , R.TypeRep <- R.typeRepKind rif
+  , Just Refl <- eqT @x @(Refined tif v)
+  , rInFile `R.App` _rExt <- R.TypeRep @tif
+  , Just R.HRefl <- R.eqTypeRep  rInFile (R.typeRep :: R.TypeRep p)
+  = let fp = unrefine x in tell (f fp) >> pure x
+  | otherwise = pure x
+
+instance RefinedInArgLocator (Refined (InFile e) FilePath) where
+  locateRefinedInArg _ = findRefinedStrings (Proxy @InFile) pure
+instance RefinedInArgLocator (Refined (InFile e) (NeList FilePath)) where
+  locateRefinedInArg _ = findRefinedStrings @(NeList FilePath) (Proxy @InFile) toList
+instance RefinedInArgLocator (Refined (InFile e) [FilePath]) where
+  locateRefinedInArg _ = findRefinedStrings (Proxy @InFile) id
+instance RefinedOutArgLocator (Refined (OutFile e) FilePath) where
+  locateRefinedOutArg _ = findRefinedStrings (Proxy @OutFile) pure
diff --git a/src/System/Process/Quick/Predicate/LowerCase.hs b/src/System/Process/Quick/Predicate/LowerCase.hs
new file mode 100644
--- /dev/null
+++ b/src/System/Process/Quick/Predicate/LowerCase.hs
@@ -0,0 +1,31 @@
+{-# OPTIONS_GHC -fno-warn-orphans #-}
+module System.Process.Quick.Predicate.LowerCase where
+
+import Refined
+import System.Process.Quick.Prelude
+
+
+data LowerCase
+
+instance Predicate LowerCase String where
+  validate p value =
+    if all isLower value
+      then Nothing
+      else throwRefineOtherException (typeRep p) "Not all chars are lower-case"
+
+type LowerCaseString = Refined LowerCase String
+
+
+leftError :: Show a => Text -> Either a b -> b
+leftError m = \case
+  Right v -> v
+  Left e -> error $ m <> "; due: " <> show e
+
+instance {-# OVERLAPPING #-}
+  (Arbitrary a, Typeable a, Predicate (SizeEqualTo n) [a], KnownNat n) =>
+  Arbitrary (Refined (SizeEqualTo n) [a]) where
+  arbitrary =
+    leftError "Dead code" . refine <$>
+    replicateM (fromIntegral $ natVal (Proxy @n)) arbitrary
+
+  shrink = rights . map refine . shrink . unrefine
diff --git a/src/System/Process/Quick/Predicate/Regex.hs b/src/System/Process/Quick/Predicate/Regex.hs
new file mode 100644
--- /dev/null
+++ b/src/System/Process/Quick/Predicate/Regex.hs
@@ -0,0 +1,27 @@
+module System.Process.Quick.Predicate.Regex where
+
+import System.Process.Quick.Predicate
+import System.Process.Quick.Prelude
+import System.Process.Quick.Sbv.Arbitrary
+import System.Process.Quick.TdfaToSbvRegex as P
+import Text.Regex.TDFA ((=~))
+
+
+data Regex (p :: Symbol) = Regex deriving (Generic)
+
+instance KnownSymbol s => Predicate (Regex s) String where
+  validate p x =
+    let rx = symbolVal (Proxy @s) in
+      if x =~ rx
+      then Nothing
+      else throwRefineOtherException (typeRep p) $ "Regex " <> show rx <> " mismatches [" <> toText x <> "]"
+
+instance {-# OVERLAPPING #-}
+  KnownSymbol p => Arbitrary (Refined (Regex p) String) where
+
+  arbitrary =
+    let rx = symbolVal (Proxy @p) in do
+      refinErr <$> findStringByRegex (parse rx)
+
+type FsPath = Regex "^([/~]|(~[/]|[/])?[^/\x0000-\x001F]+([/][^/\x0000-\x001F]+)*[/]?)$"
+type FsPath2 = Regex "^([/~]|(~[/]|[/])?[a-zA-Z0-9._ -]+([/][a-zA-Z0-9._ -]+)*[/]?)$"
diff --git a/src/System/Process/Quick/Prelude.hs b/src/System/Process/Quick/Prelude.hs
new file mode 100644
--- /dev/null
+++ b/src/System/Process/Quick/Prelude.hs
@@ -0,0 +1,21 @@
+{-# OPTIONS_HADDOCK hide #-}
+module System.Process.Quick.Prelude (module M, liftIO1) where
+
+import Control.Exception.Safe as M (MonadMask, MonadCatch, bracket, tryIO, try, tryAny)
+import Data.Data as M (Data, gmapM)
+import Data.Char as M (isAlphaNum, isAlpha, isLetter, isLower, toLower)
+import Data.HList as M (typeRep)
+import Data.List as M (isSuffixOf)
+import Data.Set as M (member)
+import Generic.Random as M (genericArbitraryU)
+import Relude as M hiding (Predicate)
+import Relude.Extra as M (toPairs)
+import Test.QuickCheck as M (Gen, Arbitrary (..), generate, chooseInt, sized, elements, listOf)
+import System.Process.Quick.Pretty as M
+import System.Process as M (ProcessHandle, CreateProcess (..), readCreateProcess, readCreateProcessWithExitCode)
+import System.Exit as M (ExitCode (..))
+import Refined as M (Refined, unrefine, refine, Predicate (..), throwRefineOtherException)
+import GHC.TypeLits as M (Symbol, KnownSymbol (..), symbolVal)
+
+liftIO1 :: MonadIO m => (a -> IO b) -> a -> m b
+liftIO1 = (.) liftIO
diff --git a/src/System/Process/Quick/Pretty.hs b/src/System/Process/Quick/Pretty.hs
new file mode 100644
--- /dev/null
+++ b/src/System/Process/Quick/Pretty.hs
@@ -0,0 +1,68 @@
+module System.Process.Quick.Pretty
+  ( Pretty (..)
+  , (&!)
+  , escArg
+  , tab
+  , printDoc
+  , apNe
+  , module PP
+  ) where
+
+import Control.Exception.Safe
+import GHC.ResponseFile (escapeArgs)
+import Relude
+import Text.PrettyPrint as PP hiding (hsep, (<>), empty, isEmpty)
+import Text.PrettyPrint qualified as PP
+
+
+class Pretty a where
+  default doc :: Show a => a -> Doc
+  doc = text . show
+  doc :: a -> Doc
+
+  hsep :: [a] -> Doc
+  hsep = PP.hsep . fmap doc
+  {-# INLINE hsep #-}
+
+  vsep :: [a] -> Doc
+  vsep = vcat . fmap doc
+  {-# INLINE vsep #-}
+
+instance Pretty Doc where
+  doc = id
+  {-# INLINE doc #-}
+instance Pretty String where
+  doc = text
+  {-# INLINE doc #-}
+instance Pretty IOException
+instance Pretty Int
+instance Pretty Integer
+instance Pretty [String]
+
+
+printDoc :: MonadIO m => Doc -> m ()
+printDoc = putStrLn . render
+
+tab :: Pretty a => a -> Doc
+tab = nest 2 . doc
+
+class IsEmpty a where
+  isEmpty :: a -> Bool
+
+instance IsEmpty [a] where
+  isEmpty = null
+
+apNe :: (IsEmpty a, Pretty a) => a -> (Doc -> Doc) -> Doc
+apNe d f
+  | isEmpty d = d'
+  | otherwise = f d'
+  where
+    d' = doc d
+
+(&!) :: (IsEmpty a, Pretty a) => a -> (Doc -> Doc) -> Doc
+(&!) = apNe
+
+infixl 7 &!
+
+escArg :: String -> String
+escArg = reverse . drop 1 . reverse . escapeArgs . pure
diff --git a/src/System/Process/Quick/Sbv/Arbitrary.hs b/src/System/Process/Quick/Sbv/Arbitrary.hs
new file mode 100644
--- /dev/null
+++ b/src/System/Process/Quick/Sbv/Arbitrary.hs
@@ -0,0 +1,52 @@
+module System.Process.Quick.Sbv.Arbitrary where
+
+import System.Process.Quick.Prelude
+import Data.SBV -- (Satisfiable, SymVal, Modelable (..), SString, sat, (.==), (.&&), literal)
+import Data.SBV.String qualified as S
+-- import Data.SBV.Control qualified as C
+import System.IO.Unsafe (unsafePerformIO)
+import Data.SBV.RegExp
+
+getSingleValue :: (SymVal b, Modelable m) => m -> Maybe b
+getSingleValue m
+  | modelExists m =
+    case toPairs $ getModelDictionary m of
+      [(k, _)] -> getModelValue k m
+      _ -> Nothing
+  | otherwise = Nothing
+
+-- models
+satOne :: (Satisfiable a, SymVal b) => Int -> a -> Maybe b
+satOne _n p = unsafePerformIO (getSingleValue <$> sat p)
+
+satN :: (Satisfiable a, SymVal b) => Int -> a -> [b]
+satN n p = unsafePerformIO (mapMaybe getSingleValue . allSatResults <$> asat)
+  where
+    asat = allSatWith defaultSMTCfg { allSatMaxModelCount = Just n } p
+
+-- satStateless :: SymVal a => Int -> a -> Symbolic (Either String b)
+-- satStateless seed p = unsafePerformIO go
+--   where
+--     solve ::
+--     go = runSMT solve
+
+findStringByRegex :: (SymVal b) => RegExp -> Gen b
+findStringByRegex r = go (3 :: Int)
+  where
+    go t = sized $ \l ->
+      if t > 0
+        then do
+          n <- chooseInt (0, l)
+          case trySat n of
+            Just y -> pure y
+            Nothing -> go $ t - 1
+        else do
+          case satN l matchRx of
+            [] -> error $ "No solution for regex: " <> show r
+            ss -> elements ss
+
+    matchRx (x :: SString) = match x r
+
+    trySat n =
+      satOne n (\x -> matchRx x
+                 .&& S.length x .== literal (fromIntegral n))
diff --git a/src/System/Process/Quick/TdfaToSbvRegex.hs b/src/System/Process/Quick/TdfaToSbvRegex.hs
new file mode 100644
--- /dev/null
+++ b/src/System/Process/Quick/TdfaToSbvRegex.hs
@@ -0,0 +1,50 @@
+module System.Process.Quick.TdfaToSbvRegex (parse, match) where
+
+import Data.SBV.RegExp
+import System.Process.Quick.Prelude
+import Text.Regex.TDFA.Pattern
+import Text.Regex.TDFA.ReadRegex
+
+parse :: String -> RegExp
+parse rxp =
+  case parseRegex $ adaptAnchors rxp of
+    Right (p, _) -> tdfa2SbvRegex p
+    Left e -> error $ "Failed to parse pattern " <> show rxp <> " as TDFA due: " <> show e
+
+adaptAnchors :: String -> String
+adaptAnchors [] = ".*"
+adaptAnchors rx = tailAnchor $ headAnchor rx
+  where
+    headAnchor x =  if "^" `isPrefixOf` x then x else ".*" <> x
+    tailAnchor x =  if "$" `isSuffixOf` x then x else x <> ".*"
+
+tdfa2SbvRegex :: Pattern -> RegExp
+tdfa2SbvRegex = \case
+  PEmpty -> Literal ""
+  PGroup _ p -> tdfa2SbvRegex p -- ??
+  POr ps -> Union $ fmap tdfa2SbvRegex ps
+  PConcat ps -> Conc $ fmap tdfa2SbvRegex ps
+  PQuest p -> Opt $ tdfa2SbvRegex p
+  PPlus p -> KPlus $ tdfa2SbvRegex p
+  PStar _ p -> KStar $ tdfa2SbvRegex p
+  PBound n Nothing p -> Power n $ tdfa2SbvRegex p
+  PBound n (Just m) p -> Loop n m $ tdfa2SbvRegex p
+  PCarat _ -> Literal "" -- store in state monad as global flag
+  PDollar _ -> Literal "" -- store in state monad as global flag
+  PDot _ -> AllChar
+  PAny _ ps -> patternSetToRegex ps
+  PAnyNot _ ps -> Inter AllChar . Comp $ patternSetToRegex ps
+  PEscape _ c -> Literal [c]
+  PChar _ c -> Literal [c]
+  PNonCapture p -> tdfa2SbvRegex p -- ??
+  PNonEmpty p -> tdfa2SbvRegex p -- ??
+
+patternSetToRegex :: PatternSet -> RegExp
+patternSetToRegex = \case
+  PatternSet ps Nothing Nothing Nothing ->
+    Union (fromMaybe [] (charSetToRegex <$> ps))
+  PatternSet _ a b c ->
+    error $ "Not supported:" <> show a <> "; " <> show b <> "; " <> show c
+
+charSetToRegex :: Set Char -> [RegExp]
+charSetToRegex = fmap (Literal . (:[])) . toList
diff --git a/test/Discovery.hs b/test/Discovery.hs
new file mode 100644
--- /dev/null
+++ b/test/Discovery.hs
@@ -0,0 +1,1 @@
+{-# OPTIONS_GHC -F -pgmF tasty-discover -optF --generated-module=Discovery #-}
diff --git a/test/Driver.hs b/test/Driver.hs
new file mode 100644
--- /dev/null
+++ b/test/Driver.hs
@@ -0,0 +1,12 @@
+module Driver where
+
+import qualified Discovery
+import System.Process.Quick.Test.Prelude
+
+main :: IO ()
+main = defaultMain =<< testTree
+  where
+    testTree :: IO TestTree
+    testTree = do
+      tests <- Discovery.tests
+      pure $ testGroup "quick-process" [ tests ]
diff --git a/test/System/Process/Quick/Test/CallSpec.hs b/test/System/Process/Quick/Test/CallSpec.hs
new file mode 100644
--- /dev/null
+++ b/test/System/Process/Quick/Test/CallSpec.hs
@@ -0,0 +1,16 @@
+{-# LANGUAGE TemplateHaskell #-}
+-- {-# OPTIONS_GHC -ddump-splices -ddump-to-file -dth-dec-file #-}
+-- {-# OPTIONS_GHC -ddump-splices #-}
+module System.Process.Quick.Test.CallSpec where
+
+import Data.HList as HL
+import Refined
+import System.Process.Quick.Test.Prelude
+import System.Process.Quick.CallArgument
+import TH.Utilities qualified as TU
+import Language.Haskell.TH
+type VarStrArg = VarArg String
+
+
+x :: String
+x = $(stringE . show =<< TU.typeRepToType (typeRep (Proxy @(Refined (SizeEqualTo 2) String))))
diff --git a/test/System/Process/Quick/Test/CallSpec/Const.hs b/test/System/Process/Quick/Test/CallSpec/Const.hs
new file mode 100644
--- /dev/null
+++ b/test/System/Process/Quick/Test/CallSpec/Const.hs
@@ -0,0 +1,35 @@
+-- {-# OPTIONS_GHC -ddump-splices #-}
+{-# LANGUAGE TemplateHaskell #-}
+module System.Process.Quick.Test.CallSpec.Const where
+
+
+import System.Process.Quick.Test.Prelude
+import System.Process.Quick.CallArgument
+import System.Process.Quick.CallSpec
+
+
+$(genCallSpec [TrailingHelpValidate] "rm" (ConstArg "--version" .*. HNil))
+
+prop_Rm_name :: Rm -> Bool
+prop_Rm_name cs = programName (pure cs) == "rm"
+
+prop_Rm_args :: Rm -> Bool
+prop_Rm_args cs = programArgs cs == [ "--version" ]
+
+
+$(genCallSpec [TrailingHelpValidate] "mkdir" (ConstArg "--help" .*. HNil))
+
+prop_Mkdir_name :: Mkdir -> Property
+prop_Mkdir_name cs = programName (pure cs) === "mkdir"
+
+prop_Mkdir_args :: Mkdir -> Property
+prop_Mkdir_args cs = programArgs cs === [ "--help" ]
+
+
+$(genCallSpec [TrailingHelpValidate] "rmdir" (ConstArg "-x" .*. ConstArg "-v" .*. ConstArg "--help" .*. HNil))
+
+prop_Rmdir_name :: Rmdir -> Property
+prop_Rmdir_name cs = programName (pure cs) === "rmdir"
+
+prop_Rmdir_args :: Rmdir -> Property
+prop_Rmdir_args cs = programArgs cs === [ "-x", "-v", "--help" ]
diff --git a/test/System/Process/Quick/Test/CallSpec/VarArg.hs b/test/System/Process/Quick/Test/CallSpec/VarArg.hs
new file mode 100644
--- /dev/null
+++ b/test/System/Process/Quick/Test/CallSpec/VarArg.hs
@@ -0,0 +1,15 @@
+{-# LANGUAGE TemplateHaskell #-}
+module System.Process.Quick.Test.CallSpec.VarArg where
+
+import System.Process.Quick.Test.Prelude
+import System.Process.Quick.CallArgument
+import System.Process.Quick.CallSpec
+
+
+$(genCallSpec [TrailingHelpValidate] "mkdir" (VarArg @String "dirName" .*. HNil))
+
+prop_BinMkdir_name :: Mkdir -> Bool
+prop_BinMkdir_name cs = programName (pure cs) == "mkdir"
+
+prop_BinMkdir_args :: Mkdir -> Bool
+prop_BinMkdir_args cs = length (programArgs cs) == 1
diff --git a/test/System/Process/Quick/Test/CallSpec/VarArg/Refined.hs b/test/System/Process/Quick/Test/CallSpec/VarArg/Refined.hs
new file mode 100644
--- /dev/null
+++ b/test/System/Process/Quick/Test/CallSpec/VarArg/Refined.hs
@@ -0,0 +1,16 @@
+{-# LANGUAGE TemplateHaskell #-}
+module System.Process.Quick.Test.CallSpec.VarArg.Refined where
+
+
+import System.Process.Quick.Test.Prelude
+import System.Process.Quick.CallArgument
+import System.Process.Quick.CallSpec
+import System.Process.Quick ()
+
+type M = Refined (SizeEqualTo 2) String
+
+
+$(genCallSpec [TrailingHelpValidate] "rm" (VarArg @M "fileName" .*. HNil))
+
+prop_rm_filename_of_2_chars_args :: Rm -> Property
+prop_rm_filename_of_2_chars_args cs = (length <$> (programArgs cs ^? ix 0)) === Just 2
diff --git a/test/System/Process/Quick/Test/Prelude.hs b/test/System/Process/Quick/Test/Prelude.hs
new file mode 100644
--- /dev/null
+++ b/test/System/Process/Quick/Test/Prelude.hs
@@ -0,0 +1,12 @@
+module System.Process.Quick.Test.Prelude (module M) where
+
+import Control.Lens as M ((^.), (^?), at, ix)
+import Data.HList as M (HList(..), HExtend(..))
+import Refined as M (SizeEqualTo)
+import System.Directory as M (doesFileExist, removeFile)
+import System.Process.Quick.Prelude as M
+import Test.QuickCheck.Instances as M ()
+import Test.Tasty as M
+import Test.Tasty.HUnit as M
+import Test.Tasty.QuickCheck as M hiding (Failure, Success, tables, (.&&.))
+import UnliftIO as M (withSystemTempDirectory, withSystemTempFile)
diff --git a/test/System/Process/Quick/Test/Th.hs b/test/System/Process/Quick/Test/Th.hs
new file mode 100644
--- /dev/null
+++ b/test/System/Process/Quick/Test/Th.hs
@@ -0,0 +1,30 @@
+module System.Process.Quick.Test.Th where
+
+import System.Process.Quick.Test.Prelude
+
+import Refined
+test_tree :: TestTree
+test_tree =
+  testGroup
+    "hello"
+    [ testCase "hello" (assertEqual "1 == 2 - 1" (1 :: Int) (2 - 1))
+
+    ]
+
+-- hMap (Fun show :: Fun Show (String)) (HCons () (HCons True HNil))
+-- hFoldr (Fun show :: Fun Show (String)) [] (HCons () (HCons True HNil))
+
+{-
+class HFoldr f v (l :: [*]) r where
+    hFoldr :: f -> v -> HList l -> r
+
+instance (v ~ v') => HFoldr f v '[] v' where
+    hFoldr       _ v _   = v
+
+instance (ApplyAB f (e, r) r', HFoldr f v l r)
+    => HFoldr f v (e ': l) r' where
+    hFoldr f v (HCons x l)    = applyAB f (x, hFoldr f v l :: r)
+
+-}
+prop_refined_less_than_5 :: Refined (LessThan 5) Int -> Bool
+prop_refined_less_than_5 x = unrefine x < 5
diff --git a/verify-call-specs/CallSpecs/Find.hs b/verify-call-specs/CallSpecs/Find.hs
new file mode 100644
--- /dev/null
+++ b/verify-call-specs/CallSpecs/Find.hs
@@ -0,0 +1,11 @@
+-- {-# OPTIONS_GHC -ddump-splices #-}
+{-# LANGUAGE TemplateHaskell #-}
+module CallSpecs.Find where
+
+import CallSpecs.Find.Type
+import System.Process.Quick
+import System.Process.Quick.Prelude hiding (NonEmpty, Type)
+
+type DirPath = Refined FsPath String
+
+$(genCallSpec [TrailingHelpValidate] "find" (ConstArg "-H" .*. VarArg @DirPath "path" .*. KeyArg @NodeType "-type" .*. HNil))
diff --git a/verify-call-specs/CallSpecs/Find/Type.hs b/verify-call-specs/CallSpecs/Find/Type.hs
new file mode 100644
--- /dev/null
+++ b/verify-call-specs/CallSpecs/Find/Type.hs
@@ -0,0 +1,14 @@
+module CallSpecs.Find.Type where
+
+import System.Process.Quick
+import System.Process.Quick.Prelude
+
+data NodeType = FileNode | DirNode deriving (Show, Eq, Generic, Typeable, Data)
+
+instance Arbitrary NodeType where
+  arbitrary = genericArbitraryU
+
+instance CallArgument NodeType where
+  toExecString = pure . \case
+    FileNode -> "f"
+    DirNode -> "d"
diff --git a/verify-call-specs/VerifyCallSpecs.hs b/verify-call-specs/VerifyCallSpecs.hs
new file mode 100644
--- /dev/null
+++ b/verify-call-specs/VerifyCallSpecs.hs
@@ -0,0 +1,57 @@
+-- {-# OPTIONS_GHC -ddump-splices #-}
+{-# LANGUAGE TemplateHaskell #-}
+
+module VerifyCallSpecs where
+
+import CallSpecs.Find ()
+import System.Process.Quick
+import System.Process.Quick.Prelude
+
+
+-- goRef :: forall x. (Typeable x, Data x) => x -> IO x
+-- goRef x =
+--   case cast x of
+--     Just (i :: Refined Positive Int) -> do
+--       putStrLn $ "i " <> show (unrefine i * 22)
+--       case refine $ (unrefine i) * 22 of
+--         Left _e -> pure x
+--         Right (caed :: Refined Positive Int) ->
+--           case cast caed of
+--             Nothing -> pure x
+--             Just r -> pure r
+--     _ -> pure x
+
+-- go :: forall x. (Typeable x, Data x) => x -> IO x
+-- go x =
+--   case cast x of
+--     Just (Tagged i :: Tagged "a" Int) -> do
+--       putStrLn $ "i " <> show (i * 22)
+--       case cast (Tagged @"a" $ i * 22) of
+--         Nothing -> pure x
+--         Just r -> pure r
+--     _ -> pure x
+
+-- go1 :: forall x. (Typeable x, Data x) => x -> IO x
+-- go1 x =
+--   case cast x of
+--     Just (Fo i :: Fo "a" Int) -> do
+--       putStrLn $ "i " <> show (i * 22)
+--       case cast (Fo @"a" $ i * 22) of
+--         Nothing -> pure x
+--         Just r -> pure r
+--     _ -> pure x
+
+
+-- go2 :: forall x. (Typeable x, Data x) => x -> IO x
+-- go2 x
+--   | _ `App` a@(TypeRep @(aa :: k2)) `App` _ <- typeOf x -- TypeRep @x
+--   , TypeRep <- typeRepKind a -- ?
+--   , Just Refl <- eqT @x @(Fo (aa) Int)
+--   = do let Fo i = x
+--        putStrLn $ "i " <> show (i * 22)
+--        pure . Fo $ i * 22
+
+--   | otherwise = pure x
+
+main :: IO ()
+main = $(discoverAndVerifyCallSpecs (fromList [TrailingHelpValidate]) 1)