diff --git a/CHANGELOG.md b/CHANGELOG.md
--- a/CHANGELOG.md
+++ b/CHANGELOG.md
@@ -1,3 +1,7 @@
+## 0.7.0 (2024-05-11)
+* replaced refined1 with rerefined
+* simplify failures
+
 ## 0.6.1 (2024-04-03)
   * tests: relax hspec upper bound
 
diff --git a/README.md b/README.md
--- a/README.md
+++ b/README.md
@@ -100,7 +100,6 @@
 
   * 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
diff --git a/src/Strongweak/Generic.hs b/src/Strongweak/Generic.hs
--- a/src/Strongweak/Generic.hs
+++ b/src/Strongweak/Generic.hs
@@ -1,3 +1,5 @@
+{-# LANGUAGE UndecidableInstances #-} -- required due to nested constraints
+
 -- | Generic 'strengthen' and 'weaken'.
 
 module Strongweak.Generic
@@ -13,10 +15,14 @@
   , GenericallySW(..)
   ) where
 
-import Strongweak.Generic.Weaken
-import Strongweak.Generic.Strengthen
-import Strongweak.Generic.Via
+import Strongweak.Weaken.Generic
+import Strongweak.Strengthen.Generic
 
+import Strongweak.Weaken ( Weaken(Weak, weaken) )
+import Strongweak.Strengthen ( Strengthen(strengthen) )
+import GHC.Generics
+import Data.Kind ( Type )
+
 {- $generic-derivation-compatibility
 
 The 'Strengthen' and 'Weaken' generic derivers allow you to derive instances
@@ -41,3 +47,44 @@
 metadata for you, but manually-derived Generic instances (which are usually a
 bad idea) do not require it.
 -}
