diff --git a/README.md b/README.md
index cfa9a30..b7948e7 100644
--- a/README.md
+++ b/README.md
@@ -17,15 +17,14 @@ Define a type-level parser:
 
 ```haskell
 import Symparsec
-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_etc"
-Run ...
+ghci> :k! Run' PExample "xFF_etc"
+Run' ...
 = Right '( '(255, "etc"), "")
 ```
 
diff --git a/TODO.md b/TODO.md
index e0d97af..f1d1652 100644
--- a/TODO.md
+++ b/TODO.md
@@ -1,16 +1,31 @@
 # Symparsec to-dos
+* custom state necessitates `TypeAbstractions` (GHC 9.8) sometimes: clarify
+
 ## Proofs (tests?)
 * `Isolate n TakeRest` is equivalent to `Take n`
 
 ## Combinators
-* `Choice :: [PParser a] -> PParser a`
-* various from parser-combinators, megaparsec (e.g. `sepBy`)
+* `Fold`. `Foldr`, I guess? Idk.
+* various from parser-combinators, megaparsec. find out the most common/used
 
 ## Example uses of Symparsec to write, present
-### generic-data-functions
-Fiddly and awfully abstract. WIP.
+### Generics, parsing constructor & field names
+* generic-data-functions: done for 1.0. fiddly and awfully abstract. TODO
+* aeson: super real world! do constructor & field name parsing, instead of
+  `constructorTagModifier` and such. pretty daunting though (nasty generics)
+
+### JSON parser
+Big, real world, funny. Roll it by hand (Aeson's parsing is very complex).
+
+## Completed examples
+Just to remind myself what is already attempted.
+
+### Expression parser
+Not very well-written, mind you, but it works. I could probably write a
+`MakeExprParser` like in megaparsec, but it's terribly complex.
+
+### Format string parser
+Directly from typelits-printf, minimal changes.
 
-### aeson
-Big but real world. Write some new aeson generics which do type-level
-constructor name parsing, instead of using `constructorTagModifier`. Daunting
-because aeson has complex generics.
+### Something that uses multi-line `Symbol`s
+Threw into the expression parser. 9.12 exclusive due to `MultinelineStrings`.
diff --git a/docs/formatting.md b/docs/formatting.md
index 954e118..dd2cc19 100644
--- a/docs/formatting.md
+++ b/docs/formatting.md
@@ -16,15 +16,19 @@ defunctionalized arrow. This means some promoted types might not actually use
 the term-level type directly. That's fine.
 
 ## Binders
-* parser string type binder: `str`
+* parser state string type: `str`
   * don't use `sym`.
-* parser return type binder: `a`
-* parser reply type binder: `rep`
+* parser state numeric type: `n`
+  * slightly preferred over `i` because it's a `Natural`
+* parser return type: `a`
+* parser reply: `rep`
   * ? `r` is fine, but it's often used for continuations. `rep` sounds like
     `representation` but that's it, so I consider it fairly unambiguous
-* parser state type binder: `s`
-* parser state index type binder: `idx`
+* parser state: `ps`
+* parser state custom state: `s`
+  * TODO. term/type s/s is fine because separate namespaces, but type/kind s/s
+    doesn't work, so I need to use type/kind custom/s. I should do the same for
+    all uses. TODO annoying refactor. maybe use `cst` if you want shorter?
+* parser state index: `idx`
   * simple, obvious
-* parser state number kind binder: `n`
-  * slightly preferred over `i` because it's a `Natural`
-* parser error type binder: `e`
+* parser error: `e`
diff --git a/src/Symparsec.hs b/src/Symparsec.hs
index 548a2b7..8f82b59 100644
--- a/src/Symparsec.hs
+++ b/src/Symparsec.hs
@@ -5,7 +5,7 @@ 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"
+-- > :k! Symparsec.'Run'' (P.Take 1) "hello"
 @
 -}
 
@@ -13,7 +13,9 @@ module Symparsec
   (
   -- * Base definitions
     type Run
+  , type Run'
   , type RunTest
+  , type RunTest'
 
   -- * Parsers
   , module Symparsec.Parsers
diff --git a/src/Symparsec/Example/Expr.hs b/src/Symparsec/Example/Expr.hs
index b3c4adb..4708345 100644
--- a/src/Symparsec/Example/Expr.hs
+++ b/src/Symparsec/Example/Expr.hs
@@ -1,73 +1,56 @@
 {-# LANGUAGE UndecidableInstances #-}
-
--- | An example Symparsec parser for a basic expression tree.
+{-# LANGUAGE TypeAbstractions #-}
+{-# LANGUAGE MultilineStrings #-} -- GHC 9.12, for TestProg
 
 module Symparsec.Example.Expr where
 
 import Symparsec.Parser.Common
 import Symparsec.Utils ( type IfNatLte )
-import Symparsec.Parser.Natural
+import Symparsec.Parsers
 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.
--}
+import Symparsec.Parser.While.Predicates ( type IsDecDigitSym, type IsAlphaSym, type IsChar )
+--import GHC.TypeNats qualified as TypeNats
+import DeFun.Core
 
--- | A basic expression tree, polymorphic over a single literal type.
-data Expr a
-  = EBOp BOp (Expr a) (Expr a)
-  | ELit a
+-- SAKS necessitates TypeAbstractions
+type VarParser :: PParser s Symbol
+type VarParser @s = TakeWhile1 @s IsAlphaSym
 
 -- | A binary operator.
 data BOp = Add | Sub | Mul | Div
 
--- | 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
-
-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 Expr str a
+  = EBOp BOp (Expr str a) (Expr str a)
+  | ELit a
+  | EVar str
+--  | ELet str (Expr str a) (Expr str a)
+type PExpr = Expr Symbol Natural
 
 data ExprTok
   = TokBOp BOp
   | TokParenL
   | TokParenR
 
-type PExpr :: PParser (Expr Natural)
-data PExpr s
-type instance App PExpr s = PExprNext s '[] '[] (UnconsState s)
+type ExprParser :: PParser s PExpr
+data ExprParser ps
+type instance App ExprParser ps = PExprNext ps '[] '[] (UnconsState ps)
 type PExprNext
-    :: PState
+    :: PState s
     -> [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 family PExprEnd sPrev s ops exprs where
-    PExprEnd sPrev s (TokBOp op:ops) exprs      = PExprEndPopOp sPrev s ops exprs op
+    -> [PExpr]
+    -> (Maybe Char, PState s)
+    -> PReply s PExpr
+type family PExprNext psPrev ops exprs mps where
+    PExprNext psPrev ops exprs '(Just ch, ps) =
+        PExprCh psPrev ps ops exprs ch
+    PExprNext psPrev ops exprs '(Nothing, ps) = PExprEnd psPrev ps ops exprs
+
+type family PExprEnd psPrev ps ops exprs where
+    PExprEnd psPrev ps (TokBOp op:ops) exprs = PExprEndPopOp psPrev ps 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
+    PExprEnd psPrev ps '[]      (expr:'[]) = 'Reply (OK expr) ps
+    PExprEnd psPrev ps '[]      _          =
+        'Reply (Err (Error1 "badly formed expression")) psPrev
 
 type family PExprEndPopOp sPrev s ops exprs op where
     PExprEndPopOp sPrev s ops (r:l:exprs) bop =
@@ -79,50 +62,61 @@ 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) =
+type family PExprELit psPrev ps ops exprs ch mDigit where
+    PExprELit psPrev ps 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)
+            (While IsDecDigitSym (NatBase1 10 ParseDigitDecSym digit) @@ ps)
+    PExprELit psPrev ps ops exprs  ch Nothing      =
+        PExprEVarEnd ps ch ops exprs (VarParser @@ psPrev)
 
 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) =
