diff --git a/CHANGELOG.md b/CHANGELOG.md
--- a/CHANGELOG.md
+++ b/CHANGELOG.md
@@ -1,3 +1,7 @@
+## 0.6.0 (2024-10-01)
+* remove `Via` predicate, only need `validateVia`
+* swap `validateBool` args
+
 ## 0.5.1 (2024-06-11)
 * add `Via` predicate
 
diff --git a/rerefined.cabal b/rerefined.cabal
--- a/rerefined.cabal
+++ b/rerefined.cabal
@@ -1,11 +1,11 @@
 cabal-version: 1.12
 
--- This file has been generated from package.yaml by hpack version 0.35.2.
+-- This file has been generated from package.yaml by hpack version 0.36.1.
 --
 -- see: https://github.com/sol/hpack
 
 name:           rerefined
-version:        0.5.1
+version:        0.6.0
 synopsis:       Refinement types, again
 description:    Please see README.md.
 category:       Types, Data
diff --git a/src/Rerefined/Predicate.hs b/src/Rerefined/Predicate.hs
--- a/src/Rerefined/Predicate.hs
+++ b/src/Rerefined/Predicate.hs
@@ -38,6 +38,16 @@
 predicateName = symbolVal' (proxy# @(PredicateName 0 p))
 
 -- | Refine @a@ with predicate @p@.
+--
+-- Note that 'validate' implementations decide what failure information is
+-- emitted. They don't even have to emit their own predicate name, even though
+-- 'Predicate' is in the context. This is useful in certain cases such as
+-- "Rerefined.Predicate.Via".
+--
+-- That does mean that the 'Predicate' context may not be used occasionally. But
+-- it's very useful, since otherwise combinator predicates have to constantly
+-- state @(Refine p a, Predicate p)@, and all predicates should have a pretty
+-- name even if it doesn't get printed under normal circumstances.
 class Predicate p => Refine p a where
     -- | Validate predicate @p@ for the given @a@.
     --
diff --git a/src/Rerefined/Predicate/Common.hs b/src/Rerefined/Predicate/Common.hs
--- a/src/Rerefined/Predicate/Common.hs
+++ b/src/Rerefined/Predicate/Common.hs
@@ -30,8 +30,6 @@
 validateBool
     :: forall p
     .  (Predicate p, KnownPredicateName p)
-    => Proxy# p -> TBL.Builder -> Bool
+    => Proxy# p -> Bool -> TBL.Builder
     -> Maybe RefineFailure
-validateBool p e = \case
-  True  -> Nothing
-  False -> validateFail p e []
+validateBool p b msg = case b of True -> Nothing; False -> validateFail p msg []
diff --git a/src/Rerefined/Predicate/Relational/Length.hs b/src/Rerefined/Predicate/Relational/Length.hs
--- a/src/Rerefined/Predicate/Relational/Length.hs
+++ b/src/Rerefined/Predicate/Relational/Length.hs
@@ -46,7 +46,7 @@
        , KnownPredicateName (CompareLength op n)
     ) => Proxy# (CompareLength op n) -> Int -> Maybe RefineFailure
 validateCompareLength p len =
-    validateBool p ("length: "<>TBL.fromDec n) (reifyRelOp @op len n)
+    validateBool p (reifyRelOp @op len n) $ "length: "<>TBL.fromDec n
   where n = fromIntegral (natVal' (proxy# @n))
 
 -- | Widen a length comparison predicate.
diff --git a/src/Rerefined/Predicate/Relational/Value.hs b/src/Rerefined/Predicate/Relational/Value.hs
--- a/src/Rerefined/Predicate/Relational/Value.hs
+++ b/src/Rerefined/Predicate/Relational/Value.hs
@@ -27,10 +27,8 @@
   ) => Refine (CompareValue op sign n) a where
     -- note that we show the reified 'Natural' rather than the coerced numeric
     -- type, as otherwise we'd need a @'Show' a@
-    validate p a =
-        validateBool p
-            ("bad value")
-            (reifyRelOp @op a (reifySignedNat @sign @n))
+    validate p a = validateBool p (reifyRelOp @op a (reifySignedNat @sign @n)) $
+        "bad value"
 
 data Sign = Pos | Neg
 
