diff --git a/CHANGELOG.md b/CHANGELOG.md
--- a/CHANGELOG.md
+++ b/CHANGELOG.md
@@ -1,3 +1,8 @@
+## 0.5.0 (2023-05-05)
+  * allow text-2.0
+  * refactor strengthening code, rename some definitions
+  * use NeAcc instead of NonEmpty for strengthening failures
+
 ## 0.4.1 (2023-02-22)
   * add `DerivingVia` wrapper for generic instances (like `Generically`)
 
diff --git a/README.md b/README.md
--- a/README.md
+++ b/README.md
@@ -2,64 +2,132 @@
 [lib-barbies-hackage]: https://hackage.haskell.org/package/barbies
 
 # strongweak
-Purely convert between pairs of "weak" and "strong"/"validated" types, with good
-errors and generic derivers.
+Purely convert between pairs of "weak" and "strong"/"validated" types, with
+extensive failure reporting and powerful generic derivers. Alexis King's [Parse,
+don't validate][parse-dont-validate] pattern as a library.
 
-## Definition of strong and weak types
-Take a pair of types `(strong, weak)`. We state the following:
+## What? Why?
+[refined-blog]: http://nikita-volkov.github.io/refined/
 
-  * You may safely convert ("weaken") any `strong` value to a `weak` value.
-  * You can try to convert ("strengthen") any `weak` value to a `strong` value,
-    but it may fail.
+Haskell is a wonderful language for accurate data modelling. Algebraic data
+types (and GADTs as a fancy extension) enable defining highly restricted types
+which prevent even *representing* invalid or unwanted values. Great! And for the
+common case where you want to assert some predicate on a value but not change it
+(i.e. validate), we have the powerful [refined][refined-blog] library to reflect
+the existence of an asserted predicate in types. Fantastic!
 
-As a rule, a weak type should be *easier to use* than its related strong type.
-That is, it should have fewer invariants to consider or maintain. You could
-weaken an `a` to a `Maybe a`, but since a `Maybe a` is harder to use, it's not a
-candidate for this library.
+Sadly I'm often grounded by "Reality", who insists that we don't use these
+features everywhere because manipulating more complex types often means more
+busywork on the term level. So I resort to less accurate data models, or
+validating somewhat arbitrarily without assistance from the type system. I can
+often feel Alexis King looking disapprovingly at me.
 
-As an arbitrary limitation for ease of use, a strong type has only one
-associated weak type. The same weak type may be used for multiple strong types.
-This restriction guides the design of "good" strong-weak type pairs & keeps them
-synchronized, plus helps type inference.
+What if we defined two separate representations for a given model?
 
-### Examples
-The [refined][lib-refined-hackage] library defines a `newtype Refined p a =
-Refined a`. To get a `Refined`, you must test its associated predicate. You may
-recover the unrefined value by removing the newtype wrapper. Thus, you may
-strengthen `a`s into `Refined p a`s, and weaken vice versa.
+  * A **strong** representation, where no invalid values are permitted.
+    (Promise.)
+  * A **weak** representation, which doesn't necessarily enforce all the
+    invariants that the strong representation does, but is easier to manipulate.
 
-The `WordX` family are like bounded `Natural`s. We can consider `Natural` as a
-weak type, which can be strengthened into e.g. `Word8` by asserting
-well-boundedness.
+This way, we can use strong representations wherever possible e.g. passing
+between subsystems, and shift to the weak representation for intensive
+manipulation (and then back to strong at the end). Potential wins for
+simplicity, brevity and performance, albeit for some conversion overhead.
 
+Let's formalize the above as a pair of types `S` and `W`.
+
+  * Given a `strong :: S`, we can always turn it into a `weak :: W`.
+  * Given a `weak :: W`, we can only turn it into a `strong :: S` if it passes
+    all the checks
+
+We can write these as pure functions.
+
+```haskell
+weaken     :: S ->       W
+strengthen :: W -> Maybe S
+```
+
+Oh! So this is like a parser-printer pair for arbitrary data. It seems like a
+useful enough pattern. Let's think of some strongweak pairs:
+
+  * `Word8` is a bounded natural number. `Natural` can represent any natural
+    number. So `Natural` is a weak type, which can be strengthened into `Word8`
+    (or `Word16`, `Word32`, ...) by asserting well-boundedness.
+  * `[a]` doesn't have state any predicates. But we could weaken every `a` in
+    the list. So `[a]` is a strong type, which can be weakened to `[Weak a]`.
+  * `NonEmpty a` *does* have a predicate. For useability and other reasons, we
+    only handle this predicate, and don't also weaken each `a` like above.
+    `NonEmpty a` weakens to `[a]`.
+
+But there's a hefty amount of boilerplate:
+
+  * You need to model all the data types you want to use like this twice.
+  * You need to write tons more definitions.
+
+Aaaand it's already not worth it. Sigh.
+
+## Library introduction
+strongweak encodes the above strong/weak representation pattern for convenient
+use, automating as much as possible. Some decisions restrict usage for nicer
+behaviour. The primary definitions are below:
+
+```haskell
+class Weaken a where
+    type Weak a :: Type
+    weaken :: a :: Weak a
+
+type Result = Validation Fails
+type Fails = NeAcc Fail
+class Weaken a => Strengthen a where
+    strengthen :: Weak a -> Result a
+```
+
+Note that a strong type may have only one associated weak type. The same weak
+type may be used for multiple strong types. This restriction guides the design
+of "good" strong-weak type pairs, keeps them synchronized, and aids type
+inference.
+
+See the documentation on Hackage for further details.
+
 ## Cool points