+    PExprELitEnd ops exprs ('Reply (OK  n) ps) =
+        PExprNext ps ops (ELit n : exprs) (UnconsState ps)
+    PExprELitEnd ops exprs ('Reply (Err e) ps) =
         -- 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
+-- TODO weird state parsing here. usually we're looking ahead by 1 char, but my
+-- VarParser is better and doesn't need to. BUT, we need to keep our lookahead
+-- state for the BOp parser. lol
+type family PExprEVarEnd ps ch ops exprs rep where
+    PExprEVarEnd ps ch ops exprs ('Reply (OK  v) ps') =
+        PExprNext ps' ops (EVar v : exprs) (UnconsState ps')
+    PExprEVarEnd ps ch ops exprs ('Reply (Err e) psPrev) =
+        PExprEBOp psPrev ps ops exprs ch (PExprEBOpOpCh ch)
+
+type family PExprEBOp psPrev ps ops exprs ch mbop where
+    PExprEBOp psPrev ps ops exprs ch (Just (TokBOp bop)) =
+        PExprEBOp' psPrev ps bop (BOpPrec bop) exprs ops
+    PExprEBOp psPrev ps ops exprs ch (Just TokParenL) =
+        PExprNext psPrev (TokParenL:ops) exprs (UnconsState ps)
+    PExprEBOp psPrev ps ops exprs ch (Just TokParenR) =
+        PExprParenRStart psPrev ps exprs ops
+    PExprEBOp psPrev ps ops exprs ch Nothing =
+        -- TODO erroring here means PExpr must consume WHOLE string lol.
+        -- 'Reply (Err (Error1 "bad expression, expected digit or operator")) psPrev
+        PExprEnd psPrev psPrev ops exprs
+
+type family PExprParenRStart psPrev ps exprs ops where
+    PExprParenRStart psPrev ps exprs (TokParenL : ops) =
+        'Reply (Err (Error1 "invalid bracket syntax (empty brackets, or otherwise bad)")) psPrev
+    PExprParenRStart psPrev ps exprs ops =
+        PExprParenR psPrev ps exprs ops
+
+type family PExprParenR psPrev ps exprs ops where
+    PExprParenR psPrev ps exprs (TokBOp bop : ops) =
+        PExprParenRPopBOp psPrev ps bop ops exprs
+    PExprParenR psPrev ps exprs (TokParenL : ops) =
+        PExprNext psPrev ops exprs (UnconsState ps)
+    PExprParenR psPrev ps exprs ops =
+        'Reply (Err (Error1 "badly formed expression")) psPrev
+
+type family PExprParenRPopBOp psPrev ps bop ops exprs where
+    PExprParenRPopBOp psPrev ps bop ops (r:l:exprs) =
+        PExprParenR psPrev ps (EBOp bop l r : exprs) ops
+    PExprParenRPopBOp psPrev ps bop ops      exprs  =
+        'Reply (Err (Error1 "badly formed expression")) psPrev
 
 type family PExprEBOpOpCh ch where
     PExprEBOpOpCh '+' = Just (TokBOp Add)
@@ -134,28 +128,28 @@ type family PExprEBOpOpCh ch where
     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) =
+    :: PState s -> PState s -> BOp -> Natural -> [PExpr] -> [ExprTok]
+    -> PReply s PExpr
+type family PExprEBOp' psPrev ps op prec exprs ops where
+    PExprEBOp' psPrev ps 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)
+            (PExprEBOpPop psPrev ps op prec opPrev ops exprs)
+            (PExprNext psPrev (TokBOp op : TokBOp opPrev : ops) exprs (UnconsState ps))
+    PExprEBOp' psPrev ps op prec exprs '[]          =
+        PExprNext ps '[TokBOp op] exprs (UnconsState ps)
 
     -- 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
+    PExprEBOp' psPrev ps op prec exprs (TokParenL : ops) =
+        PExprNext psPrev (TokBOp op : TokParenL : ops) exprs (UnconsState ps)
+    PExprEBOp' psPrev ps op prec exprs (TokParenR : ops) =
+        PExprNext psPrev (TokBOp op : TokParenR : ops) exprs (UnconsState ps)
+
+type family PExprEBOpPop psPrev ps op prec opPrev ops exprs where
+    PExprEBOpPop psPrev ps op prec opPrev ops (r:l:exprs) =
+        PExprEBOp' psPrev ps op prec (EBOp opPrev l r : exprs) ops
+    PExprEBOpPop psPrev ps op prec opPrev ops exprs =
+        'Reply (Err (Error1 "badly formed expression")) psPrev
 
 type BOpPrec :: BOp -> Natural
 type family BOpPrec bop where
@@ -165,24 +159,35 @@ type family BOpPrec bop where
     BOpPrec Div = 3
 
 {-
-import GHC.TypeError qualified as TE
-
--- | Build an 'Expr' from a postfix stack (RPN style).
+-- | Evaluate an 'Expr' of 'Natural's on the type level.
 --
--- 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")
+-- 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
+
+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 Decl str a = Decl
+  { name :: str
+  , expr :: Expr str a
+  }
+type PDecl = Decl Symbol Natural
+
+type DeclParser :: PParser s PDecl
+type DeclParser @s = LiftA2 @s (Con2 'Decl) (VarParser @s <* TakeWhile (IsChar ' ')) (Literal @s ":=" *> ExprParser @s)
+
+type DeclListParser :: PParser s [PDecl]
+type DeclListParser @s = SepBy DeclParser (TakeWhile1 (IsChar '\n')) <* Eof
+
+type TestProg = """
+abc := 1+2+3
+xyz := abc / 2
+"""
diff --git a/src/Symparsec/Example/Printf.hs b/src/Symparsec/Example/Printf.hs
index e1adf2b..df4646f 100644
--- a/src/Symparsec/Example/Printf.hs
+++ b/src/Symparsec/Example/Printf.hs
@@ -1,4 +1,5 @@
 {-# LANGUAGE UndecidableInstances #-}
+{-# LANGUAGE TypeAbstractions #-}
 
 {- | The typelits-printf format string parser.
 
@@ -25,20 +26,28 @@ import Symparsec.Parser.Try
 
 -- typelits-printf compatibility layer
 -- typelits-printf actually does @<* Pure c@ after. but I prefer not to
+type AsChar :: Char -> PParser s ()
 type AsChar c = Literal (ConsSymbol c "")
+type AnyChar :: PParser s Char
 type AnyChar = Take1
+-- TODO: adding the following kind signature makes GHC type error, it
+-- initialises an inner s0 and doesn't see s ~ s0. omitting it has GHC
+-- understand the kind polymorphism just fine.
+-- doesn't happen for other parsers e.g. Literal. why?
+-- TODO: looks like it happens with type synonyms. oh dear
+--type Number :: PParser s Natural
 type Number = NatBaseWhile 10 ParseDigitDecSym
 
 -- special parser that I probably don't want (surely can just combine)
 -- backtracks!!
-type NotChar :: Char -> PParser Char
-data NotChar c s
-type instance App (NotChar c) s = NotChar' c s (UnconsState s)
-type family NotChar' cNo sPrev s where
-    NotChar' cNo sPrev '(Just  c, s) = If (c == cNo)
-        ('Reply (Err (Error1 "got the char we didn't want")) sPrev)
-        ('Reply (OK c) s)
-    NotChar' cNo sPrev '(Nothing, s) = 'Reply (Err (Error1 "empty string")) sPrev
+type NotChar :: Char -> PParser s Char
+data NotChar c ps
+type instance App (NotChar c) ps = NotChar' c ps (UnconsState ps)
+type family NotChar' cNo psPrev ps where
+    NotChar' cNo psPrev '(Just  c, ps) = If (c == cNo)
+        ('Reply (Err (Error1 "got the char we didn't want")) psPrev)
+        ('Reply (OK c) ps)
+    NotChar' cNo psPrev '(Nothing, ps) = 'Reply (Err (Error1 "empty string")) psPrev
 
 -- extras missing from defun-core
 type Con4 :: (a -> b -> c -> d -> e) -> a ~> b ~> c ~> d ~> e
@@ -71,26 +80,26 @@ data Flags = Flags
   , fAlternate :: Bool
   }
 
-type FlagParser :: PParser Flags
-data FlagParser s
-type instance App FlagParser s = PFlags' EmptyFlags s (UnconsState s)
+type FlagParser :: PParser s Flags
+data FlagParser ps
+type instance App FlagParser ps = PFlags' EmptyFlags ps (UnconsState ps)
 
 type EmptyFlags = 'Flags Nothing Nothing False
 
-type PFlags' :: Flags -> PState -> (Maybe Char, PState) -> PReply Flags
-type family PFlags' flags sPrev s where
-  PFlags' ('Flags d i l) sPrev '(Just '-', s) =
-    PFlags' ('Flags (Just (UpdateAdjust d LeftAdjust)) i l) s (UnconsState s)
-  PFlags' ('Flags d i l) sPrev '(Just '0', s) =
-    PFlags' ('Flags (Just (UpdateAdjust d ZeroPad))    i l) s (UnconsState s)
-  PFlags' ('Flags d i l) sPrev '(Just '+', s) =
-    PFlags' ('Flags d (Just (UpdateSign i SignPlus))     l) s (UnconsState s)
-  PFlags' ('Flags d i l) sPrev '(Just ' ', s) =
-    PFlags' ('Flags d (Just (UpdateSign i SignSpace))    l) s (UnconsState s)
-  PFlags' ('Flags d i l) sPrev '(Just '#', s) =
-    PFlags' ('Flags d i True)                               s (UnconsState s)
-  PFlags' flags sPrev '(_, s) =
-    'Reply (OK flags) sPrev
+type PFlags' :: Flags -> PState s -> (Maybe Char, PState s) -> PReply s Flags
+type family PFlags' flags psPrev mps where
+  PFlags' ('Flags d i l) psPrev '(Just '-', ps) =
+    PFlags' ('Flags (Just (UpdateAdjust d LeftAdjust)) i l) ps (UnconsState ps)
+  PFlags' ('Flags d i l) psPrev '(Just '0', ps) =
+    PFlags' ('Flags (Just (UpdateAdjust d ZeroPad))    i l) ps (UnconsState ps)
+  PFlags' ('Flags d i l) psPrev '(Just '+', ps) =
+    PFlags' ('Flags d (Just (UpdateSign i SignPlus))     l) ps (UnconsState ps)
+  PFlags' ('Flags d i l) psPrev '(Just ' ', ps) =
+    PFlags' ('Flags d (Just (UpdateSign i SignSpace))    l) ps (UnconsState ps)
+  PFlags' ('Flags d i l) psPrev '(Just '#', ps) =
+    PFlags' ('Flags d i True)                               ps (UnconsState ps)
+  PFlags' flags psPrev '(_, ps) =
+    'Reply (OK flags) psPrev
 
 type family UpdateAdjust d1 d2 where
   UpdateAdjust Nothing d2 = d2
