diff --git a/CHANGELOG.md b/CHANGELOG.md
--- a/CHANGELOG.md
+++ b/CHANGELOG.md
@@ -1,3 +1,14 @@
+## 2.0.0 (2025-10-11)
+Full rewrite.
+
+* parsers are now much more general: mutually-recursive parsers are game
+  * added an example parser for a simple expression AST
+* added parsers matching `Functor`, `Applicative`, `Monad` type class methods
+* temporarily removed singling (will be lots of work)
+
+Simple parsers written with the provided combinators should still function the
+same, or with minimal changes.
+
 ## 1.1.1 (2024-06-15)
 * add `Apply` combinator (effectively `fmap`)
 * add some more runners and utils (handy for generic-data-functions)
diff --git a/LICENSE b/LICENSE
--- a/LICENSE
+++ b/LICENSE
@@ -1,4 +1,4 @@
-Copyright (c) 2024 Ben Orchard (@raehik) <thefirstmuffinman@gmail.com>
+Copyright (c) 2024-2025 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
@@ -1,15 +1,14 @@
 # Symparsec
 [hackage-parsec]: https://hackage.haskell.org/package/parsec
 
-Type level string (`Symbol`) parser combinators. A [Parsec][hackage-parsec]-like
-for `Symbol`s; thus, Symparsec! With many of the features you'd expect:
+Type level string parser combinators. A [Parsec][hackage-parsec]-like for
+`Symbol`s; thus, Symparsec! With many of the features you'd expect:
 
 * define parsers compositionally, largely as you would on the term level
+* define complex parsers, including mutually recursive ones (e.g. expression
+  parsers!)
 * pretty, detailed parse errors
-* decent performance (for simple parsers)
-
-Parsers may also be reified and used at runtime with _guaranteed identical
-behaviour_ via a healthy dose of singletons.
+* good performance (probably? please help me benchmark!)
 
 Requires GHC >= 9.6.
 
@@ -18,24 +17,19 @@
 
 ```haskell
 import Symparsec
-type PExample = Skip 1 :*>: Isolate 2 NatHex :<*>: (Literal "_" :*>: TakeRest)
+import DeFun.Core
+type PExample = Skip 1 *> Tuple (Isolate 2 NatHex) (Literal "_" *> TakeRest)
 ```
 
 Use it to parse a type-level string (in a GHCi session):
 
 ```haskell
-ghci> :k! Run PExample "xFF_"
+ghci> :k! Run PExample "xFF_etc"
 Run ...
 = Right '( '(255, "etc"), "")
 ```
 
-Use it to parse a different, term-level string:
-
-```haskell
-ghci> import Singleraeh.Demote ( demote )
-ghci> run' @PExample demote "abc_123"
-Right ((188,"123"),"")
-```
+See the `Symparsec.Example` namespace for further examples.
 
 ## Why?
 Via `GHC.Generics`, we may inspect Haskell data types on the type level.
@@ -45,28 +39,22 @@
 
 Also type-level Haskell authors deserve fun libraries too!!
 
-## Design
-### The parser
-A parser is a 3-tuple of:
-
-* a character parser; given a character and a state, returns
-  * `Cont s`: keep going, here's the next state `s`
-  * `Done r`: parse successful with value `r`, _do not consume character_
-  * `Err  E`: parse error, details in the `E` (a structured error)
-* an end handler, which takes only a state, and can only return `Done` or `Err`
-* an initial state
-
-Running such a parser is very simple:
+## Limitations
+Symparsec defines a lot of low-level parsers you would expect on the term level,
+even monadic (bind) and applicative (ap) parser combinators. The key limitation
+Symparsec grapples with is Haskell having _no type-level binders_. This means:
 
-* initialize state
-* parse character by character until end of input, or `Done`/`Err`
+* no `let`s, no `where`s
+* no `do` notation
 
-Parsers may not communicate with the runner any other way. This means no
-backtracking, chunking etc. This is a conscious decision, made for simplicity.
-We're still able to implement a good handful of parser combinators regardless,
-including a limited form of backtracking.
+The workaround is writing extra functions, and writing uglier functions.
+Otherwise, I believe an average term-level Parsec-like parser should look
+comparable to a type-level `Symparsec` one.
 
-This is a rough overview. See the code & Haddocks for precise details.
+Writing complex type-level Haskell programs in 2025 is unintuitive. I intend to
+provide guides on writing Symparsec parsers that walk through type-level
+programming design patterns and solutions. Please ping me on the issues tab if
+you read this, and can't find any such guides!
 
 ## Contributing
 I would gladly accept further combinators or other suggestions. Please add an