-### Validates as much as possible
-This is primarily a validation library. Thus, we don't fail on the first error
--- we attempt to validate every part of a data type, and collate the errors into
-a big list. (`ApplicativeDo` plus `Validation` is magical.)
+### Extreme error clarity
+strongweak is primarily a validation library. As such, strengthening failure
+handling receives special attention:
 
+  * Failures do not short-circuit; if a strengthening is made up of multiple
+    smaller strengthenings, all are run and any failures collated.
+  * Failures display the weak and strong (target) type.
+  * Generic strengthening is scarily verbose: see below for details.
+
 ### One definition, strong + weak views
 Using a type-level `Strength` switch and the `SW` type family, you can write a
 single datatype definition and receive both a strong and a weak representation,
 which the generic derivers can work with. See the `Strongweak.SW` module for
 details.
 
-### Generic strengthening is extremely powerful
+### Powerful generic instances
 There are generic derivers for generating `Strengthen` and `Weaken` instances
-between arbitrary data types. The `Strengthen` instances annotate errors
-extensively, telling you the datatype & record for which strengthening failed -
-recursively, for nested types!
+between *compatible* data types. The `Strengthen` instances annotate errors
+extensively, telling you the datatype, constructor and field for which
+strengthening failed!
 
-Note that the generic derivers work with any pair of matching data types. But
-they must match very closely: both types are traversed in tandem, so every pair
-of fields must be compatible. If you need to do calculation to move between your
-strong and weak types, consider splitting it into calculation -> strengthening
-and using the generic derivers. Or write your own instances.
+Two types are *compatible* if
 
+  * their generic SOP representations match precisely, and
+  * every pair of leaf types is either identical or has the appropriate
+    strengthen/weaken instance
+
+The `SW` type family is here to help for accomplishing that. Otherwise, if your
+types don't fit:
+
+  * convert to a "closer" representation first
+  * write your own instances (fairly simple with `ApplicativeDo`).
+
 ### Backdoors included
 Sometimes you have can guarantee that a weak value can be safely strengthened,
 but the compiler doesn't know - a common problem in parsing. In such cases, you
 may use efficient unsafe strengthenings, which don't perform invariant checks.
+Even better, they might explode your computer if you use them wrong!
 
 ## What this library isn't
 ### Not a convertible