@@ -113,7 +122,6 @@ data FieldFormat = FF
   }
 
 -- copied as-is except for 'Con5'
-type FFParser :: PParser FieldFormat
 type FFParser = Con5 FF
     <$> FlagParser
     <*> Optional Number
@@ -132,3 +140,28 @@ type FmtStrParser =
     ( (Con1 Left <$> ((Some (NotChar '%' <|> Try (AsChar '%' *> AsChar '%' *> Pure '%')))))
         <|> (Con1 Right <$> (AsChar '%' *> FFParser))
     )
+
+type Test1 :: PParser s Char
+type Test1 = Take1
+
+type Test2 :: PParser s Char
+type Test2 = Test1
+
+type Test3 :: PParser s Char
+type Test3 = AnyChar
+
+-- This one works with or without the visible kind argument.
+type Test4 :: Char -> PParser s Char
+type Test4 c = Pure c
+
+-- Standalone kind signature causes type error.
+-- Adding type abstraction syntax fixes.
+type Test5 :: PParser s Char
+type Test5 @s = Pure @s 'c'
+
+type Test6 :: PParser s a
+type Test6 = Empty
+
+-- Kind signature causes type error.
+--type Test7 :: PParser s ()
+type Test7 = Literal "asd"
diff --git a/src/Symparsec/Parser.hs b/src/Symparsec/Parser.hs
index 696f31d..5f743b9 100644
--- a/src/Symparsec/Parser.hs
+++ b/src/Symparsec/Parser.hs
@@ -14,9 +14,12 @@ import Singleraeh.List
 --import Singleraeh.Symbol
 
 -- | Parser state.