+
+{- | @DerivingVia@ wrapper for strongweak instances.
+
+We can't use 'Generically' conveniently because we need to talk about two data
+types, not one -- we would have to do something like @'Generically' ('Tagged' w
+s)@, which is ugly. So we instead define our own adorable little "via type"
+here!
+
+Use like so:
+
+@
+data XYZ (s :: Strength) = XYZ
+  { xyz1 :: SW s Word8
+  , xyz2 :: Word8
+  , xyz3 :: ()
+  } deriving stock Generic
+deriving via (GenericallySW (XYZ 'Strong) (XYZ 'Weak)) instance Weaken (XYZ 'Strong)
+deriving via (GenericallySW (XYZ 'Strong) (XYZ 'Weak)) instance Strengthen (XYZ 'Strong)
+@
+
+TODO can't figure out a way around multiple standalone deriving declarations :(
+
+TODO maybe GenericallySW1? but even so instances differ between weaken and
+strengthen (weaken needs nothing) so it's kinda better this way. :)
+-}
+
+newtype GenericallySW s (w :: Type) = GenericallySW { unGenericallySW :: s }
+
+instance
+  ( Generic s, Generic w
+  , GWeaken (Rep s) (Rep w)
+  ) => Weaken (GenericallySW s w) where
+    type Weak (GenericallySW s w) = w
+    weaken = weakenGeneric . unGenericallySW
+
+instance
+  ( Generic s, Generic w
+  , GStrengthenD (Rep w) (Rep s)
+  , Weaken (GenericallySW s w)
+  ) => Strengthen (GenericallySW s w) where
+    strengthen = fmap GenericallySW . strengthenGeneric
diff --git a/src/Strongweak/Generic/Strengthen.hs b/src/Strongweak/Generic/Strengthen.hs
deleted file mode 100644
--- a/src/Strongweak/Generic/Strengthen.hs
+++ /dev/null
@@ -1,147 +0,0 @@
-{- | 'strengthen' over generic representations.
-
-Strengthen failures are annotated with precise information describing where the
-failure occurred: datatype name, constructor name, field index (and name if
-present). To achieve this, we split the generic derivation into 3 classes, each
-handling/"unwrapping" a different layer of the generic representation: datatype
-(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 GHC.Generics
-import Data.Kind
-import GHC.TypeNats
-import GHC.Exts ( proxy#, Proxy# )
-
-import Control.Applicative ( liftA2 )
-
--- | Strengthen a value generically.
---
--- The weak and strong types must be /compatible/. See 'Strongweak.Generic' for
--- the definition of compatibility in this context.
-strengthenGeneric
-    :: (Generic w, Generic s, GStrengthenD (Rep w) (Rep s))
-    => w -> Result s
-strengthenGeneric = fmap to . gstrengthenD . from
-
--- | Generic strengthening at the datatype level.
-class GStrengthenD w s where
-    gstrengthenD :: w p -> Result (s p)
-
--- | Enter a datatype, stripping its metadata wrapper.
-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 wcd scd w s where
-    gstrengthenC :: w p -> Result (s p)
-
--- | Nothing to do for empty datatypes.
-instance GStrengthenC wcd scd V1 V1 where gstrengthenC = Success
-
--- | Strengthen sum types by casing and strengthening left or right.
-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 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
-
--- | 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 wcd scd wcc scc si U1 U1 where gstrengthenS = Success
-
--- | Strengthen product types by strengthening left and right.
-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 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 #-}
-  ( 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
--- reification is done using @fromMaybe ""@. So we have to inspect the resulting
--- string to determine whether the field uses record syntax or not. (Silly.)
-selName'' :: forall s. Selector s => Maybe String
-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
-conName' = conName @c undefined
-
--- | 'datatypeName' without the value (only used as a proxy). Lets us push our
---   'undefined's into one place.
-datatypeName' :: forall d. Datatype d => String
-datatypeName' = datatypeName @d undefined
-
--- | 'selName' without the value (only used as a proxy). Lets us push our
---   '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/Generic/Via.hs b/src/Strongweak/Generic/Via.hs
deleted file mode 100644
--- a/src/Strongweak/Generic/Via.hs
+++ /dev/null
@@ -1,47 +0,0 @@
-{-# LANGUAGE UndecidableInstances #-} -- required due to nested constraints
-
-module Strongweak.Generic.Via where
-
-import Strongweak.Generic.Weaken
-import Strongweak.Generic.Strengthen
-import Strongweak
-import GHC.Generics
-import Data.Kind
-
-{- | @DerivingVia@ wrapper for strongweak instances.
-
-We can't use 'Generically' conveniently because we need to talk about two data
-types, not one -- we would have to do something like @'Generically' ('Tagged' w
-s)@, which is ugly. So we instead define our own adorable little "via type"
-here!
-
-Use like so:
-
-@
-data XYZ (s :: Strength) = XYZ
-  { xyz1 :: SW s Word8
-  , xyz2 :: Word8
-  , xyz3 :: ()
-  } deriving stock Generic
-deriving via (GenericallySW (XYZ 'Strong) (XYZ 'Weak)) instance Weaken (XYZ 'Strong)
-deriving via (GenericallySW (XYZ 'Strong) (XYZ 'Weak)) instance Strengthen (XYZ 'Strong)
-@
-
-TODO can't figure out a way around multiple standalone deriving declarations :(
--}
-
-newtype GenericallySW s (w :: Type) = GenericallySW { unGenericallySW :: s }
-
-instance
-  ( Generic s, Generic w
-  , GWeaken (Rep s) (Rep w)
-  ) => Weaken (GenericallySW s w) where
-    type Weak (GenericallySW s w) = w
-    weaken = weakenGeneric . unGenericallySW
-
-instance
-  ( Generic s, Generic w
-  , GStrengthenD (Rep w) (Rep s)
-  , Weaken (GenericallySW s w)
-  ) => Strengthen (GenericallySW s w) where
-    strengthen = fmap GenericallySW . strengthenGeneric
diff --git a/src/Strongweak/Generic/Weaken.hs b/src/Strongweak/Generic/Weaken.hs
deleted file mode 100644
--- a/src/Strongweak/Generic/Weaken.hs
+++ /dev/null
@@ -1,46 +0,0 @@
--- | 'weaken' over generic representations.
-
-module Strongweak.Generic.Weaken where
-
-import Strongweak.Weaken
-
-import GHC.Generics
-
--- | Weaken a value generically.
---
--- The weak and strong types must be /compatible/. See 'Strongweak.Generic' for
--- the definition of compatibility in this context.
-weakenGeneric :: (Generic s, Generic w, GWeaken (Rep s) (Rep w)) => s -> w
-weakenGeneric = to . gweaken . from
-
-class GWeaken s w where
-    gweaken :: s p -> w p
-
--- | Strip all meta.
-instance GWeaken s w => GWeaken (M1 is ms s) (M1 iw mw w) where
-    gweaken = M1 . gweaken . unM1
-
--- | Nothing to do for empty datatypes.
-instance GWeaken V1 V1 where
-    gweaken = id
-
--- | Nothing to do for empty constructors.
-instance GWeaken U1 U1 where
-    gweaken = id
-
--- | Special case: if source and target types are equal, copy the value through.
-instance GWeaken (Rec0 s) (Rec0 s) where
-    gweaken = id
-
--- | Weaken a field using the existing 'Weaken' instance.
-instance {-# OVERLAPS #-} (Weaken s, Weak s ~ w) => GWeaken (Rec0 s) (Rec0 w) where
-    gweaken = K1 . weaken . unK1
-
--- | Weaken product types by weakening left and right.
-instance (GWeaken ls lw, GWeaken rs rw) => GWeaken (ls :*: rs) (lw :*: rw) where
-    gweaken (l :*: r) = gweaken l :*: gweaken r
-
--- | Weaken sum types by casing and weakening left or right.
-instance (GWeaken ls lw, GWeaken rs rw) => GWeaken (ls :+: rs) (lw :+: rw) where
-    gweaken = \case L1 l -> L1 $ gweaken l
-                    R1 r -> R1 $ gweaken r
diff --git a/src/Strongweak/Strengthen.hs b/src/Strongweak/Strengthen.hs
--- a/src/Strongweak/Strengthen.hs
+++ b/src/Strongweak/Strengthen.hs
@@ -12,49 +12,38 @@
   , strengthenBounded
 
   -- * Strengthen failures
-  , Fails
-  , Fail(..)
-  , prettyFail
-
-  -- ** Helpers
-  , fail1
-  , failOther
-  , failShow
-  , maybeFailShow
+  , StrengthenFailure(..)
+  , failStrengthen1
+  , failStrengthen
 
   -- * Re-exports
   , Strongweak.Weaken.Weak
   ) where
 
 import Strongweak.Util.Typeable ( typeRep' )
-import Strongweak.Util.Text ( tshow )
+import Strongweak.Util.TypeNats ( natVal'' )
 import Strongweak.Weaken ( Weaken(..) )
 import Data.Either.Validation
-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.Typeable ( Typeable )
 
-import Data.Text ( Text )
-import Data.Text.Lazy qualified as Text.Lazy
-import GHC.TypeNats ( Natural, KnownNat )
+import GHC.TypeNats ( KnownNat )
 import Data.Word
 import Data.Int
-import Refined hiding ( Weaken, weaken, strengthen, NonEmpty )
+import Rerefined
 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 Acc.NeAcc
 import Data.List.NonEmpty qualified as NonEmpty
 import Data.List.NonEmpty ( NonEmpty )
 
-type Result = Validation Fails
-type Fails = NeAcc Fail
+import Data.Text.Builder.Linear qualified as TBL
+import GHC.Exts ( fromString )
 
+import Data.Bits ( FiniteBits )
+
+type Result = Validation StrengthenFailure
+
 {- | Attempt to strengthen some @'Weak' a@, asserting certain invariants.
 
 We take 'Weaken' as a superclass in order to maintain strong/weak type pair
@@ -84,150 +73,67 @@
 restrengthen = strengthen . weaken
 
 -- | 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
-
-  -- | 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.
+data StrengthenFailure = StrengthenFailure
+  { strengthenFailDetail :: [TBL.Builder]
+  -- ^ Detail on strengthen failure.
   --
-  -- This is primarily intended to be used by generic strengtheners.
-  | FailField
-        String                      -- ^ weak   datatype name
-        String                      -- ^ strong datatype name
-        String                      -- ^ weak   constructor name
-        String                      -- ^ strong constructor name
-        Natural                     -- ^ weak   field index
-        (Maybe String)              -- ^ weak   field name (if present)
-        Natural                     -- ^ strong field index
-        (Maybe String)              -- ^ strong field name (if present)
-        Fails                       -- ^ failures
-
-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 Fail where
-    pretty = \case
-      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
+  -- We use a list here for the cases where you want multiple lines of detail.
+  -- Separating with a newline would make prettifying later harder, so we delay.
 
-      -- 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  Pretty.nest 0 $ pretty dw<>"."<>pretty cw<>"."<>pretty sw<>Pretty.line<>prettyList es
+  , strengthenFailInner  :: [(TBL.Builder, StrengthenFailure)]
+  -- ^ Indexed.
+  } deriving stock Show
 
--- mutually recursive with its 'Pretty' instance. safe, but a bit confusing -
--- clean up
-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)
+failStrengthen
+    :: [TBL.Builder] -> [(TBL.Builder, StrengthenFailure)] -> Result a
+failStrengthen t fs = Failure $ StrengthenFailure t fs
 
--- | 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
+failStrengthen1 :: [TBL.Builder] -> Result a
+failStrengthen1 t = failStrengthen t []
 
--- | Assert a predicate to refine a type.
-instance (Predicate p a, Typeable a)
-  => Strengthen (Refined p a) where
+-- | Strengthen a type by refining it with a predicate.
+instance Refine p 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
+      Right ra -> Success ra
+      Left  rf -> failStrengthen1
+        [ "refinement failure:"
+        , TBL.fromText (prettyRefineFailure rf) ]
+        -- ^ TODO rerefined: provide a TBL pretty function
 
--- | Assert a functor predicate to refine a type.
-instance (Predicate1 p f, Typeable f, Typeable (a :: ak), Typeable ak)
-  => Strengthen (Refined1 p f a) where
+-- | Strengthen a type by refining it with a functor predicate.
+instance Refine1 p f => Strengthen (Refined1 p f a) where
     strengthen = refine1 .> \case
-      Left  rex -> failShowNoVal @(f a)
-        [ "refinement: "<>tshow (typeRep' @p)
-        , "failed with..."
-        , tshow (displayRefineException rex)
-        ]
-      Right ra  -> Success ra
+      Right ra -> Success ra
+      Left  rf -> failStrengthen1
+        [ "refinement failure:"
+        , TBL.fromText (prettyRefineFailure rf) ]
 
 -- | Strengthen a plain list into a non-empty list by asserting non-emptiness.
-instance Typeable a => Strengthen (NonEmpty a) where
-    strengthen = NonEmpty.nonEmpty .> maybeFailShow ["empty list"]
+instance Strengthen (NonEmpty a) where
+    strengthen = NonEmpty.nonEmpty .> \case
+      Just neas -> Success neas
+      Nothing   -> failStrengthen1 $
+        [ "type: [a] -> NonEmpty a"
+        , "fail: empty list" ]
 
 -- | Strengthen a plain list into a sized vector by asserting length.
-instance
-  ( VG.Vector v a, KnownNat n
-  , Typeable v, Typeable a
-  ) => Strengthen (VGS.Vector v n a) where
-      strengthen = VGS.fromList .> maybeFailShow ["incorrect length"]
+instance (VG.Vector v a, KnownNat n) => Strengthen (VGS.Vector v n a) where
+    -- TODO another case of TBL not supporting unbounded integrals
+    strengthen as =
+        case VGS.fromList as of
+          Just va -> Success va
+          Nothing -> failStrengthen1 $
+            [ "type: [a] -> Vector v "<>fromString (show n)<>" a"
+            , "fail: wrong length (got "<>TBL.fromDec (length as)<>")" ]
+      where n = natVal'' @n
 
 -- | Add wrapper.
 instance Strengthen (Identity a) where
-    strengthen = pure <$> Identity
+    strengthen = Success . Identity
 
 -- | Add wrapper.
 instance Strengthen (Const a b) where
-    strengthen = pure <$> Const
+    strengthen = Success . Const
 
 {- TODO controversial. seems logical, but also kinda annoying.
 instance (Show a, Typeable a) => Strengthen (Maybe a) where
@@ -251,30 +157,67 @@
 -- | Strengthen one numeric type into another.
 --
 -- @n@ must be "wider" than @m@.
+--
+-- @'FiniteBits' m@ and @'Show' n@ are for error printing. We're forced to
+-- @'Show' n@ because linear-text-builder can't print unbounded integrals. PR:
+-- https://github.com/Bodigrim/linear-builder/pull/20
 strengthenBounded
     :: forall m n
     .  ( Typeable n, Integral n, Show n
-       , Typeable m, Integral m, Show m, Bounded m
+       , Typeable m, Integral m, Bounded m, FiniteBits 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
+  | n <= maxBn && n >= minBn = Success (fromIntegral n)
+  | otherwise = failStrengthen1
+        [ "numeric strengthen: "<>fromString (show (typeRep' @n))
+          <>" -> "<>fromString (show (typeRep' @m))
+        , "bounds check does not hold: "
+          <>TBL.fromDec minBm<>" <= "<>fromString (show n)
+          <>" <= "<>TBL.fromDec maxBm
         ]
   where
-    maxB = fromIntegral @m @n maxBound
-    minB = fromIntegral @m @n minBound
+    maxBn = fromIntegral @m @n maxBm
+    minBn = fromIntegral @m @n minBm
+    maxBm = maxBound @m
+    minBm = minBound @m
 
 --------------------------------------------------------------------------------
 
 -- | Decomposer. Strengthen every element in a list.
 instance Strengthen a => Strengthen [a] where
-    strengthen = traverse strengthen
+    strengthen = strengthenList
 
+strengthenList :: Strengthen a => [Weak a] -> Result [a]
+strengthenList = goR (0 :: Int) [] . map strengthen
+  where
+    goR i as = \case
+      r:rs ->
+        case r of
+          Success a -> goR (i+1) (a:as) rs
+          Failure e -> goL (i+1) [(TBL.fromDec i, e)]    rs
+      []   -> Success as
+    goL i es = \case
+      r:rs ->
+        case r of
+          Success _ -> goL (i+1) es                      rs
+          Failure e -> goL (i+1) ((TBL.fromDec i, e):es) rs
+      []   -> failStrengthen ["list had failures"] es
+
 -- | Decomposer. Strengthen both elements of a tuple.
-instance (Strengthen a, Strengthen b) => Strengthen (a, b) where
-    strengthen (a, b) = liftA2 (,) (strengthen a) (strengthen b)
+instance (Strengthen l, Strengthen r) => Strengthen (l, r) where
+    strengthen (l, r) =
+        case strengthen l of
+          Success sl ->
+            case strengthen r of
+              Success sr -> Success (sl, sr)
+              Failure er -> failStrengthen ["2-tuple: right failed"]
+                [("R", er)]
+          Failure el ->
+            case strengthen @r r of
+              Success _  -> failStrengthen ["2-tuple:  left failed"]
+                [("L", el)]
+              Failure er -> failStrengthen ["2-tuple:   l&r failed"]
+                [("R", er), ("L", el)]
 
 -- | Decomposer. Strengthen either side of an 'Either'.
 instance (Strengthen a, Strengthen b) => Strengthen (Either a b) where
@@ -282,9 +225,6 @@
                        Right b -> Right <$> strengthen b
 
 --------------------------------------------------------------------------------
-
-prettyTypeRep :: TypeRep -> Pretty.Doc a
-prettyTypeRep = pretty . show
 
 -- from flow
 (.>) :: (a -> b) -> (b -> c) -> a -> c
diff --git a/src/Strongweak/Strengthen/Generic.hs b/src/Strongweak/Strengthen/Generic.hs
new file mode 100644
--- /dev/null
+++ b/src/Strongweak/Strengthen/Generic.hs
@@ -0,0 +1,213 @@
+{- | 'strengthen' over generic representations.
+
+As with base instances, generic strengthening collates all failures rather than
+short-circuiting on the first failure. Failures are annotated with precise
+information describing where the failure occurred:
+
+  * data type name
+  * constructor name
+  * field index
+  * field name (if present)
+-}
+
+-- required due to type class design
+{-# LANGUAGE AllowAmbiguousTypes, UndecidableInstances #-}
+
+{-# LANGUAGE OverloadedStrings #-} -- required for failure
+
+module Strongweak.Strengthen.Generic where
+
+import Strongweak.Strengthen
+import GHC.Generics
+import Data.Either.Validation
+import Data.Kind ( Type )
+import GHC.TypeNats ( Natural, type (+), KnownNat )
+import Control.Applicative qualified as A -- liftA2 export workaround
+import Strongweak.Util.TypeNats ( natVal'' )
+import Data.Text.Builder.Linear qualified as TBL
+import GHC.Exts ( Symbol, fromString, proxy# )
+import GHC.TypeLits ( KnownSymbol, symbolVal' )
+
+{- TODO
+So, now that we're improving the error story, we can do so here as well.
+
+At product level in these generics, we know that neither data type names or
+constructor names (weak or strong) will change. So individual fields can simply
+annotate themselves with the weak & strong field identifiers. Then those can get
+wrapped into a nice clean error higher up, that says "this constructor had the
+following errors".
+
+It's gonna look like the tuple and list 'Strengthen' instances but worse. Lots
+of fiddly stuff.
+
+Also, we can do the data type equality check I noted earlier. If weak & strong
+data type names/constructor names match, we're probably doing @SW@ tricks, and
+could probably shorten the error a bit.
+-}
+
+-- | Strengthen a value generically.
+--
+-- The weak and strong types must be /compatible/. See 'Strongweak.Generic' for
+-- the definition of compatibility in this context.
+strengthenGeneric
+    :: (Generic w, Generic s, GStrengthenD (Rep w) (Rep s))
+    => w -> Result s
+strengthenGeneric = fmap to . gstrengthenD . from
+
+-- | Generic strengthening at the datatype level.
+class GStrengthenD w s where
+    gstrengthenD :: w p -> Result (s p)
+
+-- | Strengthen a generic data type, replacing its metadata wrapping.
+instance GStrengthenC wdn sdn w s
+  => GStrengthenD
+        (D1 (MetaData wdn _wmd2 _wmd3 _wmd4) w)
+        (D1 (MetaData sdn _smd2 _smd3 _smd4) s) where
+    gstrengthenD = fmap M1 . gstrengthenC @wdn @sdn . unM1
+
+-- | Generic strengthening at the constructor sum level.
+class GStrengthenC (wdn :: Symbol) (sdn :: Symbol) w s where
+    gstrengthenC :: w p -> Result (s p)
+
+-- | Nothing to do for empty datatypes.
+instance GStrengthenC wdn sdn V1 V1 where gstrengthenC = Success
+
+-- | Strengthen sum types by casing and strengthening left or right.
+instance
+  ( GStrengthenC wdn sdn wl sl
+  , GStrengthenC wdn sdn wr sr
+  ) => GStrengthenC wdn sdn (wl :+: wr) (sl :+: sr) where
+    gstrengthenC = \case L1 l -> L1 <$> gstrengthenC @wdn @sdn l
+                         R1 r -> R1 <$> gstrengthenC @wdn @sdn r
+
+-- | Enter a constructor, stripping its metadata wrapper.
+instance (GStrengthenS 0 w s, ReifyCstrs wcd wcn scd scn)
+  => GStrengthenC wcd scd
+        (C1 (MetaCons wcn _wmc2 _wmc3) w)
+        (C1 (MetaCons scn _smc2 _smc3) s) where
+    gstrengthenC (M1 w) =
+        case gstrengthenS @0 w of
+          Success s  -> Success (M1 s)
+          Failure es -> failStrengthen [reifyCstrs @wcd @wcn @scd @scn] es
+
+class ReifyCstrs (ld :: Symbol) (lc :: Symbol) (rd :: Symbol) (rc :: Symbol) where
+    reifyCstrs :: TBL.Builder
+
+-- | Special case: data type and constructor names are equivalent: simplify
+instance {-# OVERLAPPING #-} (KnownSymbol d, KnownSymbol c)
+  => ReifyCstrs d c d c where
+    {-# INLINE reifyCstrs #-}
+    reifyCstrs = d<>"."<>c
+      where
+        d = fromString (symbolVal' (proxy# @d))
+        c = fromString (symbolVal' (proxy# @c))
+
+instance (KnownSymbol ld, KnownSymbol lc, KnownSymbol rd, KnownSymbol rc)
+  => ReifyCstrs ld lc rd rc where
+    {-# INLINE reifyCstrs #-}
+    reifyCstrs = ld<>"."<>lc<>" -> "<>rd<>"."<>rc
+      where
+        ld = fromString (symbolVal' (proxy# @ld))
+        lc = fromString (symbolVal' (proxy# @lc))
+        rd = fromString (symbolVal' (proxy# @rd))
+        rc = fromString (symbolVal' (proxy# @rc))
+
+-- | Generic strengthening at the constructor level.
+class GStrengthenS (i :: Natural) w s where
+    gstrengthenS :: w p -> Validation [(TBL.Builder, StrengthenFailure)] (s p)
+
+-- | Nothing to do for empty constructors.
+instance GStrengthenS i U1 U1 where gstrengthenS = Success
+
+-- | Strengthen product types by strengthening left and right.
+instance
+  ( GStrengthenS i                  wl sl
+  , GStrengthenS (i + ProdArity wl) wr sr
+  ) => GStrengthenS i (wl :*: wr) (sl :*: sr) where
+    gstrengthenS (l :*: r) =
+        A.liftA2 (:*:)
+               (gstrengthenS @i                  l)
+               (gstrengthenS @(i + ProdArity wl) r)
+
+-- | Special case: if source and target types are equivalent, just replace meta.
+--
+-- Note that we have to expand the metadata awkwardly for the overlapping
+-- instances to work correctly. (There should be a better way to write this, but
+-- it's purely style, so light TODO.)
+instance {-# OVERLAPPING #-} GStrengthenS i
+  (S1 (MetaSel _wms1 _wms2 _wms3 _wms4) (Rec0 a))
+  (S1 (MetaSel _sms1 _sms2 _sms3 _sms4) (Rec0 a)) where
+    gstrengthenS = Success . M1 . unM1
+
+-- | Strengthen a field using the existing 'Strengthen' instance.
+instance
+  ( Weak s ~ w -- has to be here, else "illegal typesym family app in instance"
+  , Strengthen s
+  , ReifySelector i wmr smr
+  ) => GStrengthenS i
+        (S1 (MetaSel wmr _wms2 _wms3 _wms4) (Rec0 w))
+        (S1 (MetaSel smr _sms2 _sms3 _sms4) (Rec0 s)) where
+    gstrengthenS = unM1 .> unK1 .> strengthen .> \case
+      Success s -> Success $ M1 $ K1 s
+      Failure e -> Failure [(reifySelector @i @wmr @smr, e)]
+
+{- TODO
+* how to separate index and record name? @.@ is good and bad, uses same syntax
+  as @dt.cstr@ for different reason BUT is pretty clear
+* how to lay out precisely? fairly arbitrary
+-}
+class ReifySelector (i :: Natural) (l :: Maybe Symbol) (r :: Maybe Symbol) where
+    reifySelector :: TBL.Builder
+
+-- | Special case: both types had a record name, and they're equal
+instance {-# OVERLAPPING #-} (KnownNat i, KnownSymbol lnm)
+  => ReifySelector i (Just lnm) (Just lnm) where
+    -- TODO check overlap works correct
+    {-# INLINE reifySelector #-}
+    reifySelector = i<>"."<>lnm
+      where
+        i   = fromString $ show $ natVal'' @i
+        lnm = fromString $ symbolVal' (proxy# @lnm)
+
+instance (KnownNat i, KnownSymbol lnm, KnownSymbol rnm)
+  => ReifySelector i (Just lnm) (Just rnm) where
+    {-# INLINE reifySelector #-}
+    reifySelector = i<>"."<>lnm<>" -> "<>rnm
+      where
+        i   = fromString $ show $ natVal'' @i
+        lnm = fromString $ symbolVal' (proxy# @lnm)
+        rnm = fromString $ symbolVal' (proxy# @rnm)
+
+instance KnownNat i => ReifySelector i Nothing Nothing where
+    {-# INLINE reifySelector #-}
+    reifySelector = fromString $ show $ natVal'' @i
+
+instance (KnownNat i, KnownSymbol lnm)
+  => ReifySelector i (Just lnm) Nothing where
+    {-# INLINE reifySelector #-}
+    reifySelector = i<>"."<>lnm
+      where
+        i   = fromString $ show $ natVal'' @i
+        lnm = fromString $ symbolVal' (proxy# @lnm)
+
+instance (KnownNat i, KnownSymbol rnm)
+  => ReifySelector i Nothing (Just rnm) where
+    {-# INLINE reifySelector #-}
+    reifySelector = i<>" -> "<>rnm
+      where
+        i   = fromString $ show $ natVal'' @i
+        rnm = fromString $ symbolVal' (proxy# @rnm)
+
+--------------------------------------------------------------------------------
+
+-- from flow
+(.>) :: (a -> b) -> (b -> c) -> a -> c
+f .> g = g . f
+
+--------------------------------------------------------------------------------
+
+-- could define this with @Generic.Type.Function.FoldMap.GTFoldMapC (+) 0 _@...
+-- but pretty dumb LOL
+type family ProdArity (f :: k -> Type) :: Natural where
+    ProdArity (S1 c f)  = 1
+    ProdArity (l :*: r) = ProdArity l + ProdArity r
diff --git a/src/Strongweak/Strengthen/Unsafe.hs b/src/Strongweak/Strengthen/Unsafe.hs
--- a/src/Strongweak/Strengthen/Unsafe.hs
+++ b/src/Strongweak/Strengthen/Unsafe.hs
@@ -3,8 +3,7 @@
 import Strongweak.Weaken
 import Data.Word
 import Data.Int
-import Refined ( Refined )
-import Refined.Unsafe ( reallyUnsafeRefine )
+import Rerefined.Refine
 import Data.Vector.Generic.Sized qualified as VGS -- Shazbot!
 import Data.Vector.Generic qualified as VG
 import Data.Vector.Generic.Sized.Internal qualified
@@ -37,7 +36,7 @@
 
 -- | Add a refinement to a type without checking the associated predicate.
 instance UnsafeStrengthen (Refined p a) where
-    unsafeStrengthen = reallyUnsafeRefine
+    unsafeStrengthen = unsafeRefine
 
 -- | Assume a plain list is non-empty.
 instance UnsafeStrengthen (NonEmpty a) where
diff --git a/src/Strongweak/Util/TypeNats.hs b/src/Strongweak/Util/TypeNats.hs
new file mode 100644
--- /dev/null
+++ b/src/Strongweak/Util/TypeNats.hs
@@ -0,0 +1,10 @@
+{-# LANGUAGE AllowAmbiguousTypes #-}
+
+module Strongweak.Util.TypeNats where
+
+import GHC.TypeNats
+import GHC.Exts ( proxy# )
+
+natVal'' :: forall n. KnownNat n => Natural
+natVal'' = natVal' (proxy# @n)
+{-# INLINE natVal'' #-}
diff --git a/src/Strongweak/Weaken.hs b/src/Strongweak/Weaken.hs
--- a/src/Strongweak/Weaken.hs
+++ b/src/Strongweak/Weaken.hs
@@ -12,7 +12,7 @@
   , type SWDepth
   ) where
 
-import Refined ( Refined, unrefine, Refined1, unrefine1 )
+import Rerefined
 import Data.Word
 import Data.Int
 import Data.Vector.Generic.Sized qualified as VGS -- Shazbot!
@@ -35,15 +35,15 @@
     -- | 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 by weakening
---   first.
-liftWeakF :: Weaken a => (Weak a -> b) -> (a -> b)
-liftWeakF f = f . weaken
-
 -- | Strength enumeration: is it strong, or weak?
 --
 -- Primarily interesting at the type level (using DataKinds).
 data Strength = Strong | Weak
+
+-- | 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
 
 {- | Get either the strong or weak representation of a type, depending on the
      type-level "switch" provided.
diff --git a/src/Strongweak/Weaken/Generic.hs b/src/Strongweak/Weaken/Generic.hs
new file mode 100644
--- /dev/null
+++ b/src/Strongweak/Weaken/Generic.hs
@@ -0,0 +1,45 @@
+-- | 'weaken' over generic representations.
+
+module Strongweak.Weaken.Generic where
+
+import Strongweak.Weaken
+import GHC.Generics
+
+-- | Weaken a value generically.
+--
+-- The weak and strong types must be /compatible/. See 'Strongweak.Generic' for
+-- the definition of compatibility in this context.
+weakenGeneric :: (Generic s, Generic w, GWeaken (Rep s) (Rep w)) => s -> w
+weakenGeneric = to . gweaken . from
+
+class GWeaken s w where
+    gweaken :: s p -> w p
+
+-- | Strip all meta.
+instance GWeaken s w => GWeaken (M1 is ms s) (M1 iw mw w) where
+    gweaken = M1 . gweaken . unM1
+
+-- | Nothing to do for empty datatypes.
+instance GWeaken V1 V1 where
+    gweaken = id
+
+-- | Nothing to do for empty constructors.
+instance GWeaken U1 U1 where
+    gweaken = id
+
+-- | Special case: if source and target types are equal, copy the value through.
+instance {-# OVERLAPPING #-} GWeaken (Rec0 s) (Rec0 s) where
+    gweaken = id
+
+-- | Weaken a field using the existing 'Weaken' instance.
+instance (Weaken s, Weak s ~ w) => GWeaken (Rec0 s) (Rec0 w) where
+    gweaken = K1 . weaken . unK1
+
+-- | Weaken product types by weakening left and right.
+instance (GWeaken ls lw, GWeaken rs rw) => GWeaken (ls :*: rs) (lw :*: rw) where
+    gweaken (l :*: r) = gweaken l :*: gweaken r
+
+-- | Weaken sum types by casing and weakening left or right.
+instance (GWeaken ls lw, GWeaken rs rw) => GWeaken (ls :+: rs) (lw :+: rw) where
+    gweaken = \case L1 l -> L1 $ gweaken l
+                    R1 r -> R1 $ gweaken r
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.6.1
+version:        0.7.0
 synopsis:       Convert between strong and weak representations of types
 description:    Please see README.md.
 category:       Data
@@ -17,7 +17,8 @@
 license-file:   LICENSE
 build-type:     Simple
 tested-with:
-    GHC ==9.2.2
+    GHC==9.8
+  , GHC==9.6
 extra-source-files:
     README.md
     CHANGELOG.md
@@ -30,14 +31,14 @@
   exposed-modules:
       Strongweak
       Strongweak.Generic
-      Strongweak.Generic.Strengthen
-      Strongweak.Generic.Via
-      Strongweak.Generic.Weaken
       Strongweak.Strengthen
+      Strongweak.Strengthen.Generic
       Strongweak.Strengthen.Unsafe
       Strongweak.Util.Text
       Strongweak.Util.Typeable
+      Strongweak.Util.TypeNats
       Strongweak.Weaken
+      Strongweak.Weaken.Generic
   other-modules:
       Paths_strongweak
   hs-source-dirs:
@@ -53,14 +54,13 @@
       TypeFamilies
       DataKinds
       MagicHash
-  ghc-options: -Wall
+  ghc-options: -Wall -Wno-unticked-promoted-constructors
   build-depends:
-      acc >=0.2.0.1 && <0.3
-    , base >=4.14 && <5
+      base >=4.17 && <5
     , either >=5.0.1.1 && <5.1
-    , prettyprinter >=1.7.1 && <1.8
-    , refined1 ==0.9.*
-    , text >=1.2.5.0 && <2.1
+    , rerefined >=0.4.0 && <0.5
+    , text >=1.2.5.0 && <2.2
+    , text-builder-linear >=0.1.2 && <0.2
     , vector >=0.12.3.1 && <0.14
     , vector-sized >=1.5.0 && <1.6
   default-language: GHC2021
@@ -71,7 +71,6 @@
   other-modules:
       Common
       Strongweak.LawsSpec
-      Strongweak.StrengthenSpec
       Paths_strongweak
   hs-source-dirs:
       test
@@ -86,21 +85,20 @@
       TypeFamilies
       DataKinds
       MagicHash
-  ghc-options: -Wall
+  ghc-options: -Wall -Wno-unticked-promoted-constructors
   build-tool-depends:
       hspec-discover:hspec-discover >=2.7 && <2.12
   build-depends:
-      QuickCheck >=2.14.2 && <2.15
-    , acc >=0.2.0.1 && <0.3
-    , base >=4.14 && <5
+      QuickCheck >=2.14.2 && <2.16
+    , base >=4.17 && <5
     , either >=5.0.1.1 && <5.1
     , generic-random >=1.5.0.1 && <1.6
     , hspec >=2.7 && <2.12
-    , prettyprinter >=1.7.1 && <1.8
     , quickcheck-instances >=0.3.26 && <0.4
-    , refined1 ==0.9.*
+    , rerefined >=0.4.0 && <0.5
     , strongweak
-    , text >=1.2.5.0 && <2.1
+    , text >=1.2.5.0 && <2.2
+    , text-builder-linear >=0.1.2 && <0.2
     , 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
@@ -3,9 +3,10 @@
 import Strongweak
 import Strongweak.Strengthen qualified as Strengthen
 import Strongweak.Generic
-import Refined hiding ( Weaken, weaken, strengthen, NonEmpty )
+import Rerefined
+import Rerefined.Predicates
 import GHC.Generics ( Generic )
-import Generic.Random
+import Generic.Random ( GenericArbitraryU(..), AndShrinking(..) )
 import Test.QuickCheck ( Arbitrary )
 import Numeric.Natural ( Natural )
 import Data.Word
@@ -14,7 +15,7 @@
 
 data DS (s :: Strength)
   = DS0 (SW s Word8) (SW s Word8) Word8 (SW s Word8) (SW s Word8)
-  | DS1 (SW s (Refined (LessThan 100) Natural))
+  | DS1 (SW s (Refined (CompareValue LT Pos 100) Natural))
     deriving stock (Generic)
 
 deriving stock instance Eq   (DS 'Strong)
@@ -32,7 +33,7 @@
 
 data DP (s :: Strength) = DP
   { dp1f0 :: SW s Word32
-  , dp1f1 :: SW s (Refined (GreaterThan 42) Natural)
+  , dp1f1 :: SW s (Refined (CompareValue GT Pos 42) Natural)
   , dp1f2 :: SW s Word8
   , dp1f3 :: Word8
   , dp1f4 :: SW s Word8
diff --git a/test/Strongweak/StrengthenSpec.hs b/test/Strongweak/StrengthenSpec.hs
deleted file mode 100644
--- a/test/Strongweak/StrengthenSpec.hs
+++ /dev/null
@@ -1,70 +0,0 @@
-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.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 = 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 = sfGenericSW1Show
-                    "DS" "DS0" 4 Nothing
-                    (typeRep' @Natural) (typeRep' @Word8) w
-        strengthen @(DS 'Strong) d `shouldSatisfy` svEqFail e
-
--- build strengthen failure
--- one failure, generic with SW, one wrapped failure (detailed)
-sfGenericSW1Show
-    :: Show w
-    => 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)"
-
--- 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
-  FailShow   wt  st  wv  _ -> case s2 of
-    FailShow wt' st' wv' _ ->
-         wt  == wt' && st == st'
-      && wv  == wv'
-    _ -> False
-  _ -> error "unexpected strengthen fail"
-
-svEqFail :: Fail -> Result s -> Bool
-svEqFail e = \case
-  Success{}  -> False
-  Failure es ->
-    case Foldable.toList es of
-      [e'] -> sfEq e e'
-      _    -> False