@@ -70,13 +138,19 @@
 [witch](https://hackage.haskell.org/package/witch) library.
 
 ### Not particularly speedy
-The emphasis is on safety, possibly at the detriment of performance. However, my
-expectation is that you only strengthen & weaken at the "edges" of your program,
-and most of the time will be spent transforming weak representations. This may
-improve performance if it means invariants don't have to be continually asserted
-inline, but it also may slow things down e.g. `Natural`s are slower than
-`Word`s.
+The emphasis is on safety, which may come at the detriment of performance:
 
+  * Strengthening and weakening might be slow. This depends on the type and the
+    implementation. I try a little to ensure good performance, but not a lot.
+  * Strong types can be more performant than their weak counterparts. For
+    example, swapping all integrals for `Natural`s and `Integer`s will make your
+    program slow.
+    * You may avoid this fairly easily by simply not wrapping certain fields.
+
+On the other hand, by only strengthening at the "edges" of your program and
+knowing that between those you may transform the weak representation as you
+like, you may find good performance easier to maintain.
+
 ## Related projects
 ### barbies
 The [barbies][lib-barbies-hackage] library is an investigation into how far the
@@ -97,3 +171,10 @@
 via traverse (rather than doing both at once via applicative do). That thinking
 helps reassure me that these ideas are separate. *(Note: I would hesitate to
 write such a type, because the definition would start to get mighty complex.)*
+
+## Other
+### Can this be formalized or generalized in some useful way?
+I note that this library is basically a couple of type classes and utilities for
+automating writing parsers and printers for types which are "close". I can't
+find anything in the literature that discusses this sort of thing. If you would
+have some info there, please do let me know!
diff --git a/src/Strongweak.hs b/src/Strongweak.hs
--- a/src/Strongweak.hs
+++ b/src/Strongweak.hs
@@ -1,12 +1,24 @@
-{-# LANGUAGE UndecidableInstances #-}
+{- | Main import module for basic use.
+
+For defining 'Strengthen' instances, import "Strongweak.Strengthen".
+-}
+
 module Strongweak
   (
   -- * Instance design
   -- $strongweak-instance-design
 
-  -- * Re-exports
-    module Strongweak.Weaken
-  , module Strongweak.Strengthen
+  -- * Classes
+    Weaken(..)
+  , Strengthen(..)
+
+  -- * Other definitions
+  , liftWeakF
+
+  -- * Strength switch wrapper
+  , Strength(..)
+  , type SW
+
   ) where
 
 import Strongweak.Weaken
diff --git a/src/Strongweak/Generic/Strengthen.hs b/src/Strongweak/Generic/Strengthen.hs
--- a/src/Strongweak/Generic/Strengthen.hs
+++ b/src/Strongweak/Generic/Strengthen.hs
@@ -7,16 +7,19 @@
 (D), constructor (C) and selector (S).
 -}
 
+-- both required due to type class design
 {-# LANGUAGE AllowAmbiguousTypes #-}
+{-# LANGUAGE UndecidableInstances #-}
 
 module Strongweak.Generic.Strengthen where
 
 import Strongweak.Strengthen
 import Data.Either.Validation
-import Data.List.NonEmpty
 import GHC.Generics
+import Data.Kind
+import GHC.TypeNats
+import GHC.Exts ( proxy#, Proxy# )
 
-import Numeric.Natural
 import Control.Applicative ( liftA2 )
 
 -- | Strengthen a value generically.
@@ -25,78 +28,88 @@
 -- the definition of compatibility in this context.
 strengthenGeneric
     :: (Generic w, Generic s, GStrengthenD (Rep w) (Rep s))
-    => w -> Validation (NonEmpty StrengthenFail) s
+    => w -> Result s
 strengthenGeneric = fmap to . gstrengthenD . from
 
 -- | Generic strengthening at the datatype level.
 class GStrengthenD w s where
-    gstrengthenD :: w p -> Validation (NonEmpty StrengthenFail) (s p)
+    gstrengthenD :: w p -> Result (s p)
 
 -- | Enter a datatype, stripping its metadata wrapper.
-instance (GStrengthenC w s, Datatype dw, Datatype ds) => GStrengthenD (D1 dw w) (D1 ds s) where
-    gstrengthenD = fmap M1 . gstrengthenC (datatypeName' @dw) (datatypeName' @ds) . unM1
+instance GStrengthenC wcd scd w s => GStrengthenD (D1 wcd w) (D1 scd s) where
+    gstrengthenD = fmap M1 . gstrengthenC @wcd @scd . unM1
 
 -- | Generic strengthening at the constructor sum level.
-class GStrengthenC w s where
-    gstrengthenC :: String -> String -> w p -> Validation (NonEmpty StrengthenFail) (s p)
+class GStrengthenC wcd scd w s where
+    gstrengthenC :: w p -> Result (s p)
 
 -- | Nothing to do for empty datatypes.
-instance GStrengthenC V1 V1 where
-    gstrengthenC _ _ = Success
+instance GStrengthenC wcd scd V1 V1 where gstrengthenC = Success
 
 -- | Strengthen sum types by casing and strengthening left or right.
-instance (GStrengthenC lw ls, GStrengthenC rw rs) => GStrengthenC (lw :+: rw) (ls :+: rs) where
-    gstrengthenC dw ds = \case L1 l -> L1 <$> gstrengthenC dw ds l
-                               R1 r -> R1 <$> gstrengthenC dw ds r
+instance
+  ( GStrengthenC wcd scd wl sl
+  , GStrengthenC wcd scd wr sr
+  ) => GStrengthenC wcd scd (wl :+: wr) (sl :+: sr) where
+    gstrengthenC = \case L1 l -> L1 <$> gstrengthenC @wcd @scd l
+                         R1 r -> R1 <$> gstrengthenC @wcd @scd r
 
 -- | Enter a constructor, stripping its metadata wrapper.
-instance (GStrengthenS w s, Constructor cw, Constructor cs) => GStrengthenC (C1 cw w) (C1 cs s) where
-    gstrengthenC dw ds = fmap M1 . snd . gstrengthenS dw ds (conName' @cw) (conName' @cs) 0 . unM1
-
-{- | Generic strengthening at the selector product level.
+instance GStrengthenS wcd scd wcc scc 0 w s
+  => GStrengthenC wcd scd (C1 wcc w) (C1 scc s) where
+    gstrengthenC = fmap M1 . gstrengthenS @wcd @scd @wcc @scc @0 . unM1
 
-In order to calculate field indices, we return the current field index alongside
-the result. This way, the product case can strengthen the left branch, then
-increment the returned field index and use it for strengthening the right
-branch.
--}
-class GStrengthenS w s where
-    gstrengthenS
-        :: String  -- ^ weak   datatype name
-        -> String  -- ^ strong datatype name
-        -> String  -- ^ weak   constructor name
-        -> String  -- ^ strong constructor name
-        -> Natural -- ^ current field index (0, from left)
-        -> w p -> (Natural, Validation (NonEmpty StrengthenFail) (s p))
+-- | Generic strengthening at the constructor level.
+class GStrengthenS wcd scd wcc scc (si :: Natural) w s where
+    gstrengthenS :: w p -> Result (s p)
 
 -- | Nothing to do for empty constructors.
-instance GStrengthenS U1 U1 where
-    gstrengthenS _ _ _ _ n x = (n, Success x)
+instance GStrengthenS wcd scd wcc scc si U1 U1 where gstrengthenS = Success
 
 -- | Strengthen product types by strengthening left and right.
---
--- This is ordered (left then right) in order to pass the field index along.
-instance (GStrengthenS lw ls, GStrengthenS rw rs) => GStrengthenS (lw :*: rw) (ls :*: rs) where
-    gstrengthenS dw ds cw cs n (l :*: r) = (n'', liftA2 (:*:) l' r')
-      where
-        (n',  l') = gstrengthenS dw ds cw cs n      l
-        (n'', r') = gstrengthenS dw ds cw cs (n'+1) r
+instance
+  ( GStrengthenS wcd scd wcc scc si                  wl sl
+  , GStrengthenS wcd scd wcc scc (si + ProdArity wl) wr sr
+  ) => GStrengthenS wcd scd wcc scc si (wl :*: wr) (sl :*: sr) where
+    gstrengthenS (l :*: r) =
+        liftA2 (:*:)
+               (gstrengthenS @wcd @scd @wcc @scc @si                  l)
+               (gstrengthenS @wcd @scd @wcc @scc @(si + ProdArity wl) r)
 
 -- | Special case: if source and target types are equal, copy the value through.
-instance GStrengthenS (S1 mw (Rec0 w)) (S1 ms (Rec0 w)) where
-    gstrengthenS _ _ _ _ n x = (n, Success (M1 (unM1 x)))
+instance GStrengthenS wcd scd wcc scc si (S1 wcs (Rec0 a)) (S1 scs (Rec0 a)) where
+    gstrengthenS = Success . M1 . unM1
 
 -- | Strengthen a field using the existing 'Strengthen' instance.
-instance {-# OVERLAPS #-} (Strengthen s, Weak s ~ w, Selector mw, Selector ms) => GStrengthenS (S1 mw (Rec0 w)) (S1 ms (Rec0 s)) where
-    gstrengthenS dw ds cw cs n (M1 (K1 w)) =
-        case strengthen w of
-          Failure es ->
-            let fw = selName'' @mw
-                fs = selName'' @ms
-                e  = StrengthenFailField dw ds cw cs n fw n fs es
-            in  (n, Failure $ e :| [])
-          Success s   -> (n, Success $ M1 $ K1 s)
+instance {-# OVERLAPS #-}
+  ( Weak s ~ w -- has to be here, else "illegal typesym family app in instance"
+  , Strengthen s
+  , Datatype wcd, Datatype scd
+  , Constructor wcc, Constructor scc
+  , Selector wcs, Selector scs
+  , KnownNat si
+  ) => GStrengthenS wcd scd wcc scc si (S1 wcs (Rec0 w)) (S1 scs (Rec0 s)) where
+    gstrengthenS = unM1 .> unK1 .> strengthen .> \case
+      Success s  -> Success $ M1 $ K1 s
+      Failure es -> Failure $ pure e
+        where
+          e = FailField wcd scd wcc scc si wcs si scs es
+          wcd = datatypeName' @wcd
+          scd = datatypeName' @scd
+          wcc = conName' @wcc
+          scc = conName' @scc
+          wcs = selName'' @wcs
+          scs = selName'' @scs
+          si = natVal'' @si
 
+--------------------------------------------------------------------------------
+
+-- from flow
+(.>) :: (a -> b) -> (b -> c) -> a -> c
+f .> g = g . f
+
+--------------------------------------------------------------------------------
+
 -- | Get the record name for a selector if present.
 --
 -- On the type level, a 'Maybe Symbol' is stored for record names. But the
@@ -106,8 +119,6 @@
 selName'' = case selName' @s of "" -> Nothing
                                 s  -> Just s
 
---------------------------------------------------------------------------------
-
 -- | 'conName' without the value (only used as a proxy). Lets us push our
 --   'undefined's into one place.
 conName' :: forall c. Constructor c => String
@@ -122,3 +133,15 @@
 --   'undefined's into one place.
 selName' :: forall s. Selector s => String
 selName' = selName @s undefined
+
+--------------------------------------------------------------------------------
+
+type family ProdArity (f :: Type -> Type) :: Natural where
+    ProdArity (S1 c f)  = 1
+    ProdArity (l :*: r) = ProdArity l + ProdArity r
+
+--------------------------------------------------------------------------------
+
+natVal'' :: forall n. KnownNat n => Natural
+natVal'' = natVal' (proxy# :: Proxy# n)
+{-# INLINE natVal'' #-}
diff --git a/src/Strongweak/Strengthen.hs b/src/Strongweak/Strengthen.hs
--- a/src/Strongweak/Strengthen.hs
+++ b/src/Strongweak/Strengthen.hs
@@ -1,45 +1,60 @@
 {-# LANGUAGE OverloadedStrings #-}
-{-# LANGUAGE CPP #-}
+{-# LANGUAGE AllowAmbiguousTypes #-}
 
 module Strongweak.Strengthen
   (
   -- * 'Strengthen' class
     Strengthen(..)
-
-  -- * Strengthen failures
-  , StrengthenFail(..)
-  , strengthenFailPretty
-  , strengthenFailBase
-
-  -- * Restrengthening
   , restrengthen
+  , Result
 
-  -- * Helpers
+  -- ** Helpers
   , strengthenBounded
 
+  -- * Strengthen failures
+  , Fails
+  , Fail(..)
+  , prettyFail
+
+  -- ** Helpers
+  , fail1
+  , failOther
+  , failShow
+  , maybeFailShow
+
   -- * Re-exports
   , Strongweak.Weaken.Weak
   ) where
 
+import Strongweak.Util.Typeable ( typeRep' )
+import Strongweak.Util.Text ( tshow )
 import Strongweak.Weaken ( Weaken(..) )
 import Data.Either.Validation
-import Type.Reflection ( Typeable, typeRep )
-import Prettyprinter
-import Prettyprinter.Render.String
+import Data.Typeable ( Typeable, TypeRep )
+import Prettyprinter qualified as Pretty
+import Prettyprinter ( Pretty(pretty), (<+>) )
+import Prettyprinter.Render.String qualified as Pretty
+import Prettyprinter.Render.Text qualified as Pretty
 
+import Data.Text ( Text )
+import Data.Text.Lazy qualified as Text.Lazy
 import GHC.TypeNats ( Natural, KnownNat )
 import Data.Word
 import Data.Int
-import Refined ( Refined, refine, Predicate )
+import Refined hiding ( Weaken, weaken, strengthen, NonEmpty )
 import Data.Vector.Generic.Sized qualified as VGS -- Shazbot!
 import Data.Vector.Generic qualified as VG
 import Data.Foldable qualified as Foldable
 import Control.Applicative ( liftA2 )
 import Data.Functor.Identity
 import Data.Functor.Const
-import Data.List.NonEmpty ( NonEmpty( (:|) ) )
+import Acc.NeAcc
 import Data.List.NonEmpty qualified as NonEmpty
+import Data.List.NonEmpty ( NonEmpty )
 
+type Result = Validation Fails
+type Fails = NeAcc Fail
+
 {- | Attempt to strengthen some @'Weak' a@, asserting certain invariants.
 
 We take 'Weaken' as a superclass in order to maintain strong/weak type pair
@@ -53,7 +68,7 @@
 class Weaken a => Strengthen a where
     -- | Attempt to strengthen some @'Weak' a@ to its associated strong type
     --   @a@.
-    strengthen :: Weak a -> Validation (NonEmpty StrengthenFail) a
+    strengthen :: Weak a -> Result a
 
 -- | Weaken a strong value, then strengthen it again.
 --
@@ -65,22 +80,31 @@
 -- Failure ...
 restrengthen
     :: (Strengthen a, Weaken a)
-    => a -> Validation (NonEmpty StrengthenFail) a
+    => a -> Result a
 restrengthen = strengthen . weaken
 
--- | Strengthen failure data type. Don't use these constructors directly, use
---   the existing helper functions.
---
--- Field indices are from 0 in the respective constructor. Field names are
--- provided if present.
-data StrengthenFail
-  = StrengthenFailBase
-        String -- ^ weak   type
-        String -- ^ strong type
-        String -- ^ weak value
-        String -- ^ msg
+-- | A failure encountered during strengthening.
+data Fail
+  -- | A failure containing lots of detail. Use in concrete instances where you
+  --   already have the 'Show's and 'Typeable's needed.
+  = FailShow
+        TypeRep -- ^ weak   type
+        TypeRep -- ^ strong type
+        (Maybe Text) -- ^ weak value
+        [Text] -- ^ failure description
 
-  | StrengthenFailField
+  -- | A failure. Use in abstract instances to avoid heavy contexts. (Remember
+  --   that generic strengtheners should wrap these nicely anyway!)
+  | FailOther
+        [Text] -- ^ failure description
+
+  -- | Some failures occurred when strengthening from one data type to another.
+  --
+  -- Field indices are from 0 in the respective constructor. Field names are
+  -- provided if are present in the type.
+  --
+  -- This is primarily intended to be used by generic strengtheners.
+  | FailField
         String                      -- ^ weak   datatype name
         String                      -- ^ strong datatype name
         String                      -- ^ weak   constructor name
@@ -89,56 +113,102 @@
         (Maybe String)              -- ^ weak   field name (if present)
         Natural                     -- ^ strong field index
         (Maybe String)              -- ^ strong field name (if present)
-        (NonEmpty StrengthenFail)   -- ^ failures
-    deriving stock Eq
+        Fails                       -- ^ failures
 
-instance Show StrengthenFail where
-    showsPrec _ = renderShowS . layoutPretty defaultLayoutOptions . pretty
+prettyFail :: Fail -> Text.Lazy.Text
+prettyFail = Pretty.renderLazy . prettyLayoutFail
 
+prettyLayoutFail :: Fail -> Pretty.SimpleDocStream ann
+prettyLayoutFail = Pretty.layoutPretty Pretty.defaultLayoutOptions . pretty
+
+fail1 :: Fail -> Result a
+fail1 = Failure . pure
+
+failOther :: [Text] -> Result a
+failOther = fail1 . FailOther
+
+buildFailShow
+    :: forall w s. (Typeable w, Typeable s)
+    => Maybe Text -> [Text] -> Result s
+buildFailShow mwv = fail1 . FailShow (typeRep' @w) (typeRep' @s) mwv
+
+failShow'
+    :: forall s w. (Typeable w, Show w, Typeable s)
+    => (w -> Text) -> w -> [Text] -> Result s
+failShow' f w = buildFailShow @w @s (Just (f w))
+
+failShow
+    :: forall s w. (Typeable w, Show w, Typeable s)
+    => w -> [Text] -> Result s
+failShow = failShow' tshow
+
+-- | This reports the weak and strong type, so no need to include those in the
+--   failure detail.
+failShowNoVal :: forall w s. (Typeable w, Typeable s) => [Text] -> Result s
+failShowNoVal = buildFailShow @w @s Nothing
+
+instance Show Fail where
+    showsPrec _ = Pretty.renderShowS . prettyLayoutFail
+
 -- TODO shorten value if over e.g. 50 chars. e.g. @[0,1,2,...,255] -> FAIL@
-instance Pretty StrengthenFail where
+instance Pretty Fail where
     pretty = \case
-      StrengthenFailBase wt st wv msg ->
-        vsep [ pretty wt<+>"->"<+>pretty st
-             , pretty wv<+>"->"<+>"FAIL"
-             , pretty msg ]
-      StrengthenFailField dw _ds cw _cs iw fw _is _fs es ->
+      FailShow wt st mwv detail -> Pretty.vsep $
+        case mwv of
+          Nothing -> [typeDoc, detailDoc]
+          Just wv ->
+            let valueDoc = "value: "<+>pretty wv<+>"->"<+>"FAIL"
+            in  [typeDoc, valueDoc, detailDoc]
+        where
+          typeDoc   = "type:  "<+>prettyTypeRep wt<+>"->"<+>prettyTypeRep st
+          detailDoc = case detail of
+            []           -> "<no detail>"
+            [detailLine] -> "detail:"<+>pretty detailLine
+            _            -> "detail:"<>Pretty.line<>prettyList detail
+
+      FailOther detail -> pretty detail
+
+      -- TODO should inspect meta, shorten if identical (currently only using
+      -- weak)
+      FailField dw _ds cw _cs iw fw _is _fs es ->
         let sw = maybe (show iw) id fw
-        in  nest 0 $ pretty dw<>"."<>pretty cw<>"."<>pretty sw<>line<>strengthenFailPretty es
+        in  Pretty.nest 0 $ pretty dw<>"."<>pretty cw<>"."<>pretty sw<>Pretty.line<>prettyList es
 
 -- mutually recursive with its 'Pretty' instance. safe, but a bit confusing -
 -- clean up
-strengthenFailPretty :: NonEmpty StrengthenFail -> Doc a
-strengthenFailPretty = vsep . map go . Foldable.toList
-  where go e = "-"<+>indent 0 (pretty e)
+prettyList :: (Foldable f, Pretty a) => f a -> Pretty.Doc ann
+prettyList = Pretty.vsep . map go . Foldable.toList
+  where go e = "-"<+>Pretty.indent 0 (pretty e)
 
-strengthenFailBase
-    :: forall s w. (Typeable w, Show w, Typeable s)
-    => w -> String -> Validation (NonEmpty StrengthenFail) s
-strengthenFailBase w msg = Failure (e :| [])
-  where e = StrengthenFailBase (show $ typeRep @w) (show $ typeRep @s) (show w) msg
+-- | Succeed on 'Just', fail with given detail on 'Nothing'.
+maybeFailShow
+    :: forall a. (Typeable (Weak a), Typeable a)
+    => [Text] -> Maybe a -> Result a
+maybeFailShow detail = \case
+    Just a  -> Success a
+    Nothing -> failShowNoVal @(Weak a) detail
 
 -- | Assert a predicate to refine a type.
-instance (Predicate (p :: k) a, Typeable k, Typeable a, Show a) => Strengthen (Refined p a) where
-    strengthen a =
-        case refine a of
-          Left  err -> strengthenFailBase a (show err)
-          Right ra  -> Success ra
+instance (Predicate (p :: k) a, Typeable k, Typeable a)
+  => Strengthen (Refined p a) where
+    strengthen = refine .> \case
+      Left  rex -> failShowNoVal @a
+        [ "refinement: "<>tshow (typeRep' @p)
+        , "failed with..."
+        , tshow (displayRefineException rex)
+        ]
+      Right ra  -> Success ra
 
 -- | Strengthen a plain list into a non-empty list by asserting non-emptiness.
-instance (Typeable a, Show a) => Strengthen (NonEmpty a) where
-    strengthen a =
-        case NonEmpty.nonEmpty a of
-          Just a' -> Success a'
-          Nothing -> strengthenFailBase a "empty list"
+instance Typeable a => Strengthen (NonEmpty a) where
+    strengthen = NonEmpty.nonEmpty .> maybeFailShow ["empty list"]
 
 -- | Strengthen a plain list into a sized vector by asserting length.
-instance (VG.Vector v a, KnownNat n, Typeable v, Typeable a, Show a)
-  => Strengthen (VGS.Vector v n a) where
-    strengthen w =
-        case VGS.fromList w of
-          Nothing -> strengthenFailBase w "TODO bad size vector"
-          Just s  -> Success s
+instance
+  ( VG.Vector v a, KnownNat n
+  , Typeable v, Typeable a
+  ) => Strengthen (VGS.Vector v n a) where
+      strengthen = VGS.fromList .> maybeFailShow ["incorrect length"]
 
 -- | Add wrapper.
 instance Strengthen (Identity a) where
@@ -167,17 +237,23 @@
 instance Strengthen Int32  where strengthen = strengthenBounded
 instance Strengthen Int64  where strengthen = strengthenBounded
 
+-- | Strengthen one numeric type into another.
+--
+-- @n@ must be "wider" than @m@.
 strengthenBounded
-    :: forall b n
-    .  (Integral b, Bounded b, Show b, Typeable b, Integral n, Show n, Typeable n)
-    => n -> Validation (NonEmpty StrengthenFail) b
-strengthenBounded n =
-    if   n <= maxB && n >= minB then Success (fromIntegral n)
-    else strengthenFailBase n $ "not well bounded, require: "
-                                 <>show minB<>" <= n <= "<>show maxB
+    :: forall m n
+    .  ( Typeable n, Integral n, Show n
+       , Typeable m, Integral m, Show m, Bounded m
+       ) => n -> Result m
+strengthenBounded n
+  | n <= maxB && n >= minB = Success (fromIntegral n)
+  | otherwise = failShow n
+        [ "not well bounded, require: "
+          <>tshow minB<>" <= n <= "<>tshow maxB
+        ]
   where
-    maxB = fromIntegral @b @n maxBound
-    minB = fromIntegral @b @n minBound
+    maxB = fromIntegral @m @n maxBound
+    minB = fromIntegral @m @n minBound
 
 --------------------------------------------------------------------------------
 
@@ -193,3 +269,12 @@
 instance (Strengthen a, Strengthen b) => Strengthen (Either a b) where
     strengthen = \case Left  a -> Left  <$> strengthen a
                        Right b -> Right <$> strengthen b
+
+--------------------------------------------------------------------------------
+
+prettyTypeRep :: TypeRep -> Pretty.Doc a
+prettyTypeRep = pretty . show
+
+-- from flow
+(.>) :: (a -> b) -> (b -> c) -> a -> c
+f .> g = g . f
diff --git a/src/Strongweak/Util/Text.hs b/src/Strongweak/Util/Text.hs
new file mode 100644
--- /dev/null
+++ b/src/Strongweak/Util/Text.hs
@@ -0,0 +1,7 @@
+module Strongweak.Util.Text where
+
+import Data.Text qualified as Text
+import Data.Text ( Text )
+
+tshow :: Show a => a -> Text
+tshow = Text.pack . show
diff --git a/src/Strongweak/Util/Typeable.hs b/src/Strongweak/Util/Typeable.hs
new file mode 100644
--- /dev/null
+++ b/src/Strongweak/Util/Typeable.hs
@@ -0,0 +1,8 @@
+{-# LANGUAGE AllowAmbiguousTypes #-}
+
+module Strongweak.Util.Typeable where
+
+import Data.Typeable
+
+typeRep' :: forall a. Typeable a => TypeRep
+typeRep' = typeRep (Proxy @a)
diff --git a/src/Strongweak/Weaken.hs b/src/Strongweak/Weaken.hs
--- a/src/Strongweak/Weaken.hs
+++ b/src/Strongweak/Weaken.hs
@@ -1,16 +1,18 @@
+{-# LANGUAGE UndecidableInstances #-} -- for SWDepth
+
 module Strongweak.Weaken
   (
   -- * 'Weaken' class
     Weaken(..)
   , liftWeakF
 
-  -- * 'SW' helper
+  -- * Strength switch helper
   , Strength(..)
-  , SW
+  , type SW
+  , type SWDepth
   ) where
 
 import Refined ( Refined, unrefine )
-import Numeric.Natural ( Natural )
 import Data.Word
 import Data.Int
 import Data.Vector.Generic.Sized qualified as VGS -- Shazbot!
@@ -20,6 +22,7 @@
 import Data.Functor.Const
 import Data.List.NonEmpty qualified as NonEmpty
 import Data.List.NonEmpty ( NonEmpty )
+import GHC.TypeNats
 
 {- | Weaken some @a@, relaxing certain invariants.
 
@@ -32,7 +35,8 @@
     -- | Weaken some @a@ to its associated weak type @'Weak' a@.
     weaken :: a -> Weak a
 
--- | Lift a function on a weak type to the associated strong type.
+-- | Lift a function on a weak type to the associated strong type by weakening
+--   first.
 liftWeakF :: Weaken a => (Weak a -> b) -> (a -> b)
 liftWeakF f = f . weaken
 
@@ -57,6 +61,12 @@
 type family SW (s :: Strength) a :: Type where
     SW 'Strong a = a
     SW 'Weak   a = Weak a
+
+-- | Track multiple levels of weakening. Silly thought I had, don't think it's
+--   useful.
+type family SWDepth (n :: Natural) a :: Type where
+    SWDepth 0 a = a
+    SWDepth n a = Weak (SWDepth (n-1) a)
 
 -- | Strip refined type refinement.
 instance Weaken (Refined p a) where
diff --git a/strongweak.cabal b/strongweak.cabal
--- a/strongweak.cabal
+++ b/strongweak.cabal
@@ -5,7 +5,7 @@
 -- see: https://github.com/sol/hpack
 
 name:           strongweak
-version:        0.4.1
+version:        0.5.0
 synopsis:       Convert between strong and weak representations of types
 description:    Please see README.md.
 category:       Data
@@ -35,6 +35,8 @@
       Strongweak.Generic.Weaken
       Strongweak.Strengthen
       Strongweak.Strengthen.Unsafe
+      Strongweak.Util.Text
+      Strongweak.Util.Typeable
       Strongweak.Weaken
   other-modules:
       Paths_strongweak
@@ -53,10 +55,12 @@
       MagicHash
   ghc-options: -Wall
   build-depends:
-      base >=4.14 && <5
+      acc >=0.2.0.1 && <0.3
+    , base >=4.14 && <5
     , either >=5.0.1.1 && <5.1
     , prettyprinter >=1.7.1 && <1.8
     , refined >=0.7 && <0.9
+    , text >=1.2.5.0 && <2.1
     , vector >=0.12.3.1 && <0.14
     , vector-sized >=1.5.0 && <1.6
   default-language: GHC2021
@@ -87,6 +91,7 @@
       hspec-discover:hspec-discover >=2.7 && <2.10
   build-depends:
       QuickCheck >=2.14.2 && <2.15
+    , acc >=0.2.0.1 && <0.3
     , base >=4.14 && <5
     , either >=5.0.1.1 && <5.1
     , generic-random >=1.5.0.1 && <1.6
@@ -95,6 +100,7 @@
     , quickcheck-instances >=0.3.26 && <0.4
     , refined >=0.7 && <0.9
     , strongweak
+    , text >=1.2.5.0 && <2.1
     , vector >=0.12.3.1 && <0.14
     , vector-sized >=1.5.0 && <1.6
   default-language: GHC2021
diff --git a/test/Common.hs b/test/Common.hs
--- a/test/Common.hs
+++ b/test/Common.hs
@@ -1,6 +1,7 @@
 module Common where
 
 import Strongweak
+import Strongweak.Strengthen qualified as Strengthen
 import Strongweak.Generic
 import Refined hiding ( Weaken, weaken, strengthen, NonEmpty )
 import GHC.Generics ( Generic )
@@ -9,6 +10,7 @@
 import Numeric.Natural ( Natural )
 import Data.Word
 import Test.QuickCheck.Instances.Natural()
+import Data.Either.Validation
 
 data DS (s :: Strength)
   = DS0 (SW s Word8) (SW s Word8) Word8 (SW s Word8) (SW s Word8)
@@ -48,3 +50,6 @@
     type Weak (DP 'Strong) = DP 'Weak
     weaken = weakenGeneric
 instance Strengthen (DP 'Strong) where strengthen = strengthenGeneric
+
+tryStrengthenSuccessEq :: Eq a => a -> Strengthen.Result a -> Bool
+tryStrengthenSuccessEq a = \case Success a' -> a == a'; Failure{} -> False
diff --git a/test/Strongweak/LawsSpec.hs b/test/Strongweak/LawsSpec.hs
--- a/test/Strongweak/LawsSpec.hs
+++ b/test/Strongweak/LawsSpec.hs
@@ -9,10 +9,11 @@
 spec :: Spec
 spec = modifyMaxSize (+1000) $ do
     prop "weaken-strengthen roundtrip isomorphism (generic)" $ do
-      \(d :: DS 'Strong) -> strengthen (weaken d) `shouldBe` Success d
+      \(d :: DS 'Strong) ->
+        strengthen (weaken d) `shouldSatisfy` tryStrengthenSuccessEq d
     prop "strengthen-weaken-strengthen roundtrip partial isomorphism (generic)" $ do
       \(dw :: DS 'Weak) ->
         case strengthen @(DS 'Strong) dw of
-          Failure _  -> pure ()
+          Failure{}  -> pure ()
           Success ds ->
-            strengthen (weaken ds) `shouldBe` Success ds
+            strengthen (weaken ds) `shouldSatisfy` tryStrengthenSuccessEq ds
diff --git a/test/Strongweak/StrengthenSpec.hs b/test/Strongweak/StrengthenSpec.hs
--- a/test/Strongweak/StrengthenSpec.hs
+++ b/test/Strongweak/StrengthenSpec.hs
@@ -1,63 +1,70 @@
 module Strongweak.StrengthenSpec ( spec ) where
 
+import Strongweak.Util.Typeable
+import Strongweak.Util.Text
 import Strongweak
+import Strongweak.Strengthen
 import Common
 import Data.Either.Validation
 import Test.Hspec
 
 import Numeric.Natural ( Natural )
 import Data.Word
-import Data.List.NonEmpty ( NonEmpty(..) )
 import Data.Foldable qualified as Foldable
+import Data.Typeable ( TypeRep )
 
 spec :: Spec
 spec = do
     it "returns a precise error for failed generic strengthening (named field)" $ do
         let w = fromIntegral (maxBound @Word32) + 1
             d = DP w 43 1 2 3 :: DP 'Weak
-            e = sfGeneric1
-                    "DP" "DP" "DP" "DP" 0 (Just "dp1f0") 0 (Just "dp1f0")
-                    "Natural" "Word32" w
+            e = sfGenericSW1Show
+                    "DP" "DP" 0 (Just "dp1f0")
+                    (typeRep' @Natural) (typeRep' @Word32) w
         strengthen @(DP 'Strong) d `shouldSatisfy` svEqFail e
     it "returns a precise error for failed generic strengthening (unnamed field)" $ do
         let w = fromIntegral (maxBound @Word8) + 1
             d = DS0 0 1 2 3 w :: DS 'Weak
-            e = sfGeneric1
-                    "DS" "DS" "DS0" "DS0" 4 Nothing 4 Nothing
-                    "Natural" "Word8" w
+            e = sfGenericSW1Show
+                    "DS" "DS0" 4 Nothing
+                    (typeRep' @Natural) (typeRep' @Word8) w
         strengthen @(DS 'Strong) d `shouldSatisfy` svEqFail e
 
-sfGeneric1
+-- build strengthen failure
+-- one failure, generic with SW, one wrapped failure (detailed)
+sfGenericSW1Show
     :: Show w
-    => String -> String -> String -> String
-    -> Natural -> Maybe String -> Natural -> Maybe String
-    -> String -> String -> w
-    -> StrengthenFail
-sfGeneric1 dw ds cw cs iw fw is fs tw ts w =
-    StrengthenFailField dw ds cw cs iw fw is fs (e :| [])
-  where e = StrengthenFailBase tw ts (show w) (error "TODO ignoring msg")
+    => String -> String -> Natural -> Maybe String
+    -> TypeRep -> TypeRep -> w
+    -> Fail
+sfGenericSW1Show d c i f tw ts w =
+    FailField d d c c i f i f (pure e)
+  where
+    e = FailShow tw ts (Just (tshow w)) detail
+    detail = error "tried to check failure descriptions in tests (bad idea)"
 
-sfEqIgnoreMsg :: StrengthenFail -> StrengthenFail -> Bool
-sfEqIgnoreMsg s1 s2 = case s1 of
-  StrengthenFailField   dw  ds  cw  cs  iw  fw  is  fs  es -> case s2 of
-    StrengthenFailField dw' ds' cw' cs' iw' fw' is' fs' es' ->
-         dw == dw'
-      && ds == ds'
-      && cw == cw'
-      && cs == cs'
-      && iw == iw'
-      && fw == fw'
-      && is == is'
-      && fs == fs'
-      && and (zipWith sfEqIgnoreMsg (Foldable.toList es) (Foldable.toList es'))
+-- only test field and show, and ignore message in latter
+sfEq :: Fail -> Fail -> Bool
+sfEq s1 s2 = case s1 of
+  FailField   dw  ds  cw  cs  iw  fw  is  fs  es -> case s2 of
+    FailField dw' ds' cw' cs' iw' fw' is' fs' es' ->
+         dw == dw' && ds == ds'
+      && cw == cw' && cs == cs'
+      && iw == iw' && is == is'
+      && fw == fw' && fs == fs'
+      && and (zipWith sfEq (Foldable.toList es) (Foldable.toList es'))
     _ -> False
-  StrengthenFailBase   wt  st  wv  _ -> case s2 of
-    StrengthenFailBase wt' st' wv' _ ->
-         wt == wt'
-      && st == st'
-      && wv == wv'
+  FailShow   wt  st  wv  _ -> case s2 of
+    FailShow wt' st' wv' _ ->
+         wt  == wt' && st == st'
+      && wv  == wv'
     _ -> False
+  _ -> error "unexpected strengthen fail"
 
-svEqFail :: StrengthenFail -> Validation (NonEmpty StrengthenFail) s -> Bool
-svEqFail e = \case Failure (e' :| []) -> sfEqIgnoreMsg e e'
-                   _ -> False
+svEqFail :: Fail -> Result s -> Bool
+svEqFail e = \case
+  Success{}  -> False
+  Failure es ->
+    case Foldable.toList es of
+      [e'] -> sfEq e e'
+      _    -> False