-data State str n = State
+data State str n s = State
+  -- | Custom state.
+  { custom :: s
+
   -- | Remaining input.
-  { remaining :: str
+  , remaining :: str
 
   -- | Remaining permitted length.
   --
@@ -40,17 +43,20 @@ data State str n = State
 type PState = State Symbol Natural
 
 -- | Singled 'State'.
-data SState (s :: PState) where
-    SState :: SSymbol rem -> SNat len -> SNat idx -> SState ('State rem len idx)
+data SState (ss :: s -> Type) (ps :: PState s) where
+    SState :: ss s -> SSymbol rem -> SNat len -> SNat idx -> SState ss ('State s rem len idx)
 
 -- | Demote an 'SState'.
-demoteSState :: SState s -> State String Natural
-demoteSState (SState srem slen sidx) =
-    State (fromSSymbol srem) (fromSNat slen) (fromSNat sidx)
+demoteSState
+    :: (forall s. ss s -> ds)
+    -> SState ss ps
+    -> State String Natural ds
+demoteSState demoteSS (SState ss srem slen sidx) =
+    State (demoteSS ss) (fromSSymbol srem) (fromSNat slen) (fromSNat sidx)
 
-instance Demotable SState where
-    type Demote SState = State String Natural
-    demote = demoteSState
+instance Demotable ss => Demotable (SState ss) where
+    type Demote (SState ss) = State String Natural (Demote ss)
+    demote = demoteSState demote
 
 {-
 data Span n = Span
@@ -82,29 +88,30 @@ instance Demotable SError where
 --
 -- TODO: megaparsec also returns a bool indicating if any input was consumed.
 -- Unsure what it's used for.
-data Reply str n a = Reply
+data Reply str n s a = Reply
   { result :: Result str n a -- ^ Parse result.
-  , state  :: State str n    -- ^ Final parser state.
+  , state  ::  State str n s -- ^ Final parser state.
   } deriving stock Show
 
 -- | Promoted 'Reply'.
 type PReply = Reply Symbol Natural
 
 -- | Singled 'Reply'.
-data SReply (sa :: a -> Type) (rep :: PReply a) where
-    SReply :: SResult sa result -> SState state -> SReply sa ('Reply result state)
+data SReply (ss :: s -> Type) (sa :: a -> Type) (rep :: PReply s a) where
+    SReply :: SResult sa result -> SState ss state -> SReply ss sa ('Reply result state)
 
 -- | 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)
+    :: (forall s. ss s -> ds)
+    -> (forall a. sa a -> da)
+    -> SReply ss sa rep
+    -> Reply String Natural ds da
+demoteSReply demoteSS demoteSA (SReply sresult sstate) =
+    Reply (demoteSResult demoteSA sresult) (demoteSState demoteSS sstate)
 
-instance Demotable sa => Demotable (SReply sa) where
-    type Demote (SReply sa) = Reply String Natural (Demote sa)
-    demote = demoteSReply demote
+instance (Demotable ss, Demotable sa) => Demotable (SReply ss sa) where
+    type Demote (SReply ss sa) = Reply String Natural (Demote ss) (Demote sa)
+    demote = demoteSReply demote demote
 
 -- | Parse result: a value, or an error.
 data Result str n a = OK a            -- ^ Parser succeeded.
@@ -137,14 +144,14 @@ instance Demotable sa => Demotable (SResult sa) where
     demote = demoteSResult demote
 
 -- | A parser is a function on parser state.
-type Parser str n a = State str n -> Reply str n a
+type Parser str n s a = State str n s -> Reply str n s a
 
 -- | Promoted 'Parser': a defunctionalization symbol to a function on promoted
 --   parser state.
-type PParser a = PState ~> PReply a
+type PParser s a = PState s ~> PReply s a
 
 -- | Singled 'Parser'.
-type SParser sa p = Lam SState (SReply sa) p
+type SParser ss sa p = Lam (SState ss) (SReply ss sa) p
 --data SParser (sa :: a -> Type) (p :: PParser a) where
  --   SParser :: Lam SState (SReply sa) (PParser a)
 
diff --git a/src/Symparsec/Parser/Alternative.hs b/src/Symparsec/Parser/Alternative.hs
index ff3f9bd..ff75cad 100644
--- a/src/Symparsec/Parser/Alternative.hs
+++ b/src/Symparsec/Parser/Alternative.hs
@@ -6,6 +6,8 @@ module Symparsec.Parser.Alternative
   ( type (<|>), type Empty
   , type Optional
   , type Many, type Some
+  , type SepBy, type SepBy1
+  , type Choice
   ) where
 
 import Symparsec.Parser.Functor
@@ -20,22 +22,22 @@ import qualified Singleraeh.List as List
 -- Does not backtrack. Wrap parsers with 'Symparsec.Parser.Try' as needed.
 --
 -- TODO shitty errors
-type (<|>) :: PParser a -> PParser a -> PParser a
+type (<|>) :: PParser s a -> PParser s a -> PParser s 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
+data (<|>) l r ps
+type instance App (l <|> r) ps = Plus r (l @@ ps)
+type Plus :: PParser s a -> PReply s a -> PReply s 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
+    Plus r ('Reply (OK   a) ps) = 'Reply (OK a) ps
+    Plus r ('Reply (Err _e) ps) = r @@ ps
 
 -- | '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
+type Empty :: PParser s a
+data Empty ps
+type instance App Empty ps = 'Reply (Err (Error1 "called empty parser")) ps
 
 -- | 'Control.Alternative.optional' for parsers.
-type Optional :: PParser a -> PParser (Maybe a)
+type Optional :: PParser s a -> PParser s (Maybe a)
 type Optional p = Con1 Just <$> p <|> Pure Nothing
 
 {- Wow, I guess that works. But also, the manual version:
@@ -50,15 +52,39 @@ type family OptionalEnd rep where
 -- | 'Control.Alternative.many' for parsers.
 --
 -- Does not backtrack. Wrap parsers with 'Symparsec.Parser.Try' as needed.
-type Many :: PParser a -> PParser [a]
-data Many p s
-type instance App (Many p) s = Many' p '[] (p @@ s)
+type Many :: PParser s a -> PParser s [a]
+data Many p ps
+type instance App (Many p) ps = Many' p '[] (p @@ ps)
 type family Many' p as rep where
-    Many' p as ('Reply (OK   a) s) = Many' p (a:as) (p @@ s)
-    Many' p as ('Reply (Err _e) s) = 'Reply (OK (List.Reverse as)) s
+    Many' p as ('Reply (OK   a) ps) = Many' p (a:as) (p @@ ps)
+    Many' p as ('Reply (Err _e) ps) = 'Reply (OK (List.Reverse as)) ps
 
 -- | 'Control.Alternative.some' for parsers.
 --
 -- Does not backtrack. Wrap parsers with 'Symparsec.Parser.Try' as needed.
-type Some :: PParser a -> PParser [a]
+type Some :: PParser s a -> PParser s [a]
 type Some p = LiftA2 (Con2 '(:)) p (Many p)
+
+-- | @'SepBy' p sep@ parses zero or more occurrences of @p@, separated by @sep@.
+--   Returns a list of values parsed by @p@.
+type SepBy :: PParser s a -> PParser s sep -> PParser s [a]
+type SepBy p sep = SepBy1 p sep <|> Pure '[]
+
+-- | @'SepBy1' p sep@ parses one or more occurrences of @p@, separated by @sep@.
+--   Returns a list of values parsed by @p@.
+type SepBy1 :: PParser s a -> PParser s sep -> PParser s [a]
+type SepBy1 p sep = LiftA2 (Con2 '(:)) p (Many (sep *> p))
+
+-- TODO doesn't backtrack, matching megaparsec.
+type Choice :: [PParser s a] -> PParser s a
+data Choice pList ps
+type instance App (Choice pList) ps = ChoiceStart pList ps
+
+type family ChoiceStart pList ps where
+    ChoiceStart '[]       ps = Empty @@ ps
+    ChoiceStart (p:pList) ps = ChoiceLoop pList (p @@ ps)
+
+type family ChoiceLoop pList rep where
+    ChoiceLoop _         ('Reply (OK  a) ps) = 'Reply (OK a) ps
+    ChoiceLoop (p:pList) ('Reply (Err e) ps) = ChoiceLoop pList (p @@ ps)
+    ChoiceLoop '[]       rep                 = rep -- TODO meh, not the best error
diff --git a/src/Symparsec/Parser/Applicative.hs b/src/Symparsec/Parser/Applicative.hs
index 7528525..cacb4d7 100644
--- a/src/Symparsec/Parser/Applicative.hs
+++ b/src/Symparsec/Parser/Applicative.hs
@@ -13,33 +13,35 @@ 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
+type (<*>) :: PParser s (a ~> b) -> PParser s a -> PParser s 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
+data (<*>) l r ps
+type instance App (l <*> r) ps = ApL r (l @@ ps)
+type ApL :: PParser s a -> PReply s (a ~> b) -> PReply s 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
+    ApL r ('Reply (OK  fa) ps) = (fa <$> r) @@ ps
+    ApL r ('Reply (Err e)  ps) = 'Reply (Err e) ps
 
 -- | '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
+type Pure :: forall s a. a -> PParser s a
+data Pure a ps
+type instance App (Pure a) ps = 'Reply (OK a) ps
 
 -- | '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
+    :: forall s a b c
+    .  (a ~> b ~> c) -> PParser s a -> PParser s b -> PParser s 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
+type (*>) :: PParser s a -> PParser s b -> PParser s 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
+type (<*) :: PParser s a -> PParser s b -> PParser s a
 infixl 4 <*
 type l <* r = LiftA2 ConstSym l r
diff --git a/src/Symparsec/Parser/Common.hs b/src/Symparsec/Parser/Common.hs
index 6db9507..60fe3d3 100644
--- a/src/Symparsec/Parser/Common.hs
+++ b/src/Symparsec/Parser/Common.hs
@@ -45,17 +45,17 @@ import GHC.TypeError qualified as TE
 --
 -- 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
+type UnconsState :: PState s -> (Maybe Char, PState s)
+type family UnconsState ps where
+    UnconsState ('State s rem 0   idx) = '(Nothing, 'State s rem 0 idx)
+    UnconsState ('State s rem len idx) = UnconsState' s (UnconsSymbol rem) len idx
 
 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 =
+    :: s -> Maybe (Char, Symbol) -> Natural -> Natural -> (Maybe Char, PState s)
+type family UnconsState' s mstr len idx where
+    UnconsState' s (Just '(ch, rem)) len idx =
+        '(Just ch, 'State s rem (len-1) (idx+1))
+    UnconsState' s 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")
 
diff --git a/src/Symparsec/Parser/Count.hs b/src/Symparsec/Parser/Count.hs
index e35b505..3554ac0 100644
--- a/src/Symparsec/Parser/Count.hs
+++ b/src/Symparsec/Parser/Count.hs
@@ -8,17 +8,17 @@ import qualified Singleraeh.List as List
 -- TODO Could possibly make more efficient.
 
 -- | @'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 Count :: Natural -> PParser s a -> PParser s [a]
+data Count n p ps
+type instance App (Count n p) ps = CountLoop p '[] n ps
 
-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)
+type family CountLoop p as n ps where
+    CountLoop p as 0 ps = 'Reply (OK (List.Reverse as)) ps
+    CountLoop p as n ps = CountLoopWrap p as n (p @@ ps)
 
 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) =
+    CountLoopWrap p as n ('Reply (OK  a) ps) =
+        CountLoop p (a:as) (n-1) ps
+    CountLoopWrap p as n ('Reply (Err e) ps) =
         -- TODO am I passing the wrong state back here?
-        'Reply (Err e) s
+        'Reply (Err e) ps
diff --git a/src/Symparsec/Parser/Ensure.hs b/src/Symparsec/Parser/Ensure.hs
index a249106..09a92d1 100644
--- a/src/Symparsec/Parser/Ensure.hs
+++ b/src/Symparsec/Parser/Ensure.hs
@@ -6,11 +6,11 @@ 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) =
+type Ensure :: Natural -> PParser s ()
+data Ensure n ps
+type instance App (Ensure n) ps = Ensure' n ps
+type family Ensure' n ps where
+    Ensure' n ('State s rem len idx) =
         IfNatLte n len
-            ('Reply (OK '()) ('State rem len idx))
-            ('Reply (Err (Error1 (EStrInputTooShort n len))) ('State rem len idx))
+            ('Reply (OK '()) ('State s rem len idx))
+            ('Reply (Err (Error1 (EStrInputTooShort n len))) ('State s rem len idx))
diff --git a/src/Symparsec/Parser/Eof.hs b/src/Symparsec/Parser/Eof.hs
index a403036..0c21e2a 100644
--- a/src/Symparsec/Parser/Eof.hs
+++ b/src/Symparsec/Parser/Eof.hs
@@ -5,11 +5,11 @@ 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 Eof :: PParser s ()
+data Eof ps
+type instance App Eof ps = Eof' (UnconsState ps)
+type family Eof' mps where
+    Eof' '(Nothing,  ps) = 'Reply (OK '()) ps
+    Eof' '(Just _ch, ps) = 'Reply (Err EEof) ps
 
 type EEof = Error1 "expected end of string"
diff --git a/src/Symparsec/Parser/Functor.hs b/src/Symparsec/Parser/Functor.hs
index 04c723f..57914b6 100644
--- a/src/Symparsec/Parser/Functor.hs
+++ b/src/Symparsec/Parser/Functor.hs
@@ -10,21 +10,21 @@ 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
+type (<$>) :: (a ~> b) -> PParser s a -> PParser s b
 infixl 4 <$>
-data (<$>) f p s
-type instance App (f <$> p) s = FmapEnd f (p @@ s)
+data (<$>) f p ps
+type instance App (f <$> p) ps = FmapEnd f (p @@ ps)
 
 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
+    FmapEnd f ('Reply (OK  a) ps) = 'Reply (OK  (f @@ a)) ps
+    FmapEnd f ('Reply (Err e) ps) = 'Reply (Err e)        ps
 
 -- | '<$' for parsers. Replace the parser result with the given value.
-type (<$) :: a -> PParser b -> PParser a
+type (<$) :: a -> PParser s b -> PParser s a
 infixl 4 <$
 type a <$ p = ConstSym1 a <$> p
 
 -- | 'Data.Functor.$>' for parsers. Flipped t'Symparsec.Parser.Functor.<$'.
-type ($>) :: PParser a -> b -> PParser b
+type ($>) :: PParser s a -> b -> PParser s b
 infixl 4 $>
 type p $> a = ConstSym1 a <$> p
diff --git a/src/Symparsec/Parser/Isolate.hs b/src/Symparsec/Parser/Isolate.hs
index f51827b..f9678da 100644
--- a/src/Symparsec/Parser/Isolate.hs
+++ b/src/Symparsec/Parser/Isolate.hs
@@ -6,39 +6,39 @@ import Symparsec.Parser.Common
 import Symparsec.Utils ( type IfNatLte )
 
 -- 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) =
+type Isolate :: Natural -> PParser s a -> PParser s a
+data Isolate n p ps
+type instance App (Isolate n p) ps = Isolate' n p ps
+type family Isolate' n p ps where
+    Isolate' n p ('State s 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))
+            (IsolateEnd len n (p @@ ('State s rem n idx)))
+            ('Reply (Err (Error1 (EStrInputTooShort n len))) ('State s rem len idx))
 
 --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)
+    IsolateEnd lenOrig n ('Reply (OK  a) ('State s rem 0   idx)) =
+        'Reply (OK  a) ('State s rem (lenOrig-n)     idx)
 
     -- isolated parser failed
-    IsolateEnd lenOrig n ('Reply (Err e) ('State rem len idx)) =
+    IsolateEnd lenOrig n ('Reply (Err e) ('State s rem len idx)) =
         -- TODO add some isolate meta
-        'Reply (Err e) ('State rem (lenOrig-n+len) idx)
+        'Reply (Err e) ('State s rem (lenOrig-n+len) idx)
 
     -- 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)
+    IsolateEnd lenOrig n ('Reply (OK _a) ('State s rem len idx)) =
+        'Reply (Err (EIsolateIncomplete len)) ('State s rem (lenOrig-n+len) idx)
 
 type EIsolateIncomplete n = Error1
     (    "isolated parser completed without consuming all input ("
       ++ ShowNatDec n ++ " remaining)" )
 
 -- TODO testing. args flipped because you're more likely to defun the len
