diff --git a/CHANGELOG.md b/CHANGELOG.md
--- a/CHANGELOG.md
+++ b/CHANGELOG.md
@@ -1,3 +1,12 @@
+## 1.0.0 (2024-10-03)
+* fix `NullTerminate` check being inverted (OOPS LOL)
+* fix `Get [a]` instance (list backwards xd)
+* add type-level constructor parsing for generics (!!)
+* rewrite `AsciiNat`
+* switch from refined to rerefined (my refined rewrite)
+* add missing `BLen (GenericallyNonSum a)` instance
+* other various cleanup
+
 ## 0.8.0 (2024-04-13)
 * add missing `And` predicate combinators instances (`PutC`, `GetC`)
 * add `Type.Derived.NullTermPadded` (type synonym over `And`)
diff --git a/LICENSE b/LICENSE
--- a/LICENSE
+++ b/LICENSE
@@ -1,4 +1,4 @@
-Copyright (c) 2022 Ben Orchard (@raehik) <thefirstmuffinman@gmail.com>
+Copyright (c) 2022-2024 Ben Orchard (@raehik) <thefirstmuffinman@gmail.com>
 
 Permission is hereby granted, free of charge, to any person obtaining
 a copy of this software and associated documentation files (the
diff --git a/README.md b/README.md
--- a/README.md
+++ b/README.md
@@ -7,14 +7,13 @@
 
 # binrep
 binrep is a Haskell library for *precisely modelling binary schemas*, especially
-byte-oriented file formats, and working with them effectively and efficiently.
-Here's why it's useful:
+low-context byte-oriented file formats e.g. C enums, and working with them
+effectively and efficiently. Here's why it's useful:
 
   * **Explicit:** Define Haskell data types with the binary schema "baked in".
     Use highly parameterized binary representation primitives including
     null-terminated data (e.g. C-style strings), Pascal-style data (length
-    prefixed), sized explicit-endian machine integers, null-padded data. Write
-    your own primitives if you want (if so, please consider making a PR!).
+    prefixed), sized explicit-endian machine integers, null-padded data.
   * **Low boilerplate:** Free performant parsers and serializers via generics.
     _(See [Generic binary representation](#generic-binary-representation).)_
   * **Easy validation:** Use the [strongweak][gh-strongweak] library design
@@ -70,12 +69,23 @@
 _(Generics are now handled by [generic-data-functions][hackage-gdf]. This info
 is largely the same, but the code is elsewhere.)_
 
-binrep's generic deriving makes very few decisions:
+binrep includes powerful generics for automatically writing instances.
+They all work the same way:
 
   * Constructors are encoded by sequentially encoding every enclosed field.
     * Empty constructors thus serialize to 0 bytes.
-  * Sum types are encoded via a tag obtained from the constructor names.
-    * It's the same approach as aeson, with a bit more flexibility: see below.
+  * For sum types, the constructor is disambiguated via a tag obtained from the
+    constructor name.
+    * Tags may be parsed on the type or term level.
+
+Note that when parsing sum types, we compare tags sequentially. You may design
+your tag schema to have a more efficient approach. In such cases, consider using
+`Generic.Data.FOnCstr` from [generic-data-functions][hackage-gdf].
+
+As an example, you could encode constructor names as a null-terminated ASCII
+bytestring for a tag. (This is provided at `Binrep.Generic.nullTermCstrPfxTag`.)
+Alternatively, you may encode each constructor at a unique byte value, stated at
+the end of the constructor name.
 
 Sum types (data types with multiple constructors) are handled by first encoding
 a "tag field", the value of which then indicates which constructor to use. You
diff --git a/binrep.cabal b/binrep.cabal
--- a/binrep.cabal
+++ b/binrep.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:           binrep
-version:        0.8.0
+version:        1.0.0
 synopsis:       Encode precise binary representations directly in types
 description:    Please see README.md.
 category:       Data, Serialization, Generics
@@ -17,7 +17,7 @@
 license-file:   LICENSE
 build-type:     Simple
 tested-with:
-    GHC ==9.4.4
+    GHC==9.8
 extra-source-files:
     README.md
     CHANGELOG.md
@@ -39,18 +39,21 @@
       Binrep.Common.Class.TypeErrors
       Binrep.Common.Via.Generically.NonSum
       Binrep.Common.Via.Prim
+      Binrep.Example.Sum
+      Binrep.Example.Tga
       Binrep.Generic
       Binrep.Get
       Binrep.Get.Error
       Binrep.Get.Struct
       Binrep.Put
       Binrep.Put.Struct
-      Binrep.Test
+      Binrep.Type.AsciiNat
       Binrep.Type.Derived.NullTermPadded
       Binrep.Type.Magic
       Binrep.Type.NullPadded
       Binrep.Type.NullTerminated
       Binrep.Type.Prefix.Count
+      Binrep.Type.Prefix.Internal
       Binrep.Type.Prefix.Size
       Binrep.Type.Sized
       Binrep.Type.Text
@@ -61,10 +64,9 @@
       Binrep.Type.Text.Encoding.Utf8
       Binrep.Type.Text.Internal
       Binrep.Type.Thin
-      Binrep.Util
       Binrep.Util.ByteOrder
       Binrep.Util.Generic
-      Binrep.Util.Prefix
+      Raehik.Compat.FlatParse.Basic.CutWithPos
       Raehik.Compat.FlatParse.Basic.Prim
       Raehik.Compat.FlatParse.Basic.WithLength
       Util.TypeNats
@@ -83,22 +85,25 @@
       TypeFamilies
       DataKinds
       MagicHash
-  ghc-options: -Wall
+  ghc-options: -Wall -Wno-unticked-promoted-constructors
   build-depends:
-      base >=4.14 && <5
+      base >=4.18 && <5
     , bytestring >=0.11 && <0.13
-    , bytezap >=1.2.0 && <1.3
+    , bytezap >=1.6.0 && <1.7
     , deepseq >=1.4.6.1 && <1.6
     , defun-core ==0.1.*
     , flatparse >=0.5.0.2 && <0.6
-    , generic-data-functions >=0.5.0 && <0.6
+    , generic-data-functions >=0.6.0 && <0.7
     , generic-type-asserts >=0.3.0 && <0.4
     , generic-type-functions >=0.1.0 && <0.2
+    , ghc-bignum ==1.3.*
     , parser-combinators >=1.3.0 && <1.4
-    , refined1 ==0.9.*
-    , strongweak >=0.6.0 && <0.7
-    , text >=1.2.5.0 && <2.1
-    , type-level-bytestrings >=0.1.0 && <0.2
+    , rerefined >=0.6.0 && <0.7
+    , strongweak >=0.9.1 && <0.10
+    , text >=2.0 && <2.2
+    , text-builder-linear >=0.1.3 && <0.2
+    , type-level-bytestrings >=0.1.0 && <0.3
+    , type-level-show >=0.3.0 && <0.4
   default-language: GHC2021
   if flag(icu)
     cpp-options: -DHAVE_ICU
@@ -110,7 +115,8 @@
   main-is: Spec.hs
   other-modules:
       ArbitraryOrphans
-      Binrep.LawsSpec
+      Binrep.GenericSpec
+      Binrep.TypesSpec
       Paths_binrep
   hs-source-dirs:
       test
@@ -125,29 +131,32 @@
       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
-    , base >=4.14 && <5
+    , base >=4.18 && <5
     , binrep
     , bytestring >=0.11 && <0.13
-    , bytezap >=1.2.0 && <1.3
+    , bytezap >=1.6.0 && <1.7
     , deepseq >=1.4.6.1 && <1.6
     , defun-core ==0.1.*
     , flatparse >=0.5.0.2 && <0.6
-    , generic-data-functions >=0.5.0 && <0.6
+    , generic-data-functions >=0.6.0 && <0.7
     , generic-random >=1.5.0.1 && <1.6
     , generic-type-asserts >=0.3.0 && <0.4
     , generic-type-functions >=0.1.0 && <0.2
+    , ghc-bignum ==1.3.*
     , hspec >=2.7 && <2.12
     , parser-combinators >=1.3.0 && <1.4
     , quickcheck-instances >=0.3.26 && <0.4
-    , refined1 ==0.9.*
-    , strongweak >=0.6.0 && <0.7
-    , text >=1.2.5.0 && <2.1
-    , type-level-bytestrings >=0.1.0 && <0.2
+    , rerefined >=0.6.0 && <0.7
+    , strongweak >=0.9.1 && <0.10
+    , text >=2.0 && <2.2
+    , text-builder-linear >=0.1.3 && <0.2
+    , type-level-bytestrings >=0.1.0 && <0.3
+    , type-level-show >=0.3.0 && <0.4
   default-language: GHC2021
   if flag(icu)
     cpp-options: -DHAVE_ICU
@@ -172,24 +181,27 @@
       TypeFamilies
       DataKinds
       MagicHash
-  ghc-options: -Wall
+  ghc-options: -Wall -Wno-unticked-promoted-constructors
   build-depends:
-      base >=4.14 && <5
+      base >=4.18 && <5
     , binrep
     , bytestring >=0.11 && <0.13
-    , bytezap >=1.2.0 && <1.3
+    , bytezap >=1.6.0 && <1.7
     , deepseq >=1.4.6.1 && <1.6
     , defun-core ==0.1.*
     , flatparse >=0.5.0.2 && <0.6
     , gauge
-    , generic-data-functions >=0.5.0 && <0.6
+    , generic-data-functions >=0.6.0 && <0.7
     , generic-type-asserts >=0.3.0 && <0.4
     , generic-type-functions >=0.1.0 && <0.2
+    , ghc-bignum ==1.3.*
     , parser-combinators >=1.3.0 && <1.4
-    , refined1 ==0.9.*
-    , strongweak >=0.6.0 && <0.7
-    , text >=1.2.5.0 && <2.1
-    , type-level-bytestrings >=0.1.0 && <0.2
+    , rerefined >=0.6.0 && <0.7
+    , strongweak >=0.9.1 && <0.10
+    , text >=2.0 && <2.2
+    , text-builder-linear >=0.1.3 && <0.2
+    , type-level-bytestrings >=0.1.0 && <0.3
+    , type-level-show >=0.3.0 && <0.4
   default-language: GHC2021
   if flag(icu)
     cpp-options: -DHAVE_ICU
diff --git a/src/Binrep/BLen.hs b/src/Binrep/BLen.hs
--- a/src/Binrep/BLen.hs
+++ b/src/Binrep/BLen.hs
@@ -1,4 +1,5 @@
 {-# LANGUAGE UndecidableInstances #-} -- for 'ViaCBLen', 'TypeError'
+{-# LANGUAGE AllowAmbiguousTypes #-} -- for type-level sum type handling
 
 {- | Byte length as a simple pure function, no bells or whistles.
 
@@ -18,7 +19,7 @@
 
 module Binrep.BLen
   ( BLen(blen)
-  , blenGenericNonSum, blenGenericSum
+  , blenGenericNonSum, blenGenericSum, blenGenericSumRaw
   , ViaCBLen(..), cblen
   ) where
 
@@ -37,10 +38,12 @@
 import Data.Monoid qualified as Monoid
 import GHC.Generics
 import Generic.Data.Function.FoldMap
+import Generic.Data.MetaParse.Cstr ( Raw, ParseCstrTo )
 import Generic.Type.Assert
+import Binrep.Common.Via.Generically.NonSum
 
-import Refined
-import Refined.Unsafe
+import Rerefined.Refine
+import Rerefined.Predicate.Logical.And
 
 -- | Class for types with easily-calculated length in bytes.
 --
@@ -65,26 +68,41 @@
     ) => a -> Int
 blenGenericNonSum = Monoid.getSum . genericFoldMapNonSum @BLen
 
+instance
+  ( Generic a, GFoldMapNonSum BLen (Rep a)
+  , GAssertNotVoid a, GAssertNotSum a
+  ) => BLen (GenericallyNonSum a) where
+    blen = blenGenericNonSum . unGenericallyNonSum
+
 -- | Measure the byte length of a term of the sum type @a@ via its 'Generic'
 --   instance.
---
--- You must provide a function to obtain the byte length for the prefix tag, via
--- inspecting the reified constructor names. This is regrettably inefficient.
--- Alas. Do write your own instance if you want better performance!
 blenGenericSum
+    :: forall sumtag a
+    .  ( Generic a, GFoldMapSum BLen sumtag (Rep a)
+       , GAssertNotVoid a, GAssertSum a
+    ) => ParseCstrTo sumtag Int -> a -> Int
+blenGenericSum f =
+    Monoid.getSum . genericFoldMapSum @BLen @sumtag (\p -> Monoid.Sum (f p))
+
+-- TODO perhaps provide some handy wrappers that fill in blen for sumtag type
+-- with cblen? how to do this well?
+
+-- | Measure the byte length of a term of the sum type @a@ via its 'Generic'
+--   instance.
+blenGenericSumRaw
     :: forall a
-    .  ( Generic a, GFoldMapSum BLen (Rep a)
+    .  ( Generic a, GFoldMapSum BLen Raw (Rep a)
        , GAssertNotVoid a, GAssertSum a
     ) => (String -> Int) -> a -> Int
-blenGenericSum f =
-    Monoid.getSum . genericFoldMapSum @BLen (Monoid.Sum <$> f)
+blenGenericSumRaw f =
+    Monoid.getSum . genericFoldMapSumRaw @BLen (Monoid.Sum <$> f)
 
 -- We can't provide a Generically instance because the user must choose between
 -- sum and non-sum handlers.
 
 instance BLen (Refined pr (Refined pl a))
   => BLen (Refined (pl `And` pr) a) where
-    blen = blen . reallyUnsafeRefine @_ @pr . reallyUnsafeRefine @_ @pl . unrefine
+    blen = blen . unsafeRefine @_ @pr . unsafeRefine @_ @pl . unrefine
 
 instance TypeError ENoEmpty => BLen Void where blen = undefined
 instance TypeError ENoSum => BLen (Either a b) where blen = undefined
diff --git a/src/Binrep/CBLen.hs b/src/Binrep/CBLen.hs
--- a/src/Binrep/CBLen.hs
+++ b/src/Binrep/CBLen.hs
@@ -13,7 +13,8 @@
 
 import DeFun.Core ( type (~>), type App )
 
-import Refined
+import Rerefined.Refine
+import Rerefined.Predicate.Logical.And
 
 import Binrep.Common.Class.TypeErrors ( ENoEmpty )
 
diff --git a/src/Binrep/Example/Sum.hs b/src/Binrep/Example/Sum.hs
new file mode 100644
--- /dev/null
+++ b/src/Binrep/Example/Sum.hs
@@ -0,0 +1,16 @@
+module Binrep.Example.Sum where
+
+import Binrep
+import Data.Word
+import GHC.Generics ( type Generic )
+import Generic.Data.FOnCstr
+
+data SumType = SumType1 Word8 | SumType2 Word8 Word8
+    deriving stock (Generic, Show)
+
+instance Get SumType where
+    get = do
+        get @Word8 >>= \case
+          1 -> genericFOnCstr @Get @"SumType1"
+          2 -> genericFOnCstr @Get @"SumType2"
+          _ -> error "TODO"
diff --git a/src/Binrep/Example/Tga.hs b/src/Binrep/Example/Tga.hs
new file mode 100644
--- /dev/null
+++ b/src/Binrep/Example/Tga.hs
@@ -0,0 +1,28 @@
+module Binrep.Example.Tga where
+
+{-
+import Binrep
+import Binrep.Type.Derived.NullTermPadded
+import Binrep.Type.AsciiNat
+import Rerefined
+-}
+import Strongweak
+import Data.Word
+
+data Header (s :: Strength) a = Header
+  { idLen :: SW s Word8
+  , colorMapType :: ColorMapType
+  , imageType :: ImageType
+  --, colorMapSpec :: 
+  --, imageSpec
+  }
+
+data ColorMapType = NoColorMap {- ^ 0 -} | HasColorMap {- ^ 1 -}
+data ImageType
+  = NoImageData
+  | UncompColorMapped
+  | UncompTrueColor
+  | UncompBW
+  | RLEColorMapped
+  | RLETrueColor
+  | RLEBW
diff --git a/src/Binrep/Generic.hs b/src/Binrep/Generic.hs
--- a/src/Binrep/Generic.hs
+++ b/src/Binrep/Generic.hs
@@ -4,12 +4,12 @@
 import Data.ByteString qualified as B
 import Data.Text qualified as Text
 import Data.Text.Encoding qualified as Text
-import Refined.Unsafe
+import Rerefined.Refine ( unsafeRefine )
 
 -- | Turn a constructor name into a prefix tag by adding a null terminator.
 --
 -- Not common in binary data representations, but safe and useful for debugging.
 nullTermCstrPfxTag :: String -> NullTerminated B.ByteString
-nullTermCstrPfxTag = reallyUnsafeRefine . Text.encodeUtf8 . Text.pack
+nullTermCstrPfxTag = unsafeRefine . Text.encodeUtf8 . Text.pack
 -- ^ reallyUnsafeRefine : safe assuming Haskell constructor names are UTF-8 with
 -- no null bytes allowed
diff --git a/src/Binrep/Get.hs b/src/Binrep/Get.hs
--- a/src/Binrep/Get.hs
+++ b/src/Binrep/Get.hs
@@ -1,5 +1,6 @@
-{-# LANGUAGE UndecidableInstances #-} -- required below GHC 9.6
-{-# LANGUAGE BlockArguments #-}
+{-# LANGUAGE UndecidableInstances #-} -- for various stuff
+{-# LANGUAGE AllowAmbiguousTypes #-} -- for type-level sum type handling
+{-# LANGUAGE OverloadedStrings #-} -- for easy error building
 
 module Binrep.Get
   ( module Binrep.Get
@@ -7,18 +8,20 @@
   ) where
 
 import Binrep.Get.Error
+import Data.Text.Builder.Linear qualified as TBL
 import Binrep.Util.ByteOrder
 import Binrep.Common.Via.Prim ( ViaPrim(..) )
-import Raehik.Compat.Data.Primitive.Types ( Prim', sizeOf )
+import Raehik.Compat.Data.Primitive.Types ( Prim' )
 import Raehik.Compat.Data.Primitive.Types.Endian ( ByteSwap )
 
-import Binrep.Get.Struct ( GetC(getC) )
+import Binrep.Get.Struct ( GetC(getC), GetterC )
 import Bytezap.Parser.Struct qualified as BZ
 import Binrep.CBLen ( IsCBLen(CBLen), cblen )
 import GHC.TypeLits ( KnownNat )
 
 import FlatParse.Basic qualified as FP
 import Raehik.Compat.FlatParse.Basic.Prim qualified as FP
+import Raehik.Compat.FlatParse.Basic.CutWithPos qualified as FP
 
 import Data.ByteString qualified as B
 
@@ -27,12 +30,13 @@
 
 import GHC.Generics
 import Generic.Data.Function.Traverse
+import Generic.Data.MetaParse.Cstr ( Raw, ParseCstrTo )
 import Generic.Type.Assert
 
 import GHC.Exts ( minusAddr#, Int(I#), Int#, plusAddr#, (+#) )
 
-import Refined
-import Refined.Unsafe
+import Rerefined.Refine
+import Rerefined.Predicate.Logical.And
 
 import Data.Word
 import Data.Int
@@ -40,33 +44,42 @@
 import Data.Functor.Identity
 import Binrep.Common.Via.Generically.NonSum
 
-type Getter a = FP.Parser E a
+import Generic.Data.FOnCstr
+import Generic.Data.Function.Traverse.Constructor hiding ( ENoEmpty )
+import GHC.Exts ( Proxy# )
 
+type Getter = FP.Parser (ParseError FP.Pos TBL.Builder)
+
 class Get a where
     -- | Parse from binary.
     get :: Getter a
 
-runGet :: Get a => B.ByteString -> Either E (a, B.ByteString)
+runGet
+    :: Get a
+    => B.ByteString
+    -> Either (ParseError Int TBL.Builder) (a, B.ByteString)
 runGet = runGetter get
 
-runGetter :: Getter a -> B.ByteString -> Either E (a, B.ByteString)
-runGetter g bs = case FP.runParser g bs of
-                   FP.OK a bs' -> Right (a, bs')
-                   FP.Fail     -> Left EFail
-                   FP.Err e    -> Left e
+runGetter
+    :: Getter a
+    -> B.ByteString
+    -> Either (ParseError Int TBL.Builder) (a, B.ByteString)
+runGetter p bs =
+    case FP.runParser p bs of
+      FP.OK   a bs' -> Right (a, bs')
+      FP.Err  e     ->
+        -- TODO check this is right. might need length of bs' ... ?
+        Left $ fmap (mapParseErrorSinglePos (\(FP.Pos pos) -> len - pos)) e
+      FP.Fail       -> Left []
+  where len = B.length bs
 
 instance GenericTraverse Get where
-    type GenericTraverseF Get = FP.Parser E
+    type GenericTraverseF Get = Getter
     type GenericTraverseC Get a = Get a
-    genericTraverseAction cd cc mcs si =
-        getWrapGeneric cd $ EGenericField cc mcs si
-
-instance GenericTraverseSum Get where
-    genericTraverseSumPfxTagAction cd =
-        getWrapGeneric cd $ EGenericSum . EGenericSumTag
-    -- TODO proper offset info
-    genericTraverseSumNoMatchingCstrAction cd cstrs ptText =
-        FP.err $ E 0 $ EGeneric cd $ EGenericSum $ EGenericSumTagNoMatch cstrs ptText
+    genericTraverseAction dtName cstrName mFieldName fieldIdx =
+        get `cutting1` e
+      where
+        e = parseErrorTextGenericFieldBld dtName cstrName mFieldName fieldIdx
 
 getGenericNonSum
     :: forall a
@@ -82,72 +95,111 @@
     get = GenericallyNonSum <$> getGenericNonSum
 
 getGenericSum
+    :: forall sumtag pt a
+    .  ( Generic a, GTraverseSum Get sumtag (Rep a)
+       , Get pt
+       , GAssertNotVoid a, GAssertSum a
+    ) => ParseCstrTo sumtag pt
+      -> (pt -> pt -> Bool)
+      -> Getter a
+getGenericSum parseCstr ptEq =
+    genericTraverseSum @Get @sumtag parseCstr ptGet fNoMatch ptEq
+  where
+      fNoMatch dtName = err1 (parseErrorTextGenericNoCstrMatchBld dtName)
+      ptGet dtName = get `cutting1` parseErrorTextGenericSumTagBld dtName
+
+getGenericSumRaw
     :: forall pt a
-    .  ( Generic a, GTraverseSum Get (Rep a)
+    .  ( Generic a, GTraverseSum Get Raw (Rep a)
        , Get pt
        , GAssertNotVoid a, GAssertSum a
-    ) => PfxTagCfg pt -> Getter a
-getGenericSum = genericTraverseSum @Get
+    ) => (String -> pt)
+      -> (pt -> pt -> Bool)
+      -> Getter a
+getGenericSumRaw parseCstr ptEq =
+    genericTraverseSumRaw @Get parseCstr ptGet fNoMatch ptEq
+  where
+      fNoMatch dtName = err1 (parseErrorTextGenericNoCstrMatchBld dtName)
+      ptGet dtName = get `cutting1` parseErrorTextGenericSumTagBld dtName
 
--- We can't provide a Generically instance because the user must choose between
--- sum and non-sum handlers.
+-- | Emit a single error. Use with flatparse primitives that only 'FP.Fail'.
+err1 :: [text] -> FP.ParserT st (ParseError FP.Pos text) a
+err1 = FP.err' . parseError1
 
-eBase :: EBase -> Getter a
-eBase eb = FP.ParserT \_fp eob s st ->
-    let os = I# (minusAddr# eob s)
-     in FP.Err# st (E os $ EBase eb)
+-- | Turn a 'FP.Fail' into a single error. (Re-emits existing 'FP.Error's.)
+--
+-- Use when wrapping flatparse primitives that directly only 'FP.Fail'. (It's
+-- fine to use with combinators if the combinator itself doesn't 'FP.Error'.)
+cut1
+    :: FP.ParserT st (ParseError FP.Pos text) a -> [text]
+    -> FP.ParserT st (ParseError FP.Pos text) a
+cut1 p texts = p `FP.cut'` parseError1 texts
 
-getEBase :: Getter a -> EBase -> Getter a
-getEBase (FP.ParserT f) eb =
-    FP.ParserT \fp eob s st ->
-        let os = I# (minusAddr# eob s)
-         in case f fp eob s st of
-              FP.Fail# st'   -> FP.Err# st' (E os $ EBase eb)
-              FP.Err#  st' e -> FP.Err# st' (E os $ EAnd e eb)
-              x -> x
+-- | Turn a 'FP.Fail' into a single error, or prepend it to any existing ones.
+--
+-- Use when wrapping other 'get'ters.
+--
+-- We reimplement 'FP.cutting' with a tweak. Otherwise, we'd have to join lists
+-- in the error case (instead of simply prepending).
+cutting1
+    :: FP.ParserT st (ParseError FP.Pos text) a -> [text]
+    -> FP.ParserT st (ParseError FP.Pos text) a
+cutting1 (FP.ParserT p) texts =
+    FP.getPos >>= \pos -> FP.ParserT $ \fp eob s st ->
+        case p fp eob s st of
+          FP.Fail# st'    -> FP.Err# st' [ParseErrorSingle pos texts]
+          FP.Err#  st' e' -> FP.Err# st' (ParseErrorSingle pos texts : e')
+          x            -> x
 
--- | Convert a bytezap struct parser to a flatparse parser.
-bzToFp
-    :: forall a e st. KnownNat (CBLen a)
-    => BZ.ParserT st e a -> FP.ParserT st e a
-bzToFp (BZ.ParserT p) = FP.ensure (I# len#) >> (FP.ParserT $ \fpc _eob s st0 ->
-    case p fpc s 0# st0 of
-      BZ.OK#   st1 a -> FP.OK#   st1 a (s `plusAddr#` len#)
-      BZ.Fail# st1   -> FP.Fail# st1
-      BZ.Err#  st1 e -> FP.Err#  st1 e
-    )
-  where
-    !(I# len#) = cblen @a
+-- We can't provide a Generically instance because the user must choose between
+-- sum and non-sum handlers.
 
+instance GenericFOnCstr Get where
+    type GenericFOnCstrF Get = Getter
+    type GenericFOnCstrC Get dtName cstrName gf =
+        GTraverseC Get dtName cstrName 0 gf
+    genericFOnCstrF (_ :: Proxy# '(dtName, cstrName)) =
+        gTraverseC @Get @dtName @cstrName @0
+
+-- TODO this is hard to parse visually. document...?
 fpToBz
-    :: FP.ParserT st e a -> Int#
-    -> (a -> Int# -> BZ.ParserT st e r) -> BZ.ParserT st e r
+    :: FP.ParserT st (ParseError FP.Pos text) a -> Int#
+    -> (a -> Int# -> BZ.ParserT st (ParseError Int text) r)
+    -> BZ.ParserT st (ParseError Int text) r
 fpToBz (FP.ParserT p) len# fp = BZ.ParserT $ \fpc base# os# st0 ->
     case p fpc (base# `plusAddr#` (os# +# len#)) (base# `plusAddr#` os#) st0 of
       FP.OK#   st1 a s ->
         let unconsumed# = s `minusAddr#` (base# `plusAddr#` os#)
         in  BZ.runParserT# (fp a unconsumed#) fpc base# (os# +# unconsumed#) st1
+      FP.Err#  st1 e   ->
+        -- on error, we turn the flatparse 'FP.Pos' indices into actual byte
+        -- offsets (which bytezap deals in), then emit
+        let e' = fmap (mapParseErrorSinglePos (\(FP.Pos pos) -> I# len# - pos)) e
+        in  BZ.Err# st1 e'
       FP.Fail# st1     -> BZ.Fail# st1
-      FP.Err#  st1 e   -> BZ.Err#  st1 e
 
--- | Parse. On parse error, coat it in a generic context layer.
-getWrapGeneric :: Get a => String -> (E -> EGeneric E) -> Getter a
-getWrapGeneric = getWrapGeneric' get
-
-getWrapGeneric' :: Getter a -> String -> (E -> EGeneric E) -> Getter a
-getWrapGeneric' (FP.ParserT f) cd fe =
-    FP.ParserT \fp eob s st ->
-        let os = I# (minusAddr# eob s)
-         in case f fp eob s st of
-              FP.Fail# st'   -> FP.Err# st' (E os $ EGeneric cd $ fe EFail)
-              FP.Err#  st' e -> FP.Err# st' (E os $ EGeneric cd $ fe e)
-              x -> x
-
 newtype ViaGetC a = ViaGetC { unViaGetC :: a }
 instance (GetC a, KnownNat (CBLen a)) => Get (ViaGetC a) where
     {-# INLINE get #-}
     get = ViaGetC <$> bzToFp getC
 
+-- TODO messy ran out of input handling. should be a util for it
+-- TODO pos handling seems correct on quick test. need stronger assertion plz
+bzToFp :: forall a. KnownNat (CBLen a) => GetterC a -> Getter a
+bzToFp (BZ.ParserT p) =
+    (FP.ensure (I# len#) `cut1` eRanOut) >> FP.getPos >>= \(FP.Pos pos) ->
+        FP.ParserT $ \fpc _eob s st0 ->
+            case p fpc s 0# st0 of
+              BZ.OK#   st1 a -> FP.OK#   st1 a (s `plusAddr#` len#)
+              BZ.Err#  st1 e ->
+                let e' = fmap (mapParseErrorSinglePos (\idx -> FP.Pos (pos - idx))) e
+                in  FP.Err# st1 e'
+              BZ.Fail# st1   -> FP.Fail# st1
+  where
+    !(I# len#) = cblen @a
+    eRanOut = [ "ran out of input while running inner parser"
+              , "bytes needed: "<>TBL.fromDec (I# len#) ]
+
 instance TypeError ENoEmpty => Get Void where get = undefined
 instance TypeError ENoSum => Get (Either a b) where get = undefined
 
@@ -181,13 +233,10 @@
 
 -- | Parse elements until EOF. Sometimes used at the "top" of binary formats.
 instance Get a => Get [a] where
-    get = go
+    -- TODO slow, uses reverse. build a DList instead
+    get = go []
       where
-        go = do
-            FP.withOption FP.eof (\() -> pure []) $ do
-                a <- get
-                as <- go
-                pure $ a : as
+        go as = FP.branch FP.eof (pure (reverse as)) (get >>= \a -> go (a : as))
 
 -- | Return the rest of the input.
 --
@@ -217,7 +266,7 @@
 
 -- | Parse any 'Prim''.
 getPrim :: forall a. Prim' a => Getter a
-getPrim = getEBase FP.anyPrim (ERanOut (sizeOf (undefined :: a)))
+getPrim = FP.anyPrim `FP.cut'` parseError1 ["IDK"]
 
 instance Prim' a => Get (ViaPrim a) where get = ViaPrim <$> getPrim
 
@@ -229,7 +278,7 @@
     instance (Prim' a, ByteSwap a) => Get (ByteOrdered    'BigEndian a)
 
 instance Get (Refined pr (Refined pl a)) => Get (Refined (pl `And` pr) a) where
-    get = (reallyUnsafeRefine . unrefine @pl . unrefine @pr) <$> get
+    get = (unsafeRefine . unrefine @pl . unrefine @pr) <$> get
 
 {-
 
diff --git a/src/Binrep/Get/Error.hs b/src/Binrep/Get/Error.hs
--- a/src/Binrep/Get/Error.hs
+++ b/src/Binrep/Get/Error.hs
@@ -1,92 +1,60 @@
--- | Error data type definitions (shared between parsers).
+{-# LANGUAGE OverloadedStrings #-} -- for easy error building
 
+-- | Common parser error definitions.
+
 module Binrep.Get.Error where
 
-import GHC.Generics ( Generic )
-import Data.Text ( Text )
+import Data.Text.Builder.Linear qualified as TBL
+import Data.Text qualified as Text
 import Numeric.Natural ( Natural )
-import Data.Word ( Word8 )
-import Data.ByteString ( ByteString )
 
--- | Structured parse error.
-data E
-  = E Int EMiddle
-
-  -- | Unhandled parse error.
-  --
-  -- You get this if you don't change a flatparse fail to an error.
-  --
-  -- Should not be set except by library code.
-  | EFail
-
-    deriving stock (Eq, Show, Generic)
-
-data EMiddle
-
-  -- | Parse error with no further context.
-  = EBase EBase
-
-  -- | Somehow, we got two parse errors.
-  --
-  -- I have a feeling that seeing this indicates a problem in your code.
-  | EAnd E EBase
-
-  -- | Parse error decorated with generic info.
-  --
-  -- Should not be set except by library code.
-  | EGeneric String {- ^ data type name -} (EGeneric E)
-
-    deriving stock (Eq, Show, Generic)
-
-data EBase
-  = EExpectedByte Word8 Word8
-  -- ^ expected first, got second
-
-  | EOverlong Int Int
-  -- ^ expected first, got second
-
-  | EExpected ByteString ByteString
-  -- ^ expected first, got second
-
-  | EFailNamed String
-  -- ^ known fail
-
-  | EFailParse String ByteString Word8
-  -- ^ parse fail (where you parse a larger object, then a smaller one in it)
+-- | Top-level parse error.
+--
+-- The final element is the concrete error. Prior elements should "contain" the
+-- error (i.e. be the larger part that the error occurred in).
+--
+-- Really should be non-empty-- but by using List, we can use the empty list for
+-- Fail. Bit of a cute cheat.
+type ParseError pos text = [ParseErrorSingle pos text]
 
-  | ERanOut Int
-  -- ^ ran out of input, needed precisely @n@ bytes for this part (n > 0)
-  --
-  -- Actually a 'Natural', but we use 'Int' because that's what flatparse uses
-  -- internally.
+-- | A single indexed parse error.
+data ParseErrorSingle pos text = ParseErrorSingle
+  { parseErrorSinglePos  :: pos
+  , parseErrorSingleText :: [text]
+  } deriving stock Show
 
-    deriving stock (Eq, Show, Generic)
+-- | Map over the @pos@ index type of a 'ParseErrorSingle'.
+mapParseErrorSinglePos
+    :: (pos1 -> pos2)
+    -> ParseErrorSingle pos1 text
+    -> ParseErrorSingle pos2 text
+mapParseErrorSinglePos f (ParseErrorSingle pos text) =
+    ParseErrorSingle (f pos) text
 
--- | A generic context layer for a parse error of type @e@.
---
--- Recursive: parse errors occurring in fields are wrapped up here. (Those
--- errors may also have a generic context layer.)
---
--- Making this explicitly recursive may seem strange, but it clarifies that this
--- data type is to be seen as a layer over a top-level type.
-data EGeneric e
-  -- | Parse error relating to sum types (constructors).
-  = EGenericSum (EGenericSum e)
+-- | Shorthand for one parse error.
+parseError1 :: [text] -> pos -> ParseError pos text
+parseError1 texts pos = [ParseErrorSingle pos texts]
 
-  -- | Parse error in a constructor field.
-  | EGenericField
-        String          -- ^ constructor name
-        (Maybe String)  -- ^ field record name (if present)
-        Natural         -- ^ field index in constructor
-        e               -- ^ field parse error
-    deriving stock (Eq, Show, Generic)
+-- | Construct a parse error message for a generic field failure.
+parseErrorTextGenericFieldBld
+    :: String -> String -> Maybe String -> Natural
+    -> [TBL.Builder]
+parseErrorTextGenericFieldBld dtName cstrName (Just fieldName) _fieldIdx =
+  [    "in " <> TBL.fromText (Text.pack dtName)
+    <>   "." <> TBL.fromText (Text.pack cstrName)
+    <>   "." <> TBL.fromText (Text.pack fieldName) ]
+parseErrorTextGenericFieldBld dtName cstrName Nothing           fieldIdx =
+  [    "in " <> TBL.fromText (Text.pack dtName)
+    <>   "." <> TBL.fromText (Text.pack cstrName)
+    <>   "." <> TBL.fromUnboundedDec fieldIdx ]
 
-data EGenericSum e
-  -- | Parse error parsing prefix tag.
-  = EGenericSumTag e
+-- | Construct a parse error message for a generic sum tag no-match.
+parseErrorTextGenericNoCstrMatchBld :: String -> [TBL.Builder]
+parseErrorTextGenericNoCstrMatchBld dtName =
+  [    "sum tag did not match any constructors in "
+    <> TBL.fromText (Text.pack dtName) ]
 
-  -- | Unable to match a constructor to the parsed prefix tag.
-  | EGenericSumTagNoMatch
-        [String] -- ^ constructors tested
-        Text     -- ^ prettified prefix tag
-    deriving stock (Eq, Show, Generic)
+-- | Construct a parse error message for a generic sum tag parse error.
+parseErrorTextGenericSumTagBld :: String -> [TBL.Builder]
+parseErrorTextGenericSumTagBld dtName =
+  [    "while parsing sum tag in " <> TBL.fromText (Text.pack dtName) ]
diff --git a/src/Binrep/Get/Struct.hs b/src/Binrep/Get/Struct.hs
--- a/src/Binrep/Get/Struct.hs
+++ b/src/Binrep/Get/Struct.hs
@@ -1,8 +1,15 @@
 {-# LANGUAGE UndecidableInstances #-} -- for Generically instance
+{-# LANGUAGE OverloadedStrings #-} -- for easy error building
 
-module Binrep.Get.Struct where
+module Binrep.Get.Struct
+  ( GetterC, GetC(getC)
+  , getGenericStruct
+  , runGetCBs
+  , unsafeRunGetCPtr
+  ) where
 
 import Binrep.Get.Error
+import Data.Text.Builder.Linear qualified as TBL
 import Bytezap.Parser.Struct
 import Bytezap.Parser.Struct.Generic
 import Binrep.CBLen
@@ -27,46 +34,67 @@
 
 import Binrep.Common.Via.Generically.NonSum
 
-import Refined
-import Refined.Unsafe
+import Rerefined.Refine
+import Rerefined.Predicate.Logical.And
 
-type GetterC = Parser E
+type GetterC = Parser (ParseError Int TBL.Builder)
 
 -- | constant size parser
 class GetC a where getC :: GetterC a
 
+-- | Consume 'Result'.
+finishGetterC
+    :: Result (ParseError Int TBL.Builder) a
+    -> Either (ParseError Int TBL.Builder) a
+finishGetterC = \case
+  OK  a -> Right a
+  Err e -> Left  e
+  Fail  -> Left  []
+
 runGetCBs
     :: forall a. (GetC a, KnownNat (CBLen a))
-    => B.ByteString -> Either E a
+    => B.ByteString -> Either (ParseError Int TBL.Builder) a
 runGetCBs bs =
-    if   cblen @a <= B.length bs
-    then unsafeRunGetC' unsafeRunParserBs bs
-    else Left $ E 0 $ EBase $ ERanOut 0 -- TODO made up numbers
-
--- | doesn't check len
-unsafeRunGetC'
-    :: forall a buf. GetC a
-    => (forall e. buf -> Parser e a -> Result e a)
-    -> buf -> Either E a
-unsafeRunGetC' p buf =
-    case p buf getC of
-      OK   a -> Right a
-      Fail   -> Left EFail
-      Err  e -> Left e
+    if   lenReq <= lenAvail
+    then finishGetterC $ unsafeRunParserBs bs getC
+    else Left [ParseErrorSingle 0 [errMsg]]
+  where
+    lenReq   = cblen @a
+    lenAvail = B.length bs
+    errMsg   =
+        "input too short (need "<>TBL.fromDec lenReq
+                      <>", got "<>TBL.fromDec lenAvail<>")"
 
 -- | doesn't check len
 unsafeRunGetCPtr
     :: forall a. GetC a
-    => Ptr Word8 -> Either E a
-unsafeRunGetCPtr = unsafeRunGetC' unsafeRunParserPtr
+    => Ptr Word8 -> Either (ParseError Int TBL.Builder) a
+unsafeRunGetCPtr ptr = finishGetterC $ unsafeRunParserPtr ptr getC
 
 instance GParseBase GetC where
     type GParseBaseSt GetC = Proxy# Void
     type GParseBaseC  GetC a = GetC a
-    type GParseBaseE  GetC = E
-    gParseBase = getC
+    type GParseBaseE  GetC = ParseError Int TBL.Builder
+    gParseBase dtName cstrName mFieldName fieldIdx = getC `cutting1` e
+      where
+        e = parseErrorTextGenericFieldBld dtName cstrName mFieldName fieldIdx
     type GParseBaseLenTF GetC = CBLenSym
 
+-- | Turn a 'Fail' into a single error, or prepend it to any existing ones.
+--
+-- Use when wrapping other 'get'ters.
+--
+-- We reimplement @cutting@ with a tweak. Otherwise, we'd have to join lists in
+-- the error case (instead of simply prepending).
+cutting1
+    :: ParserT st (ParseError Int text) a -> [text]
+    -> ParserT st (ParseError Int text) a
+cutting1 (ParserT p) texts = ParserT $ \fpc base# os# st ->
+    case p fpc base# os# st of
+      Fail# st'    -> Err# st' [ParseErrorSingle (I# os#) texts]
+      Err#  st' e' -> Err# st' (ParseErrorSingle (I# os#) texts : e')
+      x               -> x
+
 -- | Serialize a term of the struct-like type @a@ via its 'Generic' instance.
 getGenericStruct
     :: forall a
@@ -89,7 +117,7 @@
 
 instance GetC (Refined pr (Refined pl a))
   => GetC (Refined (pl `And` pr) a) where
-    getC = (reallyUnsafeRefine . unrefine @pl . unrefine @pr) <$> getC
+    getC = (unsafeRefine . unrefine @pl . unrefine @pr) <$> getC
 
 instance GetC () where
     {-# INLINE getC #-}
@@ -128,14 +156,3 @@
     putC (l, r) = sequencePokes (putC l) (cblen @l) (putC r)
 
 -}
-
-eCBase :: EBase -> GetterC a
-eCBase eb = ParserT $ \_fpc _base os# st ->
-    Err# st (E (I# os#) $ EBase eb)
-
-getECBase :: GetterC a -> EBase -> GetterC a
-getECBase (ParserT p) eb = ParserT $ \fpc base os# st0 ->
-    case p fpc base os# st0 of
-      Fail# st1   -> Err# st1 (E (I# os#) $ EBase eb)
-      Err#  st1 e -> Err# st1 (E (I# os#) $ EAnd e eb)
-      x -> x
diff --git a/src/Binrep/Put.hs b/src/Binrep/Put.hs
--- a/src/Binrep/Put.hs
+++ b/src/Binrep/Put.hs
@@ -1,4 +1,5 @@
-{-# LANGUAGE UndecidableInstances #-} -- required below GHC 9.6
+{-# LANGUAGE UndecidableInstances #-} -- for various stuff
+{-# LANGUAGE AllowAmbiguousTypes #-} -- for type-level sum type handling
 
 module Binrep.Put where
 
@@ -17,14 +18,15 @@
 
 import GHC.Generics
 import Generic.Data.Function.FoldMap
+import Generic.Data.MetaParse.Cstr ( Raw, ParseCstrTo )
 import Generic.Type.Assert
 
 import Control.Monad.ST ( RealWorld )
 
 import Binrep.Put.Struct ( PutC(putC) )
 
-import Refined
-import Refined.Unsafe
+import Rerefined.Refine
+import Rerefined.Predicate.Logical.And
 
 import Data.Word
 import Data.Int
@@ -59,16 +61,21 @@
     put = putGenericNonSum . unGenericallyNonSum
 
 -- | Serialize a term of the sum type @a@ via its 'Generic' instance.
---
--- You must provide a serializer for @a@'s constructors. This is regrettably
--- inefficient due to having to use 'String's. Alas. Do write your own instance
--- if you want better performance!
 putGenericSum
+    :: forall sumtag a
+    .  ( Generic a, GFoldMapSum Put sumtag (Rep a)
+       , GAssertNotVoid a, GAssertSum a
+    ) => ParseCstrTo sumtag Putter -> a -> Putter
+putGenericSum = genericFoldMapSum @Put @sumtag
+
+-- | Serialize a term of the sum type @a@ via its 'Generic' instance, without
+--   pre-parsing constructor names.
+putGenericSumRaw
     :: forall a
-    .  ( Generic a, GFoldMapSum Put (Rep a)
+    .  ( Generic a, GFoldMapSum Put Raw (Rep a)
        , GAssertNotVoid a, GAssertSum a
     ) => (String -> Putter) -> a -> Putter
-putGenericSum = genericFoldMapSum @Put
+putGenericSumRaw = genericFoldMapSumRaw @Put
 
 newtype ViaPutC a = ViaPutC { unViaPutC :: a }
 instance (PutC a, KnownNat (CBLen a)) => Put (ViaPutC a) where
@@ -129,4 +136,4 @@
 -- | Put types refined with multiple predicates by wrapping the left
 --   predicate with the right. LOL REALLY?
 instance Put (Refined pr (Refined pl a)) => Put (Refined (pl `And` pr) a) where
-    put = put . reallyUnsafeRefine @_ @pr . reallyUnsafeRefine @_ @pl . unrefine
+    put = put . unsafeRefine @_ @pr . unsafeRefine @_ @pl . unrefine
diff --git a/src/Binrep/Put/Struct.hs b/src/Binrep/Put/Struct.hs
--- a/src/Binrep/Put/Struct.hs
+++ b/src/Binrep/Put/Struct.hs
@@ -26,8 +26,8 @@
 
 import Binrep.Common.Via.Generically.NonSum
 
-import Refined
-import Refined.Unsafe
+import Rerefined.Refine
+import Rerefined.Predicate.Logical.And
 
 type PutterC = Struct.Poke RealWorld
 
@@ -65,8 +65,7 @@
 
 instance PutC (Refined pr (Refined pl a))
   => PutC (Refined (pl `And` pr) a) where
-    putC =
-        putC . reallyUnsafeRefine @_ @pr . reallyUnsafeRefine @_ @pl . unrefine
+    putC = putC . unsafeRefine @_ @pr . unsafeRefine @_ @pl . unrefine
 
 instance Prim' a => PutC (ViaPrim a) where
     putC = Struct.prim . unViaPrim
diff --git a/src/Binrep/Test.hs b/src/Binrep/Test.hs
deleted file mode 100644
--- a/src/Binrep/Test.hs
+++ /dev/null
@@ -1,26 +0,0 @@
-{-# LANGUAGE UndecidableInstances #-} -- for CBLen instances
-
-module Binrep.Test where
-
-import Binrep
-import Binrep.Type.Magic
-import GHC.Generics ( Generic )
-import Data.Word
-import Binrep.Util.ByteOrder
-
-import Binrep.Common.Via.Generically.NonSum
-
-data DMagic = DMagic
-  { dMagic1_8b :: Magic '[0xFF, 0, 1, 0, 1, 0, 1, 0xFF]
-  } deriving stock Generic
-    deriving (IsCBLen, PutC) via GenericallyNonSum DMagic
-
-data DMagicSum = DMagicSum1 (Magic '[0]) | DMagicSum2 (Magic '[0xFF])
-    deriving stock Generic
-
-data DStruct = DStruct
-  { dStruct1 :: Magic '[0xFF, 0, 1, 0xFF]
-  , dStruct2 :: ByteOrdered LE Word32
-  , dStruct3 :: ()
-  } deriving stock (Generic, Show)
-    deriving (IsCBLen, PutC, GetC) via GenericallyNonSum DStruct
diff --git a/src/Binrep/Type/AsciiNat.hs b/src/Binrep/Type/AsciiNat.hs
new file mode 100644
--- /dev/null
+++ b/src/Binrep/Type/AsciiNat.hs
@@ -0,0 +1,257 @@
+{-| Naturals represented via ASCII digits.
+
+A concept which sees occasional use in places where neither speed nor size
+efficiency matter. The tar file format uses it, apparently to sidestep making a
+decision on byte ordering. Pretty silly.
+
+As with other binrep string-likes, you probably want to wrap this with
+'Binrep.Type.Sized.Sized' or 'Binrep.Type.Prefix.Size.SizePrefixed'.
+
+We use a refinement to permit using any numeric type, while ensuring that
+negative values are not permitted.
+-}
+
+{-# LANGUAGE AllowAmbiguousTypes #-}
+{-# LANGUAGE OverloadedStrings #-} -- for refined error
+{-# LANGUAGE UndecidableInstances #-} -- for deriving predicate instance
+
+module Binrep.Type.AsciiNat where
+
+import Binrep
+
+import GHC.Exts ( Word(W#), Word#, Int(I#), word2Int#, eqWord#, plusWord# )
+import Util.TypeNats ( natValWord )
+import Data.Semigroup ( sconcat )
+
+import GHC.Num.Primitives ( wordLogBase# )
+import GHC.Num.Natural ( naturalSizeInBase# )
+
+import Data.Word
+import Data.Int
+import Data.List.NonEmpty ( NonEmpty( (:|) ) )
+
+import GHC.TypeNats ( Natural, KnownNat )
+
+import Data.ByteString qualified as B
+import Binrep.Type.Thin ( Thin(Thin) )
+
+import Rerefined.Predicate
+import Rerefined.Predicate.Via
+import Rerefined.Predicate.Relational.Value
+import Rerefined.Predicate.Relational
+import Rerefined.Refine
+import TypeLevelShow.Natural
+import TypeLevelShow.Utils
+
+import Data.Text.Builder.Linear qualified as TBL
+
+-- | A natural represented in binary as an ASCII string, where each character is
+--   a digit in the given base.
+--
+-- Only certain bases are supported: 2, 8, 10 and 16.
+--
+-- Hex parsing permits mixed case digits when parsing (@1-9a-fA-F@), and
+-- serializes with lower-case ASCII hex digits.
+data AsciiNat (base :: Natural)
+--type AsciiNat base = Refined (AsciiNat base)
+
+instance Predicate (AsciiNat base) where
+    type PredicateName d (AsciiNat base) = ShowParen (d > 9)
+        ("AsciiNat " ++ ShowNatDec base)
+
+instance (KnownPredicateName (AsciiNat base), Num a, Ord a)
+  => Refine (AsciiNat base) a where
+    validate = validateVia @(CompareValue GTE Pos 0)
+
+-- | Compare two 'AsciiNat's, ignoring base information.
+asciiNatCompare
+    :: Ord a => Refined (AsciiNat bl) a -> Refined (AsciiNat br) a -> Ordering
+asciiNatCompare l r = compare (unrefine l) (unrefine r)
+
+-- | The bytelength of an 'AsciiNat' is the number of digits in the number in
+--   the given base. We can calculate this generally with great efficiency
+--   using GHC (ghc-bignum) primitives!
+instance (HasBaseOps a, KnownNat base) => BLen (Refined (AsciiNat base) a) where
+    blen n = I# (word2Int# (sizeInBase# base# (unrefine n)))
+      where
+        !(W# base#) = natValWord @base
+
+class HasBaseOps a where
+    -- | See ghc-bignum internals at @GHC.Num.*@.
+    sizeInBase# :: Word# -> a -> Word#
+
+instance HasBaseOps Word    where sizeInBase# = sizeInBaseWordSize
+instance HasBaseOps Natural where
+    sizeInBase# base = \case
+      0 -> 1##
+      a -> naturalSizeInBase# base a
+
+instance HasBaseOps Word8  where sizeInBase# = sizeInBaseWordSize
+instance HasBaseOps Word16 where sizeInBase# = sizeInBaseWordSize
+instance HasBaseOps Word32 where sizeInBase# = sizeInBaseWordSize
+
+-- | TODO unsafe for 32-bit platform
+instance HasBaseOps Word64 where sizeInBase# = sizeInBaseWordSize
+
+instance HasBaseOps Int8   where sizeInBase# = sizeInBaseWordSize
+instance HasBaseOps Int16  where sizeInBase# = sizeInBaseWordSize
+instance HasBaseOps Int32  where sizeInBase# = sizeInBaseWordSize
+
+-- | TODO unsafe for 32-bit platform
+instance HasBaseOps Int64  where sizeInBase# = sizeInBaseWordSize
+
+-- | 'Int' can use 'Word' size (but TODO what happens for negatives?)
+instance HasBaseOps Int  where sizeInBase# = sizeInBaseWordSize
+
+-- | Safe for types smaller than a 'Word'.
+--
+-- Uses ghc-bignum internals. Slightly unwrapped for better performance.
+--
+-- One could perhaps write faster algorithms for smaller primitive types too...
+-- but performance increase would be minimal if even present.
+sizeInBaseWordSize :: Integral a => Word# -> a -> Word#
+sizeInBaseWordSize base a =
+    case w# `eqWord#` 0## of
+      1# -> 1##
+      _  -> 1## `plusWord#` wordLogBase# base w#
+  where
+    !(W# w#) = fromIntegral a
+
+-- | Serialize any term of an 'Integral' type to binary (base 2) ASCII.
+instance Integral a => Put (Refined (AsciiNat  2) a) where
+    put = sconcat . fmap (put . (+) 0x30) . unsafeDigits @Word8  2 . unrefine
+
+-- | Serialize any term of an 'Integral' type to octal (base 8) ASCII.
+instance Integral a => Put (Refined (AsciiNat  8) a) where
+    put = sconcat . fmap (put . (+) 0x30) . unsafeDigits @Word8  8 . unrefine
+
+-- | Serialize any term of an 'Integral' type to decimal (base 10) ASCII.
+instance Integral a => Put (Refined (AsciiNat 10) a) where
+    put = sconcat . fmap (put . (+) 0x30) . unsafeDigits @Word8 10 . unrefine
+
+-- | Serialize any term of an 'Integral' type to hex (base 16) ASCII.
+--
+-- Uses lower-case ASCII.
+instance Integral a => Put (Refined (AsciiNat 16) a) where
+    put =
+          sconcat . fmap (put . unsafeHexDigitToAsciiLower)
+        . unsafeDigits @Word8 16 . unrefine
+
+-- | Parse a  binary  (base 2) ASCII natural to any 'Num' type.
+instance (Num a, Ord a) => Get (Refined (AsciiNat  2)  a) where
+    get = unsafeRefine <$> getAsciiNatByByte 2  "binary"  parseBinaryAsciiDigit
+
+-- | Parse an octal   (base 8) ASCII natural to any 'Num' type.
+instance (Num a, Ord a) => Get (Refined (AsciiNat  8)  a) where
+    get = unsafeRefine <$> getAsciiNatByByte 8  "octal"   parseOctalAsciiDigit
+
+-- | Parse a  decimal (base 10) ASCII natural to any 'Num' type.
+instance (Num a, Ord a) => Get (Refined (AsciiNat 10) a) where
+    get = unsafeRefine <$> getAsciiNatByByte 10 "decimal" parseDecimalAsciiDigit
+
+-- | Parse a  hex     (base 16) ASCII natural to any 'Num' type.
+--
+-- Parses lower and upper case (mixed permitted).
+instance (Num a, Ord a) => Get (Refined (AsciiNat 16) a) where
+    get = unsafeRefine <$> getAsciiNatByByte 16 "hex"     parseHexAsciiDigit
+
+-- | Parse an ASCII natural in the given base with the given digit parser.
+--
+-- Parses byte-by-byte. As such, it only supports bases up to 256.
+getAsciiNatByByte :: Num a => a -> TBL.Builder -> (a -> Maybe a) -> Getter a
+getAsciiNatByByte base baseStr f = do
+    Thin bs <- get -- no need to copy since we consume during parsing!
+    if   B.null bs
+    then err1 ["ASCII natural cannot be empty"]
+    else case asciiBytesToNat f base bs of
+          Left  b -> err1 [
+            "non-"<>baseStr<>" ASCII digit in "
+            <>baseStr<>" ASCII natural: "<>TBL.fromDec b]
+          Right n -> pure n
+
+{- | Get the digits in the given number as rendered in the given base.
+
+Digits will be between 0-base. The return type must be sized to support this.
+
+Base must be > 2. This is not checked. (Internal function eh.)
+
+Note the 'NonEmpty' return type. Returns @[0]@ for 0 input. (This does not match
+ghc-bignum's @sizeInBase@ primitives!)
+-}
+unsafeDigits :: forall b a. (Integral a, Integral b) => a -> a -> NonEmpty b
+unsafeDigits base = go []
+  where
+    go s x = loop (head' :| s) tail'
+      where
+        head' = fromIntegral (x `mod` base)
+        tail' = x `div` base
+    loop s@(r :| rs) = \case
+        0 -> s
+        x -> go (r : rs) x
+
+asciiBytesToNat
+    :: Num a => (a -> Maybe a) -> a -> B.ByteString -> Either Word8 a
+asciiBytesToNat f base bs =
+    -- we use Int for exponent because it seems most sensible & gets SPECIALISEd
+    case B.foldr go (Right (0, (0 :: Int))) bs of
+      Left w -> Left w
+      Right (n, _) -> Right n
+  where
+    go _ (Left w) = Left w
+    go w (Right (n, expo)) =
+        case f (fromIntegral w) of
+          Nothing -> Left w
+          Just d  -> Right (n + d * base^expo, expo+1)
+
+parseBinaryAsciiDigit :: (Num a, Ord a) => a -> Maybe a
+parseBinaryAsciiDigit = \case
+  0x30 -> Just 0 -- 0
+  0x31 -> Just 1 -- 1
+  _    -> Nothing
+
+parseOctalAsciiDigit :: (Num a, Ord a) => a -> Maybe a
+parseOctalAsciiDigit a
+  | a >= 0x30 && a <= 0x37 = Just $ a - 0x30 -- 0-7
+  | otherwise = Nothing
+
+parseDecimalAsciiDigit :: (Num a, Ord a) => a -> Maybe a
+parseDecimalAsciiDigit a
+  | a >= 0x30 && a <= 0x39 = Just $ a - 0x30 -- 0-9
+  | otherwise = Nothing
+
+parseHexAsciiDigit :: (Num a, Ord a) => a -> Maybe a
+parseHexAsciiDigit a
+  | a >= 0x30 && a <= 0x39 = Just $ a - 0x30 -- 0-9
+  | a >= 0x41 && a <= 0x46 = Just $ a - 0x37 -- A-F (upper case)
+  | a >= 0x61 && a <= 0x66 = Just $ a - 0x57 -- a-f (lower case)
+  | otherwise = Nothing
+
+-- | May only be called with 0<=n<=15.
+unsafeHexDigitToAsciiLower :: (Num a, Ord a) => a -> a
+unsafeHexDigitToAsciiLower a
+  | a <= 9    = 0x30 + a
+  | otherwise = 0x57 + a
+
+{-
+
+-- | Print a binary (base 2) ASCII natural with an @0b@ prefix.
+prettyAsciiNat2 :: Integral a => Int -> a -> ShowS
+prettyAsciiNat2 _ n = showString "0b" . showBin n
+
+-- | Show binary (base 2) ASCII naturals with an @0b@ prefix.
+instance Integral a => Show (AsciiNat 2 a) where
+    showsPrec _ n = showString "0b" . showBin (unAsciiNat n)
+
+-- | Show octal (base 8) ASCII naturals with an @0o@ prefix.
+instance Integral a => Show (AsciiNat 8  a) where
+    showsPrec _ n = showString "0o" . showOct (unAsciiNat n)
+
+-- | Show decimal (base 10) ASCII naturals with no prefix.
+instance Integral a => Show (AsciiNat 10 a) where
+    showsPrec _ = showInt . unAsciiNat
+
+-- | Show hex (base 16) ASCII naturals with an @0x@ prefix.
+instance Integral a => Show (AsciiNat 16 a) where
+    showsPrec _ n = showString "0x" . showHex (unAsciiNat n)
+
+-}
diff --git a/src/Binrep/Type/Derived/NullTermPadded.hs b/src/Binrep/Type/Derived/NullTermPadded.hs
--- a/src/Binrep/Type/Derived/NullTermPadded.hs
+++ b/src/Binrep/Type/Derived/NullTermPadded.hs
@@ -10,7 +10,8 @@
 import Binrep.Type.NullTerminated
 import Binrep.Type.NullPadded
 
-import Refined
+import Rerefined.Predicate.Logical.And
+import Rerefined.Refine ( Refined )
 
 -- | Predicate for null-terminated, then null-padded data.
 type NullTermPad n = NullTerminate `And` NullPad n
diff --git a/src/Binrep/Type/Magic.hs b/src/Binrep/Type/Magic.hs
--- a/src/Binrep/Type/Magic.hs
+++ b/src/Binrep/Type/Magic.hs
@@ -1,4 +1,6 @@
-{-# LANGUAGE UndecidableInstances #-} -- for weirder type families
+{-# LANGUAGE UndecidableInstances #-} -- for tons of stuff
+{-# LANGUAGE PatternSynonyms #-} -- TODO wip
+{-# LANGUAGE OverloadedStrings #-} -- for easy error building
 
 {- | Magic numbers (also just magic): short constant bytestrings usually
      found at the top of a file, often used as an early sanity check.
@@ -8,8 +10,8 @@
   * byte magics e.g. Zstandard: @28 B5 2F FD@
   * printable magics e.g. Ogg: @4F 67 67 53@ -> @OggS@ (in ASCII)
 
-For byte magics, use type-level 'Natural' lists.
-For printable magics, use 'Symbol's (type-level strings).
+For byte magics, use type-level 'Natural' lists e.g. @'Magic' \@'[0xFF, 0x01]@
+For printable (UTF-8) magics, use 'Symbol's e.g. @'Magic' \@"hello"@.
 -}
 
 module Binrep.Type.Magic
@@ -20,7 +22,6 @@
 
 import Data.Type.Symbol.Utf8 ( type SymbolToUtf8 )
 
-import Util.TypeNats ( natValInt )
 import GHC.TypeLits ( type Natural, type Symbol, type KnownNat, type (+) )
 
 import GHC.Generics ( Generic )
@@ -32,80 +33,71 @@
 import Bytezap.Parser.Struct.TypeLits.Bytes
   ( ParseReifyBytesW64(parseReifyBytesW64) )
 import Bytezap.Parser.Struct qualified as BZ
-import Data.ByteString.Internal qualified as B
-import GHC.Exts ( Int(I#), plusAddr#, Ptr(Ptr) )
-import Foreign.Marshal.Utils ( copyBytes )
+import GHC.Exts ( Int(I#) )
 import FlatParse.Basic qualified as FP
+import Data.Text.Builder.Linear qualified as TBL
 
--- | A singleton data type representing a "magic number" via a phantom type.
---
--- The phantom type variable unambiguously defines a constant bytestring.
--- A handful of types are supported for using magics conveniently, e.g. for pure
--- ASCII magics, you may use a 'Symbol' type-level string.
-data Magic (a :: k) = Magic deriving stock (Generic, Data, Show, Eq)
+{- | A unit data type representing a "magic number" via a phantom type.
 
--- | Weaken a @'Magic' a@ to the unit.
+The phantom type unambiguously defines a bytestring at compile time. This
+depends on the type's kind. See 'MagicBytes' for details.
+
+This is defined using GADT syntax to permit labelling the phantom type kind as
+/inferred/, which effectively means hidden (not available for visible type
+applications). That kind is always evident from the type, so it's just nicer.
+-}
+data Magic a where Magic :: forall {k} (a :: k). Magic a
+    deriving stock (Generic, Data, Show, Eq)
+
+-- | Weaken a @'Magic' a@ to the unit '()'.
 instance Weaken (Magic a) where
     type Weak (Magic a) = ()
     weaken Magic = ()
 
--- | Strengthen the unit to some @'Magic' a@.
-instance Strengthen (Magic a) where strengthen () = pure Magic
+-- | Strengthen the unit '()' to some @'Magic' a@.
+instance Strengthen (Magic a) where strengthen () = Right Magic
 
 -- | The byte length of a magic is known at compile time.
 instance IsCBLen (Magic a) where type CBLen (Magic a) = Length (MagicBytes a)
 
--- | The byte length of a magic is obtained via reifying.
 deriving via ViaCBLen (Magic a) instance
     KnownNat (Length (MagicBytes a)) => BLen (Magic a)
 
+-- | Efficiently serialize a @'Magic' a@.
 instance (bs ~ MagicBytes a, ReifyBytesW64 bs) => PutC (Magic a) where
     putC Magic = reifyBytesW64 @bs
 
 deriving via (ViaPutC (Magic a)) instance
   (bs ~ MagicBytes a, ReifyBytesW64 bs, KnownNat (Length bs)) => Put (Magic a)
 
-{- this works, but is ugly.
-* we have to duplicate our error wrapping because errors use parser internals
-* we throw the magic into the error, so we need the serializer constraints too
-I mean, it's fine. It's correct. It's as fast as possible. But it looks bad :<
--}
-instance
-  ( bs ~ MagicBytes a, ParseReifyBytesW64 bs
-  , ReifyBytesW64 bs, KnownNat (Length bs)
-  ) => GetC (Magic a) where
-    getC = BZ.ParserT $ \fpc base os# st0 ->
-        case BZ.runParserT# (parseReifyBytesW64 @bs) fpc base os# st0 of
-          BZ.OK#   st1 () -> BZ.OK#  st1 Magic
-          BZ.Fail# st1    ->
-            let bsActual = B.unsafeCreate len (\buf -> copyBytes buf (Ptr (base `plusAddr#` os#)) len)
-                eb = EExpected bsExpected bsActual
-            in  BZ.Err# st1 (E (I# os#) $ EBase eb)
-          BZ.Err#  st1 e  ->
-            let bsActual = B.unsafeCreate len (\buf -> copyBytes buf (Ptr (base `plusAddr#` os#)) len)
-                eb = EExpected bsExpected bsActual
-            in  BZ.Err# st1 (E (I# os#) $ EAnd e eb)
-      where
-        len = natValInt @(Length bs)
-        bsExpected = runPutC (Magic :: Magic a)
+-- | Efficiently parse a @'Magic' a@. Serialization constraints are included as
+--   we emit the expected bytestring in errors.
+instance (bs ~ MagicBytes a, ParseReifyBytesW64 0 bs) => GetC (Magic a) where
+    getC = BZ.ParserT $ \fpc base# os# st0 ->
+        case BZ.runParserT# (parseReifyBytesW64 @0 @bs) fpc base# os# st0 of
+          BZ.OK#   st1 ()             -> BZ.OK#   st1 Magic
+          BZ.Err#  st1 (pos, bActual) -> BZ.Err#  st1 (parseError1
+            ["TODO magic parse error: "<>TBL.fromDec bActual]
+            (pos + I# os#))
+          BZ.Fail# st1                -> BZ.Fail# st1 -- shouldn't occur
 
 deriving via ViaGetC (Magic a) instance
-  ( bs ~ MagicBytes a, ParseReifyBytesW64 bs
+  ( bs ~ MagicBytes a, ParseReifyBytesW64 0 bs
   , ReifyBytesW64 bs, KnownNat (Length bs)
   ) => Get (Magic a)
 
 -- | Types which define a magic value.
 class Magical (a :: k) where
-    -- | How to turn the type into a list of bytes.
+    -- | How to turn the type into a list of bytes (stored using 'Natural's).
     type MagicBytes a :: [Natural]
 
 -- | Type-level naturals go as-is. (Make sure you don't go over 255, though!)
-instance Magical (ns :: [Natural]) where type MagicBytes ns = ns
+instance Magical (bs :: [Natural]) where type MagicBytes bs = bs
 
 -- | Type-level symbols are converted to UTF-8.
 instance Magical (sym :: Symbol) where type MagicBytes sym = SymbolToUtf8 sym
 
 -- | The length of a type-level list.
 type family Length (a :: [k]) :: Natural where
-    Length '[]       = 0
     Length (a ': as) = 1 + Length as
+    Length '[]       = 0
diff --git a/src/Binrep/Type/NullPadded.hs b/src/Binrep/Type/NullPadded.hs
--- a/src/Binrep/Type/NullPadded.hs
+++ b/src/Binrep/Type/NullPadded.hs
@@ -1,6 +1,7 @@
 -- | Data null-padded to a given length.
 
-{-# LANGUAGE OverloadedStrings #-}
+{-# LANGUAGE UndecidableInstances #-} -- for PredicateName
+{-# LANGUAGE OverloadedStrings #-} -- for refine error builder
 
 module Binrep.Type.NullPadded where
 
@@ -11,20 +12,22 @@
 import Raehik.Compat.FlatParse.Basic.WithLength qualified as FP
 import Control.Monad.Combinators ( skipCount )
 
-import Binrep.Util ( tshow )
-
-import Refined
-import Refined.Unsafe
+import Rerefined.Predicate.Common
+import Rerefined.Refine
+import TypeLevelShow.Natural
+import TypeLevelShow.Utils
+import Data.Text.Builder.Linear qualified as TBL
 
 import GHC.TypeNats
 import Util.TypeNats ( natValInt )
 
-import Data.Typeable ( typeRep )
-
 import Bytezap.Parser.Struct qualified as BZG
 import GHC.Exts ( Int(I#) )
 
 data NullPad (n :: Natural)
+instance Predicate (NullPad n) where
+    type PredicateName d (NullPad n) = ShowParen (d > 9)
+        ("NullPad " ++ ShowNatDec n)
 
 {- | A type which is to be null-padded to a given total length.
 
@@ -48,12 +51,10 @@
 deriving via ViaCBLen (NullPadded n a) instance KnownNat n => BLen (NullPadded n a)
 
 -- | Assert that term will fit.
-instance (BLen a, KnownNat n) => Predicate (NullPad n) a where
-    validate p a
-      | len <= n = success
-      | otherwise
-          = throwRefineOtherException (typeRep p) $
-                   "too long: " <> tshow len <> " > " <> tshow n
+instance (KnownPredicateName (NullPad n), BLen a, KnownNat n)
+  => Refine (NullPad n) a where
+    validate p a = validateBool p (len <= n) $
+        "too long: " <> TBL.fromDec len <> " > " <> TBL.fromDec n
       where
         n = natValInt @n
         len = blen a
@@ -78,7 +79,7 @@
 instance (KnownNat n, Get a) => GetC (NullPadded n a) where
     getC = fpToBz get len# $ \a _unconsumed# ->
         -- TODO consume nulls lol
-        BZG.constParse $ reallyUnsafeRefine a
+        BZG.constParse $ unsafeRefine a
       where
         !(I# len#) = natValInt @n
 
@@ -87,7 +88,6 @@
         (a, len) <- FP.parseWithLength get
         let paddingLen = natValInt @n - len
         if   paddingLen < 0
-        then eBase $ EFailNamed "TODO used to be EOverlong, cba"
-        else do
-            skipCount paddingLen (FP.word8 0x00)
-            pure $ reallyUnsafeRefine a
+        then err1 ["TODO used to be EOverlong, cba"]
+        else do skipCount paddingLen (FP.word8 0x00)
+                pure $ unsafeRefine a
diff --git a/src/Binrep/Type/NullTerminated.hs b/src/Binrep/Type/NullTerminated.hs
--- a/src/Binrep/Type/NullTerminated.hs
+++ b/src/Binrep/Type/NullTerminated.hs
@@ -13,9 +13,8 @@
 
 import FlatParse.Basic qualified as FP
 
-import Refined
-import Refined.Unsafe
-import Data.Typeable ( typeRep )
+import Rerefined.Predicate.Common
+import Rerefined.Refine
 
 import Data.ByteString qualified as B
 import Data.Word ( Word8 )
@@ -23,20 +22,18 @@
 -- | Null-terminated data. Arbitrary length terminated with a null byte.
 --   Permits no null bytes inside the data.
 data NullTerminate
+
+instance Predicate NullTerminate where
+    type PredicateName d NullTerminate = "NullTerminate"
+
 type NullTerminated = Refined NullTerminate
 
 -- | Null-terminated data may not contain any null bytes.
-instance NullCheck a => Predicate NullTerminate a where
-    validate p a
-     | hasNoNulls a = throwRefineOtherException (typeRep p) $
+instance Refine NullTerminate B.ByteString where
+    -- TODO is there a faster check we can conjure up here...?
+    validate p a = validateBool p (not (B.any (== 0x00) a)) $
         "null byte not permitted in null-terminated data"
-     | otherwise = success
 
-class NullCheck a where hasNoNulls :: a -> Bool
-instance NullCheck B.ByteString where
-    {-# INLINE hasNoNulls #-}
-    hasNoNulls = B.any (== 0x00)
-
 instance BLen a => BLen (NullTerminated a) where
     blen ra = 1 + blen (unrefine ra)
     {-# INLINE blen #-}
@@ -48,9 +45,16 @@
     put a = put (unrefine a) <> put @Word8 0x00
 
 -- | We may parse any null-terminated data using a special flatparse combinator.
+--
+-- The combinator doesn't permit distinguishing between the two possible
+-- failures: either there was no next null, or the inner parser didn't consume
+-- up to it.
 instance Get a => Get (NullTerminated a) where
     {-# INLINE get #-}
-    get = reallyUnsafeRefine <$> getEBase (FP.isolateToNextNull get) (EFailNamed "cstring")
+    get = unsafeRefine <$> cut1 (FP.isolateToNextNull get) e
+      where e = [ "while isolating to next null"
+                , "either there was no next null in the input,"
+                , "or the inner parser didn't fully consume its input" ]
 
 {-
 I don't know how to do @[a]@. Either I nullterm each element, which is weird
diff --git a/src/Binrep/Type/Prefix/Count.hs b/src/Binrep/Type/Prefix/Count.hs
--- a/src/Binrep/Type/Prefix/Count.hs
+++ b/src/Binrep/Type/Prefix/Count.hs
@@ -3,34 +3,44 @@
 
 module Binrep.Type.Prefix.Count where
 
-import Binrep.Util.Prefix
+import Binrep.Type.Prefix.Internal
 import Binrep
 import Control.Monad.Combinators qualified as Monad
 
 import GHC.TypeNats
 import Util.TypeNats ( natValInt )
-import Refined hiding ( Weaken(..), strengthen )
-import Refined.Unsafe ( reallyUnsafeRefine1 )
 
-import Data.Typeable ( Typeable, typeRep )
-import Data.Kind
+import Rerefined.Predicate.Common
+import Rerefined.Refine
+import TypeLevelShow.Utils
 
+import Data.Kind ( type Type )
+
 import Data.Foldable qualified as Foldable
 
+-- TODO put monofoldable in here, instead of that useless @(f a)@ stuff
+
 data CountPrefix (pfx :: Type)
-type CountPrefixed pfx = Refined1 (CountPrefix pfx)
 
-instance (KnownNat (Max pfx), Foldable f, Typeable pfx)
-  => Predicate1 (CountPrefix pfx) f where
-    validate1 p fa
-      | Foldable.length fa <= natValInt @(Max pfx) = success
-      | otherwise = throwRefineOtherException (typeRep p) "TODO bad"
+instance Predicate (CountPrefix pfx) where
+    type PredicateName d (CountPrefix pfx) = ShowParen (d > 9)
+        ("CountPrefix " ++ LenNatName pfx)
 
-instance (KnownNat (Max pfx), Foldable f, Typeable pfx)
-  => Predicate (CountPrefix pfx) (f a) where
+instance
+  ( KnownPredicateName (CountPrefix pfx), KnownNat (LenNatMax pfx), Foldable f
+  ) => Refine1 (CountPrefix pfx) f where
+    validate1 p fa =
+        validateBool p (Foldable.length fa <= natValInt @(LenNatMax pfx)) $
+            "TODO too large for count prefix"
+
+instance
+  ( KnownPredicateName (CountPrefix pfx), KnownNat (LenNatMax pfx), Foldable f
+  ) => Refine (CountPrefix pfx) (f a) where
     validate = validate1
 
--- | We can know byte length at compile time _if_ we know it for the prefix and
+type CountPrefixed pfx = Refined1 (CountPrefix pfx)
+
+-- | We can know byte length at compile time /if/ we know it for the prefix and
 --   the list-like.
 --
 -- This is extremely unlikely, because then what counting are we even
@@ -42,22 +52,22 @@
 --   (holding the length of the type) plus the length of the type.
 --
 -- Bit confusing. How to explain this? TODO
-instance (Prefix pfx, Foldable f, BLen pfx, BLen (f a))
+instance (LenNat pfx, Foldable f, BLen pfx, BLen (f a))
   => BLen (CountPrefixed pfx f a) where
-    blen rfa = blen (lenToPfx @pfx (Foldable.length fa)) + blen fa
+    blen rfa = blen (lenToNat @pfx (Foldable.length fa)) + blen fa
       where fa = unrefine1 rfa
 
-instance (Prefix pfx, Foldable f, Put pfx, Put (f a))
+instance (LenNat pfx, Foldable f, Put pfx, Put (f a))
   => Put (CountPrefixed pfx f a) where
-    put rfa = put (lenToPfx @pfx (Foldable.length fa)) <> put fa
+    put rfa = put (lenToNat @pfx (Foldable.length fa)) <> put fa
       where fa = unrefine1 rfa
 
 class GetCount f where getCount :: Get a => Int -> Getter (f a)
 instance GetCount [] where getCount n = Monad.count n get
 
-instance (Prefix pfx, GetCount f, Get pfx, Get a)
+instance (LenNat pfx, GetCount f, Get pfx, Get a)
   => Get (CountPrefixed pfx f a) where
     get = do
         pfx <- get @pfx
-        fa <- getCount (pfxToLen pfx)
-        pure $ reallyUnsafeRefine1 fa
+        fa <- getCount (natToLen pfx)
+        pure $ unsafeRefine1 fa
diff --git a/src/Binrep/Type/Prefix/Internal.hs b/src/Binrep/Type/Prefix/Internal.hs
new file mode 100644
--- /dev/null
+++ b/src/Binrep/Type/Prefix/Internal.hs
@@ -0,0 +1,65 @@
+{-# LANGUAGE UndecidableInstances #-} -- for convenient type level arithmetic
+
+module Binrep.Type.Prefix.Internal where
+
+import Binrep.Util.ByteOrder ( ByteOrdered(ByteOrdered) )
+import GHC.TypeNats
+import GHC.TypeLits ( type Symbol )
+import Data.Word
+import Data.Kind ( type Type )
+
+-- | Types which can encode natural (positive integer) lengths.
+--
+-- Types must provide convert to and from 'Int', which is the most common type
+-- used for data lengths.
+class LenNat a where
+    -- | The maximum value the type can encode.
+    type LenNatMax a :: Natural
+
+    -- | The name of the type, to display when used as part of a predicate.
+    type LenNatName a :: Symbol
+
+    -- | Turn an 'Int' length into an @a@.
+    --
+    -- It is guaranteed that the 'Int' fits i.e. @<= 'LenNatMax' a@.
+    lenToNat :: Int -> a
+
+    -- | Turn an @a@ into an 'Int' length.
+    --
+    -- Don't worry if @a@ may encode larger numbers than 'Int'. I think other
+    -- things will be breaking at that point. Or perhaps it's our responsibility
+    -- to emit the runtime error? TODO.
+    natToLen :: a -> Int
+
+-- | The unit can only encode 1 value -> lengths of 0 only.
+instance LenNat () where
+    type LenNatMax  () = 0
+    type LenNatName () = "()"
+    lenToNat = \case
+      0 -> ()
+      _ -> error "you lied to refine and broke everything :("
+    natToLen () = 0
+
+-- | Byte ordering doesn't change how prefixes work.
+deriving via (a :: Type) instance LenNat a => LenNat (ByteOrdered end a)
+
+instance LenNat Word8  where
+    type LenNatMax  Word8  = 2^8  - 1
+    type LenNatName Word8 = "Word8"
+    lenToNat = fromIntegral
+    natToLen = fromIntegral
+instance LenNat Word16 where
+    type LenNatMax  Word16 = 2^16 - 1
+    type LenNatName Word16 = "Word16"
+    lenToNat = fromIntegral
+    natToLen = fromIntegral
+instance LenNat Word32 where
+    type LenNatMax  Word32 = 2^32 - 1
+    type LenNatName Word32 = "Word32"
+    lenToNat = fromIntegral
+    natToLen = fromIntegral -- TODO check for overflow?
+instance LenNat Word64 where
+    type LenNatMax  Word64 = 2^64 - 1
+    type LenNatName Word64 = "Word64"
+    lenToNat = fromIntegral
+    natToLen = fromIntegral -- TODO check for overflow?
diff --git a/src/Binrep/Type/Prefix/Size.hs b/src/Binrep/Type/Prefix/Size.hs
--- a/src/Binrep/Type/Prefix/Size.hs
+++ b/src/Binrep/Type/Prefix/Size.hs
@@ -3,7 +3,7 @@
 
 module Binrep.Type.Prefix.Size where
 
-import Binrep.Util.Prefix
+import Binrep.Type.Prefix.Internal
 import Binrep.Type.Thin
 import Binrep
 import FlatParse.Basic qualified as FP
@@ -11,43 +11,48 @@
 import GHC.TypeNats
 import Util.TypeNats ( natValInt )
 import Data.ByteString qualified as B
-import Refined hiding ( Weaken(..), strengthen )
-import Refined.Unsafe
 
-import Data.Typeable ( Typeable, typeRep )
-import Data.Kind
+import Rerefined.Predicate.Common
+import Rerefined.Refine
+import TypeLevelShow.Utils
 
+import Data.Kind ( type Type )
+
 data SizePrefix (pfx :: Type)
+
+instance Predicate (SizePrefix pfx) where
+    type PredicateName d (SizePrefix pfx) = ShowParen (d > 9)
+        ("SizePrefix " ++ LenNatName pfx)
+
 type SizePrefixed pfx = Refined (SizePrefix pfx)
 
-instance (KnownNat (Max pfx), BLen a, Typeable pfx)
-  => Predicate (SizePrefix pfx) a where
-    validate p a
-      | blen a <= natValInt @(Max pfx) = Nothing
-      | otherwise = throwRefineOtherException (typeRep p) $
-          "thing too big for length prefix type"
+instance
+  ( KnownPredicateName (SizePrefix pfx), KnownNat (LenNatMax pfx), BLen a
+  ) => Refine (SizePrefix pfx) a where
+    validate p a = validateBool p (blen a <= natValInt @(LenNatMax pfx)) $
+        "thing too big for length prefix type"
 
 -- TODO no idea if this is sensible
 instance IsCBLen (SizePrefixed pfx a) where
     type CBLen (SizePrefixed pfx a) = CBLen pfx + CBLen a
 
-instance (Prefix pfx, BLen a, BLen pfx)
+instance (LenNat pfx, BLen a, BLen pfx)
   => BLen (SizePrefixed pfx a) where
-    blen ra = blen (lenToPfx @pfx (blen a)) + blen a
+    blen ra = blen (lenToNat @pfx (blen a)) + blen a
       where a = unrefine ra
 
-instance (Prefix pfx, BLen a, Put pfx, Put a)
+instance (LenNat pfx, BLen a, Put pfx, Put a)
   => Put (SizePrefixed pfx a) where
-    put ra = put (lenToPfx @pfx (blen a)) <> put a
+    put ra = put (lenToNat @pfx (blen a)) <> put a
       where a = unrefine ra
 
 class GetSize a where getSize :: Int -> Getter a
 instance GetSize       B.ByteString  where getSize = fmap B.copy . FP.take
 instance GetSize (Thin B.ByteString) where getSize = fmap Thin . FP.take
 
-instance (Prefix pfx, GetSize a, Get pfx)
+instance (LenNat pfx, GetSize a, Get pfx)
   => Get (SizePrefixed pfx a) where
     get = do
         pfx <- get @pfx
-        a <- getSize (pfxToLen pfx)
-        pure $ reallyUnsafeRefine a
+        a <- getSize (natToLen pfx)
+        pure $ unsafeRefine a
diff --git a/src/Binrep/Type/Sized.hs b/src/Binrep/Type/Sized.hs
--- a/src/Binrep/Type/Sized.hs
+++ b/src/Binrep/Type/Sized.hs
@@ -1,31 +1,35 @@
 -- | Constant-size data.
 
-{-# LANGUAGE OverloadedStrings #-}
+{-# LANGUAGE UndecidableInstances #-} -- for PredicateName
+{-# LANGUAGE OverloadedStrings #-} -- for refine error builder
 
 module Binrep.Type.Sized where
 
 import Binrep
 import FlatParse.Basic qualified as FP
 
-import Binrep.Util ( tshow )
-
-import Refined
-import Refined.Unsafe
-import Data.Typeable ( typeRep )
+import Rerefined.Predicate.Common
+import Rerefined.Refine
+import TypeLevelShow.Natural
+import TypeLevelShow.Utils
+import Data.Text.Builder.Linear qualified as TBL
 
 import GHC.TypeNats
 import Util.TypeNats ( natValInt )
 
 -- | Essentially runtime reflection of a 'BLen' type to 'CBLen'.
 data Size (n :: Natural)
+
+instance Predicate (Size n) where
+    type PredicateName d (Size n) = ShowParen (d > 9)
+        ("Size " ++ ShowNatDec n)
+
 type Sized n = Refined (Size n)
 
-instance (BLen a, KnownNat n) => Predicate (Size n) a where
-    validate p a
-     | len /= n
-        = throwRefineOtherException (typeRep p) $
-            "not correctly sized: "<>tshow len<>" /= "<>tshow n
-     | otherwise = success
+instance (KnownPredicateName (Size n), BLen a, KnownNat n)
+  => Refine (Size n) a where
+    validate p a = validateBool p (len == n) $
+        "not correctly sized: "<>TBL.fromDec len<>" /= "<>TBL.fromDec n
       where
         n = natValInt @n
         len = blen a
@@ -42,6 +46,6 @@
 instance (Get a, KnownNat n) => Get (Sized n a) where
     get = do
         a <- FP.isolate (natValInt @n) get
-        pure $ reallyUnsafeRefine a
+        pure $ unsafeRefine a
         -- ^ REFINE SAFETY: 'FP.isolate' consumes precisely the number of bytes
         -- requested when it succeeds
diff --git a/src/Binrep/Type/Text.hs b/src/Binrep/Type/Text.hs
--- a/src/Binrep/Type/Text.hs
+++ b/src/Binrep/Type/Text.hs
@@ -22,7 +22,7 @@
 
 import Binrep.Type.Text.Internal
 
-import Refined
+import Rerefined
 
 import Binrep.Type.Text.Encoding.Utf8
 import Binrep.Type.Text.Encoding.Ascii
@@ -47,7 +47,7 @@
 -- bs :: Refined 'C Bytes
 encodeToRep
     :: forall rep enc
-    .  (Encode enc, Predicate rep Bytes)
+    .  (Encode enc, Refine rep Bytes)
     => AsText enc
-    -> Either RefineException (Refined rep Bytes)
+    -> Either RefineFailure (Refined rep Bytes)
 encodeToRep = refine . encode
diff --git a/src/Binrep/Type/Text/Encoding/Ascii.hs b/src/Binrep/Type/Text/Encoding/Ascii.hs
--- a/src/Binrep/Type/Text/Encoding/Ascii.hs
+++ b/src/Binrep/Type/Text/Encoding/Ascii.hs
@@ -1,4 +1,3 @@
-{-# LANGUAGE CPP #-}
 {-# LANGUAGE OverloadedStrings #-}
 
 module Binrep.Type.Text.Encoding.Ascii where
@@ -6,42 +5,27 @@
 import Binrep.Type.Text.Internal
 import Binrep.Type.Text.Encoding.Utf8
 
-import Refined
-import Data.Typeable ( typeRep )
+import Rerefined.Predicate.Common
+import Rerefined.Refine ( unsafeRefine )
 
-import Data.Char qualified as Char
 import Data.Text qualified as Text
 import Data.Text ( Text )
 
 import Data.Text.Encoding qualified as Text
-import Control.Exception qualified
-import System.IO.Unsafe qualified
 
 -- | 7-bit
 data Ascii
+instance Predicate Ascii where type PredicateName d Ascii = "ASCII"
 
+-- | 'Text' must be validated if you want to permit 7-bit ASCII only.
+instance Refine Ascii Text where
+    validate p t = validateBool p (Text.isAscii t) "not valid 7-bit ASCII"
+
 -- | We reuse UTF-8 encoding for ASCII, since it is a subset of UTF-8.
 instance Encode Ascii where encode' = encode' @Utf8
 
--- Pre-@text-2.0@, @decodeASCII@ generated a warning and ran @decodeUtf8@.
--- TODO can I give some compile time warning about this instance missing on
--- below text-2.0?? would be cool
-#if MIN_VERSION_text(2,0,0)
--- TODO 2023-01-26 raehik: awful UX by text. hopefully safe lol?? works at least
-instance Decode Ascii where decode = decodeText id $ catchErrorCall Text.decodeASCII
-#endif
-
-catchErrorCall :: (a -> b) -> a -> Either String b
-catchErrorCall f a = System.IO.Unsafe.unsafeDupablePerformIO $ do
-    Control.Exception.try @Control.Exception.ErrorCall (Control.Exception.evaluate (f a)) >>= \case
-      Right b -> pure $ Right b
-      Left  (Control.Exception.ErrorCallWithLocation msg _) -> pure $ Left msg
-
--- | 'Text' must be validated if you want to permit 7-bit ASCII only.
---
--- TODO there should be a MUCH faster check here in text-2.0. text-short has it,
--- text doesn't yet. see: https://github.com/haskell/text/issues/496
-instance Predicate Ascii Text where
-    validate p t = if   Text.all Char.isAscii t
-                   then success
-                   else throwRefineOtherException (typeRep p) "not valid 7-bit ASCII"
+instance Decode Ascii where
+    decode bs =
+        case Text.decodeASCII' bs of
+          Just t  -> Right $ unsafeRefine t
+          Nothing -> Left  "not valid 7-bit ASCII"
diff --git a/src/Binrep/Type/Text/Encoding/ShiftJis.hs b/src/Binrep/Type/Text/Encoding/ShiftJis.hs
--- a/src/Binrep/Type/Text/Encoding/ShiftJis.hs
+++ b/src/Binrep/Type/Text/Encoding/ShiftJis.hs
@@ -2,7 +2,7 @@
 
 module Binrep.Type.Text.Encoding.ShiftJis where
 
-import Refined
+import Rerefined.Predicate
 
 import Data.Text ( Text )
 
@@ -15,9 +15,10 @@
 #endif
 
 data ShiftJis
+instance Predicate ShiftJis where type PredicateName d ShiftJis = "Shift-JIS"
 
 -- | TODO Unsafely assume all 'Text's are valid Shift-JIS.
-instance Predicate ShiftJis Text where validate _ _ = success
+instance Refine ShiftJis Text where validate _ _ = Nothing
 
 #ifdef HAVE_ICU
 instance Encode ShiftJis where encode' = encodeViaTextICU' "Shift-JIS"
diff --git a/src/Binrep/Type/Text/Encoding/Utf16.hs b/src/Binrep/Type/Text/Encoding/Utf16.hs
--- a/src/Binrep/Type/Text/Encoding/Utf16.hs
+++ b/src/Binrep/Type/Text/Encoding/Utf16.hs
@@ -1,15 +1,19 @@
+{-# LANGUAGE UndecidableInstances #-} -- for PredicateName
+
 module Binrep.Type.Text.Encoding.Utf16 where
 
 import Binrep.Type.Text.Internal
 import Binrep.Util.ByteOrder
 
-import Refined
-import Data.Typeable ( Typeable )
+import Rerefined.Predicate
+import TypeLevelShow.Utils
 
 import Data.Text.Encoding qualified as Text
 import Data.Text ( Text )
 
 data Utf16 (end :: ByteOrder)
+instance Predicate (Utf16 end) where
+    type PredicateName d (Utf16 end) = "UTF-16" ++ EndianSuffix end
 
 instance Encode (Utf16 BE) where encode' = Text.encodeUtf16BE
 instance Encode (Utf16 LE) where encode' = Text.encodeUtf16LE
@@ -18,4 +22,4 @@
 instance Decode (Utf16 LE) where decode = decodeText show $ wrapUnsafeDecoder Text.decodeUtf16LE
 
 -- | Any 'Text' value is always valid UTF-16.
-instance Typeable end => Predicate (Utf16 end) Text where validate _ _ = success
+instance Refine (Utf16 end) Text where validate _ _ = Nothing
diff --git a/src/Binrep/Type/Text/Encoding/Utf32.hs b/src/Binrep/Type/Text/Encoding/Utf32.hs
--- a/src/Binrep/Type/Text/Encoding/Utf32.hs
+++ b/src/Binrep/Type/Text/Encoding/Utf32.hs
@@ -1,15 +1,19 @@
+{-# LANGUAGE UndecidableInstances #-} -- for PredicateName
+
 module Binrep.Type.Text.Encoding.Utf32 where
 
 import Binrep.Type.Text.Internal
 import Binrep.Util.ByteOrder
 
-import Refined
-import Data.Typeable ( Typeable )
+import Rerefined.Predicate
+import TypeLevelShow.Utils
 
 import Data.Text.Encoding qualified as Text
 import Data.Text ( Text )
 
 data Utf32 (end :: ByteOrder)
+instance Predicate (Utf32 end) where
+    type PredicateName d (Utf32 end) = "UTF-32" ++ EndianSuffix end
 
 instance Encode (Utf32 BE) where encode' = Text.encodeUtf32BE
 instance Encode (Utf32 LE) where encode' = Text.encodeUtf32LE
@@ -18,4 +22,4 @@
 instance Decode (Utf32 LE) where decode = decodeText show $ wrapUnsafeDecoder Text.decodeUtf32LE
 
 -- | Any 'Text' value is always valid UTF-32.
-instance Typeable end => Predicate (Utf32 end) Text where validate _ _ = success
+instance Refine (Utf32 end) Text where validate _ _ = Nothing
diff --git a/src/Binrep/Type/Text/Encoding/Utf8.hs b/src/Binrep/Type/Text/Encoding/Utf8.hs
--- a/src/Binrep/Type/Text/Encoding/Utf8.hs
+++ b/src/Binrep/Type/Text/Encoding/Utf8.hs
@@ -2,15 +2,16 @@
 
 import Binrep.Type.Text.Internal
 
-import Refined
+import Rerefined.Predicate
 
 import Data.Text.Encoding qualified as Text
 import Data.Text ( Text )
 
 data Utf8
+instance Predicate Utf8 where type PredicateName d Utf8 = "UTF-8"
 
 instance Encode Utf8 where encode' = Text.encodeUtf8
 instance Decode Utf8 where decode  = decodeText show Text.decodeUtf8'
 
 -- | Any 'Text' value is always valid UTF-8.
-instance Predicate Utf8 Text where validate _ _ = success
+instance Refine Utf8 Text where validate _ _ = Nothing
diff --git a/src/Binrep/Type/Text/Internal.hs b/src/Binrep/Type/Text/Internal.hs
--- a/src/Binrep/Type/Text/Internal.hs
+++ b/src/Binrep/Type/Text/Internal.hs
@@ -4,8 +4,7 @@
 
 import Data.Text ( Text )
 import Data.ByteString qualified as B
-import Refined
-import Refined.Unsafe ( reallyUnsafeRefine )
+import Rerefined.Refine
 
 import System.IO.Unsafe qualified
 import Control.Exception qualified
@@ -40,7 +39,7 @@
     :: forall enc e
     .  (e -> String) -> (Bytes -> Either e Text) -> Bytes
     -> Either String (AsText enc)
-decodeText g f = bimap g reallyUnsafeRefine . f
+decodeText g f = bimap g unsafeRefine . f
 
 -- | Run an unsafe decoder safely.
 --
diff --git a/src/Binrep/Util.hs b/src/Binrep/Util.hs
deleted file mode 100644
--- a/src/Binrep/Util.hs
+++ /dev/null
@@ -1,31 +0,0 @@
-{-# LANGUAGE AllowAmbiguousTypes #-}
-
-module Binrep.Util where
-
--- tshow
-import Data.Text qualified as Text
-import Data.Text ( Text )
-
--- posIntToNat
-import GHC.Exts ( Int(..), int2Word# )
-import GHC.Num.Natural ( Natural(..) )
-
--- natVal''
-import GHC.TypeNats ( KnownNat, natVal' )
-import GHC.Exts ( proxy#, Proxy# )
-
-tshow :: Show a => a -> Text
-tshow = Text.pack . show
-
--- | Convert some 'Int' @i@ where @i >= 0@ to a 'Natural'.
---
--- This is intended for wrapping the output of 'length' functions.
---
--- underflows if you call it with a negative 'Int' :)
-posIntToNat :: Int -> Natural
-posIntToNat (I# i#) = NS (int2Word# i#)
-{-# INLINE posIntToNat #-}
-
-natVal'' :: forall a. KnownNat a => Natural
-natVal'' = natVal' (proxy# :: Proxy# a)
-{-# INLINE natVal'' #-}
diff --git a/src/Binrep/Util/ByteOrder.hs b/src/Binrep/Util/ByteOrder.hs
--- a/src/Binrep/Util/ByteOrder.hs
+++ b/src/Binrep/Util/ByteOrder.hs
@@ -1,14 +1,15 @@
 {-# OPTIONS_GHC -fno-warn-orphans #-}
 
 module Binrep.Util.ByteOrder
-  ( ByteOrder(..), ByteOrdered(..)
+  ( ByteOrder(..), ByteOrdered(..), type EndianSuffix
   , type LE, type BE, type Endian
   ) where
 
 import Raehik.Compat.Data.Primitive.Types.Endian ( ByteOrdered(..) )
 import GHC.ByteOrder ( ByteOrder(..) )
 import Strongweak
-import Data.Kind ( Type )
+import Data.Kind ( type Type )
+import GHC.TypeLits ( type Symbol )
 
 deriving via (a :: Type) instance     Weaken a =>     Weaken (ByteOrdered end a)
 deriving via (a :: Type) instance Strengthen a => Strengthen (ByteOrdered end a)
@@ -17,3 +18,7 @@
 type LE = 'LittleEndian
 type BE =    'BigEndian
 type Endian = ByteOrdered
+
+type family EndianSuffix (end :: ByteOrder) :: Symbol where
+    EndianSuffix 'LittleEndian = "LE"
+    EndianSuffix    'BigEndian = "BE"
diff --git a/src/Binrep/Util/Prefix.hs b/src/Binrep/Util/Prefix.hs
deleted file mode 100644
--- a/src/Binrep/Util/Prefix.hs
+++ /dev/null
@@ -1,62 +0,0 @@
-{-# LANGUAGE UndecidableInstances #-} -- for convenient type level arithmetic
-
-module Binrep.Util.Prefix where
-
-import Binrep.Util.ByteOrder ( ByteOrdered(ByteOrdered) )
-import GHC.TypeNats
-import Data.Word
-
-import Data.Kind
-
--- | Types which may be used as prefixes.
---
--- Generally, these will be integer types.
---
--- Note that this is separate to binary representation, so endianness is
--- irrelevant.
---
--- Note that we are also limited by the host architecture's 'Int' type.
--- We don't try to work around this, because most types are indexed with 'Int's,
--- so I think other things will break before we do.
-class Prefix a where
-    type Max a :: Natural
-
-    -- | used by put. guaranteed that it fits from refined. that is, lenToPfx <=
-    --   Max.
-    lenToPfx :: Int -> a
-
-    -- | used by get. better not lie.
-    pfxToLen :: a -> Int
-
--- | Length prefixing with the unit means a length of 0.
---
--- This is the only sensible case. 1 doesn't work because refining checks @<=@.
---
--- I think there are laws here, where using this is the same as doing nothing at
--- all.
-instance Prefix () where
-    type Max () = 0
-    lenToPfx = \case
-      0 -> ()
-      _ -> error "you lied to refine and broke everything :("
-    pfxToLen () = 0
-
--- | Byte ordering doesn't change how prefixes work.
-deriving via (a :: Type) instance Prefix a => Prefix (ByteOrdered end a)
-
-instance Prefix Word8  where
-    type Max Word8  = 2^8  - 1
-    lenToPfx = fromIntegral
-    pfxToLen = fromIntegral
-instance Prefix Word16 where
-    type Max Word16 = 2^16 - 1
-    lenToPfx = fromIntegral
-    pfxToLen = fromIntegral
-instance Prefix Word32 where
-    type Max Word32 = 2^32 - 1
-    lenToPfx = fromIntegral
-    pfxToLen = fromIntegral
-instance Prefix Word64 where
-    type Max Word64 = 2^64 - 1
-    lenToPfx = fromIntegral
-    pfxToLen = fromIntegral
diff --git a/src/Raehik/Compat/FlatParse/Basic/CutWithPos.hs b/src/Raehik/Compat/FlatParse/Basic/CutWithPos.hs
new file mode 100644
--- /dev/null
+++ b/src/Raehik/Compat/FlatParse/Basic/CutWithPos.hs
@@ -0,0 +1,15 @@
+module Raehik.Compat.FlatParse.Basic.CutWithPos where
+
+import FlatParse.Basic ( ParserT, Pos, getPos, cut, err )
+
+-- | Convert a parsing failure to an error, which also receives the parser
+--   position (as a 'Pos', from the end of input).
+cut' :: ParserT st e a -> (Pos -> e) -> ParserT st e a
+cut' p e = getPos >>= \pos -> cut p (e pos)
+{-# inline cut' #-}
+
+-- | Throw a parsing error, which also receives the parser position (as a 'Pos',
+--   from the end of input).
+err' :: (Pos -> e) -> ParserT st e a
+err' e = getPos >>= \pos -> err (e pos)
+{-# inline err' #-}
diff --git a/src/Util/TypeNats.hs b/src/Util/TypeNats.hs
--- a/src/Util/TypeNats.hs
+++ b/src/Util/TypeNats.hs
@@ -15,3 +15,7 @@
 natValInt :: forall n. KnownNat n => Int
 natValInt = fromIntegral $ natVal'' @n
 {-# INLINE natValInt #-}
+
+natValWord :: forall n. KnownNat n => Word
+natValWord = fromIntegral $ natVal'' @n
+{-# INLINE natValWord #-}
diff --git a/test/Binrep/GenericSpec.hs b/test/Binrep/GenericSpec.hs
new file mode 100644
--- /dev/null
+++ b/test/Binrep/GenericSpec.hs
@@ -0,0 +1,39 @@
+{-# LANGUAGE OverloadedStrings #-}
+
+module Binrep.GenericSpec where
+
+import Test.Hspec
+
+spec :: Spec
+spec = pure ()
+    {-
+spec = do
+    prop "parse-print roundtrip isomorphism (generic, sum tag via nullterm constructor)" $ do
+      \(d :: D) -> runGet (runPut d) `shouldBe` Right (d, "")
+
+--------------------------------------------------------------------------------
+
+type W1   = Word8
+type W2LE = ByteOrdered LE Word16
+type W8BE = ByteOrdered BE Word64
+
+data D
+  = D01Bla     Word8 W1 W8BE
+  | D23        W2LE  B.ByteString -- dangerous bytestring, must be last
+  | DUnicode例 Word8
+  | DSymbols_#
+    deriving stock (Generic, Eq, Show)
+deriving via (GenericArbitraryU `AndShrinking` D) instance Arbitrary D
+
+instance BLen D where blen = blenGenericSum $ blen . nullTermCstrPfxTag
+instance Put  D where put  = putGenericSum  $ put . nullTermCstrPfxTag
+instance Get  D where get  = getGenericSum  $ eqShowPfxTagCfg nullTermCstrPfxTag
+
+data DNoSum = DNoSum Word8 W1 W2LE W8BE
+    deriving stock (Generic, Eq, Show)
+deriving via (GenericArbitraryU `AndShrinking` DNoSum) instance Arbitrary DNoSum
+
+instance BLen DNoSum where blen = blenGenericNonSum
+instance Put  DNoSum where put  = putGenericNonSum
+instance Get  DNoSum where get  = getGenericNonSum
+    -}
diff --git a/test/Binrep/LawsSpec.hs b/test/Binrep/LawsSpec.hs
deleted file mode 100644
--- a/test/Binrep/LawsSpec.hs
+++ /dev/null
@@ -1,54 +0,0 @@
-{-# LANGUAGE OverloadedStrings #-}
-
-module Binrep.LawsSpec where
-
-import Test.Hspec
-import Test.Hspec.QuickCheck
-import Test.QuickCheck.Instances.ByteString()
-import Generic.Random
-import Test.QuickCheck
-import ArbitraryOrphans()
-
-import Binrep
-import Binrep.Generic ( nullTermCstrPfxTag )
-import Binrep.Util.ByteOrder
-import Data.Word
-import Data.ByteString qualified as B
-import GHC.Generics ( Generic )
-
-import Generic.Data.Function.Traverse
-
-spec :: Spec
-spec = do
-    prop "put is identity on ByteString" $ do
-      \(bs :: B.ByteString) -> runPut bs  `shouldBe` bs
-    prop "parse-print roundtrip isomorphism (ByteString)" $ do
-      \(bs :: B.ByteString) -> runGet (runPut bs) `shouldBe` Right (bs, "")
-    prop "parse-print roundtrip isomorphism (generic, sum tag via nullterm constructor)" $ do
-      \(d :: D) -> runGet (runPut d) `shouldBe` Right (d, "")
-
---------------------------------------------------------------------------------
-
-type W1   = Word8
-type W2LE = ByteOrdered LE Word16
-type W8BE = ByteOrdered BE Word64
-
-data D
-  = D01Bla     Word8 W1 W8BE
-  | D23        W2LE  B.ByteString -- dangerous bytestring, must be last
-  | DUnicode例 Word8
-  | DSymbols_#
-    deriving stock (Generic, Eq, Show)
-deriving via (GenericArbitraryU `AndShrinking` D) instance Arbitrary D
-
-instance BLen D where blen = blenGenericSum $ blen . nullTermCstrPfxTag
-instance Put  D where put  = putGenericSum  $ put . nullTermCstrPfxTag
-instance Get  D where get  = getGenericSum  $ eqShowPfxTagCfg nullTermCstrPfxTag
-
-data DNoSum = DNoSum Word8 W1 W2LE W8BE
-    deriving stock (Generic, Eq, Show)
-deriving via (GenericArbitraryU `AndShrinking` DNoSum) instance Arbitrary DNoSum
-
-instance BLen DNoSum where blen = blenGenericNonSum
-instance Put  DNoSum where put  = putGenericNonSum
-instance Get  DNoSum where get  = getGenericNonSum
diff --git a/test/Binrep/TypesSpec.hs b/test/Binrep/TypesSpec.hs
new file mode 100644
--- /dev/null
+++ b/test/Binrep/TypesSpec.hs
@@ -0,0 +1,19 @@
+{-# LANGUAGE OverloadedStrings #-}
+
+module Binrep.TypesSpec where
+
+import Test.Hspec
+import Test.Hspec.QuickCheck
+import Test.QuickCheck.Instances.ByteString()
+
+import Binrep
+import Data.ByteString qualified as B
+
+spec :: Spec
+spec = do
+    prop "put is identity on ByteString" $ do
+      \(bs :: B.ByteString) -> runPut bs  `shouldBe` bs
+    prop "parse-print roundtrip isomorphism (ByteString)" $ do
+      \(bs :: B.ByteString) ->
+        runGet (runPut bs) `shouldSatisfy`
+          (\case Right (bs', "") -> bs == bs'; _ -> False)