diff --git a/src/Rerefined/Predicate/Via.hs b/src/Rerefined/Predicate/Via.hs
--- a/src/Rerefined/Predicate/Via.hs
+++ b/src/Rerefined/Predicate/Via.hs
@@ -1,47 +1,29 @@
-{-# LANGUAGE UndecidableInstances #-} -- for PredicateName
-{-# LANGUAGE OverloadedStrings #-} -- for builder
-{-# LANGUAGE AllowAmbiguousTypes #-} -- for validateVia
+{-# LANGUAGE OverloadedStrings   #-} -- for builder
+{-# LANGUAGE AllowAmbiguousTypes #-} -- 'validateVia' is designed for this
 
 module Rerefined.Predicate.Via where
 
 import Rerefined.Predicate.Common
-import TypeLevelShow.Utils
 import GHC.Exts ( Proxy# )
 
-{- | Predicate @p@ is implemented via predicate @pVia@.
+{- | Implement 'validate' for predicate @p@ via @pVia@.
 
 This is useful when you need a unique data type for a predicate (e.g. for
 instances, clarity), but the predicate it tests already exists. In such cases,
 it would be nice to reuse the existing predicate, while printing both predicates
-in failures.
-
-'Via' assists in doing this. Implement your 'Predicate' instance as normal, then
-implement 'Refine' with:
-
-    'validate' = 'validateVia' \@pVia
+in failures i.e. "predicate X, implemented via predicate Y, failed with Z".
 
-Now when this predicate fails, it will print the @pVia@ failure with a wrapper
-stating the name of the original predicate.
+Call using visible type applications:
 
-Note that you may not use @DerivingVia@ because it only works on the last
-parameter of a multi-parameter type class, and I don't want to switch the order
-of the 'Refine' parameters. Even if I did, @DerivingVia@ isn't much different to
-or easier than this.
+@
+'validate' = 'validateVia' \@pVia
+@
 -}
-data Via pVia p
-instance (Predicate p, Predicate pVia)
-  => Predicate (Via pVia p) where
-    type PredicateName d (Via pVia p) = ShowParen (d > 9)
-        ("Via " ++ PredicateName 10 p ++ " " ++ PredicateName 10 pVia)
-instance (Refine pVia a, Predicate p, KnownPredicateName p)
-  => Refine (Via pVia p) a where
-    validate _p a =
-        case validate (proxy# @pVia) a of
-          Nothing -> Nothing
-          Just e  -> validateFail (proxy# @p) "via" [e]
-
 validateVia
     :: forall pVia p a
     .  (Refine pVia a, Predicate p, KnownPredicateName p)
     => Proxy# p -> a -> Maybe RefineFailure
-validateVia _p = validate (proxy# @(Via pVia p))
+validateVia p a =
+    case validate (proxy# @pVia) a of
+      Nothing -> Nothing
+      Just e  -> validateFail p "via" [e]
diff --git a/src/Rerefined/Predicates.hs b/src/Rerefined/Predicates.hs
--- a/src/Rerefined/Predicates.hs
+++ b/src/Rerefined/Predicates.hs
@@ -5,7 +5,7 @@
   -- * Base
     Succeed
   , Fail
-  , Via, validateVia
+  , validateVia
 
   -- * Logical
   , And, Iff, If, Nand, Nor, Not, Or, Xor
diff --git a/src/Rerefined/Refine.hs b/src/Rerefined/Refine.hs
--- a/src/Rerefined/Refine.hs
+++ b/src/Rerefined/Refine.hs
@@ -49,7 +49,7 @@
 --
 -- We may derive legal 'Functor', 'Traversable' instances for this as
 -- 'Rerefined.Predicate.Refine1' guarantees that the predicate only applies to
--- the functor structure. That is, you _may_ alter a 'Refined1' without
+-- the functor structure. That is, you /may/ alter a 'Refined1' without
 -- re-asserting its predicate, provided your changes are made without altering
 -- the structure/shape of @f@ (e.g. 'fmap', 'traverse').
 newtype Refined1 p f a = Refined1 (f a)
@@ -80,7 +80,8 @@
 unsafeRefine :: a -> Refined p a
 unsafeRefine = Refined
 
--- | Replace a 'Refined''s predicate without validating the new prdicate @pNew@.
+-- | Replace a 'Refined''s predicate without validating the new predicate
+--   @pNew@.
 --
 -- Unsafe. Use only when you can manually prove that the new predicate holds.
 unsafeRerefine :: forall pNew pOld a. Refined pOld a -> Refined pNew a
@@ -105,7 +106,7 @@
 unsafeRefine1 :: f a -> Refined1 p f a
 unsafeRefine1 = Refined1
 
--- | Replace a 'Refined1''s predicate without validating the new prdicate
+-- | Replace a 'Refined1''s predicate without validating the new predicate
 --   @pNew@.
 --
 -- Unsafe. Use only when you can manually prove that the new predicate holds.
diff --git a/src/Rerefined/Refine/TH.hs b/src/Rerefined/Refine/TH.hs
--- a/src/Rerefined/Refine/TH.hs
+++ b/src/Rerefined/Refine/TH.hs
@@ -9,6 +9,8 @@
 import Data.Text qualified as Text
 
 -- | Refine @a@ with predicate @p@ at compile time via Template Haskell.
+--
+-- Use like @$$('refineTH' \@p a)@.
 refineTH
     :: forall p a m
     .  (Refine p a, TH.Lift a, TH.Quote m, MonadFail m)
@@ -18,6 +20,8 @@
 
 -- | Refine @f a@ with functor predicate @p@ at compile time via Template
 --   Haskell.
+--
+-- Use like @$$('refine1TH' \@p a)@.
 refine1TH
     :: forall p f a m
     .  (Refine1 p f, TH.Lift (f a), TH.Quote m, MonadFail m)