-type IsolateSym :: PParser a -> Natural ~> PParser a
+type IsolateSym :: PParser s a -> Natural ~> PParser s 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
index e4190b7..3a84a29 100644
--- a/src/Symparsec/Parser/Literal.hs
+++ b/src/Symparsec/Parser/Literal.hs
@@ -25,17 +25,17 @@ type EWrongChar lit chExpect chGot =
 
 type EEof lit = EDuringLit lit "EOF while still parsing literal"
 
-type Literal :: Symbol -> PParser ()
-data Literal lit s
-type instance App (Literal lit) s = LiteralCheckLen lit s (Symbol.Length lit)
+type Literal :: Symbol -> PParser s ()
+data Literal lit ps
+type instance App (Literal lit) ps = LiteralCheckLen lit ps (Symbol.Length lit)
 
 -- 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 =
+type family LiteralCheckLen lit ps n where
+    LiteralCheckLen lit ('State s rem len idx) litLen =
         IfNatLte litLen len
-            (LiteralStep lit ('State rem len idx))
-            ('Reply (Err (ETooShort lit litLen len)) ('State rem len idx))
+            (LiteralStep lit ('State s rem len idx))
+            ('Reply (Err (ETooShort lit litLen len)) ('State s rem len idx))
 
 type LiteralStep lit s = Literal' lit s (UnconsSymbol lit) (UnconsState s)
 type family Literal' lit sPrev ch ms where
diff --git a/src/Symparsec/Parser/Monad.hs b/src/Symparsec/Parser/Monad.hs
index 6ae7350..c697492 100644
--- a/src/Symparsec/Parser/Monad.hs
+++ b/src/Symparsec/Parser/Monad.hs
@@ -8,11 +8,11 @@ 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
+type (>>=) :: PParser s a -> (a ~> PParser s b) -> PParser s 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
+data (>>=) l r ps
+type instance App (l >>= r) ps = BindL r (l @@ ps)
+type BindL :: (a ~> PParser s b) -> PReply s a -> PReply s 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
+    BindL r ('Reply (OK  a) ps) = r @@ a @@ ps
+    BindL r ('Reply (Err e) ps) = 'Reply (Err e) ps
diff --git a/src/Symparsec/Parser/Natural.hs b/src/Symparsec/Parser/Natural.hs
index cda6a63..1725854 100644
--- a/src/Symparsec/Parser/Natural.hs
+++ b/src/Symparsec/Parser/Natural.hs
@@ -1,7 +1,7 @@
 {-# LANGUAGE UndecidableInstances #-}
 
 module Symparsec.Parser.Natural
-  ( type NatBase, type NatBase1
+  ( type NatBase, type NatBase1, type NatBase1Sym
   , type NatDec
   , type NatHex
   , type NatBin
@@ -39,27 +39,27 @@ type NatHex = NatBase 16 ParseDigitHexSym
 --
 -- 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
+type NatBase :: Natural -> (Char ~> Maybe Natural) -> PParser s Natural
+data NatBase base parseDigit ps
+type instance App (NatBase base parseDigit) ps =
+    NatBaseStart base parseDigit ps (UnconsState ps)
+type family NatBaseStart base parseDigit psCh ps where
+    NatBaseStart base parseDigit psCh '(Just ch, ps) =
+        NatBaseLoop base parseDigit psCh ps 0 ch (parseDigit @@ ch) (UnconsState ps)
+    NatBaseStart base parseDigit psCh '(Nothing, ps) = 'Reply (Err EEmpty) psCh
 
 -- | 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
+type NatBase1 :: Natural -> (Char ~> Maybe Natural) -> Natural -> PParser s Natural
+data NatBase1 base parseDigit digit ps
+type instance App (NatBase1 base parseDigit digit) ps =
+    NatBase1' base parseDigit ps digit (UnconsState ps)
+type family NatBase1' base parseDigit psCh digit ps where
+    NatBase1' base parseDigit psCh digit '(Just ch, ps) =
+        NatBaseLoop base parseDigit psCh ps digit ch (parseDigit @@ ch) (UnconsState ps)
+    NatBase1' base parseDigit psCh digit '(Nothing, ps) =
+        'Reply (OK digit) ps
 
 type EEmpty = Error1 "no digits parsed" -- TODO not great eh
 type EInvalidDigit ch base =
@@ -68,23 +68,23 @@ type EInvalidDigit ch base =
 type NatBaseLoop
     :: Natural
     -> (Char ~> Maybe Natural)
-    -> PState
-    -> PState
+    -> PState s
+    -> PState s
     -> Natural
     -> Char
     -> Maybe Natural
-    -> (Maybe Char, PState)
-    -> PReply Natural
-type family NatBaseLoop base parseDigit sCh s n chCur mDigit ms where
+    -> (Maybe Char, PState s)
+    -> PReply s Natural
+type family NatBaseLoop base parseDigit psCh ps n chCur mDigit mps 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) =
+    NatBaseLoop base parseDigit psCh ps n chCur (Just digit) '(Just ch, psNext) =
+        NatBaseLoop base parseDigit ps psNext (n * base + digit) ch (parseDigit @@ ch) (UnconsState psNext)
+    NatBaseLoop base parseDigit psCh ps n chCur (Just digit) '(Nothing, psNext) =
+        'Reply (OK (n * base + digit)) psNext
+    NatBaseLoop base parseDigit psCh ps n chCur Nothing      '(_, psNext) =
         -- we've consumed the next character, but digit parse failed:
         -- backtrack and return error
-        'Reply (Err (EInvalidDigit chCur base)) sCh
+        'Reply (Err (EInvalidDigit chCur base)) psCh
 
 -- | Parse a non-empty 'Natural' using the given base and digit parser.
 --
@@ -93,44 +93,48 @@ type family NatBaseLoop base parseDigit sCh s n chCur mDigit ms where
 -- 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 NatBaseWhile :: Natural -> (Char ~> Maybe Natural) -> PParser s Natural
+data NatBaseWhile base parseDigit ps
+type instance App (NatBaseWhile base parseDigit) ps =
+    NatBaseWhileStart base parseDigit ps (UnconsState ps)
+type family NatBaseWhileStart base parseDigit psCh mps where
+    NatBaseWhileStart base parseDigit psCh '(Just ch, ps) =
+        NatBaseWhileStart2 base parseDigit psCh ps ch (parseDigit @@ ch) (UnconsState ps)
+    NatBaseWhileStart base parseDigit psCh '(Nothing, ps) = 'Reply (Err EEmpty) psCh
 
 -- TODO While1
 
-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) =
+type family NatBaseWhileStart2 base parseDigit psCh ps chChur mDigit mps where
+    NatBaseWhileStart2 base parseDigit psCh ps chCur (Just digit) '(Just ch, psNext) =
+        NatBaseWhileLoop base parseDigit ps psNext digit ch (parseDigit @@ ch) (UnconsState psNext)
+    NatBaseWhileStart2 base parseDigit psCh ps chCur (Just digit) '(Nothing, psNext) =
         -- parsed first digit, no more input: done
-        'Reply (OK digit) sNext
-    NatBaseWhileStart2 base parseDigit sCh s chCur Nothing      _ =
+        'Reply (OK digit) psNext
+    NatBaseWhileStart2 base parseDigit psCh ps chCur Nothing      _ =
         -- failed to parse first digit: backtrack and error
-        'Reply (Err (EInvalidDigit chCur base)) sCh
+        'Reply (Err (EInvalidDigit chCur base)) psCh
 
 -- Note that this parser never fails.
 type NatBaseWhileLoop
     :: Natural
     -> (Char ~> Maybe Natural)
-    -> PState
-    -> PState
+    -> PState s
+    -> PState s
     -> Natural
     -> Char
     -> Maybe Natural
-    -> (Maybe Char, PState)
-    -> PReply Natural
-type family NatBaseWhileLoop base parseDigit sCh s n chCur mDigit ms where
+    -> (Maybe Char, PState s)
+    -> PReply s Natural
+type family NatBaseWhileLoop base parseDigit psCh ps n chCur mDigit mps 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      _ =
+    NatBaseWhileLoop base parseDigit psCh ps n chCur (Just digit) '(Just ch, psNext) =
+        NatBaseWhileLoop base parseDigit ps psNext (n * base + digit) ch (parseDigit @@ ch) (UnconsState psNext)
+    NatBaseWhileLoop base parseDigit psCh ps n chCur (Just digit) '(Nothing, psNext) =
+        'Reply (OK (n * base + digit)) psNext
+    NatBaseWhileLoop base parseDigit psCh ps n chCur Nothing      _ =
         -- failed to parse next digit: backtrack and finish
-        'Reply (OK n) sCh
+        'Reply (OK n) psCh
+
+type NatBase1Sym :: Natural -> (Char ~> Maybe Natural) -> Natural ~> PParser s Natural
+data NatBase1Sym base parseDigit x
+type instance App (NatBase1Sym base parseDigit) x = NatBase1 base parseDigit x
diff --git a/src/Symparsec/Parser/Satisfy.hs b/src/Symparsec/Parser/Satisfy.hs
index 536b0aa..a60fc74 100644
--- a/src/Symparsec/Parser/Satisfy.hs
+++ b/src/Symparsec/Parser/Satisfy.hs
@@ -5,7 +5,7 @@ module Symparsec.Parser.Satisfy ( type Satisfy, type OneOf, type NoneOf ) where
 import Symparsec.Parser.Common
 
 -- may also be defined using @Token@
-type Satisfy :: (Char ~> Bool) -> PParser Char
+type Satisfy :: (Char ~> Bool) -> PParser s Char
 data Satisfy chPred ps
 type instance App (Satisfy chPred) ps = SatisfyStart chPred ps (UnconsState ps)
 
@@ -19,7 +19,7 @@ type family SatisfyValidate psPrev ps ch res where
     SatisfyValidate psPrev ps ch False =
         'Reply (Err (Error1 "satisfy: char failed predicate")) psPrev
 
-type OneOf :: [Char] -> PParser Char
+type OneOf :: [Char] -> PParser s Char
 type OneOf chs = Satisfy (ElemSym chs)
 
 -- TODO put in singleraeh
@@ -35,7 +35,7 @@ data ElemSym as a
 type instance App (ElemSym as) a = Elem a as
 
 -- may also be defined using @CompSym2 NotSym (ElemSym chs)@
-type NoneOf :: [Char] -> PParser Char
+type NoneOf :: [Char] -> PParser s Char
 --type NoneOf chs = Satisfy (CompSym2 NotSym (ElemSym chs))
 type NoneOf chs = Satisfy (NotElemSym chs)
 
diff --git a/src/Symparsec/Parser/Skip.hs b/src/Symparsec/Parser/Skip.hs
index d328d4f..3514697 100644
--- a/src/Symparsec/Parser/Skip.hs
+++ b/src/Symparsec/Parser/Skip.hs
@@ -8,14 +8,14 @@ import Symparsec.Parser.Applicative
 import Data.Type.Symbol qualified as Symbol
 
 -- | Skip forward @n@ characters. Fails if fewer than @n@ characters remain.
-type Skip :: Natural -> PParser ()
+type Skip :: Natural -> PParser s ()
 type Skip n = Ensure n *> SkipUnsafe 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))
+type SkipUnsafe :: Natural -> PParser s ()
+data SkipUnsafe n ps
+type instance App (SkipUnsafe n) ps = SkipUnsafe' n ps
+type family SkipUnsafe' n ps where
+    SkipUnsafe' n ('State s rem len idx) =
+        'Reply (OK '()) ('State s (Symbol.Drop n rem) (len-n) (idx+n))
diff --git a/src/Symparsec/Parser/Take.hs b/src/Symparsec/Parser/Take.hs
index c475791..8f02b49 100644
--- a/src/Symparsec/Parser/Take.hs
+++ b/src/Symparsec/Parser/Take.hs
@@ -6,27 +6,27 @@ import Symparsec.Parser.Common
 import Singleraeh.Symbol ( type RevCharsToSymbol )
 
 -- | Return the next @n@ characters.
-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 Take :: Natural -> PParser s Symbol
+data Take n ps
+type instance App (Take n) ps = Take' '[] n ps (UnconsState ps)
+type family Take' chs n psPrev ps where
+    Take' chs 0 psPrev _             = 'Reply (OK (RevCharsToSymbol chs)) psPrev
+    Take' chs n psPrev '(Just ch, ps) = Take' (ch:chs) (n-1) ps (UnconsState ps)
+    Take' chs n psPrev '(Nothing, ps) = 'Reply (Err (ETakeEnd n)) psPrev
 
 type ETakeEnd :: Natural -> PError
 type ETakeEnd n = Error1
     ( "tried to take " ++ ShowNatDec n ++ " chars from empty string" )
 
 -- | 'Take' defunctionalization symbol.
-type TakeSym :: Natural ~> PParser Symbol
+type TakeSym :: Natural ~> PParser s Symbol
 data TakeSym n
 type instance App TakeSym n = Take n
 
 -- | Return the next character.
-type Take1 :: PParser Char
-data Take1 s
-type instance App Take1 s = Take1' s (UnconsState s)
-type family Take1' sPrev s where
-    Take1' sPrev '(Just ch, s) = 'Reply (OK ch) s
-    Take1' sPrev '(Nothing, s) = 'Reply (Err (ETakeEnd 1)) sPrev
+type Take1 :: PParser s Char
+data Take1 ps
+type instance App Take1 ps = Take1' ps (UnconsState ps)
+type family Take1' psPrev ps where
+    Take1' psPrev '(Just ch, ps) = 'Reply (OK ch) ps
+    Take1' psPrev '(Nothing, ps) = 'Reply (Err (ETakeEnd 1)) psPrev
diff --git a/src/Symparsec/Parser/TakeRest.hs b/src/Symparsec/Parser/TakeRest.hs
index dd186b5..09d0567 100644
--- a/src/Symparsec/Parser/TakeRest.hs
+++ b/src/Symparsec/Parser/TakeRest.hs
@@ -8,12 +8,12 @@ import qualified Data.Type.Symbol as Symbol
 -- | 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 TakeRest :: PParser s Symbol
+data TakeRest ps
+type instance App TakeRest ps = TakeRest' ps
+type family TakeRest' ps where
+    TakeRest' ('State s rem len idx) =
+        'Reply (OK (Symbol.Take len rem)) ('State s (Symbol.Drop len rem) 0 (idx+len))
 
 {-
 import GHC.TypeLits
diff --git a/src/Symparsec/Parser/TakeWhile.hs b/src/Symparsec/Parser/TakeWhile.hs
index dcbb12c..b683638 100644
--- a/src/Symparsec/Parser/TakeWhile.hs
+++ b/src/Symparsec/Parser/TakeWhile.hs
@@ -1,6 +1,6 @@
 {-# LANGUAGE UndecidableInstances #-}
 
-module Symparsec.Parser.TakeWhile ( type TakeWhile ) where
+module Symparsec.Parser.TakeWhile ( type TakeWhile, type TakeWhile1 ) where
 
 import Symparsec.Parser.Common
 import Singleraeh.Symbol ( type RevCharsToSymbol )
@@ -10,25 +10,46 @@ import Singleraeh.Symbol ( type RevCharsToSymbol )
 -- 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 TakeWhile :: (Char ~> Bool) -> PParser s Symbol
+data TakeWhile chPred ps
+type instance App (TakeWhile chPred) ps = TakeWhileStart chPred ps (UnconsState ps)
 
-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 TakeWhileStart chPred psPrev mps where
+    TakeWhileStart chPred psPrev '(Just ch, ps) =
+        TakeWhileLoop chPred psPrev ps ch '[] (chPred @@ ch) (UnconsState ps)
+    TakeWhileStart chPred psPrev '(Nothing, ps) =
+        'Reply (OK "") psPrev
 
-type family TakeWhileLoop chPred sPrev sCh ch taken res ms where
+type family TakeWhileLoop chPred psPrev psCh ch taken res mps 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)
+    TakeWhileLoop chPred psPrev psCh ch taken True '(Just chNext, ps) =
+        TakeWhileLoop chPred psCh ps chNext (ch:taken) (chPred @@ chNext) (UnconsState ps)
 
     -- 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
+    TakeWhileLoop chPred sPrev psCh ch taken True '(Nothing, ps) =
+        'Reply (OK (RevCharsToSymbol (ch:taken))) psCh -- @psCh == ps@ should hold
 
     -- next char failed: backtrack and end
-    TakeWhileLoop chPred sPrev sCh ch taken False _ =
-        'Reply (OK (RevCharsToSymbol taken)) sPrev
+    TakeWhileLoop chPred psPrev psCh ch taken False _ =
+        'Reply (OK (RevCharsToSymbol taken)) psPrev
+
+-- | Take one or more 'Char's for which the supplied predicate holds.
+--
+-- Backtracks on failure. Same as megaparsec.
+type TakeWhile1 :: (Char ~> Bool) -> PParser s Symbol
+data TakeWhile1 chPred ps
+type instance App (TakeWhile1 chPred) ps = TakeWhile1Start chPred ps (UnconsState ps)
+
+type family TakeWhile1Start chPred psPrev mps where
+    TakeWhile1Start chPred psPrev '(Just ch, ps) =
+        TakeWhile1Start2 chPred psPrev ps ch (chPred @@ ch) (UnconsState ps)
+    TakeWhile1Start chPred psPrev '(Nothing, ps) =
+        'Reply (Err (Error1 "empty string")) psPrev
+
+type family TakeWhile1Start2 chPred psPrev ps ch res mps where
+    TakeWhile1Start2 chPred psPrev psCh ch True  '(Just chNext, ps) =
+        TakeWhileLoop chPred psCh ps chNext '[ch] (chPred @@ chNext) (UnconsState ps)
+    TakeWhile1Start2 chPred psPrev psCh ch True  '(Nothing,     ps) =
+        'Reply (OK (ConsSymbol ch "")) ps
+    TakeWhile1Start2 chPred psPrev psCh ch False _ =
+        'Reply (Err (Error1 "TakeWhile1 didn't even get 1 char")) psPrev
diff --git a/src/Symparsec/Parser/Token.hs b/src/Symparsec/Parser/Token.hs
index 4b3f6d6..e1fc246 100644
--- a/src/Symparsec/Parser/Token.hs
+++ b/src/Symparsec/Parser/Token.hs
@@ -5,7 +5,7 @@ module Symparsec.Parser.Token ( type Token ) where
 import Symparsec.Parser.Common
 
 -- | Should match @token@ from megaparsec. Backtracks.
-type Token :: (Char ~> Maybe a) -> PParser a
+type Token :: (Char ~> Maybe a) -> PParser s a
 data Token chParse ps
 type instance App (Token chParse) ps = TokenStart chParse ps (UnconsState ps)
 type family TokenStart chParse psPrev mps where
diff --git a/src/Symparsec/Parser/Try.hs b/src/Symparsec/Parser/Try.hs
index 720ddd1..32673e1 100644
--- a/src/Symparsec/Parser/Try.hs
+++ b/src/Symparsec/Parser/Try.hs
@@ -5,10 +5,10 @@ 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
+type Try :: PParser s a -> PParser s a
+data Try p ps
+type instance App (Try p) ps = Try' ps (p @@ ps)
+type Try' :: PState s -> PReply s a -> PReply s a
+type family Try' psPrev rep where
+    Try' psPrev ('Reply (OK  a) ps) = 'Reply (OK  a) ps
+    Try' psPrev ('Reply (Err e) ps) = 'Reply (Err e) psPrev
diff --git a/src/Symparsec/Parser/While.hs b/src/Symparsec/Parser/While.hs
index f88b580..5c38e91 100644
--- a/src/Symparsec/Parser/While.hs
+++ b/src/Symparsec/Parser/While.hs
@@ -5,28 +5,28 @@ module Symparsec.Parser.While ( type While ) where
 import Symparsec.Parser.Common
 
 -- | Run the given parser while the given character predicate succeeds.