diff --git a/src/Data/Type/Symbol.hs b/src/Data/Type/Symbol.hs
new file mode 100644
--- /dev/null
+++ b/src/Data/Type/Symbol.hs
@@ -0,0 +1,60 @@
+{-# LANGUAGE UndecidableInstances #-}
+
+-- TODO move this to singleraeh!
+
+-- | Type families on 'Symbol's.
+module Data.Type.Symbol
+  ( type Length
+  , type Take, type TakeNoTailRec
+  , type Drop
+  , type Replicate
+  ) where
+
+import GHC.TypeLits ( type Symbol, type UnconsSymbol, type ConsSymbol )
+import GHC.TypeNats ( type Natural, type (+), type (-) )
+import Singleraeh.Symbol ( type RevCharsToSymbol )
+
+-- | Calculate the length of a 'Symbol'.
+type Length  ::            Symbol               -> Natural
+type Length' :: Natural -> Maybe (Char, Symbol) -> Natural
+type Length str = Length' 0 (UnconsSymbol str)
+type family Length' len mstr where
+    Length' len Nothing            = len
+    Length' len (Just '(_ch, str)) = Length' (len+1) (UnconsSymbol str)
+
+-- | Take the prefix of the given 'Symbol' of the given length.
+--
+-- Returns less than requested if the 'Symbol' is too short.
+type Take :: Natural -> Symbol -> Symbol
+type Take n str = TakeLoop '[] n (UnconsSymbol str)
+type family TakeLoop chs n mstr where
+    TakeLoop chs 0 _                 = RevCharsToSymbol chs
+    TakeLoop chs n (Just '(ch, str)) = TakeLoop (ch:chs) (n-1) (UnconsSymbol str)
+    TakeLoop chs n Nothing           = RevCharsToSymbol chs
+
+-- | Take the prefix of the given 'Symbol' of the given length.
+--
+-- Returns less than requested if the 'Symbol' is too short.
+--
+-- Does not do tail-call recursion, but avoids doing extra work.
+-- Unsure which is better.
+type TakeNoTailRec :: Natural -> Symbol -> Symbol
+type TakeNoTailRec n str = TakeNoTailRec' n (UnconsSymbol str)
+type family TakeNoTailRec' n mstr where
+  TakeNoTailRec' 0 _                 = ""
+  TakeNoTailRec' n (Just '(ch, str)) = ConsSymbol ch (TakeNoTailRec' (n-1) (UnconsSymbol str))
+  TakeNoTailRec' _ Nothing           = ""
+
+-- | Drop the prefix of the given 'Symbol' of the given length.
+type Drop :: Natural -> Symbol -> Symbol
+type Drop n str = Drop' n (UnconsSymbol str)
+type family Drop' n mstr where
+    Drop' 0 (Just '(ch, str)) = ConsSymbol ch str
+    Drop' n (Just '(ch, str)) = Drop' (n-1) (UnconsSymbol str)
+    Drop' _ Nothing           = ""
+
+type Replicate :: Natural -> Char -> Symbol
+type Replicate n ch = ReplicateLoop ch '[] n
+type family ReplicateLoop ch chs n where
+    ReplicateLoop ch chs 0 = RevCharsToSymbol chs
+    ReplicateLoop ch chs n = ReplicateLoop ch (ch:chs) (n-1)
diff --git a/src/Symparsec.hs b/src/Symparsec.hs
--- a/src/Symparsec.hs
+++ b/src/Symparsec.hs
@@ -1,7 +1,19 @@
+{- | Top-level Symparsec module, exporting builtin parsers and runners.
+
+I suggest importing this module qualified. Or, consider the following imports:
+
+@
+import "Symparsec.Run" qualified as Symparsec
+import "Symparsec.Parsers" qualified as P
+-- > :k! Symparsec.Run (P.Take 1) "hello"
+@
+-}
+
 module Symparsec
   (
   -- * Base definitions
-    Run, run'
+    type Run
+  , type RunTest
 
   -- * Parsers
   , module Symparsec.Parsers
diff --git a/src/Symparsec/Example/Expr.hs b/src/Symparsec/Example/Expr.hs
--- a/src/Symparsec/Example/Expr.hs
+++ b/src/Symparsec/Example/Expr.hs
@@ -1,50 +1,188 @@
-{-# LANGUAGE UndecidableInstances#-}
+{-# LANGUAGE UndecidableInstances #-}
 
-{- | Experiments.
+-- | An example Symparsec parser for a basic expression tree.
 
-Turns out we can't write recursive parsers. But 'P.Apply' can help us write
-handier parsers.
+module Symparsec.Example.Expr where
+
+import Symparsec.Parser.Common
+import Symparsec.Utils ( type IfNatLte )
+import Symparsec.Parser.Natural
+import Symparsec.Parser.Natural.Digits
+import Symparsec.Parser.While ( type While )
+import Symparsec.Parser.While.Predicates ( type IsDecDigitSym )
+import GHC.TypeNats qualified as TypeNats
+
+{- TODO
+* empty paren pairs are permitted in many cases e.g. @()1() -> ELit 1@
+  * probably I should assert that >=1 thing gets parsed inside parens
+  * well, I solved it. but I think in the wrong way. surely I should not be
+    parsing parens in certain places. like I can't parse parens immediately
+    after a number. or if I do, I need to implicitly parse a Mult.
 -}
 
-module Symparsec.Example.Expr where
+-- | A basic expression tree, polymorphic over a single literal type.
+data Expr a
+  = EBOp BOp (Expr a) (Expr a)
+  | ELit a
 
-import Numeric.Natural
-import Symparsec.Parsers qualified as P
-import Symparsec.Parser.While.Predicates qualified as P
-import Symparsec.Parser.Apply qualified as P
-import DeFun.Core
-import DeFun.Function
+-- | A binary operator.
+data BOp = Add | Sub | Mul | Div
 
-data Expr
-  = ELit Lit
-  | EBOp Expr BOp Expr
+-- | Evaluate an 'Expr' of 'Natural's on the type level.
+--
+-- Naive, doesn't attempt to tail-call recurse.
+type Eval :: Expr Natural -> Natural
+type family Eval expr where
+    Eval (EBOp bop l r) = EvalBOp bop (Eval l) (Eval r)
+    Eval (ELit n) = n
 
-data BOp = Plus
+type EvalBOp :: BOp -> Natural -> Natural -> Natural
+type family EvalBOp bop l r where
+    EvalBOp Add l r = l + r
+    EvalBOp Sub l r = l - r
+    EvalBOp Mul l r = l * r
+    EvalBOp Div l r = l `TypeNats.Div` r
 
-data Lit
-  = LNat Natural
+data ExprTok
+  = TokBOp BOp
+  | TokParenL
+  | TokParenR
 
-type PLit  = PLNat
-type PLNat = Con1 LNat P.:<$>: P.While P.IsHexDigitSym P.NatHex
-type PELit = Con1 ELit P.:<$>: PLit
-type PEBOp = Curry3Sym (Con3 EBOp) P.:<$>: (PExpr P.:<*>: PBOp P.:<*>: PExpr)
-type PExpr = PELit
---type PExpr :: PParser (P.OrS (Maybe Natural) (Maybe Natural)) Expr
---type PExpr = FromEitherSym P.:<$>: (PELit P.:<|>: PEBOp)
-type PBOp  = ConstSym1 Plus P.:<$>: P.Literal "+"
+type PExpr :: PParser (Expr Natural)
+data PExpr s
+type instance App PExpr s = PExprNext s '[] '[] (UnconsState s)
+type PExprNext
+    :: PState
+    -> [ExprTok]
+    -> [Expr Natural]
+    -> (Maybe Char, PState)
+    -> PReply (Expr Natural)
+type family PExprNext sPrev ops exprs s where
+    PExprNext sPrev ops exprs '(Just ch, s) =
+        PExprCh sPrev s ops exprs ch
+    PExprNext sPrev ops exprs '(Nothing, s) = PExprEnd sPrev s ops exprs
 
-type Curry3Sym
-    :: (a ~> b ~> c ~> r)
-    -> ((a, b), c)
-    ~> r
-data Curry3Sym f abc
-type instance App (Curry3Sym f) '( '(a, b), c) = f @@ a @@ b @@ c
+type family PExprEnd sPrev s ops exprs where
+    PExprEnd sPrev s (TokBOp op:ops) exprs      = PExprEndPopOp sPrev s ops exprs op
+    -- TODO what about parens
+    PExprEnd sPrev s '[]      (expr:'[]) = 'Reply (OK expr) s
+    PExprEnd sPrev s '[]      _          =
+        'Reply (Err (Error1 "badly formed expression")) sPrev
 
-type FromEither :: Either a a -> a
-type family FromEither eaa where
-    FromEither (Right a) = a
-    FromEither (Left  a) = a
+type family PExprEndPopOp sPrev s ops exprs op where
+    PExprEndPopOp sPrev s ops (r:l:exprs) bop =
+        PExprEnd sPrev s ops (EBOp bop l r : exprs)
+    PExprEndPopOp sPrev s ops exprs bop =
+        'Reply (Err (Error1 "badly formed expression")) sPrev
 
-type FromEitherSym :: Either a a ~> a
-data FromEitherSym eaa
-type instance App FromEitherSym eaa = FromEither eaa
+type family PExprCh sPrev s ops exprs ch where
+    PExprCh sPrev s ops exprs ' ' = PExprNext s ops exprs (UnconsState s)
+    PExprCh sPrev s ops exprs ch  = PExprELit sPrev s ops exprs ch (ParseDigitDecSym @@ ch)
+
+type family PExprELit sPrev s ops exprs ch mDigit where
+    PExprELit sPrev s ops exprs _ch (Just digit) =
+        PExprELitEnd ops exprs
+            (While IsDecDigitSym (NatBase1 10 ParseDigitDecSym digit) @@ s)
+    PExprELit sPrev s ops exprs  ch Nothing      =
+        PExprEBOp sPrev s ops exprs ch (PExprEBOpOpCh ch)
+
+type family PExprELitEnd ops exprs res where
+    PExprELitEnd ops exprs ('Reply (OK  n) s) =
+        PExprNext s ops (ELit n : exprs) (UnconsState s)
+    PExprELitEnd ops exprs ('Reply (Err e) s) =
+        -- The digit parser we're wrapping shouldn't ever fail, due to how
+        -- 'While' works, and that we've already handled the 0-length case.
+        Impossible
+
+type family PExprEBOp sPrev s ops exprs ch mbop where
+    PExprEBOp sPrev s ops exprs ch (Just (TokBOp bop)) =
+        PExprEBOp' sPrev s bop (BOpPrec bop) exprs ops
+    PExprEBOp sPrev s ops exprs ch (Just TokParenL) =
+        PExprNext sPrev (TokParenL:ops) exprs (UnconsState s)
+    PExprEBOp sPrev s ops exprs ch (Just TokParenR) =
+        PExprParenRStart sPrev s exprs ops
+    PExprEBOp sPrev s ops exprs ch Nothing =
+        'Reply (Err (Error1 "bad expression, expected digit or operator")) sPrev
+
+type family PExprParenRStart sPrev s exprs ops where
+    PExprParenRStart sPrev s exprs (TokParenL : ops) =
+        'Reply (Err (Error1 "invalid bracket syntax (empty brackets, or otherwise bad)")) sPrev
+    PExprParenRStart sPrev s exprs ops =
+        PExprParenR sPrev s exprs ops
+
+type family PExprParenR sPrev s exprs ops where
+    PExprParenR sPrev s exprs (TokBOp bop : ops) =
+        PExprParenRPopBOp sPrev s bop ops exprs
+    PExprParenR sPrev s exprs (TokParenL : ops) =
+        PExprNext sPrev ops exprs (UnconsState s)
+    PExprParenR sPrev s exprs ops =
+        'Reply (Err (Error1 "badly formed expression")) sPrev
+
+type family PExprParenRPopBOp sPrev s bop ops exprs where
+    PExprParenRPopBOp sPrev s bop ops (r:l:exprs) =
+        PExprParenR sPrev s (EBOp bop l r : exprs) ops
+    PExprParenRPopBOp sPrev s bop ops      exprs  =
+        'Reply (Err (Error1 "badly formed expression")) sPrev
+
+type family PExprEBOpOpCh ch where
+    PExprEBOpOpCh '+' = Just (TokBOp Add)
+    PExprEBOpOpCh '-' = Just (TokBOp Sub)
+    PExprEBOpOpCh '*' = Just (TokBOp Mul)
+    PExprEBOpOpCh '/' = Just (TokBOp Div)
+    PExprEBOpOpCh '(' = Just TokParenL
+    PExprEBOpOpCh ')' = Just TokParenR
+    PExprEBOpOpCh _   = Nothing
+
+type PExprEBOp'
+    :: PState -> PState -> BOp -> Natural -> [Expr Natural] -> [ExprTok]
+    -> PReply (Expr Natural)
+type family PExprEBOp' sPrev s op prec exprs ops where
+    PExprEBOp' sPrev s op prec exprs (TokBOp opPrev : ops) =
+        IfNatLte prec (BOpPrec opPrev)
+            (PExprEBOpPop sPrev s op prec opPrev ops exprs)
+            (PExprNext sPrev (TokBOp op : TokBOp opPrev : ops) exprs (UnconsState s))
+    PExprEBOp' sPrev s op prec exprs '[]          =
+        PExprNext s '[TokBOp op] exprs (UnconsState s)
+
+    -- both parens treated same as LTE prec
+    -- (how could I better design this?)
+    PExprEBOp' sPrev s op prec exprs (TokParenL : ops) =
+        PExprNext sPrev (TokBOp op : TokParenL : ops) exprs (UnconsState s)
+    PExprEBOp' sPrev s op prec exprs (TokParenR : ops) =
+        PExprNext sPrev (TokBOp op : TokParenR : ops) exprs (UnconsState s)
+
+type family PExprEBOpPop sPrev s op prec opPrev ops exprs where
+    PExprEBOpPop sPrev s op prec opPrev ops (r:l:exprs) =
+        PExprEBOp' sPrev s op prec (EBOp opPrev l r : exprs) ops
+    PExprEBOpPop sPrev s op prec opPrev ops exprs =
+        'Reply (Err (Error1 "badly formed expression")) sPrev
+
+type BOpPrec :: BOp -> Natural
+type family BOpPrec bop where
+    BOpPrec Add = 2
+    BOpPrec Sub = 2
+    BOpPrec Mul = 3
+    BOpPrec Div = 3
+
+{-
+import GHC.TypeError qualified as TE
+
+-- | Build an 'Expr' from a postfix stack (RPN style).
+--
+-- The stack must be a valid 'Expr'. It will type error if not.
+type FromRpn:: [ExprTok a] -> Expr a
+type FromRpn toks = FromRpnEnd (FromRpn' '[] toks)
+
+type FromRpn' :: [Expr a] -> [ExprTok a] -> [Expr a]
+type family FromRpn' es toks where
+    FromRpn' es       (TokLit a   : toks) =
+        FromRpn' (ELit a       : es) toks
+    FromRpn' (r:l:es) (TokBOp bop : toks) =
+        FromRpn' (EBOp bop l r : es) toks
+    FromRpn' es       '[]                 = es
+
+type family FromRpnEnd res where
+    FromRpnEnd    '[]  = TE.TypeError (TE.Text "bad RPN: empty")
+    FromRpnEnd (e:'[]) = e
+    FromRpnEnd _       = TE.TypeError (TE.Text "bad RPN: unused operands")
+-}
diff --git a/src/Symparsec/Parser.hs b/src/Symparsec/Parser.hs
--- a/src/Symparsec/Parser.hs
+++ b/src/Symparsec/Parser.hs
@@ -1,195 +1,152 @@
-{-# LANGUAGE AllowAmbiguousTypes #-} -- for singling
-
-{- | Base definitions for Symparsec parsers.
-
-Some types are useable both on term-level, and promoted on type-level e.g.
-'Result'. For ease of use, you can access the promoted version via type synonyms
-like 'PResult' (for promoted X). (This pattern is copied from @singletons@.)
-
-Some definitions I use:
-
-  * "defun symbol": Short for "defunctionalization symbol". A method of passing
-    type-level functions (type families) around, without applying them. We use
-    phadej's @defun@ library for the basic functionality.
-  * "consuming [parser]": A parser which must consume its input. Symparsec
-    parsers are always consuming, as it helps keep parser running simple. This
-    is problematic, as you can define non-consuming parsers e.g. @Take 0@. We
-    handle this by preprocessing initial parser state, to check for such cases.
--}
-
-module Symparsec.Parser
-  (
-  -- * Parser
-    Parser(..), PParser(..), ResultOf, SParser(..)
-  , ParserCh, PParserCh, ParserChSym, ParserChSym1, SParserChSym, SParserChSym1
-  , ParserEnd, PParserEnd, ParserEndSym, SParserEndSym
-  , ParserSInit, ParserSInitSym, SParserSInitSym
-  , Result(..), PResult, SResult(..)
-  , PResultEnd, SResultEnd
-  , PResultSInit, SResultSInit
-
-  -- * Error
-  , E(..), PE, SE(..), demoteSE, SingE(singE), withSingE
+{-# LANGUAGE UndecidableInstances #-}
 
-  -- * Singling
-  , SingParser(..)
-  , singParser
-  ) where
+module Symparsec.Parser where
 
-import GHC.TypeLits
 import DeFun.Core
-import GHC.Exts ( withDict )
-import TypeLevelShow.Doc
-import Singleraeh.Either ( SEither )
+import GHC.TypeLits ( type Symbol )
+import GHC.TypeNats ( type Natural )
+
 import Singleraeh.Demote
-import Singleraeh.Tuple ( STuple2 )
-import Data.Kind ( Type )
+import Data.Kind ( type Type )
+import GHC.TypeLits ( type SSymbol, fromSSymbol )
+import GHC.TypeNats ( type SNat, fromSNat )
+import Singleraeh.List
+--import Singleraeh.Symbol
 
-data Parser str s r = Parser
-  { parserCh  :: ParserCh  str s r
-  , parserEnd :: ParserEnd str s r
-  , parserS0  :: s
-  }
+-- | Parser state.
+data State str n = State
+  -- | Remaining input.
+  { remaining :: str
 
--- | A type-level parser, containing defunctionalization symbols.
---
--- Only intended for promoted use. For singled term-level parsers, use
--- 'SParser'. (Symparsec doesn't provide "regular" term-level parsers.)
---
--- I would make this demotable, but the defun symbols get in the way.
-data PParser s r = PParser
-  { pparserCh  :: ParserChSym s r
-  , pparserEnd :: ParserEndSym s r
-  , pparserS0  :: s
-  }
+  -- | Remaining permitted length.
+  --
+  -- Must be less than or equal to the actual length of the remaining input.
+  -- Parsers must use this field when reading from input:
+  --
+  -- * if ==0, treat as end of input.
+  -- * if  >0 but remaining input is empty, unrecoverable parser error
+  --
+  -- This extra bookkeeping permits much simpler parser design, specifically for
+  -- parsers that act on a substring of the input.
+  , length :: n
 
--- | The result type of a type-level parser. (Sometimes handy.)
-type ResultOf (p :: PParser s r) = r
+  -- | Index in the input string.
+  --
+  -- Overall index. Used for nicer error reporting after parse completion.
+  , index :: n
+  } deriving stock Show
 
--- | A singled parser.
---
--- TODO consider swapping for STuple3...? this is much easier though
-type SParser
-    :: (s -> Type) -> (r -> Type) -> PParser s r
-    -> Type
-data SParser ss sr p where
-    SParser
-        :: SParserChSym  ss sr pCh
-        -> SParserEndSym ss sr pEnd
-        -> ss s0
-        -> SParser ss sr ('PParser pCh pEnd s0)
+-- | Promoted 'State'.
+type PState = State Symbol Natural
 
--- | Parse a 'Char' with the given state.
-type  ParserCh str s r = Char -> s -> Result str s r
-type PParserCh     s r = ParserCh Symbol s r
+-- | Singled 'State'.
+data SState (s :: PState) where
+    SState :: SSymbol rem -> SNat len -> SNat idx -> SState ('State rem len idx)
 
--- | A defunctionalization symbol for a 'ParserCh'.
-type ParserChSym s r = Char ~> s ~> PResult s r
+-- | Demote an 'SState'.
+demoteSState :: SState s -> State String Natural
+demoteSState (SState srem slen sidx) =
+    State (fromSSymbol srem) (fromSNat slen) (fromSNat sidx)
 
--- | A partially-applied defunctionalization symbol for a 'ParserCh'.
-type ParserChSym1 s r = Char -> s ~> PResult s r
+instance Demotable SState where
+    type Demote SState = State String Natural
+    demote = demoteSState
 
-type SParserChSym ss sr pCh = Lam2 SChar ss (SResult ss sr) pCh
-type SParserChSym1 ch ss sr pCh = SChar ch -> Lam ss (SResult ss sr) (pCh ch)
+{-
+data Span n = Span
+  { start :: n
+  , end   :: n
+  } deriving stock Show
+-}
 
--- | What a parser should do at the end of a 'Symbol'.
-type  ParserEnd str s r = s -> ResultEnd str r
-type PParserEnd     s r = ParserEnd Symbol s r
+data Error str = Error
+  { detail :: [str]
+  } deriving stock Show
 
--- | A defunctionalization symbol for a 'ParserEnd'.
-type ParserEndSym s r = s ~> PResultEnd r
+-- | Promoted 'Error'.
+type PError = Error Symbol
 
-type SParserEndSym ss sr pEnd = Lam ss (SResultEnd sr) pEnd
+-- | Singled 'Error'.
+data SError (e :: PError) where
+    SError :: SList SSymbol detail -> SError ('Error detail)
 
-type ParserSInit s0 s = s0 -> PResultSInit s
-type ParserSInitSym s0 s = s0 ~> PResultSInit s
-type SParserSInitSym ss0 ss sInit = Lam ss0 (SResultSInit ss) sInit
+-- | Demote an 'SError'.
+demoteSError :: SError e -> Error String
+demoteSError (SError sdetail) = Error $ demoteSList fromSSymbol sdetail
 
--- | The result of a single step of a parser.
---
--- Promotable. Instantiate with 'String' for term-level, 'Symbol' for
--- type-level.
---
--- Note that a 'Done' indicates the parser has not consumed the character. In
--- the original design, it did consume it, and parsers did their own "lookahead"
--- to handle this. The non-consuming behaviour simplifies permitting
--- non-consuming parsers such as @Take 0@.
-data Result str s r
-  = Cont s       -- ^ OK,     consumed, continue with state @s@
-  | Done r       -- ^ OK, not consumed, parse succeeded with result @r@
-  | Err  (E str) -- ^ parse error
+instance Demotable SError where
+    type Demote SError = Error String
+    demote = demoteSError
 
--- | Promoted 'Result'.
-type PResult = Result Symbol
+-- | Parser completion: result, and final state.
+--
+-- TODO: megaparsec also returns a bool indicating if any input was consumed.
+-- Unsure what it's used for.
+data Reply str n a = Reply
+  { result :: Result str n a -- ^ Parse result.
+  , state  :: State str n    -- ^ Final parser state.
+  } deriving stock Show
 
-data SResult (ss :: s -> Type) (sr :: r -> Type) (res :: PResult s r) where
-    SCont :: ss s -> SResult ss sr (Cont s)
-    SDone :: sr r -> SResult ss sr (Done r)
-    SErr  :: SE e -> SResult ss sr (Err e)
+-- | Promoted 'Reply'.
+type PReply = Reply Symbol Natural
 
-type  ResultEnd str =  Either (E str)
-type PResultEnd     =  Either PE
-type SResultEnd     = SEither SE
+-- | Singled 'Reply'.
+data SReply (sa :: a -> Type) (rep :: PReply a) where
+    SReply :: SResult sa result -> SState state -> SReply sa ('Reply result state)
 
-type PResultSInit s = Either (PE, s) s
-type SResultSInit ss = SEither (STuple2 SE ss) ss
+-- | Demote an 'SReply.
+demoteSReply
+    :: (forall a. sa a -> da)
+    -> SReply sa rep
+    -> Reply String Natural da
+demoteSReply demoteSA (SReply sresult sstate) =
+    Reply (demoteSResult demoteSA sresult) (demoteSState sstate)
 
--- | Parser error.
---
--- Promotable. Instantiate with 'String' for term-level, 'Symbol' for
--- type-level.
-data E str
-  -- | Base parser error.
-  = EBase
-        str       -- ^ parser name
-        (Doc str) -- ^ error message
+instance Demotable sa => Demotable (SReply sa) where
+    type Demote (SReply sa) = Reply String Natural (Demote sa)
+    demote = demoteSReply demote
 
-  -- | Inner parser error inside combinator.
-  | EIn
-        str     -- ^ combinator name
-        (E str) -- ^ inner error
+-- | Parse result: a value, or an error.
+data Result str n a = OK a            -- ^ Parser succeeded.
+                    | Err (Error str) -- ^ Parser failed.
     deriving stock Show
 
--- | Promoted 'E'.
-type PE = E Symbol
-
-data SE (e :: PE) where
-    SEBase :: SSymbol name -> SDoc doc -> SE (EBase name doc)
-    SEIn   :: SSymbol name -> SE   e   -> SE (EIn name e)
+-- | Promoted 'Result'.
+type PResult = Result Symbol Natural
 
-demoteSE :: SE e -> E String
-demoteSE = \case
-  SEBase sname sdoc -> EBase (fromSSymbol sname) (demoteDoc sdoc)
-  SEIn   sname se   -> EIn   (fromSSymbol sname) (demoteSE  se)
+--type SState = State 
+--type SResult :: _ -> Type
+-- TODO ^ how to do explicit kind signature for GADT?
 
-instance Demotable SE where
-    type Demote SE = E String
-    demote = demoteSE
+-- | Singled 'Result'.
+data SResult (sa :: a -> Type) (res :: PResult a) where
+    SOK  :: sa a     -> SResult sa (OK a)
+    SErr :: SError e -> SResult sa (Err e)
 
-class SingE (e :: PE) where singE :: SE e
-instance (KnownSymbol name, SingDoc doc) => SingE (EBase name doc) where
-    singE = SEBase (SSymbol @name) (singDoc @doc)
-instance (KnownSymbol name, SingE e) => SingE (EIn name e) where
-    singE = SEIn   (SSymbol @name) (singE   @e)
+-- | Demote an 'SResult'.
+demoteSResult
+    :: (forall a. sa a -> da)
+    -> SResult sa res
+    -> Result String Natural da
+demoteSResult demoteSA = \case
+  SOK  sa -> OK  $ demoteSA sa
+  SErr se -> Err $ demoteSError se
 
-withSingE :: forall e r. SE e -> (SingE e => r) -> r
-withSingE = withDict @(SingE e)
+instance Demotable sa => Demotable (SResult sa) where
+    type Demote (SResult sa) = Result String Natural (Demote sa)
+    demote = demoteSResult demote
 
--- | Promoted parsers with singled implementations.
-class SingParser (p :: PParser s r) where
-    -- | A singleton for the parser state.
-    type PS  p :: s -> Type
+-- | A parser is a function on parser state.
+type Parser str n a = State str n -> Reply str n a
 
-    -- | A singleton for the parser return type.
-    type PR  p :: r -> Type
+-- | Promoted 'Parser': a defunctionalization symbol to a function on promoted
+--   parser state.
+type PParser a = PState ~> PReply a
 
-    -- | The singled parser.
-    singParser' :: SParser (PS p) (PR p) p
+-- | Singled 'Parser'.
+type SParser sa p = Lam SState (SReply sa) p
+--data SParser (sa :: a -> Type) (p :: PParser a) where
+ --   SParser :: Lam SState (SReply sa) (PParser a)
 
--- | Get the singled version of the requested parser.
---
--- 'singParser'' with better type application ergonomics.
-singParser
-    :: forall {s} {r} (p :: PParser s r). SingParser p
-    => SParser (PS p) (PR p) p
-singParser = singParser' @_ @_ @p
+--class SingParser (p :: PParser a) where
+--    singParser :: SParser sa p
diff --git a/src/Symparsec/Parser/Alternative.hs b/src/Symparsec/Parser/Alternative.hs
new file mode 100644
--- /dev/null
+++ b/src/Symparsec/Parser/Alternative.hs
@@ -0,0 +1,46 @@
+{-# LANGUAGE UndecidableInstances #-}
+
+-- | Type-level string parsers shaped like 'Alternative' functions.
+
+module Symparsec.Parser.Alternative
+  ( type (<|>), type Empty
+  , type Optional
+  ) where
+
+import Symparsec.Parser.Functor
+import Symparsec.Parser.Applicative
+import Symparsec.Parser.Common
+import DeFun.Core
+
+-- | 'Control.Alternative.<|>' for parsers. Try the left parser; if it succeeds, return the result,
+-- else try the right parser with the left parser's output state.
+--
+-- Does not backtrack. Wrap parsers with 'Symparsec.Parser.Try' as needed.
+--
+-- TODO shitty errors
+type (<|>) :: PParser a -> PParser a -> PParser a
+infixl 3 <|>
+data (<|>) l r s
+type instance App (l <|> r) s = Plus r (l @@ s)
+type Plus :: PParser a -> PReply a -> PReply a
+type family Plus r rep where
+    Plus r ('Reply (OK   a) s) = 'Reply (OK a) s
+    Plus r ('Reply (Err _e) s) = r @@ s
+
+-- | 'Control.Alternative.empty' for parsers. Immediately fail with no consumption.
+type Empty :: PParser a
+data Empty s
+type instance App Empty s = 'Reply (Err (Error1 "called empty parser")) s
+
+-- | 'Control.Alternative.optional' for parsers.
+type Optional :: PParser a -> PParser (Maybe a)
+type Optional p = Con1 Just <$> p <|> Pure Nothing
+
+{- Wow, I guess that works. But also, the manual version:
+data Optional p s
+type instance App (Optional p) s = OptionalEnd (p @@ s)
+
+type family OptionalEnd rep where
+    OptionalEnd ('Reply (OK   a) s) = 'Reply (OK (Just a)) s
+    OptionalEnd ('Reply (Err _e) s) = 'Reply (OK Nothing)  s
+-}
diff --git a/src/Symparsec/Parser/Applicative.hs b/src/Symparsec/Parser/Applicative.hs
new file mode 100644
--- /dev/null
+++ b/src/Symparsec/Parser/Applicative.hs
@@ -0,0 +1,45 @@
+{-# LANGUAGE UndecidableInstances #-}
+
+-- | Type-level string parsers shaped like 'Applicative' functions.
+
+module Symparsec.Parser.Applicative
+  ( type (<*>), type Pure
+  , type LiftA2
+  , type (*>), type (<*)
+  ) where
+
+import Symparsec.Parser.Common
+import Symparsec.Parser.Functor
+import DeFun.Function ( type IdSym, type ConstSym )
+
+-- | '<*>' for parsers. Sequence two parsers, left to right.
+type (<*>) :: PParser (a ~> b) -> PParser a -> PParser b
+infixl 4 <*>
+data (<*>) l r s
+type instance App (l <*> r) s = ApL r (l @@ s)
+type ApL :: PParser a -> PReply (a ~> b) -> PReply b
+type family ApL r rep where
+    ApL r ('Reply (OK  fa) s) = (fa <$> r) @@ s
+    ApL r ('Reply (Err e)  s) = 'Reply (Err e) s
+
+-- | 'pure' for parsers. Non-consuming parser that just returns the given value.
+type Pure :: a -> PParser a
+data Pure a s
+type instance App (Pure a) s = 'Reply (OK a) s
+
+-- | 'liftA2' for parsers. Sequence two parsers, and combine their results with
+-- a binary type function.
+type LiftA2 :: (a ~> b ~> c) -> PParser a -> PParser b -> PParser c
+type LiftA2 f l r = (f <$> l) <*> r
+
+-- | '*>' for parsers. Sequence two parsers left to right, discarding the value
+-- of the left parser.
+type (*>) :: PParser a -> PParser b -> PParser b
+infixl 4 *>
+type l *> r = (IdSym <$ l) <*> r
+
+-- | '<*' for parsers. Sequence two parsers left to right, discarding the value
+-- of the right parser.
+type (<*) :: PParser a -> PParser b -> PParser a
+infixl 4 <*
+type l <* r = LiftA2 ConstSym l r
diff --git a/src/Symparsec/Parser/Apply.hs b/src/Symparsec/Parser/Apply.hs
deleted file mode 100644
--- a/src/Symparsec/Parser/Apply.hs
+++ /dev/null
@@ -1,61 +0,0 @@
-{-# LANGUAGE UndecidableInstances #-}
-
-module Symparsec.Parser.Apply where
-
-import Symparsec.Parser.Common
-
--- | Apply the given type function to the result.
---
--- Effectively 'fmap' for parsers.
-type (:<$>:) :: (r ~> r') -> PParser s r -> PParser s r'
-type family f :<$>: p where
-    f :<$>: 'PParser pCh pEnd s0 = Apply' f pCh pEnd s0
-
--- unwrapped for instances
-type Apply' f pCh pEnd s0 = 'PParser (ApplyChSym f pCh) (ApplyEndSym f pEnd) s0
-
--- TODO: Singling is a pain, similar to While. Let's ignore it for now.
-
-type ApplyCh
-    :: (r ~> r')
-    -> ParserChSym s r
-    -> PParserCh s r'
-type family ApplyCh f pCh ch s where
-    ApplyCh f pCh ch s = ApplyCh' f (pCh @@ ch @@ s)
-
-type family ApplyCh' f res where
-    ApplyCh' f (Cont s) = Cont s
-    ApplyCh' f (Done r) = Done (f @@ r)
-    ApplyCh' f (Err  e) = Err e
-
-type ApplyChSym
-    :: (r ~> r')
-    -> ParserChSym s r
-    -> ParserChSym s r'
-data ApplyChSym f pCh x
-type instance App (ApplyChSym f pCh) x = ApplyChSym1 f pCh x
-
-type ApplyChSym1
-    :: (r ~> r')
-    -> ParserChSym  s r
-    -> ParserChSym1 s r'
-data ApplyChSym1 f pCh ch s
-type instance App (ApplyChSym1 f pCh ch) s = ApplyCh f pCh ch s
-
-type ApplyEnd
-    :: (r ~> r')
-    -> ParserEndSym s r
-    -> PParserEnd s r'
-type family ApplyEnd f pEnd s where
-    ApplyEnd f pEnd s = ApplyEnd' f (pEnd @@ s)
-
-type family ApplyEnd' f res where
-    ApplyEnd' f (Right r) = Right (f @@ r)
-    ApplyEnd' f (Left  e) = Left  e
-
-type ApplyEndSym
-    :: (r ~> r')
-    -> ParserEndSym s r
-    -> ParserEndSym s r'
-data ApplyEndSym f pEnd s
-type instance App (ApplyEndSym f pEnd) s = ApplyEnd f pEnd s
diff --git a/src/Symparsec/Parser/Common.hs b/src/Symparsec/Parser/Common.hs
--- a/src/Symparsec/Parser/Common.hs
+++ b/src/Symparsec/Parser/Common.hs
@@ -1,49 +1,82 @@
--- | Common definitions for parsers.
+{-# LANGUAGE UndecidableInstances #-}
 
+-- | Common definitions used by parsers.
+
 module Symparsec.Parser.Common
   (
+  -- * Common definitions
+    type UnconsState
+  , type Error1
+  --, type Err1
+  , type EStrInputTooShort, type EStrWrongChar
+  --, type Err, type Done
+  , type Impossible
+
   -- * Re-exports
-    module Symparsec.Parser
-  , Doc(..)
-  , type (~>), type (@@), type App
+  , module Symparsec.Parser
+  , Doc(..), type (++)
+  , type App
 
-  -- * Common definitions
-  , FailChSym,  failChSym
-  , FailEndSym, failEndSym
-  , ErrParserLimitation
+  -- ** Common imports
+  -- $common-imports
+  , type Symbol, type UnconsSymbol, ConsSymbol
+  , type Natural, type (+), type (-), type (*)
+  , type ShowNatDec, type ShowChar
+  , type (@@), type (~>)
   ) where
 
 import Symparsec.Parser
-import GHC.TypeLits hiding ( ErrorMessage(..) )
 import DeFun.Core
+import GHC.TypeLits ( type Symbol, type UnconsSymbol, type ConsSymbol )
+import GHC.TypeNats ( type Natural, type (+), type (-), type (*) )
 import TypeLevelShow.Doc
-import Singleraeh.Either
+import TypeLevelShow.Natural ( type ShowNatDec )
+import TypeLevelShow.Utils ( type ShowChar, type (++) )
+-- TODO clean up (++) stuff, probably just export my own one
+import GHC.TypeError qualified as TE
 
--- | Fail with the given message when given any character to parse.
-type FailCh name e = Err (EBase name e)
+-- $common-imports
+-- Not used by all parsers, but common enough that we'll export them here.
 
-type FailChSym :: Symbol -> PDoc -> ParserChSym s r
-data FailChSym name e f
-type instance App (FailChSym name e) f = FailChSym1 name e f
+-- TODO this is pre-spans
+--type EBase parserName = 'Error '[(Text parserName) ('Span 0 0) '[]
 
-type FailChSym1 :: Symbol -> PDoc -> ParserChSym1 s r
-data FailChSym1 name e ch s
-type instance App (FailChSym1 name e ch) s = FailCh name e
+-- | Get the next character in the string and update the parser state.
+--
+-- If at end of the string, the state is returned untouched, and @len@ is
+-- guaranteed to be 0.
+type UnconsState :: PState -> (Maybe Char, PState)
+type family UnconsState s where
+    UnconsState ('State rem 0   idx) = '(Nothing, 'State rem 0 idx)
+    UnconsState ('State rem len idx) = UnconsState' (UnconsSymbol rem) len idx
 
-failChSym
-    :: SSymbol name -> SDoc e -> SParserChSym ss sr (FailChSym name e)
-failChSym name e = Lam2 $ \_ch _s -> SErr $ SEBase name e
+type UnconsState'
+    :: Maybe (Char, Symbol) -> Natural -> Natural -> (Maybe Char, PState)
+type family UnconsState' mstr len idx where
+    UnconsState' (Just '(ch, rem)) len idx =
+        '(Just ch, 'State rem (len-1) (idx+1))
+    UnconsState' Nothing           len idx =
+        -- TODO could I change this to a regular parser error? should I?
+        TE.TypeError (TE.Text "unrecoverable parser error: got to end of input string before len=0")
 
--- | Fail with the given message if we're at the end of the symbol.
-type FailEndSym :: Symbol -> PDoc -> ParserEndSym s r
-data FailEndSym name e s
-type instance App (FailEndSym name e) s = Left (EBase name e)
+-- TODO: add type synonym for @(Maybe Char, PState) -> PResult res@
 
-failEndSym
-    :: SSymbol name -> SDoc e -> SParserEndSym ss sr (FailEndSym name e)
-failEndSym name e = Lam $ \_s -> SLeft $ SEBase name e
+-- TODO
+type Error1 str = 'Error '[str]
+--type Err1 str = Err (Error1 str)
+--type OK' a s = 'Reply (OK a) s
 
--- | Helper for writing error messages to do with parser limitations (e.g. if
---   you tried to use a non-consuming parser like @Skip 0@).
-type ErrParserLimitation :: Symbol -> PDoc
-type ErrParserLimitation msg = Text "parser limitation: " :<>: Text msg
+type EStrInputTooShort :: Natural -> Natural -> Symbol
+type EStrInputTooShort nNeed nGot =
+         "needed " ++ ShowNatDec nNeed
+      ++ " chars, but only " ++ ShowNatDec nGot ++ " remain"
+
+type EStrWrongChar :: Char -> Char -> Symbol
+type EStrWrongChar chExpect chGot =
+         "expected '" ++ ShowChar chExpect
+      ++  "', got '"  ++ ShowChar chGot ++ "'"
+
+-- | Impossible parser state.
+--
+-- Use when you can prove that an equation is impossible.
+type Impossible = TE.TypeError (TE.Text "impossible parser state")
diff --git a/src/Symparsec/Parser/Count.hs b/src/Symparsec/Parser/Count.hs
--- a/src/Symparsec/Parser/Count.hs
+++ b/src/Symparsec/Parser/Count.hs
@@ -1,147 +1,24 @@
 {-# LANGUAGE UndecidableInstances #-}
 
-module Symparsec.Parser.Count where
+module Symparsec.Parser.Count ( type Count ) where
 
 import Symparsec.Parser.Common
-import GHC.TypeLits hiding ( ErrorMessage(..) )
-import Singleraeh.Tuple
-import Singleraeh.List
-import Singleraeh.Either
-import Singleraeh.Natural
-import DeFun.Core
-import Data.Type.Equality
-import Unsafe.Coerce ( unsafeCoerce )
-
-type CountS s r = (Natural, [r], s)
-
-type family Count n p where
-    Count n ('PParser pCh pEnd s0) = Count' n pCh pEnd s0
-type Count' n pCh pEnd s0 =
-    'PParser (CountChSym pCh s0) (CountEndSym pEnd s0) '(n, '[], s0)
-
-type SCountS ss sr = STuple3 SNat (SList sr) ss
-
-sCount
-    :: SNat n
-    -> SParser ss sr ('PParser pCh pEnd s0)
-    -> SParser (SCountS ss sr) (SList sr) (Count' n pCh pEnd s0)
-sCount n (SParser pCh pEnd s0) =
-    SParser (sCountChSym pCh s0) (sCountEndSym pEnd s0) (STuple3 n SNil s0)
-
-instance
-  ( p ~ 'PParser pCh pEnd s0, SingParser p, KnownNat n
-  ) => SingParser (Count' n pCh pEnd s0) where
-    type PS (Count' n pCh pEnd s0) =
-          SCountS (PS ('PParser pCh pEnd s0)) (PR ('PParser pCh pEnd s0))
-    type PR (Count' n pCh pEnd s0) = SList (PR ('PParser pCh pEnd s0))
-    singParser' = sCount SNat (singParser @p)
-
-type family CountCh pCh s0 ch s where
-    CountCh pCh s0 ch '(n, rs, s) = CountCh' pCh s0 ch n rs s
-
-sCountChSym
-    :: SParserChSym  ss sr pCh
-    -> ss s0
-    -> SParserChSym (SCountS ss sr) (SList sr) (CountChSym pCh s0)
-sCountChSym pCh s0 = Lam2 $ \ch (STuple3 n rs s) ->
-    sCountCh' pCh s0 ch n rs s
-
-type family CountCh' pCh s0 ch n rs s where
-    CountCh' pCh s0 ch 0 rs s = Done (Reverse rs)
-    CountCh' pCh s0 ch n rs s = CountChN pCh ch n rs s0 (pCh @@ ch @@ s)
-
-sCountCh'
-    :: SParserChSym ss sr pCh
-    -> ss s0
-    -> SChar ch
-    -> SNat n
-    -> SList sr rs
-    -> ss s
-    -> SResult (SCountS ss sr) (SList sr) (CountCh' pCh s0 ch n rs s)
-sCountCh' pCh s0 ch n rs s =
-    case testEquality n (SNat @0) of
-      Just Refl -> SDone $ sReverse rs
-      Nothing   -> unsafeCoerce $ sCountChN pCh ch n rs s0 (pCh @@ ch @@ s)
-
-type family CountChN pCh ch n rs s0 res where
-    CountChN pCh ch n rs s0 (Cont s) = Cont '(n, rs, s)
-    CountChN pCh ch n rs s0 (Done r) = CountCh' pCh s0 ch (n-1) (r:rs) s0
-    CountChN pCh ch n rs s0 (Err  e) = Err (ECount e)
-
-sCountChN
-    :: SParserChSym ss sr pCh
-    -> SChar ch
-    -> SNat n
-    -> SList sr rs
-    -> ss s0
-    -> SResult ss sr res
-    -> SResult (SCountS ss sr) (SList sr) (CountChN pCh ch n rs s0 res)
-sCountChN pCh ch n rs s0 = \case
-  SCont s -> SCont $ STuple3 n rs s
-  SDone r -> sCountCh' pCh s0 ch (n %- SNat @1) (SCons r rs) s0
-  SErr  e -> SErr  $ eCount e
-
-type ECount e = EIn "Count" e
-eCount :: SE e -> SE (ECount e)
-eCount e = withSingE e $ singE
-
-type CountChSym
-    :: ParserChSym  s r
-    -> s
-    -> ParserChSym  (CountS s r) [r]
-data CountChSym pCh s0 f
-type instance App (CountChSym pCh s0) f = CountChSym1 pCh s0 f
-
-type CountChSym1
-    :: ParserChSym  s r
-    -> s
-    -> ParserChSym1 (CountS s r) [r]
-data CountChSym1 pCh s0 ch s
-type instance App (CountChSym1 pCh s0 ch) s = CountCh pCh s0 ch s
-
-type family CountEnd pEnd s0 s where
-    CountEnd pEnd s0 '(n, rs, s) = CountEnd' pEnd s0 n rs s
-
-type family CountEnd' pEnd s0 n rs s where
-    CountEnd' pEnd s0 0 rs s = Right (Reverse rs)
-    CountEnd' pEnd s0 n rs s = CountEndN pEnd s0 n rs (pEnd @@ s)
-
-sCountEnd'
-    :: SParserEndSym ss sr pEnd
-    -> ss s0
-    -> SNat n
-    -> SList sr rs
-    -> ss s
-    -> SResultEnd (SList sr) (CountEnd' pEnd s0 n rs s)
-sCountEnd' pEnd s0 n rs s =
-    case testEquality n (SNat @0) of
-      Just Refl -> SRight $ sReverse rs
-      Nothing   -> unsafeCoerce $ sCountEndN pEnd s0 n rs (pEnd @@ s)
+import qualified Singleraeh.List as List
 
-type family CountEndN pEnd s0 n rs res where
-    CountEndN pEnd s0 n rs (Right r) = CountEnd' pEnd s0 (n-1) (r:rs) s0
-    CountEndN pEnd s0 n rs (Left  e) = Left (ECount e)
+-- TODO Could possibly make more efficient.
 
-sCountEndN
-    :: SParserEndSym ss sr pEnd
-    -> ss s0
-    -> SNat n
-    -> SList sr rs
-    -> SResultEnd sr res
-    -> SResultEnd (SList sr) (CountEndN pEnd s0 n rs res)
-sCountEndN pEnd s0 n rs = \case
-  SRight r -> sCountEnd' pEnd s0 (n %- SNat @1) (SCons r rs) s0
-  SLeft  e -> SLeft $ eCount e
+-- | @'Count' n p@ parses @n@ occurrences of @p@.
+type Count :: Natural -> PParser a -> PParser [a]
+data Count n p s
+type instance App (Count n p) s = CountLoop p '[] n s
 
-type CountEndSym
-    :: ParserEndSym s r
-    -> s
-    -> ParserEndSym (CountS s r) [r]
-data CountEndSym pEnd s0 s
-type instance App (CountEndSym pEnd s0) s = CountEnd pEnd s0 s
+type family CountLoop p as n s where
+    CountLoop p as 0 s = 'Reply (OK (List.Reverse as)) s
+    CountLoop p as n s = CountLoopWrap p as n (p @@ s)
 
-sCountEndSym
-    :: SParserEndSym ss              sr         pEnd
-    -> ss s0
-    -> SParserEndSym (SCountS ss sr) (SList sr) (CountEndSym pEnd s0)
-sCountEndSym pEnd s0 = Lam $ \(STuple3 n rs s) -> sCountEnd' pEnd s0 n rs s
+type family CountLoopWrap p as n rep where
+    CountLoopWrap p as n ('Reply (OK  a) s) =
+        CountLoop p (a:as) (n-1) s
+    CountLoopWrap p as n ('Reply (Err e) s) =
+        -- TODO am I passing the wrong state back here?
+        'Reply (Err e) s
diff --git a/src/Symparsec/Parser/End.hs b/src/Symparsec/Parser/End.hs
deleted file mode 100644
--- a/src/Symparsec/Parser/End.hs
+++ /dev/null
@@ -1,32 +0,0 @@
-module Symparsec.Parser.End where
-
-import Symparsec.Parser.Common
-import DeFun.Core
-import Singleraeh.Tuple ( SUnit(..) )
-import Singleraeh.Either ( SEither(..) )
-
--- | Assert end of symbol, or fail.
-type End :: PParser () ()
-type End = 'PParser EndChSym (Con1 Right) '()
-
-sEnd :: SParser SUnit SUnit End
-sEnd = SParser sEndChSym (con1 SRight) SUnit
-
-instance SingParser End where
-    type PS  End = SUnit
-    type PR  End = SUnit
-    singParser' = sEnd
-
--- it'd be nice to just reuse FailChSym here but we get told off for writing an
--- orphan instance. fair enough, write this instead
-type EndChSym :: ParserChSym s r
-data EndChSym f
-type instance App EndChSym f = EndChSym1 f
-
-type EndChSym1 :: ParserChSym1 s r
-data EndChSym1 ch s
-type instance App (EndChSym1 ch) s =
-    Err (EBase "End" (Text "expected end of string"))
-
-sEndChSym :: SParserChSym ss rr EndChSym
-sEndChSym = Lam2 $ \_ch _s -> SErr singE
diff --git a/src/Symparsec/Parser/Ensure.hs b/src/Symparsec/Parser/Ensure.hs
new file mode 100644
--- /dev/null
+++ b/src/Symparsec/Parser/Ensure.hs
@@ -0,0 +1,16 @@
+{-# LANGUAGE UndecidableInstances #-}
+
+module Symparsec.Parser.Ensure ( type Ensure ) where
+
+import Symparsec.Parser.Common
+import Symparsec.Utils ( type IfNatLte )
+
+-- | Assert that there are at least @n@ characters remaining. Non-consuming.
+type Ensure :: Natural -> PParser ()
+data Ensure n s
+type instance App (Ensure n) s = Ensure' n s
+type family Ensure' n s where
+    Ensure' n ('State rem len idx) =
+        IfNatLte n len
+            ('Reply (OK '()) ('State rem len idx))
+            ('Reply (Err (Error1 (EStrInputTooShort n len))) ('State rem len idx))
diff --git a/src/Symparsec/Parser/Eof.hs b/src/Symparsec/Parser/Eof.hs
new file mode 100644
--- /dev/null
+++ b/src/Symparsec/Parser/Eof.hs
@@ -0,0 +1,15 @@
+{-# LANGUAGE UndecidableInstances #-}
+
+module Symparsec.Parser.Eof ( type Eof ) where
+
+import Symparsec.Parser.Common
+
+-- | Assert end of input, or fail.
+type Eof :: PParser ()
+data Eof s
+type instance App Eof s = Eof' (UnconsState s)
+type family Eof' ms where
+    Eof' '(Nothing,  s) = 'Reply (OK '()) s
+    Eof' '(Just _ch, s) = 'Reply (Err EEof) s
+
+type EEof = Error1 "expected end of string"
diff --git a/src/Symparsec/Parser/Functor.hs b/src/Symparsec/Parser/Functor.hs
new file mode 100644
--- /dev/null
+++ b/src/Symparsec/Parser/Functor.hs
@@ -0,0 +1,30 @@
+{-# LANGUAGE UndecidableInstances #-}
+
+-- | Type-level string parsers shaped like 'Functor' functions.
+
+module Symparsec.Parser.Functor
+  ( type (<$>), type (<$), type ($>)
+  ) where
+
+import Symparsec.Parser.Common
+import DeFun.Function ( type ConstSym1 )
+
+-- | '<$>' for parsers. Apply the given type function to the result.
+type (<$>) :: (a ~> b) -> PParser a -> PParser b
+infixl 4 <$>
+data (<$>) f p s
+type instance App (f <$> p) s = FmapEnd f (p @@ s)
+
+type family FmapEnd f rep where
+    FmapEnd f ('Reply (OK  a) s) = 'Reply (OK  (f @@ a)) s
+    FmapEnd f ('Reply (Err e) s) = 'Reply (Err e)        s
+
+-- | '<$' for parsers. Replace the parser result with the given value.
+type (<$) :: a -> PParser b -> PParser a
+infixl 4 <$
+type a <$ p = ConstSym1 a <$> p
+
+-- | 'Data.Functor.$>' for parsers. Flipped t'Symparsec.Parser.Functor.<$'.
+type ($>) :: PParser a -> b -> PParser b
+infixl 4 $>
+type p $> a = ConstSym1 a <$> p
diff --git a/src/Symparsec/Parser/Isolate.hs b/src/Symparsec/Parser/Isolate.hs
--- a/src/Symparsec/Parser/Isolate.hs
+++ b/src/Symparsec/Parser/Isolate.hs
@@ -1,150 +1,44 @@
 {-# LANGUAGE UndecidableInstances #-}
 
-module Symparsec.Parser.Isolate where
+module Symparsec.Parser.Isolate ( type Isolate, type IsolateSym ) where
 
 import Symparsec.Parser.Common
-import GHC.TypeLits hiding ( ErrorMessage(..) )
-import TypeLevelShow.Natural ( ShowNatDec, sShowNatDec )
-import DeFun.Core
-import Singleraeh.Either
-import Singleraeh.Tuple
-import Singleraeh.Equality ( testEqElse )
-import Singleraeh.Natural ( (%-) )
-import Unsafe.Coerce ( unsafeCoerce )
-import Data.Type.Equality
-
--- | Run the given parser isolated to the next @n@ characters.
---
--- All isolated characters must be consumed.
-type Isolate :: Natural -> PParser s r -> PParser (Natural, s) r
-type family Isolate n p where
-    Isolate n ('PParser pCh pEnd s0) = Isolate' n pCh pEnd s0
-
--- unwrapped for instances
-type Isolate' n pCh pEnd s0 = 'PParser
-    (IsolateChSym pCh pEnd)
-    (IsolateEndSym pEnd)
-    '(n, s0)
-
-type SIsolateS ss = STuple2 SNat ss
-
-sIsolate
-    :: SNat n
-    -> SParser ss sr p
-    -> SParser (SIsolateS ss) sr (Isolate n p)
-sIsolate n (SParser pCh pEnd s0) = SParser
-    (sIsolateChSym pCh pEnd)
-    (sIsolateEndSym pEnd)
-    (STuple2 n s0)
-
-instance
-  ( p ~ 'PParser pCh pEnd s0
-  , KnownNat n, SingParser p
-  ) => SingParser (Isolate' n pCh pEnd s0) where
-    type PS (Isolate' n pCh pEnd s0) =
-        SIsolateS (PS ('PParser pCh pEnd s0))
-    type PR (Isolate' n pCh pEnd s0) =
-        PR ('PParser pCh pEnd s0)
-    singParser' = sIsolate (natSing @n) (singParser @p)
-
-type IsolateCh
-    :: ParserChSym s r
-    -> ParserEndSym s r
-    -> PParserCh (Natural, s) r
-type family IsolateCh pCh pEnd ch s where
-    IsolateCh pCh pEnd ch '(0, s) = IsolateInnerEnd (pEnd @@ s)
-    IsolateCh pCh pEnd ch '(n, s) = IsolateInner n (pCh @@ ch @@ s)
-
-sIsolateChSym
-    :: SParserChSym  ss sr pCh
-    -> SParserEndSym ss sr pEnd
-    -> SParserChSym (SIsolateS ss) sr (IsolateChSym pCh pEnd)
-sIsolateChSym pCh pEnd = Lam2 $ \ch (STuple2 n s) ->
-    case testEquality n (SNat @0) of
-      Just Refl ->
-        case pEnd @@ s of
-          SRight r -> SDone r
-          SLeft  e -> SErr $ eIsolateWrap e
-      Nothing -> unsafeCoerce $ sIsolateInner n (pCh @@ ch @@ s)
-
-type IsolateInnerEnd :: Either PE r -> PResult (Natural, s) r
-type family IsolateInnerEnd a where
-    IsolateInnerEnd (Right r) = Done r
-    IsolateInnerEnd (Left  e) = Err  (EIsolateWrap e)
-
-type IsolateInner :: Natural -> PResult s r -> PResult (Natural, s) r
-type family IsolateInner n res where
-    IsolateInner n (Cont s) = Cont '(n-1, s)
-    IsolateInner n (Done _) = Err (EIsolateRemaining n)
-    IsolateInner _ (Err  e) = Err (EIsolateWrap e)
-
-sIsolateInner
-    :: SNat n
-    -> SResult ss sr res
-    -> SResult (SIsolateS ss) sr (IsolateInner n res)
-sIsolateInner n = \case
-  SCont  s -> SCont $ STuple2 (n %- (SNat @1)) s
-  SDone _r -> SErr  $ eIsolateRemaining n
-  SErr   e -> SErr  $ eIsolateWrap e
-
-type IsolateEnd :: ParserEndSym s r -> PParserEnd (Natural, s) r
-type family IsolateEnd pEnd s where
-    IsolateEnd pEnd '(0, s) = IsolateEnd' (pEnd @@ s)
-    -- ^ will only occur on @Isolate 0@
-    IsolateEnd pEnd '(n, s) = Left (EIsolateEndN n)
-
-sIsolateEndSym
-    :: SParserEndSym ss sr pEnd
-    -> SParserEndSym (SIsolateS ss) sr (IsolateEndSym pEnd)
-sIsolateEndSym pEnd = Lam $ \(STuple2 n s) ->
-      testEqElse n (SNat @0) (sIsolateEnd' (pEnd @@ s))
-    $ unsafeCoerce $ SLeft $ eIsolateEndN n
-
-type IsolateEnd' :: Either PE r -> Either PE r
-type family IsolateEnd' res where
-    IsolateEnd' (Right r) = Right r
-    IsolateEnd' (Left  e) = Left (EIsolateWrap e)
-
-sIsolateEnd'
-    :: SResultEnd sr res
-    -> SResultEnd sr (IsolateEnd' res)
-sIsolateEnd' = \case
-  SRight r -> SRight r
-  SLeft  e -> SLeft  $ eIsolateWrap e
-
-type IsolateEndSym :: ParserEndSym s r -> ParserEndSym (Natural, s) r
-data IsolateEndSym pEnd s
-type instance App (IsolateEndSym pEnd) s = IsolateEnd pEnd s
-
-type IsolateChSym
-    :: ParserChSym s r
-    -> ParserEndSym s r
-    -> ParserChSym (Natural, s) r
-data IsolateChSym pCh pEnd f
-type instance App (IsolateChSym pCh pEnd) f = IsolateChSym1 pCh pEnd f
-
-type IsolateChSym1
-    :: ParserChSym s r
-    -> ParserEndSym s r
-    -> Char -> (Natural, s) ~> PResult (Natural, s) r
-data IsolateChSym1 pCh pEnd ch s
-type instance App (IsolateChSym1 pCh pEnd ch) s = IsolateCh pCh pEnd ch s
+import Symparsec.Utils ( type IfNatLte )
 
-type EIsolateWrap e = EIn "Isolate" e
+-- TODO can use 'Ensure' to help define this
+type Isolate :: Natural -> PParser a -> PParser a
+data Isolate n p s
+type instance App (Isolate n p) s = Isolate' n p s
+type family Isolate' n p s where
+    Isolate' n p ('State rem len idx) =
+        -- Could perhaps improve this, since 'OrdCond' probably does similar
+        -- work to @len-n@.
+        IfNatLte n len
+            (IsolateEnd len n (p @@ ('State rem n idx)))
+            ('Reply (Err (Error1 (EStrInputTooShort n len))) ('State rem len idx))
 
-eIsolateWrap :: SE e -> SE (EIsolateWrap e)
-eIsolateWrap e = withSingE e singE
+--type IsolateEnd :: Natural -> ? -> ?
+-- TODO are lenRem/lenConsumed actually good names?
+type family IsolateEnd lenOrig n rep where
+    -- isolated parser succeeded and consumed all input:
+    -- return success with state updated to have actual remaining length
+    IsolateEnd lenOrig n ('Reply (OK  a) ('State rem 0   idx)) =
+        'Reply (OK  a) ('State rem (lenOrig-n)     idx)
 
-type EIsolateEndN n = EBase "Isolate"
-    (      Text "tried to isolate more than present (needed "
-      :<>: Text (ShowNatDec n) :<>: Text " more)" )
+    -- isolated parser failed
+    IsolateEnd lenOrig n ('Reply (Err e) ('State rem len idx)) =
+        -- TODO add some isolate meta
+        'Reply (Err e) ('State rem (lenOrig-n+len) idx)
 
-eIsolateEndN :: SNat n -> SE (EIsolateEndN n)
-eIsolateEndN n = withKnownSymbol (sShowNatDec n) singE
+    -- isolated parser succeeded but didn't consume all input
+    IsolateEnd lenOrig n ('Reply (OK _a) ('State rem len idx)) =
+        'Reply (Err (EIsolateIncomplete len)) ('State rem (lenOrig-n+len) idx)
 
-type EIsolateRemaining n = EBase "Isolate"
-    (      Text "isolated parser ended without consuming all input ("
-      :<>: Text (ShowNatDec n) :<>: Text " remaining)" )
+type EIsolateIncomplete n = Error1
+    (    "isolated parser completed without consuming all input ("
+      ++ ShowNatDec n ++ " remaining)" )
 
-eIsolateRemaining :: SNat n -> SE (EIsolateRemaining n)
-eIsolateRemaining n = withKnownSymbol (sShowNatDec n) singE
+-- TODO testing. args flipped because you're more likely to defun the len
+type IsolateSym :: PParser a -> Natural ~> PParser a
+data IsolateSym p x
+type instance App (IsolateSym p) n = Isolate n p
diff --git a/src/Symparsec/Parser/Literal.hs b/src/Symparsec/Parser/Literal.hs
--- a/src/Symparsec/Parser/Literal.hs
+++ b/src/Symparsec/Parser/Literal.hs
@@ -1,80 +1,52 @@
 {-# LANGUAGE UndecidableInstances #-}
 
-module Symparsec.Parser.Literal where
+module Symparsec.Parser.Literal ( type Literal ) where
 
 import Symparsec.Parser.Common
-import GHC.TypeLits hiding ( ErrorMessage(..) )
-import TypeLevelShow.Utils ( ShowChar, sShowChar )
-import Data.Type.Equality
-import DeFun.Core
-import Singleraeh.Tuple
-import Singleraeh.Either
-import Singleraeh.Maybe
-import Singleraeh.Symbol
-import Unsafe.Coerce
-import TypeLevelShow.Doc
-
--- | Parse the given 'Symbol'.
-type Literal :: Symbol -> PParser Symbol ()
-type Literal str = 'PParser LiteralChSym LiteralEndSym str
-
-sLiteral :: SSymbol str -> SParser SSymbol SUnit (Literal str)
-sLiteral str = SParser sLiteralChSym sLiteralEndSym str
-
-instance KnownSymbol str => SingParser (Literal str) where
-    type PS (Literal str) = SSymbol
-    type PR (Literal str) = SUnit
-    singParser' = sLiteral SSymbol
-
-type LiteralCh ch str = LiteralCh' ch (UnconsSymbol str)
-type family LiteralCh' ch str where
-    LiteralCh' ch (Just '(ch, str))     = Cont str
-    LiteralCh' ch (Just '(chNext, str)) = Err (EWrongChar chNext ch)
-    LiteralCh' ch Nothing               = Done '()
-
-type EWrongChar chNext ch = EBase "Literal"
-    (      Text "expected " :<>: Text (ShowChar chNext)
-      :<>: Text    ", got " :<>: Text (ShowChar ch))
-
-eWrongChar :: SChar chNext -> SChar ch -> SE (EWrongChar chNext ch)
-eWrongChar chNext ch = SEBase symbolSing $
-          SText symbolSing :$<>: SText (sShowChar chNext)
-    :$<>: SText symbolSing :$<>: SText (sShowChar ch)
+import Symparsec.Utils ( type IfNatLte )
+import Data.Type.Symbol qualified as Symbol
 
-type LiteralChSym :: ParserChSym Symbol ()
-data LiteralChSym f
-type instance App LiteralChSym f = LiteralChSym1 f
+-- TODO megaparsec auto-backtracks its similar primitive.
+-- confusingly they write it on the type class method Haddock, even though it
+-- doesn't seem enforced (the backtracking is done internally).
+-- idk why. but should we also?
+-- (similarly to megaparsec, it doesn't really change performance.)
 
-type LiteralChSym1 :: ParserChSym1 Symbol ()
-data LiteralChSym1 ch s
-type instance App (LiteralChSym1 ch) s = LiteralCh ch s
+type EDuringLit :: Symbol -> Symbol -> PError
+type EDuringLit lit detail = 'Error
+    [ "while parsing literal '" ++ lit ++ "':"
+    , detail ]
 
-sLiteralChSym :: SParserChSym SSymbol SUnit LiteralChSym
-sLiteralChSym = Lam2 $ \ch str ->
-    case sUnconsSymbol str of
-      SJust (STuple2 chNext str') ->
-        case testEquality ch chNext of
-          Just Refl -> SCont str'
-          Nothing   -> unsafeCoerce $ SErr $ eWrongChar chNext ch
-      SNothing -> SDone SUnit
+type ETooShort lit nNeed nGot =
+    EDuringLit lit (EStrInputTooShort nNeed nGot)
 
-type LiteralEnd :: PParserEnd Symbol ()
-type family LiteralEnd str where
-    LiteralEnd ""  = Right '()
-    LiteralEnd str = Left (EStillParsing str)
+type EWrongChar lit chExpect chGot =
+    EDuringLit lit (EStrWrongChar chExpect chGot)
 
-type EStillParsing str =
-    EBase "Literal" (Text "still parsing literal: " :<>: Text str)
+type EEof lit = EDuringLit lit "EOF while still parsing literal"
 
-eStillParsing :: SSymbol str -> SE (EStillParsing str)
-eStillParsing str = withKnownSymbol str singE
+type Literal :: Symbol -> PParser ()
+data Literal lit s
+type instance App (Literal lit) s = LiteralCheckLen lit s (Symbol.Length lit)
 
-type LiteralEndSym :: ParserEndSym Symbol ()
-data LiteralEndSym s
-type instance App LiteralEndSym s = LiteralEnd s
+-- now, I could use 'Ensure' here. but we add context to errors here, which I
+-- quite like. perhaps I should provide an @Ensure'@ that lets you add e detail?
+type family LiteralCheckLen lit s n where
+    LiteralCheckLen lit ('State rem len idx) litLen =
+        IfNatLte litLen len
+            (LiteralStep lit ('State rem len idx))
+            ('Reply (Err (ETooShort lit litLen len)) ('State rem len idx))
 
-sLiteralEndSym :: SParserEndSym SSymbol SUnit LiteralEndSym
-sLiteralEndSym = Lam $ \str ->
-    case testEquality str (SSymbol @"") of
-      Just Refl -> SRight SUnit
-      Nothing   -> unsafeCoerce $ SLeft $ eStillParsing str
+type LiteralStep lit s = Literal' lit s (UnconsSymbol lit) (UnconsState s)
+type family Literal' lit sPrev ch ms where
+    Literal'  lit sPrev (Just '(litCh, litStr)) '(Just litCh,  s) =
+        Literal' lit s (UnconsSymbol litStr) (UnconsState s)
+    Literal' _lit sPrev Nothing                 _                 =
+        'Reply (OK '()) sPrev
+    Literal'  lit sPrev (Just '(litCh, litStr)) '(Just    ch, _s) =
+        -- TODO which state to pass back here?
+        'Reply (Err (EWrongChar lit litCh ch)) sPrev
+    Literal'  lit sPrev (Just '(litCh, litStr)) '(Nothing,    _s) =
+        -- note that this equation is impossible providing length is checked
+        -- both states are guaranteed the same here, but prev is morally better
+        'Reply (Err (EEof lit)) sPrev
diff --git a/src/Symparsec/Parser/Monad.hs b/src/Symparsec/Parser/Monad.hs
new file mode 100644
--- /dev/null
+++ b/src/Symparsec/Parser/Monad.hs
@@ -0,0 +1,18 @@
+{-# LANGUAGE UndecidableInstances #-}
+
+-- | Type-level string parsers shaped like 'Monad' functions.
+
+module Symparsec.Parser.Monad ( type (>>=) ) where
+
+import Symparsec.Parser.Common
+
+-- | '>>=' for parsers. Sequentially compose two parsers, passing the value from
+-- the left parser as an argument to the second.
+type (>>=) :: PParser a -> (a ~> PParser b) -> PParser b
+infixl 1 >>=
+data (>>=) l r s
+type instance App (l >>= r) s = BindL r (l @@ s)
+type BindL :: (a ~> PParser b) -> PReply a -> PReply b
+type family BindL r rep where
+    BindL r ('Reply (OK  a) s) = r @@ a @@ s
+    BindL r ('Reply (Err e) s) = 'Reply (Err e) s
diff --git a/src/Symparsec/Parser/Natural.hs b/src/Symparsec/Parser/Natural.hs
--- a/src/Symparsec/Parser/Natural.hs
+++ b/src/Symparsec/Parser/Natural.hs
@@ -1,104 +1,136 @@
 {-# LANGUAGE UndecidableInstances #-}
 
-module Symparsec.Parser.Natural where
+module Symparsec.Parser.Natural
+  ( type NatBase, type NatBase1
+  , type NatDec
+  , type NatHex
+  , type NatBin
+  , type NatOct
 
+  , type NatBaseWhile
+  ) where
+
 import Symparsec.Parser.Common
 import Symparsec.Parser.Natural.Digits
-import DeFun.Core
-import GHC.TypeLits hiding ( ErrorMessage(..) )
-import TypeLevelShow.Natural ( ShowNatDec, sShowNatDec )
-import Singleraeh.Maybe
-import Singleraeh.Either
-import Singleraeh.Natural
 
--- | Parse a binary (base 2) natural.
+-- TODO decide which version to export primarily, isolate or while
+
+{-
+The main loops here consume greedily to hopefully speed up evaluation.
+It adds to the complexity, and means we have to backtrack on failure.
+It'd be nice to assert that it /does/ help in some way.
+-}
+
+-- | Parse a binary (base 2) 'Natural'.
 type NatBin = NatBase  2 ParseDigitBinSym
 
--- | Parse an octal (base 8) natural.
+-- | Parse an octal (base 8) 'Natural'.
 type NatOct = NatBase  8 ParseDigitOctSym
 
--- | Parse a decimal (base 10) natural.
+-- | Parse a decimal (base 10) 'Natural'.
 type NatDec = NatBase 10 ParseDigitDecSym
 
--- | Parse a hexadecimal (base 16) natural. Permits mixed-case (@0-9A-Fa-f@).
+-- | Parse a hexadecimal (base 16) 'Natural'. Permits mixed-case (@0-9A-Fa-f@).
 type NatHex = NatBase 16 ParseDigitHexSym
 
--- | Parse a natural in the given base, using the given digit parser.
-type NatBase
-    :: Natural -> (Char ~> Maybe Natural) -> PParser (Maybe Natural) Natural
-type NatBase base parseDigit =
-    'PParser (NatBaseChSym base parseDigit) NatBaseEndSym Nothing
+-- | Parse a non-empty 'Natural' using the given base and digit parser.
+--
+-- Only permits parsing numbers with digits exactly one 'Char' long.
+--
+-- Returns an error if it parses zero digits, or if any character fails to
+-- parse.
+type NatBase :: Natural -> (Char ~> Maybe Natural) -> PParser Natural
+data NatBase base parseDigit s
+type instance App (NatBase base parseDigit) s =
+    NatBaseStart base parseDigit s (UnconsState s)
+type family NatBaseStart base parseDigit sCh s where
+    NatBaseStart base parseDigit sCh '(Just ch, s) =
+        NatBaseLoop base parseDigit sCh s 0 ch (parseDigit @@ ch) (UnconsState s)
+    NatBaseStart base parseDigit sCh '(Nothing, s) = 'Reply (Err EEmpty) sCh
 
-sNatBase
-    :: SNat base
-    -> SParseDigit parseDigit
-    -> SParser (SMaybe SNat) SNat (NatBase base parseDigit)
-sNatBase base parseDigit =
-    SParser (sNatBaseChSym base parseDigit) sNatBaseEndSym SNothing
+-- | Parse a 'Natural' with the given starting value.
+--
+-- Skips some extra work. May be handy for hand-written parsers.
+type NatBase1 :: Natural -> (Char ~> Maybe Natural) -> Natural -> PParser Natural
+data NatBase1 base parseDigit digit s
+type instance App (NatBase1 base parseDigit digit) s =
+    NatBase1' base parseDigit s digit (UnconsState s)
+type family NatBase1' base parseDigit sCh digit s where
+    NatBase1' base parseDigit sCh digit '(Just ch, s) =
+        NatBaseLoop base parseDigit sCh s digit ch (parseDigit @@ ch) (UnconsState s)
+    NatBase1' base parseDigit sCh digit '(Nothing, s) =
+        'Reply (OK digit) s
 
-instance (KnownNat base, SingParseDigit parseDigit)
-  => SingParser (NatBase base parseDigit) where
-    type PS (NatBase base parseDigit) = SMaybe SNat
-    type PR (NatBase base parseDigit) = SNat
-    singParser' = sNatBase natSing singParseDigit
+type EEmpty = Error1 "no digits parsed" -- TODO not great eh
+type EInvalidDigit ch base =
+    Error1 ( "not a base " ++ ShowNatDec base ++ " digit: " ++ ShowChar ch)
 
-type NatBaseCh
+type NatBaseLoop
     :: Natural
     -> (Char ~> Maybe Natural)
-    -> PParserCh (Maybe Natural) Natural
-type NatBaseCh base parseDigit ch mn = NatBaseCh' base mn (parseDigit @@ ch)
+    -> PState
+    -> PState
+    -> Natural
+    -> Char
+    -> Maybe Natural
+    -> (Maybe Char, PState)
+    -> PReply Natural
+type family NatBaseLoop base parseDigit sCh s n chCur mDigit ms where
+    -- parsed digit and have next char
+    NatBaseLoop base parseDigit sCh s n chCur (Just digit) '(Just ch, sNext) =
+        NatBaseLoop base parseDigit s sNext (n * base + digit) ch (parseDigit @@ ch) (UnconsState sNext)
+    NatBaseLoop base parseDigit sCh s n chCur (Just digit) '(Nothing, sNext) =
+        'Reply (OK (n * base + digit)) sNext
+    NatBaseLoop base parseDigit sCh s n chCur Nothing      '(_, sNext) =
+        -- we've consumed the next character, but digit parse failed:
+        -- backtrack and return error
+        'Reply (Err (EInvalidDigit chCur base)) sCh
 
-type family NatBaseCh' base mn mDigit where
-    NatBaseCh' base (Just n) (Just digit) = Cont (Just (n * base + digit))
-    NatBaseCh' base Nothing  (Just digit) = Cont (Just digit)
-    NatBaseCh' base mn       Nothing      = Err (EInvalidDigit base)
+-- | Parse a non-empty 'Natural' using the given base and digit parser.
+--
+-- Only permits parsing numbers with digits exactly one 'Char' long.
+--
+-- Returns an error if it parses zero digits, or if the first digit fails to
+-- parse. Returns success on parsing up to EOF, or just before the first failed
+-- character parse. (Should match the behaviour of Megaparsec's number parsers.)
+type NatBaseWhile :: Natural -> (Char ~> Maybe Natural) -> PParser Natural
+data NatBaseWhile base parseDigit s
+type instance App (NatBaseWhile base parseDigit) s =
+    NatBaseWhileStart base parseDigit s (UnconsState s)
+type family NatBaseWhileStart base parseDigit sCh s where
+    NatBaseWhileStart base parseDigit sCh '(Just ch, s) =
+        NatBaseWhileStart2 base parseDigit sCh s ch (parseDigit @@ ch) (UnconsState s)
+    NatBaseWhileStart base parseDigit sCh '(Nothing, s) = 'Reply (Err EEmpty) sCh
 
-type EInvalidDigit base = EBase "NatBase"
-    (Text "not a base " :<>: Text (ShowNatDec base) :<>: Text " digit")
-eInvalidDigit :: SNat base -> SE (EInvalidDigit base)
-eInvalidDigit base = withKnownSymbol (sShowNatDec base) singE
+-- TODO While1
 
-type NatBaseChSym
-    :: Natural
-    -> (Char ~> Maybe Natural)
-    -> ParserChSym (Maybe Natural) Natural
-data NatBaseChSym base parseDigit f
-type instance App (NatBaseChSym base parseDigit) f =
-    NatBaseChSym1 base parseDigit f
+type family NatBaseWhileStart2 base parseDigit sCh s chChur mDigit ms where
+    NatBaseWhileStart2 base parseDigit sCh s chCur (Just digit) '(Just ch, sNext) =
+        NatBaseWhileLoop base parseDigit s sNext digit ch (parseDigit @@ ch) (UnconsState sNext)
+    NatBaseWhileStart2 base parseDigit sCh s chCur (Just digit) '(Nothing, sNext) =
+        -- parsed first digit, no more input: done
+        'Reply (OK digit) sNext
+    NatBaseWhileStart2 base parseDigit sCh s chCur Nothing      _ =
+        -- failed to parse first digit: backtrack and error
+        'Reply (Err (EInvalidDigit chCur base)) sCh
 
-type NatBaseChSym1
+-- Note that this parser never fails.
+type NatBaseWhileLoop
     :: Natural
     -> (Char ~> Maybe Natural)
-    -> ParserChSym1 (Maybe Natural) Natural
-data NatBaseChSym1 base parseDigit ch mn
-type instance App (NatBaseChSym1 base parseDigit ch) mn =
-    NatBaseCh base parseDigit ch mn
-
-sNatBaseChSym
-    :: SNat base
-    -> SParseDigit parseDigit
-    -> SParserChSym (SMaybe SNat) SNat (NatBaseChSym base parseDigit)
-sNatBaseChSym base parseDigit = Lam2 $ \ch mn ->
-    case parseDigit @@ ch of
-      SJust digit ->
-        case mn of
-          SJust n  -> SCont $ SJust $ n %* base %+ digit
-          SNothing -> SCont $ SJust digit
-      SNothing -> SErr $ eInvalidDigit base
-
-type family NatBaseEnd mn where
-    NatBaseEnd (Just n) = Right n
-    NatBaseEnd Nothing  = Left EEmpty
-
-type EEmpty = EBase "NatBase" (Text "no digits parsed")
-eEmpty :: SE EEmpty
-eEmpty = singE
-
-type NatBaseEndSym :: ParserEndSym (Maybe Natural) Natural
-data NatBaseEndSym mn
-type instance App NatBaseEndSym mn = NatBaseEnd mn
-
-sNatBaseEndSym :: SParserEndSym (SMaybe SNat) SNat NatBaseEndSym
-sNatBaseEndSym = Lam $ \case
-  SJust n  -> SRight n
-  SNothing -> SLeft eEmpty
+    -> PState
+    -> PState
+    -> Natural
+    -> Char
+    -> Maybe Natural
+    -> (Maybe Char, PState)
+    -> PReply Natural
+type family NatBaseWhileLoop base parseDigit sCh s n chCur mDigit ms where
+    -- parsed digit and have next char
+    NatBaseWhileLoop base parseDigit sCh s n chCur (Just digit) '(Just ch, sNext) =
+        NatBaseWhileLoop base parseDigit s sNext (n * base + digit) ch (parseDigit @@ ch) (UnconsState sNext)
+    NatBaseWhileLoop base parseDigit sCh s n chCur (Just digit) '(Nothing, sNext) =
+        'Reply (OK (n * base + digit)) sNext
+    NatBaseWhileLoop base parseDigit sCh s n chCur Nothing      _ =
+        -- failed to parse next digit: backtrack and finish
+        'Reply (OK n) sCh
diff --git a/src/Symparsec/Parser/Natural/Digits.hs b/src/Symparsec/Parser/Natural/Digits.hs
--- a/src/Symparsec/Parser/Natural/Digits.hs
+++ b/src/Symparsec/Parser/Natural/Digits.hs
@@ -1,6 +1,8 @@
 {- | Parse digits from type-level 'Char's.
 
 A 'Nothing' indicates the given 'Char' was not a valid digit for the given base.
+
+raehik copied this directly from his own Symparsec library.
 -}
 
 module Symparsec.Parser.Natural.Digits where
diff --git a/src/Symparsec/Parser/Or.hs b/src/Symparsec/Parser/Or.hs
deleted file mode 100644
--- a/src/Symparsec/Parser/Or.hs
+++ /dev/null
@@ -1,330 +0,0 @@
-{-# LANGUAGE UndecidableInstances #-}
-
-module Symparsec.Parser.Or where
-
-import Symparsec.Parser
-import TypeLevelShow.Doc
-import GHC.TypeLits hiding ( ErrorMessage(..) )
-import DeFun.Core
-import Singleraeh.Tuple
-import Singleraeh.Either
-import Singleraeh.List
-
-{- | Limited parser choice. Try left; if it fails, backtrack and try right.
-     However, _the right choice must consume at least as much as the left
-     choice._ If it doesn't, then even if the right parser succeeds, it
-     will emit an error.
-
-This behaviour is due to the parser runner not supporting backtracking. We can
-emulate it by storing a record of the characters parsed so far, and "replaying"
-these on the right parser if the left parser fails. If the right parser ends
-before we finish replaying, we will have consumed extra characters that we can't
-ask the runner to revert.
-
-For example, @Literal "abcd" :<|>: Literal "ab"@ is bad. An input of @abcX@ will
-trigger the consumption error.
-
-I can't think of another way to implement this with the current parser design. I
-think it's the best we have. A more complex parser design may permit changing
-internal running state, so we could save and load state (this would permit a
-@Try p@ parser). But that's scary. And you're better off designing your
-type-level string schemas to permit non-backtracking parsing anyway...
-
-Also problematic is that we never emit a left parser error, so errors can
-degrade. Perhaps your string was one character off a successful left parse; but
-if it fails, you won't see that error.
--}
-infixl 3 :<|>:
-type (:<|>:)
-    :: PParser sl rl
-    -> PParser sr rr
-    -> PParser (OrS sl sr) (Either rl rr)
-type family pl :<|>: pr where
-    'PParser plCh plEnd s0l :<|>: 'PParser prCh prEnd s0r =
-        Or' plCh plEnd s0l prCh prEnd s0r
-
-type Or' plCh plEnd s0l prCh prEnd s0r = 'PParser
-    (OrChSym plCh prCh s0r)
-    (OrEndSym plEnd prCh prEnd s0r)
-    (Left '(s0l, '[]))
-
-type SOrS ssl ssr = SEither (STuple2 ssl (SList SChar)) ssr
-type OrS  sl  sr  = Either (sl, [Char]) sr
-type SPOr ssl srl ssr srr plCh plEnd s0l prCh prEnd s0r =
-    SParser (SOrS ssl ssr) (SEither srl srr) (Or' plCh plEnd s0l prCh prEnd s0r)
-
-sOr
-    :: SParser ssl srl ('PParser plCh plEnd s0l)
-    -> SParser ssr srr ('PParser prCh prEnd s0r)
-    -> SPOr    ssl srl ssr srr plCh plEnd s0l prCh prEnd s0r
-sOr (SParser plCh plEnd s0l) (SParser prCh prEnd s0r) = SParser
-    (sOrChSym plCh prCh s0r)
-    (sOrEndSym plEnd prCh prEnd s0r)
-    (SLeft (STuple2 s0l SNil))
-
-instance
-  ( pl ~ 'PParser plCh plEnd s0l
-  , pr ~ 'PParser prCh prEnd s0r
-  , SingParser pl
-  , SingParser pr
-  ) => SingParser (Or' plCh plEnd s0l prCh prEnd s0r) where
-    type PS (Or' plCh plEnd s0l prCh prEnd s0r) = SOrS
-        (PS ('PParser plCh plEnd s0l))
-        (PS ('PParser prCh prEnd s0r))
-    type PR (Or' plCh plEnd s0l prCh prEnd s0r) = SEither
-        (PR ('PParser plCh plEnd s0l))
-        (PR ('PParser prCh prEnd s0r))
-    singParser' = sOr (singParser @pl) (singParser @pr)
-
-type OrCh
-    :: ParserChSym sl rl
-    -> ParserChSym sr rr
-    -> sr
-    -> PParserCh (OrS sl sr) (Either rl rr)
-type family OrCh plCh prCh sr ch s where
-    -- | parsing left
-    OrCh plCh prCh s0r ch (Left  '(sl, chs)) =
-        OrChL prCh s0r ch chs (plCh @@ ch @@ sl)
-
-    -- | parsing right (after left failed and was successfully replayed)
-    OrCh plCh prCh _  ch (Right sr) =
-        OrChR (prCh @@ ch @@ sr)
-
-type OrChL
-    :: ParserChSym sr rr
-    -> sr
-    -> Char
-    -> [Char]
-    -> PResult sl rl
-    -> PResult (Either (sl, [Char]) sr) (Either rl rr)
-type family OrChL prCh s0r chLast chs resl where
-    -- | left parser OK, continue
-    OrChL _    _   chLast chs (Cont sl) = Cont (Left  '(sl, chLast : chs))
-
-    -- | left parser OK, done
-    OrChL _    _   _      _   (Done rl) = Done (Left  rl)
-
-    -- | left parser failed: ignore, replay consumed characters on right parser
-    OrChL prCh s0r chLast chs (Err  _ ) =
-        OrChLReplay prCh chLast (Reverse chs) (Cont s0r)
-
-type OrChLReplay
-    :: ParserChSym sr rr
-    -> Char
-    -> [Char]
-    -> PResult sr rr
-    -> PResult (Either (sl, [Char]) sr) (Either rl rr)
-type family OrChLReplay prCh chLast chs resr where
-    -- | right parser OK, keep replaying
-    OrChLReplay prCh chLast (ch : chs) (Cont sr) =
-        OrChLReplay prCh chLast chs (prCh @@ ch @@ sr)
-    --
-    -- | right parser OK, final replay char
-    OrChLReplay prCh chLast '[]        (Cont sr) = OrChR (prCh @@ chLast @@ sr)
-
-    -- | right parser fail: wrap error
-    OrChLReplay prCh chLast chs        (Err  er) = Err (EOrR er)
-
-    -- | right parser done but still replaying! no choice but to error out
-    OrChLReplay prCh chLast chs        (Done rr) = Err EOrStillReplaying
-        -- Done (Right rr) -- TODO
-
-sOrChLReplay
-    :: SParserChSym ssr srr prCh
-    -> SChar chLast
-    -> SList SChar chs
-    -> SResult ssr srr resr
-    -> SResult (SOrS ssl ssr) (SEither srl srr)
-        (OrChLReplay prCh chLast chs resr)
-sOrChLReplay prCh chLast chs resr =
-    case chs of
-      SCons ch chs' ->
-        case resr of
-          SCont  sr ->
-            sOrChLReplay prCh chLast chs' (prCh @@ ch @@ sr)
-          SDone _rr -> SErr eOrStillReplaying
-          SErr   er -> SErr $ eOrR er
-      SNil ->
-        case resr of
-          SCont  sr -> sOrChR (prCh @@ chLast @@ sr)
-          SDone _rr -> SErr eOrStillReplaying
-          SErr   er -> SErr $ eOrR er
-
-type EOrR er = EIn "Or(R)" er
-eOrR :: SE er -> SE (EOrR er)
-eOrR er = SEIn symbolSing er
-
-type EOrStillReplaying = EBase "Or"
-    (Text "right parser much consume at least as much as the failed left parser")
-eOrStillReplaying :: SE EOrStillReplaying
-eOrStillReplaying = singE
-
-type family OrChR resr where
-    OrChR (Cont sr) = Cont (Right sr)
-    OrChR (Done rr) = Done (Right rr)
-    OrChR (Err  er) = Err (EOrR er)
-
-sOrChR
-    :: SResult ssr srr resr
-    -> SResult (SOrS ssl ssr) (SEither srl srr) (OrChR resr)
-sOrChR = \case
-  SCont sr -> SCont $ SRight sr
-  SDone rr -> SDone $ SRight rr
-  SErr  er -> SErr  $ eOrR er
-
-type OrEnd
-    :: ParserEndSym sl rl
-    -> ParserChSym  sr rr
-    -> ParserEndSym sr rr
-    -> sr
-    -> PParserEnd (Either (sl, [Char]) sr) (Either rl rr)
-type family OrEnd plEnd prCh prEnd sr res where
-    -- | input ended during left parser
-    OrEnd plEnd prCh prEnd s0r (Left  '(sl, chs)) =
-        OrEndL prCh prEnd s0r chs (plEnd @@ sl)
-
-    -- | input ended during right parser: call right end
-    OrEnd plEnd prCh prEnd _   (Right sr)         = OrEndR (prEnd @@ sr)
-
-type OrEndR :: PResultEnd rr -> PResultEnd (Either rl rr)
-type family OrEndR resr where
-    OrEndR (Right rr) = Right (Right rr)
-    OrEndR (Left  er) = Left  (EOrR er)
-
-sOrEndR
-    :: SResultEnd srr resr
-    -> SResultEnd (SEither srl srr) (OrEndR resr)
-sOrEndR = \case
-  SRight rr -> SRight $ SRight rr
-  SLeft  er -> SLeft  $ eOrR er
-
-type OrEndL
-    :: ParserChSym  sr rr
-    -> ParserEndSym sr rr
-    -> sr
-    -> [Char]
-    -> Either PE rl
-    -> Either PE (Either rl rr)
-type family OrEndL prCh prEnd s0r chs resl where
-    -- | input ended during left parser and left end succeeeded: phew
-    OrEndL prCh prEnd s0r chs (Right rl) = Right (Left rl)
-
-    -- | input ended during left parser and left end failed. replay on right,
-    --   then eventually call right end
-    OrEndL prCh prEnd s0r chs (Left  el) =
-        OrEndLReplay prCh prEnd (Reverse chs) (Cont s0r)
-
-sOrEndL
-    :: SParserChSym  ssr srr prCh
-    -> SParserEndSym ssr srr prEnd
-    -> ssr s0r
-    -> SList SChar chs
-    -> SResultEnd srl resl
-    -> SResultEnd (SEither srl srr) (OrEndL prCh prEnd s0r chs resl)
-sOrEndL prCh prEnd s0r chs = \case
-  SRight  rl -> SRight $ SLeft rl
-  SLeft  _el -> sOrEndLReplay prCh prEnd (sReverse chs) (SCont s0r)
-
-type OrEndLReplay
-    :: ParserChSym  sr rr
-    -> ParserEndSym sr rr
-    -> [Char]
-    -> PResult sr rr
-    -> Either PE (Either rl rr)
-type family OrEndLReplay prCh prEnd chs resr where
-    -- | right parser OK, keep replaying
-    OrEndLReplay prCh prEnd (ch : chs) (Cont sr) =
-        OrEndLReplay prCh prEnd chs (prCh @@ ch @@ sr)
-
-    -- | replay complete
-    OrEndLReplay prCh prEnd '[]        resr      = OrEndLReplay' prEnd resr
-
-    -- | right parser fail: wrap error
-    OrEndLReplay prCh prEnd chs        (Err  er) = Left (EOrR er)
-
-    -- | right parser done but still replaying! no choice but to error out
-    OrEndLReplay prCh prEnd chs        (Done rr) = Left EOrStillReplaying
-        -- Right (Right rr) TODO
-
-sOrEndLReplay
-    :: SParserChSym  ssr srr prCh
-    -> SParserEndSym ssr srr prEnd
-    -> SList SChar chs
-    -> SResult ssr srr resr
-    -> SResultEnd (SEither srl srr) (OrEndLReplay prCh prEnd chs resr)
-sOrEndLReplay prCh prEnd chs resr =
-    case chs of
-      SCons ch chs' ->
-        case resr of
-          SCont  sr ->
-            sOrEndLReplay prCh prEnd chs' (prCh @@ ch @@ sr)
-          SErr   er -> SLeft $ eOrR er
-          SDone _rr -> SLeft eOrStillReplaying
-      SNil ->
-        case resr of
-          SCont sr -> sOrEndR $ prEnd @@ sr
-          SDone rr -> SRight  $ SRight rr
-          SErr  er -> SLeft   $ eOrR er
-
-type family OrEndLReplay' prEnd resr where
-    OrEndLReplay' prEnd (Cont sr) = OrEndR (prEnd @@ sr)
-    OrEndLReplay' prEnd (Done rr) = Right  (Right rr)
-    OrEndLReplay' prEnd (Err  er) = Left   (EOrR er)
-
-type OrChSym
-    :: ParserChSym sl rl
-    -> ParserChSym sr rr
-    -> sr
-    -> ParserChSym (OrS sl sr) (Either rl rr)
-data OrChSym plCh prCh s0r f
-type instance App (OrChSym plCh prCh s0r) f = OrChSym1 plCh prCh s0r f
-
-type OrChSym1
-    :: ParserChSym sl rl
-    -> ParserChSym sr rr
-    -> sr
-    -> ParserChSym1 (OrS sl sr) (Either rl rr)
-data OrChSym1 plCh prCh sr ch s
-type instance App (OrChSym1 plCh prCh sr ch) s = OrCh plCh prCh sr ch s
-
-sOrChSym
-    :: SParserChSym ssl srl plCh
-    -> SParserChSym ssr srr prCh
-    -> ssr s0r
-    -> SParserChSym (SOrS ssl ssr) (SEither srl srr) (OrChSym plCh prCh s0r)
-sOrChSym plCh prCh s0r = Lam2 $ \ch -> \case
-  SLeft  (STuple2 sl chs) -> sOrChL prCh s0r ch chs (plCh @@ ch @@ sl)
-  SRight sr -> sOrChR (prCh @@ ch @@ sr)
-
-sOrChL
-    :: SParserChSym ssr srr prCh
-    -> ssr s0r
-    -> SChar chLast
-    -> SList SChar chs
-    -> SResult ssl srl resl
-    -> SResult (SOrS ssl ssr) (SEither srl srr) (OrChL prCh s0r chLast chs resl)
-sOrChL prCh s0r chLast chs = \case
-  SCont  sl -> SCont $ SLeft $ STuple2 sl $ SCons chLast chs
-  SDone  rl -> SDone $ SLeft rl
-  SErr  _el -> sOrChLReplay prCh chLast (sReverse chs) (SCont s0r)
-
-type OrEndSym
-    :: ParserEndSym sl rl
-    -> ParserChSym  sr rr
-    -> ParserEndSym sr rr
-    -> sr
-    -> ParserEndSym (Either (sl, [Char]) sr) (Either rl rr)
-data OrEndSym plEnd prCh prEnd s0r s
-type instance App (OrEndSym plEnd prCh prEnd s0r) s =
-    OrEnd plEnd prCh prEnd s0r s
-
-sOrEndSym
-    :: SParserEndSym ssl srl plEnd
-    -> SParserChSym  ssr srr prCh
-    -> SParserEndSym ssr srr prEnd
-    -> ssr s0r
-    -> SParserEndSym (SOrS ssl ssr) (SEither srl srr)
-        (OrEndSym plEnd prCh prEnd s0r)
-sOrEndSym plEnd prCh prEnd s0r = Lam $ \case
-  SLeft (STuple2 sl chs) -> sOrEndL prCh prEnd s0r chs (plEnd @@ sl)
-  SRight sr -> sOrEndR $ prEnd @@ sr
diff --git a/src/Symparsec/Parser/Skip.hs b/src/Symparsec/Parser/Skip.hs
--- a/src/Symparsec/Parser/Skip.hs
+++ b/src/Symparsec/Parser/Skip.hs
@@ -1,66 +1,21 @@
 {-# LANGUAGE UndecidableInstances #-}
 
-module Symparsec.Parser.Skip where
+module Symparsec.Parser.Skip ( type Skip, type SkipUnsafe ) where
 
 import Symparsec.Parser.Common
-import GHC.TypeLits hiding ( ErrorMessage(..) )
-import TypeLevelShow.Natural ( ShowNatDec, sShowNatDec )
-import Data.Type.Equality
-import Singleraeh.Tuple
-import Singleraeh.Either
-import Singleraeh.Natural
-import DeFun.Core
-import Unsafe.Coerce ( unsafeCoerce )
-
--- | Skip forward @n@ characters. Fails if fewer than @n@ characters are
---   available'.
-type Skip :: Natural -> PParser Natural ()
-type Skip n = 'PParser SkipChSym SkipEndSym n
-
-sSkip :: SNat n -> SParser SNat SUnit (Skip n)
-sSkip n = SParser sSkipChSym sSkipEndSym n
-
-instance KnownNat n => SingParser (Skip n) where
-    type PS (Skip n) = SNat
-    type PR (Skip n) = SUnit
-    singParser' = sSkip SNat
-
-type SkipCh :: PParserCh Natural ()
-type family SkipCh ch n where
-    SkipCh _ 0 = Done '()
-    SkipCh _ n = Cont (n-1)
-
-type SkipChSym :: ParserChSym Natural ()
-data SkipChSym f
-type instance App SkipChSym f = SkipChSym1 f
-
-type SkipChSym1 :: ParserChSym1 Natural ()
-data SkipChSym1 ch n
-type instance App (SkipChSym1 ch) n = SkipCh ch n
-
-sSkipChSym :: SParserChSym SNat SUnit SkipChSym
-sSkipChSym = Lam2 $ \_ n ->
-    case testEquality n (SNat @0) of
-      Just Refl -> SDone SUnit
-      Nothing   -> unsafeCoerce $ SCont $ n %- (SNat @1)
-
-type SkipEnd :: PParserEnd Natural ()
-type family SkipEnd n where
-    SkipEnd 0 = Right '()
-    SkipEnd n = Left (ESkipPastEnd n)
-
-type ESkipPastEnd n = EBase "Skip"
-    (      Text "tried to skip "
-      :<>: Text (ShowNatDec n) :<>: Text " chars from empty string")
-eSkipPastEnd :: SNat n -> SE (ESkipPastEnd n)
-eSkipPastEnd n = withKnownSymbol (sShowNatDec n) singE
+import Symparsec.Parser.Ensure
+import Symparsec.Parser.Applicative
+import Data.Type.Symbol qualified as Symbol
 
-type SkipEndSym :: ParserEndSym Natural ()
-data SkipEndSym n
-type instance App SkipEndSym n = SkipEnd n
+-- | Skip forward @n@ characters. Fails if fewer than @n@ characters remain.
+type Skip :: Natural -> PParser ()
+type Skip n = Ensure n *> SkipUnsafe n
 
-sSkipEndSym :: SParserEndSym SNat SUnit SkipEndSym
-sSkipEndSym = Lam $ \n ->
-    case testEquality n (SNat @0) of
-      Just Refl -> SRight SUnit
-      Nothing   -> unsafeCoerce $ SLeft $ eSkipPastEnd n
+-- | Skip forward @n@ characters. @n@ must be less than or equal to the number
+--   of remaining characters. (Fairly unhelpful; use 'Skip' instead.)
+type SkipUnsafe :: Natural -> PParser ()
+data SkipUnsafe n s
+type instance App (SkipUnsafe n) s = SkipUnsafe' n s
+type family SkipUnsafe' n s where
+    SkipUnsafe' n ('State rem len idx) =
+        'Reply (OK '()) ('State (Symbol.Drop n rem) (len-n) (idx+n))
diff --git a/src/Symparsec/Parser/Take.hs b/src/Symparsec/Parser/Take.hs
--- a/src/Symparsec/Parser/Take.hs
+++ b/src/Symparsec/Parser/Take.hs
@@ -1,71 +1,24 @@
 {-# LANGUAGE UndecidableInstances #-}
 
-module Symparsec.Parser.Take where
+module Symparsec.Parser.Take ( type Take, type TakeSym ) where
 
 import Symparsec.Parser.Common
-import Singleraeh.Symbol ( RevCharsToSymbol, revCharsToSymbol )
-import Singleraeh.List ( SList(..) )
-import Singleraeh.Tuple ( STuple2(..) )
-import Data.Type.Equality
-import Singleraeh.Natural ( (%-) )
-import Singleraeh.Either ( SEither(..) )
-import TypeLevelShow.Natural
-import GHC.TypeLits hiding ( ErrorMessage(..) )
-import Unsafe.Coerce ( unsafeCoerce )
-import DeFun.Core
+import Singleraeh.Symbol ( type RevCharsToSymbol )
 
 -- | Return the next @n@ characters.
-type Take n = 'PParser TakeChSym TakeEndSym '(n, '[])
-
-type STakeS = STuple2 SNat (SList SChar)
-type  TakeS = (Natural, [Char])
-
-sTake :: SNat n -> SParser STakeS SSymbol (Take n)
-sTake n = SParser sTakeChSym sTakeEndSym (STuple2 n SNil)
-
-instance KnownNat n => SingParser (Take n) where
-    type PS (Take n) = STakeS
-    type PR (Take n) = SSymbol
-    singParser' = sTake SNat
-
-type TakeCh :: PParserCh TakeS Symbol
-type family TakeCh ch s where
-    TakeCh ch '(0, chs) = Done (RevCharsToSymbol chs)
-    TakeCh ch '(n, chs) = Cont '(n-1, ch : chs)
-
-type TakeChSym :: ParserChSym TakeS Symbol
-data TakeChSym f
-type instance App TakeChSym f = TakeChSym1 f
-
-sTakeChSym :: SParserChSym STakeS SSymbol TakeChSym
-sTakeChSym = Lam2 $ \ch (STuple2 n chs) ->
-    case testEquality n (SNat @0) of
-      Just Refl -> SDone $ revCharsToSymbol chs
-      Nothing   ->
-        unsafeCoerce $ SCont $ STuple2 (n %- (SNat @1)) (SCons ch chs)
-
-type TakeChSym1 :: ParserChSym1 TakeS Symbol
-data TakeChSym1 ch s
-type instance App (TakeChSym1 ch) s = TakeCh ch s
-
-type TakeEnd :: PParserEnd TakeS Symbol
-type family TakeEnd s where
-    TakeEnd '(0, chs) = Right (RevCharsToSymbol chs)
-    TakeEnd '(n, _)   = Left (ETakeEnd n)
-
-type ETakeEnd n = EBase "Take"
-    (      Text "tried to take "
-      :<>: Text (ShowNatDec n) :<>: Text " chars from empty string")
-
-eTakeEnd :: SNat n -> SE (ETakeEnd n)
-eTakeEnd sn = withKnownSymbol (sShowNatDec sn) singE
+type Take :: Natural -> PParser Symbol
+data Take n s
+type instance App (Take n) s = Take' '[] n s (UnconsState s)
+type family Take' chs n sPrev s where
+    Take' chs 0 sPrev _             = 'Reply (OK (RevCharsToSymbol chs)) sPrev
+    Take' chs n sPrev '(Just ch, s) = Take' (ch:chs) (n-1) s (UnconsState s)
+    Take' chs n sPrev '(Nothing, s) = 'Reply (Err (ETakeEnd n)) sPrev
 
-type TakeEndSym :: ParserEndSym TakeS Symbol
-data TakeEndSym s
-type instance App TakeEndSym s = TakeEnd s
+type ETakeEnd :: Natural -> PError
+type ETakeEnd n = Error1
+    ( "tried to take " ++ ShowNatDec n ++ " chars from empty string" )
 
-sTakeEndSym :: SParserEndSym STakeS SSymbol TakeEndSym
-sTakeEndSym = Lam $ \(STuple2 n chs) ->
-    case testEquality n (SNat @0) of
-      Just Refl -> SRight $ revCharsToSymbol chs
-      Nothing   -> unsafeCoerce $ SLeft $ eTakeEnd n
+-- | 'Take' defunctionalization symbol.
+type TakeSym :: Natural ~> PParser Symbol
+data TakeSym n
+type instance App TakeSym n = Take n
diff --git a/src/Symparsec/Parser/TakeRest.hs b/src/Symparsec/Parser/TakeRest.hs
--- a/src/Symparsec/Parser/TakeRest.hs
+++ b/src/Symparsec/Parser/TakeRest.hs
@@ -1,39 +1,25 @@
 {-# LANGUAGE UndecidableInstances #-}
 
-module Symparsec.Parser.TakeRest where
+module Symparsec.Parser.TakeRest ( type TakeRest ) where
 
 import Symparsec.Parser.Common
-import Singleraeh.Symbol ( RevCharsToSymbol, revCharsToSymbol )
-import Singleraeh.List ( SList(..) )
-import Singleraeh.Either ( SEither(..) )
-import GHC.TypeLits hiding ( ErrorMessage(..) )
-import DeFun.Core
-
--- | Return the remaining input string.
-type TakeRest = 'PParser TakeRestChSym TakeRestEndSym '[]
-
-sTakeRest :: SParser (SList SChar) SSymbol TakeRest
-sTakeRest = SParser sTakeRestChSym sTakeRestEndSym SNil
-
-instance SingParser TakeRest where
-    type PS TakeRest = SList SChar
-    type PR TakeRest = SSymbol
-    singParser' = sTakeRest
-
-type TakeRestChSym :: ParserChSym [Char] Symbol
-data TakeRestChSym f
-type instance App TakeRestChSym f = TakeRestChSym1 f
-
-type TakeRestChSym1 :: ParserChSym1 [Char] Symbol
-data TakeRestChSym1 ch chs
-type instance App (TakeRestChSym1 ch) chs = Cont (ch : chs)
+import qualified Data.Type.Symbol as Symbol
 
-sTakeRestChSym :: SParserChSym (SList SChar) SSymbol TakeRestChSym
-sTakeRestChSym = Lam2 $ \ch chs -> SCont $ SCons ch chs
+-- | Consume and return the rest of the input string.
+--
+-- Never fails. May return the empty string.
+type TakeRest :: PParser Symbol
+data TakeRest s
+type instance App TakeRest s = TakeRest' s
+type family TakeRest' s where
+    TakeRest' ('State rem len idx) =
+        'Reply (OK (Symbol.Take len rem)) ('State (Symbol.Drop len rem) 0 (idx+len))
 
-type TakeRestEndSym :: ParserEndSym [Char] Symbol
-data TakeRestEndSym chs
-type instance App TakeRestEndSym chs = Right (RevCharsToSymbol chs)
+{-
+import GHC.TypeLits
+import DeFun.Core
 
-sTakeRestEndSym :: SParserEndSym (SList SChar) SSymbol TakeRestEndSym
-sTakeRestEndSym = Lam $ \chs -> SRight $ revCharsToSymbol chs
+sTakeRest :: SParser SSymbol TakeRest
+sTakeRest = Lam $ \(SState srem slen sidx) ->
+        SReply (SOK _) (SState _ (SNat @0) _)
+-}
diff --git a/src/Symparsec/Parser/TakeWhile.hs b/src/Symparsec/Parser/TakeWhile.hs
new file mode 100644
--- /dev/null
+++ b/src/Symparsec/Parser/TakeWhile.hs
@@ -0,0 +1,34 @@
+{-# LANGUAGE UndecidableInstances #-}
+
+module Symparsec.Parser.TakeWhile ( type TakeWhile ) where
+
+import Symparsec.Parser.Common
+import Singleraeh.Symbol ( type RevCharsToSymbol )
+
+-- | Take zero or more 'Char's for which the supplied predicate holds.
+--
+-- May also be defined via
+-- @'Symparsec.Parser.While.While' chPred 'Symparsec.Parser.TakeRest.TakeRest'@,
+-- but a custom implementation is more efficient.
+type TakeWhile :: (Char ~> Bool) -> PParser Symbol
+data TakeWhile chPred s
+type instance App (TakeWhile chPred) s = TakeWhileStart chPred s (UnconsState s)
+
+type family TakeWhileStart chPred sPrev ms where
+    TakeWhileStart chPred sPrev '(Just ch, s) =
+        TakeWhileLoop chPred sPrev s ch '[] (chPred @@ ch) (UnconsState s)
+    TakeWhileStart chPred sPrev '(Nothing, s) =
+        'Reply (OK "") sPrev
+
+type family TakeWhileLoop chPred sPrev sCh ch taken res ms where
+    -- next char succeeded and not EOF
+    TakeWhileLoop chPred sPrev sCh ch taken True '(Just chNext, s) =
+        TakeWhileLoop chPred sCh s chNext (ch:taken) (chPred @@ chNext) (UnconsState s)
+
+    -- next char succeeded and EOF: end
+    TakeWhileLoop chPred sPrev sCh ch taken True '(Nothing, s) =
+        'Reply (OK (RevCharsToSymbol (ch:taken))) sCh -- @sCh == s@ should hold
+
+    -- next char failed: backtrack and end
+    TakeWhileLoop chPred sPrev sCh ch taken False _ =
+        'Reply (OK (RevCharsToSymbol taken)) sPrev
diff --git a/src/Symparsec/Parser/Then.hs b/src/Symparsec/Parser/Then.hs
deleted file mode 100644
--- a/src/Symparsec/Parser/Then.hs
+++ /dev/null
@@ -1,187 +0,0 @@
-{-# LANGUAGE UndecidableInstances #-}
-
-module Symparsec.Parser.Then where
-
-import Symparsec.Parser.Common
-import Singleraeh.Either ( SEither(..) )
-import Singleraeh.Tuple ( STuple2(..) )
-import DeFun.Core
-
-type SPThen ssl srl ssr srr plCh plEnd s0l prCh prEnd s0r =
-    SParser
-        (SEither ssl (STuple2 srl ssr))
-        (STuple2 srl srr)
-        (Then' plCh plEnd s0l prCh prEnd s0r)
-
-sThen
-    :: SParser ssl srl ('PParser plCh plEnd s0l)
-    -> SParser ssr srr ('PParser prCh prEnd s0r)
-    -> SPThen  ssl srl ssr srr plCh plEnd s0l prCh prEnd s0r
-sThen (SParser plCh plEnd s0l) (SParser prCh prEnd s0r) =
-    SParser (sThenChSym plCh prCh s0r) (sThenEndSym plEnd prEnd s0r) (SLeft s0l)
-
-instance
-  -- Shame I can't use pl, pr in associated type synonyms! :(
-  ( pl ~ 'PParser plCh plEnd s0l
-  , pr ~ 'PParser prCh prEnd s0r
-  , SingParser pl
-  , SingParser pr
-  ) => SingParser (Then' plCh plEnd s0l prCh prEnd s0r) where
-    type PS (Then' plCh plEnd s0l prCh prEnd s0r) =
-        SEither
-            (PS ('PParser plCh plEnd s0l))
-            (STuple2
-                (PR ('PParser plCh plEnd s0l))
-                (PS ('PParser prCh prEnd s0r)))
-    type PR (Then' plCh plEnd s0l prCh prEnd s0r) =
-        STuple2
-            (PR ('PParser plCh plEnd s0l))
-            (PR ('PParser prCh prEnd s0r))
-    singParser' = sThen (singParser @pl) (singParser @pr)
-
--- | Sequence two parsers, running left then right, and return both results.
-infixl 4 :<*>:
-type (:<*>:)
-    :: PParser sl rl
-    -> PParser sr rr
-    -> PParser (Either sl (rl, sr)) (rl, rr)
-type family pl :<*>: pr where
-    'PParser plCh plEnd s0l :<*>: 'PParser prCh prEnd s0r =
-        Then' plCh plEnd s0l prCh prEnd s0r
-
-type Then'
-    :: ParserChSym  sl rl
-    -> ParserEndSym sl rl
-    -> sl
-    -> ParserChSym  sr rr
-    -> ParserEndSym sr rr
-    -> sr
-    -> PParser (Either sl (rl, sr)) (rl, rr)
-type Then' plCh plEnd s0l prCh prEnd s0r =
-    'PParser (ThenChSym plCh prCh s0r) (ThenEndSym plEnd prEnd s0r) (Left s0l)
-
-type ThenCh
-    :: ParserChSym sl rl
-    -> ParserChSym sr rr
-    -> sr
-    -> PParserCh (Either sl (rl, sr)) (rl, rr)
-type family ThenCh plCh prCh s0r ch s where
-    ThenCh plCh prCh s0r ch (Left  sl) =
-        ThenChL prCh s0r ch (plCh @@ ch @@ sl)
-    ThenCh plCh prCh s0r ch (Right '(rl, sr)) =
-        ThenChR rl (prCh @@ ch @@ sr)
-
-type family ThenChL prCh s0r ch resl where
-    ThenChL prCh s0r ch (Cont sl) = Cont (Left  sl)
-    ThenChL prCh s0r ch (Done rl) =
-        -- 'Done' doesn't consume, so re-parse with the R parser.
-        ThenChR rl (prCh @@ ch @@ s0r)
-    ThenChL prCh s0r ch (Err  el) = Err  (EThenChL el)
-
-type EThenChL el = EIn "Then(L)" el
-eThenChL :: SE el -> SE (EThenChL el)
-eThenChL el = withSingE el $ singE
-
-type family ThenChR rl resr where
-    ThenChR rl (Cont sr) = Cont (Right '(rl, sr))
-    ThenChR rl (Done rr) = Done '(rl, rr)
-    ThenChR rl (Err  er) = Err  (EThenChR er)
-
-type EThenChR er = EIn "Then(R)" er
-eThenChR :: SE er -> SE (EThenChR er)
-eThenChR er = withSingE er $ singE
-
-sThenChR
-    :: srl rl
-    -> SResult ssr srr resr
-    -> SResult (SEither ssl (STuple2 srl ssr)) (STuple2 srl srr)
-        (ThenChR rl resr)
-sThenChR rl = \case
-  SCont sr -> SCont $ SRight $ STuple2 rl sr
-  SDone rr -> SDone $ STuple2 rl rr
-  SErr  er -> SErr  $ eThenChR er
-
-sThenChSym
-    :: SParserChSym ssl srl plCh
-    -> SParserChSym ssr srr prCh
-    -> ssr sr
-    -> SParserChSym (SEither ssl (STuple2 srl ssr)) (STuple2 srl srr)
-        (ThenChSym plCh prCh sr)
-sThenChSym plCh prCh s0r = Lam2 $ \ch -> \case
-  SLeft sl ->
-    case plCh @@ ch @@ sl of
-      SCont sl' -> SCont $ SLeft sl'
-      SDone rl  -> sThenChR rl (prCh @@ ch @@ s0r)
-      SErr  el  -> SErr  $ eThenChL el
-  SRight (STuple2 rl sr) -> sThenChR rl (prCh @@ ch @@ sr)
-
-type ThenChSym
-    :: ParserChSym sl rl
-    -> ParserChSym sr rr
-    -> sr
-    -> ParserChSym (Either sl (rl, sr)) (rl, rr)
-data ThenChSym plCh prCh s0r f
-type instance App (ThenChSym plCh prCh s0r) f = ThenChSym1 plCh prCh s0r f
-
-type ThenChSym1
-    :: ParserChSym sl rl
-    -> ParserChSym sr rr
-    -> sr
-    -> ParserChSym1 (Either sl (rl, sr)) (rl, rr)
-data ThenChSym1 plCh prCh s0r ch s
-type instance App (ThenChSym1 plCh prCh s0r ch) s = ThenCh plCh prCh s0r ch s
-
-type family ThenEnd plEnd prEnd s0r s where
-    -- | EOT during R: call R end
-    ThenEnd plEnd prEnd s0r (Right '(rl, sr)) = ThenEndR rl    (prEnd @@ sr)
-    -- | EOT during L: call L end, pass R end
-    ThenEnd plEnd prEnd s0r (Left sl)         = ThenEndL prEnd s0r (plEnd @@ sl)
-
-type family ThenEndR rl res where
-    -- | EOT during R, R end succeeds: success
-    ThenEndR rl (Right rr) = Right '(rl, rr)
-    -- | EOT during R, R end fails: error
-    ThenEndR rl (Left  er) = Left  (EThenEndR er)
-
-type EThenEndR er = EIn "Then(R) end" er
-eThenEndR :: SE er -> SE (EThenEndR er)
-eThenEndR er = withSingE er $ singE
-
-sThenEndR
-    :: srl rl
-    -> SResultEnd srr res
-    -> SResultEnd (STuple2 srl srr) (ThenEndR rl res)
-sThenEndR rl = \case
-  SRight rr -> SRight $ STuple2 rl rr
-  SLeft  er -> SLeft  $ eThenEndR er
-
-type family ThenEndL prEnd s0r res where
-    -- | EOT during L, L end succeeds: call R end on initial R state
-    ThenEndL prEnd s0r (Right rl) = ThenEndR rl (prEnd @@ s0r)
-    -- | EOT during L, L end fails: error
-    ThenEndL prEnd s0r (Left  el) = Left (EThenEndL el)
-
-type EThenEndL er = EIn "Then(L) end" er
-eThenEndL :: SE er -> SE (EThenEndL er)
-eThenEndL er = withSingE er $ singE
-
-sThenEndSym
-    :: SParserEndSym ssl srl plEnd
-    -> SParserEndSym ssr srr prEnd
-    -> ssr s0r
-    -> SParserEndSym (SEither ssl (STuple2 srl ssr)) (STuple2 srl srr)
-        (ThenEndSym plEnd prEnd s0r)
-sThenEndSym plEnd prEnd s0r = Lam $ \case
-  SRight (STuple2 rl sr) -> sThenEndR rl (prEnd @@ sr)
-  SLeft  sl ->
-    case plEnd @@ sl of
-      SRight rl -> sThenEndR rl (prEnd @@ s0r)
-      SLeft  el -> SLeft $ eThenEndL el
-
-type ThenEndSym
-    :: ParserEndSym sl rl
-    -> ParserEndSym sr rr
-    -> sr
-    -> ParserEndSym (Either sl (rl, sr)) (rl, rr)
-data ThenEndSym plEnd prEnd s0r s
-type instance App (ThenEndSym plEnd prEnd s0r) s = ThenEnd plEnd prEnd s0r s
diff --git a/src/Symparsec/Parser/Then/VoidLeft.hs b/src/Symparsec/Parser/Then/VoidLeft.hs
deleted file mode 100644
--- a/src/Symparsec/Parser/Then/VoidLeft.hs
+++ /dev/null
@@ -1,179 +0,0 @@
-{-# LANGUAGE UndecidableInstances #-}
-
-module Symparsec.Parser.Then.VoidLeft where
-
-import Symparsec.Parser.Common
-import Singleraeh.Either ( SEither(..) )
-import DeFun.Core
-
-type SPThenVL ssl srl ssr srr plCh plEnd s0l prCh prEnd s0r =
-    SParser
-        (SEither ssl ssr)
-        srr
-        (ThenVL' plCh plEnd s0l prCh prEnd s0r)
-
-sThenVL
-    :: SParser   ssl srl ('PParser plCh plEnd s0l)
-    -> SParser   ssr srr ('PParser prCh prEnd s0r)
-    -> SPThenVL  ssl srl ssr srr plCh plEnd s0l prCh prEnd s0r
-sThenVL (SParser plCh plEnd s0l) (SParser prCh prEnd s0r) =
-    SParser (sThenVLChSym plCh prCh s0r) (sThenVLEndSym plEnd prEnd s0r) (SLeft s0l)
-
-instance
-  ( pl ~ 'PParser plCh plEnd s0l
-  , pr ~ 'PParser prCh prEnd s0r
-  , SingParser pl
-  , SingParser pr
-  ) => SingParser (ThenVL' plCh plEnd s0l prCh prEnd s0r) where
-    type PS (ThenVL' plCh plEnd s0l prCh prEnd s0r) =
-        SEither
-            (PS ('PParser plCh plEnd s0l))
-            (PS ('PParser prCh prEnd s0r))
-    type PR (ThenVL' plCh plEnd s0l prCh prEnd s0r) =
-        PR ('PParser prCh prEnd s0r)
-    singParser' = sThenVL (singParser @pl) (singParser @pr)
-
--- | Sequence two parsers, running left then right, and discard the return value
---   of the left parser.
-infixl 4 :*>:
-type (:*>:)
-    :: PParser sl rl
-    -> PParser sr rr
-    -> PParser (Either sl sr) rr
-type family pl :*>: pr where
-    'PParser plCh plEnd s0l :*>: 'PParser prCh prEnd s0r =
-        ThenVL' plCh plEnd s0l prCh prEnd s0r
-
-type ThenVL'
-    :: ParserChSym  sl rl
-    -> ParserEndSym sl rl
-    -> sl
-    -> ParserChSym  sr rr
-    -> ParserEndSym sr rr
-    -> sr
-    -> PParser (Either sl sr) rr
-type ThenVL' plCh plEnd s0l prCh prEnd s0r =
-    'PParser (ThenVLChSym plCh prCh s0r) (ThenVLEndSym plEnd prEnd s0r) (Left s0l)
-
-type ThenVLCh
-    :: ParserChSym sl rl
-    -> ParserChSym sr rr
-    -> sr
-    -> PParserCh (Either sl sr) rr
-type family ThenVLCh plCh prCh s0r ch s where
-    ThenVLCh plCh prCh s0r ch (Left  sl) =
-        ThenVLChL prCh s0r ch (plCh @@ ch @@ sl)
-    ThenVLCh plCh prCh s0r ch (Right sr) =
-        ThenVLChR (prCh @@ ch @@ sr)
-
-type family ThenVLChL prCh s0r ch resl where
-    ThenVLChL prCh s0r ch (Cont sl) = Cont (Left  sl)
-    ThenVLChL prCh s0r ch (Done rl) =
-        -- 'Done' doesn't consume, so re-parse with the R parser.
-        ThenVLChR (prCh @@ ch @@ s0r)
-    ThenVLChL prCh s0r ch (Err  el) = Err  (EThenVLChL el)
-
-type EThenVLChL el = EIn "ThenVL(L)" el
-eThenVLChL :: SE el -> SE (EThenVLChL el)
-eThenVLChL el = withSingE el $ singE
-
-type family ThenVLChR resr where
-    ThenVLChR (Cont sr) = Cont (Right sr)
-    ThenVLChR (Done rr) = Done rr
-    ThenVLChR (Err  er) = Err  (EThenVLChR er)
-
-type EThenVLChR er = EIn "ThenVL(R)" er
-eThenVLChR :: SE er -> SE (EThenVLChR er)
-eThenVLChR er = withSingE er $ singE
-
-sThenVLChR
-    :: SResult ssr srr resr
-    -> SResult (SEither ssl ssr) srr (ThenVLChR resr)
-sThenVLChR = \case
-  SCont sr -> SCont $ SRight sr
-  SDone rr -> SDone rr
-  SErr  er -> SErr  $ eThenVLChR er
-
-sThenVLChSym
-    :: SParserChSym ssl srl plCh
-    -> SParserChSym ssr srr prCh
-    -> ssr sr
-    -> SParserChSym (SEither ssl ssr) srr
-        (ThenVLChSym plCh prCh sr)
-sThenVLChSym plCh prCh s0r = Lam2 $ \ch -> \case
-  SLeft  sl ->
-    case plCh @@ ch @@ sl of
-      SCont  sl' -> SCont $ SLeft sl'
-      SDone _rl  -> sThenVLChR (prCh @@ ch @@ s0r)
-      SErr   el  -> SErr  $ eThenVLChL el
-  SRight sr -> sThenVLChR (prCh @@ ch @@ sr)
-
-type ThenVLChSym
-    :: ParserChSym sl rl
-    -> ParserChSym sr rr
-    -> sr
-    -> ParserChSym (Either sl sr) rr
-data ThenVLChSym plCh prCh sr f
-type instance App (ThenVLChSym plCh prCh s0r) f = ThenVLChSym1 plCh prCh s0r f
-
-type ThenVLChSym1
-    :: ParserChSym sl rl
-    -> ParserChSym sr rr
-    -> sr
-    -> ParserChSym1 (Either sl sr) rr
-data ThenVLChSym1 plCh prCh s0r ch s
-type instance App (ThenVLChSym1 plCh prCh s0r ch) s = ThenVLCh plCh prCh s0r ch s
-
-type family ThenVLEnd plEnd prEnd s0r s where
-    -- | EOT during R: call R end
-    ThenVLEnd plEnd prEnd s0r (Right sr) = ThenVLEndR           (prEnd @@ sr)
-    -- | EOT during L: call L end, pass R end
-    ThenVLEnd plEnd prEnd s0r (Left  sl) = ThenVLEndL prEnd s0r (plEnd @@ sl)
-
-type family ThenVLEndR res where
-    -- | EOT during R, R end succeeds: success
-    ThenVLEndR (Right rr) = Right rr
-    -- | EOT during R, R end fails: error
-    ThenVLEndR (Left  er) = Left  (EThenVLEndR er)
-
-type EThenVLEndR er = EIn "ThenVL(R) end" er
-eThenVLEndR :: SE er -> SE (EThenVLEndR er)
-eThenVLEndR er = withSingE er $ singE
-
-sThenVLEndR
-    :: SResultEnd srr res
-    -> SResultEnd srr (ThenVLEndR res)
-sThenVLEndR = \case
-  SRight rr -> SRight rr
-  SLeft  er -> SLeft  $ eThenVLEndR er
-
-type family ThenVLEndL prEnd s0r res where
-    -- | EOT during L, L end succeeds: call R end on initial R state
-    ThenVLEndL prEnd s0r (Right rl) = ThenVLEndR (prEnd @@ s0r)
-    -- | EOT during L, L end fails: error
-    ThenVLEndL prEnd s0r (Left  el) = Left (EThenVLEndL el)
-
-type EThenVLEndL er = EIn "ThenVL(L) end" er
-eThenVLEndL :: SE er -> SE (EThenVLEndL er)
-eThenVLEndL er = withSingE er $ singE
-
-sThenVLEndSym
-    :: SParserEndSym ssl srl plEnd
-    -> SParserEndSym ssr srr prEnd
-    -> ssr s0r
-    -> SParserEndSym (SEither ssl ssr) srr
-        (ThenVLEndSym plEnd prEnd s0r)
-sThenVLEndSym plEnd prEnd s0r = Lam $ \case
-  SRight sr -> sThenVLEndR (prEnd @@ sr)
-  SLeft  sl ->
-    case plEnd @@ sl of
-      SRight _rl -> sThenVLEndR (prEnd @@ s0r)
-      SLeft   el -> SLeft $ eThenVLEndL el
-
-type ThenVLEndSym
-    :: ParserEndSym sl rl
-    -> ParserEndSym sr rr
-    -> sr
-    -> ParserEndSym (Either sl sr) rr
-data ThenVLEndSym plEnd prEnd s0r s
-type instance App (ThenVLEndSym plEnd prEnd s0r) s = ThenVLEnd plEnd prEnd s0r s
diff --git a/src/Symparsec/Parser/Then/VoidRight.hs b/src/Symparsec/Parser/Then/VoidRight.hs
deleted file mode 100644
--- a/src/Symparsec/Parser/Then/VoidRight.hs
+++ /dev/null
@@ -1,185 +0,0 @@
-{-# LANGUAGE UndecidableInstances #-}
-
-module Symparsec.Parser.Then.VoidRight where
-
-import Symparsec.Parser.Common
-import Singleraeh.Either ( SEither(..) )
-import Singleraeh.Tuple ( STuple2(..) )
-import DeFun.Core
-
-type SPThenVR ssl srl ssr srr plCh plEnd s0l prCh prEnd s0r =
-    SParser
-        (SEither ssl (STuple2 srl ssr))
-        srl
-        (ThenVR' plCh plEnd s0l prCh prEnd s0r)
-
-sThenVR
-    :: SParser  ssl srl ('PParser plCh plEnd s0l)
-    -> SParser  ssr srr ('PParser prCh prEnd s0r)
-    -> SPThenVR ssl srl ssr srr plCh plEnd s0l prCh prEnd s0r
-sThenVR (SParser plCh plEnd s0l) (SParser prCh prEnd s0r) =
-    SParser (sThenVRChSym plCh prCh s0r) (sThenVREndSym plEnd prEnd s0r) (SLeft s0l)
-
-instance
-  -- Shame I can't use pl, pr in associated type synonyms! :(
-  ( pl ~ 'PParser plCh plEnd s0l
-  , pr ~ 'PParser prCh prEnd s0r
-  , SingParser pl
-  , SingParser pr
-  ) => SingParser (ThenVR' plCh plEnd s0l prCh prEnd s0r) where
-    type PS (ThenVR' plCh plEnd s0l prCh prEnd s0r) =
-        SEither
-            (PS ('PParser plCh plEnd s0l))
-            (STuple2
-                (PR ('PParser plCh plEnd s0l))
-                (PS ('PParser prCh prEnd s0r)))
-    type PR (ThenVR' plCh plEnd s0l prCh prEnd s0r) =
-        PR ('PParser plCh plEnd s0l)
-    singParser' = sThenVR (singParser @pl) (singParser @pr)
-
--- | Sequence two parsers, running left then right, and discard the return value
---   of the right parser.
-infixl 4 :<*:
-type (:<*:)
-    :: PParser sl rl
-    -> PParser sr rr
-    -> PParser (Either sl (rl, sr)) rl
-type family pl :<*: pr where
-    'PParser plCh plEnd s0l :<*: 'PParser prCh prEnd s0r =
-        ThenVR' plCh plEnd s0l prCh prEnd s0r
-
-type ThenVR'
-    :: ParserChSym  sl rl
-    -> ParserEndSym sl rl
-    -> sl
-    -> ParserChSym  sr rr
-    -> ParserEndSym sr rr
-    -> sr
-    -> PParser (Either sl (rl, sr)) rl
-type ThenVR' plCh plEnd s0l prCh prEnd s0r =
-    'PParser (ThenVRChSym plCh prCh s0r) (ThenVREndSym plEnd prEnd s0r) (Left s0l)
-
-type ThenVRCh
-    :: ParserChSym sl rl
-    -> ParserChSym sr rr
-    -> sr
-    -> PParserCh (Either sl (rl, sr)) rl
-type family ThenVRCh plCh prCh s0r ch s where
-    ThenVRCh plCh prCh s0r ch (Left  sl) =
-        ThenVRChL prCh s0r ch (plCh @@ ch @@ sl)
-    ThenVRCh plCh prCh s0r ch (Right '(rl, sr)) =
-        ThenVRChR rl (prCh @@ ch @@ sr)
-
-type family ThenVRChL prCh s0r ch resl where
-    ThenVRChL prCh s0r ch (Cont sl) = Cont (Left  sl)
-    ThenVRChL prCh s0r ch (Done rl) =
-        -- 'Done' doesn't consume, so re-parse with the R parser.
-        ThenVRChR rl (prCh @@ ch @@ s0r)
-    ThenVRChL prCh s0r ch (Err  el) = Err  (EThenVRChL el)
-
-type EThenVRChL el = EIn "ThenVR(L)" el
-eThenVRChL :: SE el -> SE (EThenVRChL el)
-eThenVRChL el = withSingE el $ singE
-
-type family ThenVRChR rl resr where
-    ThenVRChR rl (Cont sr) = Cont (Right '(rl, sr))
-    ThenVRChR rl (Done rr) = Done rl
-    ThenVRChR rl (Err  er) = Err  (EThenVRChR er)
-
-type EThenVRChR er = EIn "ThenVR(R)" er
-eThenVRChR :: SE er -> SE (EThenVRChR er)
-eThenVRChR er = withSingE er $ singE
-
-sThenVRChR
-    :: srl rl
-    -> SResult ssr srr resr
-    -> SResult (SEither ssl (STuple2 srl ssr)) srl (ThenVRChR rl resr)
-sThenVRChR rl = \case
-  SCont  sr -> SCont $ SRight $ STuple2 rl sr
-  SDone _rr -> SDone rl
-  SErr   er -> SErr  $ eThenVRChR er
-
-sThenVRChSym
-    :: SParserChSym ssl srl plCh
-    -> SParserChSym ssr srr prCh
-    -> ssr sr
-    -> SParserChSym (SEither ssl (STuple2 srl ssr)) srl
-        (ThenVRChSym plCh prCh sr)
-sThenVRChSym plCh prCh s0r = Lam2 $ \ch -> \case
-  SLeft sl ->
-    case plCh @@ ch @@ sl of
-      SCont sl' -> SCont $ SLeft sl'
-      SDone rl  -> sThenVRChR rl (prCh @@ ch @@ s0r)
-      SErr  el  -> SErr  $ eThenVRChL el
-  SRight (STuple2 rl sr) -> sThenVRChR rl (prCh @@ ch @@ sr)
-
-type ThenVRChSym
-    :: ParserChSym sl rl
-    -> ParserChSym sr rr
-    -> sr
-    -> ParserChSym (Either sl (rl, sr)) rl
-data ThenVRChSym plCh prCh s0r f
-type instance App (ThenVRChSym plCh prCh s0r) f = ThenVRChSym1 plCh prCh s0r f
-
-type ThenVRChSym1
-    :: ParserChSym sl rl
-    -> ParserChSym sr rr
-    -> sr
-    -> ParserChSym1 (Either sl (rl, sr)) rl
-data ThenVRChSym1 plCh prCh s0r ch s
-type instance App (ThenVRChSym1 plCh prCh s0r ch) s = ThenVRCh plCh prCh s0r ch s
-
-type family ThenVREnd plEnd prEnd s0r s where
-    -- | EOT during R: call R end
-    ThenVREnd plEnd prEnd s0r (Right '(rl, sr)) = ThenVREndR rl    (prEnd @@ sr)
-    -- | EOT during L: call L end, pass R end
-    ThenVREnd plEnd prEnd s0r (Left sl)         = ThenVREndL prEnd s0r (plEnd @@ sl)
-
-type family ThenVREndR rl res where
-    -- | EOT during R, R end succeeds: success
-    ThenVREndR rl (Right rr) = Right rl
-    -- | EOT during R, R end fails: error
-    ThenVREndR rl (Left  er) = Left  (EThenVREndR er)
-
-type EThenVREndR er = EIn "ThenVR(R) end" er
-eThenVREndR :: SE er -> SE (EThenVREndR er)
-eThenVREndR er = withSingE er $ singE
-
-sThenVREndR
-    :: srl rl
-    -> SResultEnd srr res
-    -> SResultEnd srl (ThenVREndR rl res)
-sThenVREndR rl = \case
-  SRight _rr -> SRight rl
-  SLeft   er -> SLeft  $ eThenVREndR er
-
-type family ThenVREndL prEnd s0r res where
-    -- | EOT during L, L end succeeds: call R end on initial R state
-    ThenVREndL prEnd s0r (Right rl) = ThenVREndR rl (prEnd @@ s0r)
-    -- | EOT during L, L end fails: error
-    ThenVREndL prEnd s0r (Left  el) = Left (EThenVREndL el)
-
-type EThenVREndL er = EIn "ThenVR(L) end" er
-eThenVREndL :: SE er -> SE (EThenVREndL er)
-eThenVREndL er = withSingE er $ singE
-
-sThenVREndSym
-    :: SParserEndSym ssl srl plEnd
-    -> SParserEndSym ssr srr prEnd
-    -> ssr s0r
-    -> SParserEndSym (SEither ssl (STuple2 srl ssr)) srl
-        (ThenVREndSym plEnd prEnd s0r)
-sThenVREndSym plEnd prEnd s0r = Lam $ \case
-  SRight (STuple2 rl sr) -> sThenVREndR rl (prEnd @@ sr)
-  SLeft  sl ->
-    case plEnd @@ sl of
-      SRight rl -> sThenVREndR rl (prEnd @@ s0r)
-      SLeft  el -> SLeft $ eThenVREndL el
-
-type ThenVREndSym
-    :: ParserEndSym sl rl
-    -> ParserEndSym sr rr
-    -> sr
-    -> ParserEndSym (Either sl (rl, sr)) rl
-data ThenVREndSym plEnd prEnd s0r s
-type instance App (ThenVREndSym plEnd prEnd s0r) s = ThenVREnd plEnd prEnd s0r s
diff --git a/src/Symparsec/Parser/Try.hs b/src/Symparsec/Parser/Try.hs
new file mode 100644
--- /dev/null
+++ b/src/Symparsec/Parser/Try.hs
@@ -0,0 +1,14 @@
+{-# LANGUAGE UndecidableInstances #-}
+
+module Symparsec.Parser.Try ( type Try ) where
+
+import Symparsec.Parser.Common
+
+-- | Run the given parser, backtracking on error.
+type Try :: PParser a -> PParser a
+data Try p s
+type instance App (Try p) s = Try' s (p @@ s)
+type Try' :: PState -> PReply a -> PReply a
+type family Try' sPrev rep where
+    Try' sPrev ('Reply (OK  a) s) = 'Reply (OK  a) s
+    Try' sPrev ('Reply (Err e) s) = 'Reply (Err e) sPrev
diff --git a/src/Symparsec/Parser/While.hs b/src/Symparsec/Parser/While.hs
--- a/src/Symparsec/Parser/While.hs
+++ b/src/Symparsec/Parser/While.hs
@@ -1,72 +1,39 @@
 {-# LANGUAGE UndecidableInstances #-}
 
-module Symparsec.Parser.While where
+module Symparsec.Parser.While ( type While ) where
 
 import Symparsec.Parser.Common
-import DeFun.Core
-import GHC.TypeLits
-import Singleraeh.Bool
-import Singleraeh.Either
-import Symparsec.Parser.While.Predicates
 
 -- | Run the given parser while the given character predicate succeeds.
-type family While chPred p where
-    While chPred ('PParser pCh pEnd s0) = While' chPred pCh pEnd s0
-type While' chPred pCh pEnd s0 = 'PParser (WhileChSym chPred pCh pEnd) pEnd s0
-
-sWhile
-    :: Lam SChar SBool chPred
-    -> SParser ss sr ('PParser pCh pEnd s0)
-    -> SParser ss sr (While' chPred pCh pEnd s0)
-sWhile chPred (SParser pCh pEnd s0) =
-    SParser (sWhileChSym chPred pCh pEnd) pEnd s0
-
-instance
-  ( p ~ 'PParser pCh pEnd s0, SingParser p
-  , SingChPred chPred
-  ) => SingParser (While' chPred pCh pEnd s0) where
-    type PS (While' chPred pCh pEnd s0) = PS ('PParser pCh pEnd s0)
-    type PR (While' chPred pCh pEnd s0) = PR ('PParser pCh pEnd s0)
-    singParser' = sWhile (singChPred @chPred) (singParser @p)
-
-type WhileCh chPred pCh pEnd ch s = WhileCh' pCh pEnd ch s (chPred @@ ch)
-type family WhileCh' pCh pEnd ch s res where
-    WhileCh' pCh pEnd ch s True  = pCh @@ ch @@ s
-    WhileCh' pCh pEnd ch s False = WhileCh'' (pEnd @@ s)
-
-type family WhileCh'' res where
-    WhileCh'' (Right r) = Done r
-    WhileCh'' (Left  e) = Err (EWhile e)
+type While :: (Char ~> Bool) -> PParser a -> PParser a
+data While chPred p s
+type instance App (While chPred p) s = While' chPred p s
 
-type EWhile e = EIn "While" e
-eWhile :: SE e -> SE (EWhile e)
-eWhile e = withSingE e $ singE
+type family While' chPred p s where
+    While' chPred p ('State rem len idx) =
+        WhileCountStart len rem idx chPred p (UnconsSymbol rem)
 
-type WhileChSym
-    :: (Char ~> Bool)
-    -> ParserChSym  s r
-    -> ParserEndSym s r
-    -> ParserChSym  s r
-data WhileChSym chPred pCh pEnd f
-type instance App (WhileChSym chPred pCh pEnd) f = WhileChSym1 chPred pCh pEnd f
+type family WhileCountStart len rem idx chPred p mstr where
+    WhileCountStart len rem idx chPred p (Just '(ch, str)) =
+        WhileCount len rem idx chPred p 0 (UnconsSymbol str) (chPred @@ ch)
+    WhileCountStart len rem idx chPred p Nothing           = p @@ ('State rem 0 idx)
 
-type WhileChSym1
-    :: (Char ~> Bool)
-    -> ParserChSym  s r
-    -> ParserEndSym s r
-    -> ParserChSym1 s r
-data WhileChSym1 chPred pCh pEnd ch s
-type instance App (WhileChSym1 chPred pCh pEnd ch) s = WhileCh chPred pCh pEnd ch s
+type family WhileCount len rem idx chPred p n mstr res where
+    WhileCount len rem idx chPred p n (Just '(ch, str)) True  =
+        WhileCount len rem idx chPred p (n+1) (UnconsSymbol str) (chPred @@ ch)
+    WhileCount len rem idx chPred p n (Just '(ch, str)) False =
+        WhileEnd (len-n)     (p @@ ('State rem n     idx))
+    WhileCount len rem idx chPred p n Nothing           True  =
+        WhileEnd (len-(n+1)) (p @@ ('State rem (n+1) idx))
+    WhileCount len rem idx chPred p n Nothing           False =
+        WhileEnd (len-n)     (p @@ ('State rem n     idx))
 
-sWhileChSym
-    :: Lam SChar SBool chPred
-    -> SParserChSym  ss sr pCh
-    -> SParserEndSym ss sr pEnd
-    -> SParserChSym  ss sr (WhileChSym chPred pCh pEnd)
-sWhileChSym chPred pCh pEnd = Lam2 $ \ch s ->
-    case chPred @@ ch of
-      STrue  -> pCh @@ ch @@ s
-      SFalse ->
-        case pEnd @@ s of
-          SRight r -> SDone r
-          SLeft  e -> SErr $ eWhile e
+type family WhileEnd lenRest rep where
+    -- TODO note that we don't require that the inner parser fully consumes.
+    -- that's because we "lie" about how this parser works. you probably want a
+    -- sort of char-by-char parser, but we measure a chunk and pass that.
+    -- but by not requiring full consumption, we recover char-by-char behaviour!
+    -- and we can still get full consumption by combining with Isolate.
+    -- the inner parser should generally fully consume though, as a design point
+    WhileEnd lenRest ('Reply res ('State rem len idx)) =
+        'Reply res ('State rem (lenRest+len) idx)
diff --git a/src/Symparsec/Parser/While/Predicates.hs b/src/Symparsec/Parser/While/Predicates.hs
--- a/src/Symparsec/Parser/While/Predicates.hs
+++ b/src/Symparsec/Parser/While/Predicates.hs
@@ -1,19 +1,11 @@
 -- | Character predicates.
-
--- TODO for singling, I could cheat by inspecting the char value. should be
--- faster and better. but would need a bit more checking so cba for now.
+--
+-- raehik copied his module from Symparsec.
 
 module Symparsec.Parser.While.Predicates where
 
 import DeFun.Core
-import GHC.TypeLits
-import Singleraeh.Bool
-import Singleraeh.Equality ( testEqElse )
-import Unsafe.Coerce ( unsafeCoerce )
 
-class SingChPred chPred where
-    singChPred :: Lam SChar SBool chPred
-
 -- | @A-Za-z@
 type IsAlpha :: Char -> Bool
 type family IsAlpha ch where
@@ -75,64 +67,6 @@
 data IsAlphaSym ch
 type instance App IsAlphaSym ch = IsAlpha ch
 
-sIsAlphaSym :: Lam SChar SBool IsAlphaSym
-sIsAlphaSym = Lam $ \ch ->
-      testEqElse ch (SChar @'a') STrue
-    $ testEqElse ch (SChar @'A') STrue
-    $ testEqElse ch (SChar @'b') STrue
-    $ testEqElse ch (SChar @'B') STrue
-    $ testEqElse ch (SChar @'c') STrue
-    $ testEqElse ch (SChar @'C') STrue
-    $ testEqElse ch (SChar @'d') STrue
-    $ testEqElse ch (SChar @'D') STrue
-    $ testEqElse ch (SChar @'e') STrue
-    $ testEqElse ch (SChar @'E') STrue
-    $ testEqElse ch (SChar @'f') STrue
-    $ testEqElse ch (SChar @'F') STrue
-    $ testEqElse ch (SChar @'g') STrue
-    $ testEqElse ch (SChar @'G') STrue
-    $ testEqElse ch (SChar @'h') STrue
-    $ testEqElse ch (SChar @'H') STrue
-    $ testEqElse ch (SChar @'i') STrue
-    $ testEqElse ch (SChar @'I') STrue
-    $ testEqElse ch (SChar @'j') STrue
-    $ testEqElse ch (SChar @'J') STrue
-    $ testEqElse ch (SChar @'k') STrue
-    $ testEqElse ch (SChar @'K') STrue
-    $ testEqElse ch (SChar @'l') STrue
-    $ testEqElse ch (SChar @'L') STrue
-    $ testEqElse ch (SChar @'m') STrue
-    $ testEqElse ch (SChar @'M') STrue
-    $ testEqElse ch (SChar @'n') STrue
-    $ testEqElse ch (SChar @'N') STrue
-    $ testEqElse ch (SChar @'o') STrue
-    $ testEqElse ch (SChar @'O') STrue
-    $ testEqElse ch (SChar @'p') STrue
-    $ testEqElse ch (SChar @'P') STrue
-    $ testEqElse ch (SChar @'q') STrue
-    $ testEqElse ch (SChar @'Q') STrue
-    $ testEqElse ch (SChar @'r') STrue
-    $ testEqElse ch (SChar @'R') STrue
-    $ testEqElse ch (SChar @'s') STrue
-    $ testEqElse ch (SChar @'S') STrue
-    $ testEqElse ch (SChar @'t') STrue
-    $ testEqElse ch (SChar @'T') STrue
-    $ testEqElse ch (SChar @'u') STrue
-    $ testEqElse ch (SChar @'U') STrue
-    $ testEqElse ch (SChar @'v') STrue
-    $ testEqElse ch (SChar @'V') STrue
-    $ testEqElse ch (SChar @'w') STrue
-    $ testEqElse ch (SChar @'W') STrue
-    $ testEqElse ch (SChar @'x') STrue
-    $ testEqElse ch (SChar @'X') STrue
-    $ testEqElse ch (SChar @'y') STrue
-    $ testEqElse ch (SChar @'Y') STrue
-    $ testEqElse ch (SChar @'z') STrue
-    $ testEqElse ch (SChar @'Z') STrue
-    $ unsafeCoerce SFalse
-
-instance SingChPred IsAlphaSym where singChPred = sIsAlphaSym
-
 -- | @0-9A-Fa-f@
 type IsHexDigit :: Char -> Bool
 type family IsHexDigit ch where
@@ -164,30 +98,21 @@
 data IsHexDigitSym ch
 type instance App IsHexDigitSym ch = IsHexDigit ch
 
-sIsHexDigitSym :: Lam SChar SBool IsHexDigitSym
-sIsHexDigitSym = Lam $ \ch ->
-      testEqElse ch (SChar @'0') STrue
-    $ testEqElse ch (SChar @'1') STrue
-    $ testEqElse ch (SChar @'2') STrue
-    $ testEqElse ch (SChar @'3') STrue
-    $ testEqElse ch (SChar @'4') STrue
-    $ testEqElse ch (SChar @'5') STrue
-    $ testEqElse ch (SChar @'6') STrue
-    $ testEqElse ch (SChar @'7') STrue
-    $ testEqElse ch (SChar @'8') STrue
-    $ testEqElse ch (SChar @'9') STrue
-    $ testEqElse ch (SChar @'a') STrue
-    $ testEqElse ch (SChar @'A') STrue
-    $ testEqElse ch (SChar @'b') STrue
-    $ testEqElse ch (SChar @'B') STrue
-    $ testEqElse ch (SChar @'c') STrue
-    $ testEqElse ch (SChar @'C') STrue
-    $ testEqElse ch (SChar @'d') STrue
-    $ testEqElse ch (SChar @'D') STrue
-    $ testEqElse ch (SChar @'e') STrue
-    $ testEqElse ch (SChar @'E') STrue
-    $ testEqElse ch (SChar @'f') STrue
-    $ testEqElse ch (SChar @'F') STrue
-    $ unsafeCoerce SFalse
+-- | @0-9@
+type IsDecDigit :: Char -> Bool
+type family IsDecDigit ch where
+    IsDecDigit '0' = True
+    IsDecDigit '1' = True
+    IsDecDigit '2' = True
+    IsDecDigit '3' = True
+    IsDecDigit '4' = True
+    IsDecDigit '5' = True
+    IsDecDigit '6' = True
+    IsDecDigit '7' = True
+    IsDecDigit '8' = True
+    IsDecDigit '9' = True
+    IsDecDigit _   = False
 
-instance SingChPred IsHexDigitSym where singChPred = sIsHexDigitSym
+type IsDecDigitSym :: Char ~> Bool
+data IsDecDigitSym ch
+type instance App IsDecDigitSym ch = IsDecDigit ch
diff --git a/src/Symparsec/Parsers.hs b/src/Symparsec/Parsers.hs
--- a/src/Symparsec/Parsers.hs
+++ b/src/Symparsec/Parsers.hs
@@ -1,70 +1,106 @@
--- | Type-level string parsers.
+-- | Common type-level string parsers.
 --
--- You may ignore the equations that Haddock displays: they are internal and
--- irrelevant to library usage.
+-- Many parsers reuse term-level names, which can cause ambiguity issues.
+-- Consider importing qualified.
 
 module Symparsec.Parsers
   (
-  -- * Binary combinators
-  -- $binary-combinators
-    (:<*>:)
-  ,  (:*>:)
-  , (:<*:)
-  , (:<|>:)
+  -- * Type class-esque
+  -- $type-classes
+    type (<$>)
+  , type (<*>), type Pure, type LiftA2, type (*>), type (<*)
+  , type (>>=)
+  , type (<|>), type Empty, type Optional
 
   -- * Positional
   -- $positional
-  , Take
-  , TakeRest
-  , Skip
-  , End
-  , Isolate
-
-  -- * Predicated
-  -- $predicated
-  , While, TakeWhile
+  , type Ensure
+  , type Isolate
+  , type Take
+  , type TakeRest
+  , type Skip
+  , type Eof
 
-  -- * TODO unsorted
-  , Count
+  -- * Other combinators
+  -- $comb-etc
+  , type Try
+  , type While
+  , type TakeWhile
+  , type Count
 
-  -- * Basic
-  -- $basic
-  , Literal
+  -- * Common non-combinator
+  -- $noncomb-common
+  , type Literal
 
   -- ** Naturals
-  , NatDec
-  , NatHex
-  , NatBin
-  , NatOct
-  , NatBase
+  , type NatBase
+  , type NatDec
+  , type NatHex
+  , type NatBin
+  , type NatOct
+
+  -- * Derived
+  -- $derived
+  , type Tuple
+
+  -- * Missing parsers
+  -- $missing
   ) where
 
+import Symparsec.Parser.Alternative
+import Symparsec.Parser.Applicative
+import Symparsec.Parser.Count
+import Symparsec.Parser.Ensure
+import Symparsec.Parser.Eof
+import Symparsec.Parser.Functor
 import Symparsec.Parser.Isolate
-import Symparsec.Parser.Skip
-import Symparsec.Parser.Natural
-import Symparsec.Parser.Then
-import Symparsec.Parser.Then.VoidLeft
-import Symparsec.Parser.Then.VoidRight
 import Symparsec.Parser.Literal
-import Symparsec.Parser.End
+import Symparsec.Parser.Monad
+import Symparsec.Parser.Natural
+import Symparsec.Parser.Skip
 import Symparsec.Parser.Take
 import Symparsec.Parser.TakeRest
-import Symparsec.Parser.Or
+import Symparsec.Parser.TakeWhile
+import Symparsec.Parser.Try
 import Symparsec.Parser.While
-import Symparsec.Parser.Count
+import DeFun.Core
 
--- $binary-combinators
--- Parsers that combine two parsers. Any parsers that have term-level parallels
--- will use the same fixity e.g. ':<*>:' is @infixl 4@, same as '<*>'.
+{- $type-classes
+Parsers which mirror functions from type classes (specifically 'Functor',
+'Applicative', 'Monad' and 'Control.Alternative.Alternative'. These primitive
+combinators are powerful, but can be tough to use without type-level binders or
+do-notation, and force interacting with defunctionalization.
+-}
 
--- $positional
--- Parsers that relate to symbol position e.g. length, end of symbol.
+{- $positional
+Parsers that relate to input position e.g. length, end of input.
+-}
 
--- $predicated
--- Parsers that include character predicates.
+{- $comb-etc
+Assorted parser combinators (that wrap other parsers).
+-}
 
--- $basic
--- Simple non-combinator parsers. Probably fundamental in some way e.g. very
--- general or common.
+{- $noncomb-common
+Simple non-combinator parser. Probably fundamental in some way e.g. very general
+or common.
+-}
 
-type TakeWhile chPred = While chPred TakeRest
+{- $missing
+Certain term-level parsers you may be used to you will /not/ see in Symparsec:
+
+* Parsers that rely on underlying instances e.g. no @'Semigroup' a => Semigroup
+  (parser a)@ because we'd have to pass @Semigroup a@ manually, which defeats
+  the purpose
+-}
+
+{- $derived
+Derived parsers. Should be type synonyms.
+-}
+
+{- | Parse left, then right, and return their results in a tuple.
+
+Classic parser combinators often don't define this because it's trivial, and do
+notation is often cleaner anyway. But it's very syntactically busy on the type
+level, and we don't have do notation. So here's a convenience definition.
+-}
+type Tuple l r = LiftA2 (Con2 '(,)) l r
diff --git a/src/Symparsec/Run.hs b/src/Symparsec/Run.hs
--- a/src/Symparsec/Run.hs
+++ b/src/Symparsec/Run.hs
@@ -1,39 +1,34 @@
 {-# LANGUAGE UndecidableInstances #-}
-{-# LANGUAGE AllowAmbiguousTypes #-} -- for reifying/singled parsers
 
-module Symparsec.Run where -- ( Run, ERun(..) ) where
+-- | Running Symparsec parsers.
 
+module Symparsec.Run ( type Run, type RunTest ) where
+
 import Symparsec.Parser
-import GHC.TypeLits hiding ( ErrorMessage(..), fromSNat )
-import GHC.TypeNats ( fromSNat )
-import GHC.TypeLits qualified as TE
+import Data.Type.Symbol qualified as Symbol
 import DeFun.Core
+import GHC.TypeLits ( type Symbol )
+import GHC.TypeNats ( type Natural, type (+) )
+import GHC.TypeError qualified as TE
 import TypeLevelShow.Doc
-import TypeLevelShow.Utils ( ShowChar )
-import TypeLevelShow.Natural ( ShowNatDec )
-import Singleraeh.Tuple ( STuple2(..) )
-import Singleraeh.Maybe ( SMaybe(..) )
-import Singleraeh.Either ( SEither(..) )
-import Singleraeh.Symbol
-    ( sConsSymbol, sUnconsSymbol, ReconsSymbol, sReconsSymbol )
-import Singleraeh.Natural ( (%+) )
-import Singleraeh.Demote
-
--- | Run the given parser on the given 'Symbol', returning an 'TE.ErrorMessage'
---   on failure.
-type Run :: PParser s r -> Symbol -> Either TE.ErrorMessage (r, Symbol)
-type Run p sym = MapLeftRender (Run' p sym)
+import TypeLevelShow.Natural ( type ShowNatDec )
 
-type MapLeftRender :: Either PERun r -> Either TE.ErrorMessage r
-type family MapLeftRender eer where
-    MapLeftRender (Right a) = Right a
-    MapLeftRender (Left  e) = Left (RenderPDoc (PrettyERun e))
+-- | Run the given parser on the given 'Symbol'.
+--
+-- * On success, returns a tuple of @(result :: a, remaining :: 'Symbol')@.
+-- * On failure, returns an 'TE.ErrorMessage'.
+type Run :: PParser a -> Symbol -> Either TE.ErrorMessage (a, Symbol)
+type Run p str = RunEnd str (p @@ StateInit str)
 
--- | Run the given parser on the given 'Symbol', returning a 'PERun' on failure.
-type Run' :: PParser s r -> Symbol -> Either PERun (r, Symbol)
-type family Run' p str where
-    Run' ('PParser pCh pEnd s0) str =
-        RunStart pCh pEnd s0 (UnconsSymbol str)
+type RunEnd :: Symbol -> PReply a -> Either TE.ErrorMessage (a, Symbol)
+type family RunEnd str rep where
+    RunEnd str ('Reply (OK  a) ('State  rem _len _idx)) =
+        -- TODO I could return only @len@ of the remaining input @rem@, but
+        -- that's more work than just returning @rem@, and I don't see a way
+        -- this would matter for correct parsers.
+        Right '(a, rem)
+    RunEnd str ('Reply (Err e) ('State _rem _len  idx)) =
+        Left (RenderPDoc (PrettyErrorTop idx str e))
 
 -- | Run the given parser on the given 'Symbol', emitting a type error on
 --   failure.
@@ -41,176 +36,47 @@
 -- This /would/ be useful for @:k!@ runs, but it doesn't work properly with
 -- 'TE.TypeError's, printing @= (TypeError ...)@ instead of the error message.
 -- Alas! Instead, do something like @> Proxy \@(RunTest ...)@.
-type RunTest :: PParser s r -> Symbol -> (r, Symbol)
-type RunTest p sym = MapLeftTypeError (Run p sym)
+type RunTest :: PParser a -> Symbol -> (a, Symbol)
+type RunTest p str = FromRightTypeError (Run p str)
 
--- | Run the given parser on the given 'Symbol', returning a 'PERun' on failure,
---   and ignoring any remaining non-consumed characters.
-type Run'_ :: PParser s r -> Symbol -> Either TE.ErrorMessage r
-type Run'_ p str = Run'_Inner (Run' p str)
+type FromRightTypeError :: Either TE.ErrorMessage a -> a
+type family FromRightTypeError eea where
+    FromRightTypeError (Right a) = a
+    FromRightTypeError (Left  e) = TE.TypeError e
 
-type Run'_Inner :: Either PERun (a, b) -> Either TE.ErrorMessage a
-type family Run'_Inner eeab where
-    Run'_Inner (Right '(a, b)) = Right a
-    Run'_Inner (Left  e)       = Left (RenderPDoc (PrettyERun e))
+-- | Initial parser state for the given 'Symbol'.
+type StateInit :: Symbol -> PState
+type StateInit str = 'State str (Symbol.Length str) 0
 
--- | Run the singled version of type-level parser on the given 'String',
---   returning an 'ERun' on failure.
+-- | Pretty print a top-level parser error.
 --
--- You must provide a function for demoting the singled return type.
--- ('Singleraeh.Demote.demote' can do this for you automatically.)
-run'
-    :: forall {s} {r} (p :: PParser s r) r'. SingParser p
-    => (forall a. PR p a -> r') -> String -> Either (ERun String) (r', String)
-run' demotePR str = withSomeSSymbol str $ \sstr ->
-    case sRun' (singParser @p) sstr of
-      SRight (STuple2 pr sstr') -> Right (demotePR pr, fromSSymbol sstr')
-      SLeft  e                  -> Left $ demoteSERun e
-
--- TODO prettify error. actually run' needs an error demoter :| such a pain
-runTest
-    :: forall {s} {r} (p :: PParser s r). (SingParser p, Demotable (PR p))
-    => String -> (Demote (PR p), String)
-runTest str =
-    case run' @p demote str of
-      Right r -> r
-      Left  e -> error $ show e
-
-sRun'
-    :: SParser ss sr p
-    -> SSymbol str
-    -> SEither SERun (STuple2 sr SSymbol) (Run' p str)
-sRun' (SParser pCh pEnd s0) str =
-    sRunStart pCh pEnd s0 (sUnconsSymbol str)
-
-type family RunStart pCh pEnd s0 mstr where
-    RunStart pCh pEnd s0 (Just '(ch, str)) =
-        RunCh pCh pEnd 0 ch (UnconsSymbol str) (pCh @@ ch @@ s0)
-
-    RunStart pCh pEnd s0 Nothing =
-        RunEnd0 (pEnd @@ s0)
-
-sRunStart
-    :: SParserChSym  ss sr pCh
-    -> SParserEndSym ss sr pEnd
-    -> ss s0
-    -> SMaybe (STuple2 SChar SSymbol) mstr
-    -> SEither SERun (STuple2 sr SSymbol) (RunStart pCh pEnd s0 mstr)
-sRunStart pCh pEnd s0 = \case
-  SJust (STuple2 ch str) ->
-    sRunCh pCh pEnd (SNat @0) ch (sUnconsSymbol str) (pCh @@ ch @@ s0)
-  SNothing -> sRunEnd0 (pEnd @@ s0)
-
-type MapLeftTypeError :: Either TE.ErrorMessage a -> a
-type family MapLeftTypeError eea where
-    MapLeftTypeError (Right a) = a
-    MapLeftTypeError (Left  e) = TE.TypeError e
+-- Tries to look a bit like Megaparsec and modern compiler parser errors,
+-- except we don't actually track much for now (e.g. no line numbers, spans).
+type PrettyErrorTop :: Natural -> Symbol -> PError -> PDoc
+type PrettyErrorTop idx str e =
+             -- idx+1 because we're emitting char position here, not index
+             Text "Symparsec parse error:"
+        :$$: Text "1:" :<>: Text (ShowNatDec (idx+1))
+        :$$: PrettyErrorPosition idx str
+        :$$: PrettyError e
 
--- | Inspect character parser result.
+-- | Print a 'Symbol' and some ASCII art highlighting a character index in it.
 --
--- This is purposely written so that the main case is at the top, and a single
--- equation (we parse, prepare next character and inspect character parser
--- result at the same time). My hope is that this keeps GHC fast.
-type family RunCh pCh pEnd idx ch' mstr res where
-    -- | OK, and more to come: parse next character
-    RunCh pCh pEnd idx ch' (Just '(ch, sym)) (Cont s) =
-        RunCh pCh pEnd (idx+1) ch (UnconsSymbol sym) (pCh @@ ch @@ s)
-
-    -- | OK, and we're at the end of the string: run end parser
-    RunCh pCh pEnd idx ch' Nothing           (Cont s) =
-        RunEnd idx ch' (pEnd @@ s)
-
-    -- | OK, and we're finished early: return value and remaining string
-    RunCh pCh pEnd idx ch' mstr              (Done r) =
-        Right '(r, ConsSymbol ch' (ReconsSymbol mstr))
-
-    -- | Parse error: return error
-    RunCh pCh pEnd idx ch' mstr              (Err  e) =
-        Left ('ERun idx ch' e)
-
-sRunCh
-    :: SParserChSym  ss sr pCh
-    -> SParserEndSym ss sr pEnd
-    -> SNat idx
-    -> SChar chPrev
-    -> SMaybe (STuple2 SChar SSymbol) mstr
-    -> SResult ss sr res
-    -> SEither SERun (STuple2 sr SSymbol) (RunCh pCh pEnd idx chPrev mstr res)
-sRunCh pCh pEnd idx chPrev mstr = \case
-  SCont s ->
-    case mstr of
-      SJust (STuple2 ch str) ->
-        sRunCh pCh pEnd (idx %+ (SNat @1)) ch (sUnconsSymbol str)
-            (pCh @@ ch @@ s)
-      SNothing ->
-        sRunEnd idx chPrev (pEnd @@ s)
-  SDone r -> SRight (STuple2 r (sConsSymbol chPrev (sReconsSymbol mstr)))
-  SErr  e -> SLeft (SERun idx chPrev e)
-
--- | Inspect end parser result.
-type RunEnd
-    :: Natural -> Char
-    -> Either PE r
-    -> Either PERun (r, Symbol)
-type family RunEnd idx ch res where
-    RunEnd idx ch (Right r) = Right '(r, "")
-    RunEnd idx ch (Left  e) = Left ('ERun idx ch e)
-
-sRunEnd
-    :: SNat idx -> SChar ch
-    -> SEither SE sr res
-    -> SEither SERun (STuple2 sr SSymbol) (RunEnd idx ch res)
-sRunEnd idx ch = \case
-  SRight r -> SRight (STuple2 r (SSymbol @""))
-  SLeft  e -> SLeft (SERun idx ch e)
-
--- | Inspect end parser result for the empty string, where we have no previous
---   character or (meaningful) index.
-type family RunEnd0 res where
-    RunEnd0 (Right r) = Right '(r, "")
-    RunEnd0 (Left  e) = Left (ERun0 e)
-
-sRunEnd0
-    :: SEither SE sr res
-    -> SEither SERun (STuple2 sr SSymbol) (RunEnd0 res)
-sRunEnd0 = \case
-  SRight r -> SRight (STuple2 r (SSymbol @""))
-  SLeft  e -> SLeft (SERun0 e)
-
-type PrettyERun :: PERun -> PDoc
-type family PrettyERun e where
-    PrettyERun (ERun0 e) = Text "parse error on empty string" :$$: PrettyE e
-    PrettyERun ('ERun idx ch e) =
-             Text "parse error at index " :<>: Text (ShowNatDec idx)
-        :<>: Text ", char '" :<>: Text (ShowChar ch) :<>: Text "'"
-        :$$: PrettyE e
-
-type PrettyE :: PE -> PDoc
-type family PrettyE e where
-    PrettyE (EBase name emsg)  = Text name :<>: Text ": " :<>: emsg
-    PrettyE (EIn   name e)     = Text name :<>: Text ": " :<>: PrettyE e
-
--- | Error while running parser.
-data ERun s
-  -- | Parser error at index X, character C.
-  = ERun Natural Char (E s)
-
-  -- | Parser error on the empty string.
-  | ERun0 (E s)
-    deriving stock Show
-
--- | Promoted 'ERun'.
-type PERun = ERun Symbol
-
-data SERun (erun :: PERun) where
-    SERun  :: SNat idx -> SChar ch -> SE e -> SERun ('ERun idx ch e)
-    SERun0 ::                         SE e -> SERun (ERun0 e)
+-- Looks like Megaparsec and other modern compiler parser errors.
+type PrettyErrorPosition :: Natural -> Symbol -> PDoc
+type PrettyErrorPosition idx str =
+             Text "  |"
+        :$$: Text "1 | " :<>: Text str
+        :$$: Text "  | " :<>: Text (Symbol.Replicate idx ' ') :<>: Text "^"
 
-demoteSERun :: SERun erun -> ERun String
-demoteSERun = \case
-  SERun  idx ch e -> ERun  (fromSNat idx) (fromSChar ch) (demoteSE e)
-  SERun0        e -> ERun0                               (demoteSE e)
+-- | Pretty print a parser error.
+type PrettyError :: PError -> PDoc
+type family PrettyError e where
+    PrettyError ('Error (str:strs)) = ConcatSymbol (Text str) strs
+    PrettyError ('Error '[])        = Text "<no detail>"
 
-instance Demotable SERun where
-    type Demote SERun = ERun String
-    demote = demoteSERun
+type ConcatSymbol :: PDoc -> [Symbol] -> PDoc
+type family ConcatSymbol doc strs where
+    -- TODO get ordering right
+    ConcatSymbol doc (str:strs) = ConcatSymbol (doc :$$: Text str) strs
+    ConcatSymbol doc '[]        = doc
diff --git a/src/Symparsec/Utils.hs b/src/Symparsec/Utils.hs
new file mode 100644
--- /dev/null
+++ b/src/Symparsec/Utils.hs
@@ -0,0 +1,6 @@
+module Symparsec.Utils where
+
+import GHC.TypeNats ( type CmpNat )
+import Data.Type.Ord ( type OrdCond )
+
+type IfNatLte n m fThen fElse = OrdCond (CmpNat n m) fThen fThen fElse
diff --git a/symparsec.cabal b/symparsec.cabal
--- a/symparsec.cabal
+++ b/symparsec.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.38.2.
 --
 -- see: https://github.com/sol/hpack
 
 name:           symparsec
-version:        1.1.1
+version:        2.0.0
 synopsis:       Type level string parser combinators
 description:    Please see README.md.
 category:       Types, Data
@@ -17,8 +17,7 @@
 license-file:   LICENSE
 build-type:     Simple
 tested-with:
-    GHC==9.8
-  , GHC==9.6
+    GHC==9.12
 extra-source-files:
     README.md
     CHANGELOG.md
@@ -29,28 +28,32 @@
 
 library
   exposed-modules:
+      Data.Type.Symbol
       Symparsec
       Symparsec.Example.Expr
       Symparsec.Parser
-      Symparsec.Parser.Apply
+      Symparsec.Parser.Alternative
+      Symparsec.Parser.Applicative
       Symparsec.Parser.Common
       Symparsec.Parser.Count
-      Symparsec.Parser.End
+      Symparsec.Parser.Ensure
+      Symparsec.Parser.Eof
+      Symparsec.Parser.Functor
       Symparsec.Parser.Isolate
       Symparsec.Parser.Literal
+      Symparsec.Parser.Monad
       Symparsec.Parser.Natural
       Symparsec.Parser.Natural.Digits
-      Symparsec.Parser.Or
       Symparsec.Parser.Skip
       Symparsec.Parser.Take
       Symparsec.Parser.TakeRest
-      Symparsec.Parser.Then
-      Symparsec.Parser.Then.VoidLeft
-      Symparsec.Parser.Then.VoidRight
+      Symparsec.Parser.TakeWhile
+      Symparsec.Parser.Try
       Symparsec.Parser.While
       Symparsec.Parser.While.Predicates
       Symparsec.Parsers
       Symparsec.Run
+      Symparsec.Utils
   other-modules:
       Paths_symparsec
   hs-source-dirs:
@@ -66,7 +69,7 @@
       TypeFamilies
       DataKinds
       MagicHash
-  ghc-options: -Wall -Wno-unticked-promoted-constructors
+  ghc-options: -fhide-source-paths -Wall
   build-depends:
       base >=4.18 && <5
     , defun-core ==0.1.*
@@ -92,7 +95,7 @@
       TypeFamilies
       DataKinds
       MagicHash
-  ghc-options: -Wall -Wno-unticked-promoted-constructors
+  ghc-options: -fhide-source-paths -Wall
   build-depends:
       base >=4.18 && <5
     , defun-core ==0.1.*
diff --git a/test/Main.hs b/test/Main.hs
--- a/test/Main.hs
+++ b/test/Main.hs
@@ -2,22 +2,20 @@
 
 import Test.TypeSpec
 import Symparsec
+import DeFun.Core ( type Con2 )
 
 main :: IO ()
 main = print spec
 
--- The type errors for failures are HILARIOUS if you're into that sort of thing.
--- Try messing with a test or two and see mad GHC gets!
-
-type CstrX_Y =
-          (Literal "Cstr" :*>: Isolate 2 NatDec)
-    :<*>: (Literal "_"    :*>: Isolate 2 NatHex)
+type CstrX_Y = LiftA2 (Con2 '(,))
+    (Literal "Cstr" *> Isolate 2 NatDec)
+    (Literal "_"    *> Isolate 2 NatHex)
 
 spec :: Expect
     '[ Run (Literal "raehik") "raehik" `Is` Right '( '(), "")
      , Run (Literal "raeh") "raehraeh" `Is` Right '( '(), "raeh")
-     , Run (Skip 3 :*>: Literal "HI") "...HI" `Is` Right '( '(), "")
-     , Run (Literal "0x" :*>: NatHex) "0xfF" `Is` Right '( 255, "")
+     , Run (Skip 3 *> Literal "HI") "...HI" `Is` Right '( '(), "")
+     , Run (Literal "0x" *> NatHex) "0xfF" `Is` Right '( 255, "")
      , Run CstrX_Y "Cstr12_AB" `Is` Right '( '(12, 0xAB), "")
      ]
 spec = Valid