-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 While :: (Char ~> Bool) -> PParser s a -> PParser s a
+data While chPred p ps
+type instance App (While chPred p) ps = While' chPred p ps
 
-type family While' chPred p s where
-    While' chPred p ('State rem len idx) =
-        WhileCountStart len rem idx chPred p (UnconsSymbol rem)
+type family While' chPred p ps where
+    While' chPred p ('State s rem len idx) =
+        WhileCountStart s len rem idx chPred p (UnconsSymbol rem)
 
-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 family WhileCountStart s len rem idx chPred p mstr where
+    WhileCountStart s len rem idx chPred p (Just '(ch, str)) =
+        WhileCount s len rem idx chPred p 0 (UnconsSymbol str) (chPred @@ ch)
+    WhileCountStart s len rem idx chPred p Nothing           = p @@ ('State s rem 0 idx)
 
-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))
+type family WhileCount s len rem idx chPred p n mstr res where
+    WhileCount s len rem idx chPred p n (Just '(ch, str)) True  =
+        WhileCount s len rem idx chPred p (n+1) (UnconsSymbol str) (chPred @@ ch)
+    WhileCount s len rem idx chPred p n (Just '(ch, str)) False =
+        WhileEnd (len-n)     (p @@ ('State s rem n     idx))
+    WhileCount s len rem idx chPred p n Nothing           True  =
+        WhileEnd (len-(n+1)) (p @@ ('State s rem (n+1) idx))
+    WhileCount s len rem idx chPred p n Nothing           False =
+        WhileEnd (len-n)     (p @@ ('State s rem n     idx))
 
 type family WhileEnd lenRest rep where
     -- TODO note that we don't require that the inner parser fully consumes.
@@ -35,5 +35,5 @@ type family WhileEnd lenRest rep where
     -- 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)
+    WhileEnd lenRest ('Reply res ('State s rem len idx)) =
+        'Reply res ('State s rem (lenRest+len) idx)
diff --git a/src/Symparsec/Parser/While/Predicates.hs b/src/Symparsec/Parser/While/Predicates.hs
index 9c8336c..803372c 100644
--- a/src/Symparsec/Parser/While/Predicates.hs
+++ b/src/Symparsec/Parser/While/Predicates.hs
@@ -4,6 +4,7 @@
 
 module Symparsec.Parser.While.Predicates where
 
+import Data.Type.Equality ( type (==) )
 import DeFun.Core
 
 -- | @A-Za-z@
@@ -116,3 +117,7 @@ type family IsDecDigit ch where
 type IsDecDigitSym :: Char ~> Bool
 data IsDecDigitSym ch
 type instance App IsDecDigitSym ch = IsDecDigit ch
+
+type IsChar :: Char -> Char ~> Bool
+data IsChar chTest ch
+type instance App (IsChar chTest) ch = ch == chTest
diff --git a/src/Symparsec/Parsers.hs b/src/Symparsec/Parsers.hs
index 88fe874..5e43c9b 100644
--- a/src/Symparsec/Parsers.hs
+++ b/src/Symparsec/Parsers.hs
@@ -11,6 +11,8 @@ module Symparsec.Parsers
   , type (<*>), type Pure, type LiftA2, type (*>), type (<*)
   , type (>>=)
   , type (<|>), type Empty, type Optional, type Many, type Some
+  , type SepBy, type SepBy1
+  , type Choice
 
   -- * Positional
   -- $positional
@@ -27,6 +29,7 @@ module Symparsec.Parsers
   , type Try
   , type While
   , type TakeWhile
+  , type TakeWhile1
   , type Count
   , type Token
   , type Satisfy
@@ -38,7 +41,7 @@ module Symparsec.Parsers
   , type Literal
 
   -- ** Naturals
-  , type NatBase
+  , type NatBase, type NatBase1, type NatBase1Sym
   , type NatDec
   , type NatHex
   , type NatBin
diff --git a/src/Symparsec/Run.hs b/src/Symparsec/Run.hs
index 930bc2e..7c2755d 100644
--- a/src/Symparsec/Run.hs
+++ b/src/Symparsec/Run.hs
@@ -2,7 +2,7 @@
 
 -- | Running Symparsec parsers.
 
-module Symparsec.Run ( type Run, type RunTest ) where
+module Symparsec.Run ( type Run, type Run', type RunTest, type RunTest' ) where
 
 import Symparsec.Parser
 import Data.Type.Symbol qualified as Symbol
@@ -13,31 +13,47 @@ import GHC.TypeError qualified as TE
 import TypeLevelShow.Doc
 import TypeLevelShow.Natural ( type ShowNatDec )
 
--- | Run the given parser on the given 'Symbol'.
+-- | Run a parser with some initial custom state on a '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)
+type Run :: PParser s a -> s -> Symbol -> Either TE.ErrorMessage (a, Symbol)
+type Run p custom str = RunEnd str (p @@ StateInit custom str)
 
-type RunEnd :: Symbol -> PReply a -> Either TE.ErrorMessage (a, Symbol)
+-- | Run a parser on a 'Symbol'. The parser must not use custom state.
+--
+-- * 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 = Run p '() str
+
+type RunEnd :: Symbol -> PReply s a -> Either TE.ErrorMessage (a, Symbol)
 type family RunEnd str rep where
-    RunEnd str ('Reply (OK  a) ('State  rem _len _idx)) =
+    RunEnd str ('Reply (OK  a) ('State _s  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)) =
+    RunEnd str ('Reply (Err e) ('State _s _rem _len  idx)) =
         Left (RenderPDoc (PrettyErrorTop idx str e))
 
--- | Run the given parser on the given 'Symbol', emitting a type error on
---   failure.
+-- | Run a parser with some initial custom state on a 'Symbol',
+--   emitting a type error on failure.
+--
+-- 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 a -> s -> Symbol -> (a, Symbol)
+type RunTest p custom str = FromRightTypeError (Run p custom str)
+
+-- | Run a parser on a 'Symbol', emitting a type error on failure.
+--   The parser must not use custom. state
 --
 -- 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 a -> Symbol -> (a, Symbol)
-type RunTest p str = FromRightTypeError (Run p str)
+type RunTest' :: PParser () a -> Symbol -> (a, Symbol)
+type RunTest' p str = RunTest p '() str
 
 type FromRightTypeError :: Either TE.ErrorMessage a -> a
 type family FromRightTypeError eea where
@@ -45,8 +61,8 @@ type family FromRightTypeError eea where
     FromRightTypeError (Left  e) = TE.TypeError e
 
 -- | Initial parser state for the given 'Symbol'.
-type StateInit :: Symbol -> PState
-type StateInit str = 'State str (Symbol.Length str) 0
+type StateInit :: s -> Symbol -> PState s
+type StateInit s str = 'State s str (Symbol.Length str) 0
 
 -- | Pretty print a top-level parser error.
 --
diff --git a/test/Main.hs b/test/Main.hs
index d49cd06..8e0f714 100644
--- a/test/Main.hs
+++ b/test/Main.hs
@@ -12,10 +12,10 @@ type CstrX_Y = LiftA2 (Con2 '(,))
     (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 CstrX_Y "Cstr12_AB" `Is` Right '( '(12, 0xAB), "")
+    '[ 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' CstrX_Y "Cstr12_AB" `Is` Right '( '(12, 0xAB), "")
      ]
 spec = Valid