Rewrite for flap v2.0.0.HEADmaster

Make `foldcase` syntactic sugar.

7 files changed, 508 insertions, 607 deletions

diff --git a/inky.ipkg b/inky.ipkg
index fe90df1..3fd9258 100644
--- a/inky.ipkg
+++ b/inky.ipkg
@@ -22,6 +22,7 @@ modules
   , Inky.Term.Pretty
   , Inky.Term.Pretty.Error
   , Inky.Term.Recompute
+  , Inky.Term.Rename
   , Inky.Type
   , Inky.Type.Pretty
   , Inky.Type.Substitution
diff --git a/src/Inky.idr b/src/Inky.idr
index 7fa9cad..bf8f26f 100644
--- a/src/Inky.idr
+++ b/src/Inky.idr
@@ -80,49 +80,51 @@ lexInkyString file = do
       throw (MkBounded "unexpected character" False (MkBounds line col line col))
   pure (filter (\x => relevant x.val.kind) tokens)
 
-Interpolation (List InkyKind) where
-  interpolate [t] = interpolate t
-  interpolate ts = "one of " ++ joinBy ", " (map interpolate ts)
+ParseErr : Type
+ParseErr = ParseErr (WithBounds InkyError) InkyKind
 
 doParse :
-  HasErr (WithBounds String) es =>
+  (e : HasErr (List1 ParseErr) es) =>
   (p : InkyParser False [<] [<] a) ->
-  {auto 0 wf : collectTypeErrs @{ListSet} [<] [<] [<] [<] p = []} ->
+  {auto 0 wf : WellFormed ListSet p} ->
   List (WithBounds InkyToken) ->
-  App es a
-doParse p toks =
-  case parse @{ListSet} p toks of
+  (s : state) ->
+  App es (a s)
+doParse p toks s =
+  case (parse ListSet p).runParser s toks of
     Ok res [] _ => pure res
-    Ok res (x :: _) _ =>
-      throw ("expected end of input; got token \{x.val.kind}" <$ x)
-    Err err => throw (parseErrToString err)
-  where
-  parseErrToString : ParseErr InkyKind -> WithBounds String
-  parseErrToString (BadEOF ts) =
-    irrelevantBounds "expected \{ts}; got end of input"
-  parseErrToString (Unexpected ts got) =
-    "expected \{ts}; got token \{got.val.kind}" <$ got
+    Ok res (x :: _) _ => throw @{e} (Unexpected [] x ::: [])
+    SoftErr errs _ _ => throw errs
+    Err errs => throw errs
 
 parseType :
-  Has [HasErr (WithBounds String), HasErr Err, HasErr IOError, FileIO] es =>
+  Has
+    [ HasErr (WithBounds String)
+    , HasErr (List1 ParseErr)
+    , HasErr Err
+    , HasErr IOError
+    , FileIO
+    ] es =>
   Maybe FilePath -> App es (Ty [<])
 parseType path = do
   txt <- readFileOrStdin path
   toks <- lexInkyString txt
-  res <- doParse OpenType toks
-  let Ok a = res.try [<]
-    | Errs errs => throw errs
-  pure a
+  doParse OpenType toks [<]
 
 parseTerm :
-  Has [HasErr (WithBounds String), HasErr Err, HasErr IOError, FileIO] es =>
-  (termPath, tyPath : Maybe FilePath) -> App es (Term (Sugar [<]) Bounds [<] [<])
+  Has
+    [ HasErr (WithBounds String)
+    , HasErr (List1 ParseErr)
+    , HasErr Err
+    , HasErr IOError
+    , FileIO
+    ] es =>
+  (termPath, tyPath : Maybe FilePath) ->
+  App es (Term (Sugar [<]) Bounds [<] [<])
 parseTerm termPath tyPath = do
   txt <- readFileOrStdin termPath
   toks <- lexInkyString txt
-  res <- doParse OpenTerm toks
-  let Ok t = res.try (Sugar [<]) [<] [<]
-    | Errs errs => throw errs
+  t <- doParse OpenTerm toks (Sugar [<], [<], [<])
   -- Annotate with type
   let Just _ = tyPath
     | Nothing => pure t
@@ -237,6 +239,7 @@ process :
     [ HasErr String
     , HasErr (WithBounds String)
     , HasErr (List1 $ WithBounds String)
+    , HasErr (List1 $ ParseErr)
     , HasErr (List1 ErrorMsg)
     , HasErr SynthFailed
     , FileIO
@@ -314,6 +317,11 @@ printSynthFailed (UhOh t err) =
   map (\(bounds, msg) => group $ align $ hang 2 $ pretty "\{bounds}:" <+> line <+> msg) $
   prettyNotSynths err
 
+Interpolation (List InkyKind) where
+  interpolate [] = "end of input"
+  interpolate [t] = interpolate t
+  interpolate ts = "one of " ++ joinBy ", " (map interpolate ts)
+
 main : IO ()
 main =
   run {l = MayThrow} $
@@ -327,6 +335,8 @@ main =
     (throw . map show . forget) $
   handleErr (List1 $ WithBounds String)
     (throw . map interpolate . forget) $
+  handleErr (List1 ParseErr)
+    (throw . map errToString . forget) $
   handleErr (WithBounds String)
     (throw . (::: [])) $
   handleErr IOError
@@ -336,7 +346,19 @@ main =
       printSynthFailed err
       primIO exitFailure) $
   process
-
--- main =
---   run {l = MayThrow} $
---   handle
+  where
+  errToString : ParseErr -> String
+  errToString (BadEOF expected) = "expected \{expected}, got end of input"
+  errToString (Unexpected expected got) =
+    interpolate ("expected \{expected}, got \{got.val.kind}" <$ got)
+  errToString (MapFail e) =
+    let
+      msg =
+        case e.val of
+          (UnboundTyVar str ctx) => "unbound type variable '\{str}'"
+          (UnboundTmVar str ctx) => "unbound term variable '\{str}'"
+          (DuplicateLabel str labels) => "repeated label '\{str}'"
+          (NeedsSugar mode) => "cannot use syntactic sugar here"
+          (NeedsQuote mode) => "cannot use splicing here"
+          NoQuotedTypes => "cannot write types within quotations"
+    in interpolate (msg <$ e)
diff --git a/src/Inky/Term.idr b/src/Inky/Term.idr
index 0f05f59..3c13580 100644
--- a/src/Inky/Term.idr
+++ b/src/Inky/Term.idr
@@ -95,6 +95,10 @@ data Term where
   Str :
     (meta : m) -> String ->
     Term (Sugar qtCtx) m tyCtx tmCtx
+  FoldCase :
+    (meta : m) -> Term (Sugar qtCtx) m tyCtx tmCtx ->
+    Row (x ** Term (Sugar qtCtx) m tyCtx (tmCtx :< x)) ->
+    Term (Sugar qtCtx) m tyCtx tmCtx
 
 %name Term e, f, t, u
 
@@ -122,6 +126,7 @@ export
 (List meta _).meta = meta
 (Cons meta _ _).meta = meta
 (Str meta _).meta = meta
+(FoldCase meta _ _).meta = meta
 
 --------------------------------------------------------------------------------
 -- Well Formed -----------------------------------------------------------------
diff --git a/src/Inky/Term/Desugar.idr b/src/Inky/Term/Desugar.idr
index 2ad87c9..53dcec9 100644
--- a/src/Inky/Term/Desugar.idr
+++ b/src/Inky/Term/Desugar.idr
@@ -1,8 +1,10 @@
 module Inky.Term.Desugar
 
 import Control.Monad.State
+import Data.DPair
 import Data.SortedMap
 import Inky.Term
+import Inky.Term.Rename
 
 -- Other Sugar -----------------------------------------------------------------
 
@@ -131,6 +133,16 @@ desugar' (Cons meta t u) =
   let f = cons meta in
   [| f (desugar' t) (desugar' u) |]
 desugar' (Str meta str) = string meta str
+desugar' (FoldCase meta e (MkRow ts fresh)) =
+  let
+    f = \e, ts =>
+      Fold meta e ("__tmp" **
+        Case meta (Var meta (toVar Here))
+          (fromAll
+            (mapProperty (map (bimap id (rename Rename.NoSugar (Keep (Drop Thinning.Id))))) ts)
+            fresh))
+  in
+  [| f (desugar' e) (desugarBranches ts) |]
 
 desugarAll [] = pure []
 desugarAll (t :: ts) = [| desugar' t :: desugarAll ts |]
diff --git a/src/Inky/Term/Parser.idr b/src/Inky/Term/Parser.idr
index 5cfd06b..42fd037 100644
--- a/src/Inky/Term/Parser.idr
+++ b/src/Inky/Term/Parser.idr
@@ -272,178 +272,109 @@ tokenMap =
 -- Error Monad -----------------------------------------------------------------
 
 public export
-data Result : (a : Type) -> Type where
-  Ok : a -> Result a
-  Errs : (msgs : List1 (WithBounds String)) -> Result a
+data InkyError : Type where
+  UnboundTyVar : String -> SnocList String -> InkyError
+  UnboundTmVar : String -> SnocList String -> InkyError
+  DuplicateLabel : String -> SnocList String -> InkyError
+  NeedsSugar : Mode -> InkyError
+  NeedsQuote : Mode -> InkyError
+  NoQuotedTypes : InkyError
 
-export
-Functor Result where
-  map f (Ok x) = Ok (f x)
-  map f (Errs msgs) = Errs msgs
-
-export
-Applicative Result where
-  pure = Ok
-
-  Ok f <*> Ok x = Ok (f x)
-  Ok f <*> Errs msgs = Errs msgs
-  Errs msgs <*> Ok x = Errs msgs
-  Errs msgs1 <*> Errs msgs2 = Errs (msgs1 ++ msgs2)
-
-export
-Monad Result where
-  Ok x >>= f = f x
-  Errs msgs >>= f = Errs msgs
-
-  join (Ok x) = x
-  join (Errs msgs) = Errs msgs
+-- Parser ----------------------------------------------------------------------
 
-export
-extendResult : Row a -> WithBounds (Assoc (Result a)) -> Result (Row a)
-extendResult row x =
-  case (isFresh row.names x.val.name) of
-    True `Because` prf => Ok ((:<) row (x.val.name :- !x.val.value) @{prf})
-    False `Because` _ =>
-      [| const (Errs $ singleton $ "duplicate name \"\{x.val.name}\"" <$ x) x.val.value |]
+%inline
+public export
+TermState : Type
+TermState = (Mode, SnocList String, SnocList String)
 
--- Parser ----------------------------------------------------------------------
+%inline
+public export
+Term' : (Mode, SnocList String, SnocList String) -> Type
+Term' state = Term (fst state) Bounds (fst $ snd state) (snd $ snd state)
 
+%inline
 public export
-InkyParser : Bool -> Context Type -> Context Type -> (a : Type) -> Type
+InkyParser :
+  {state : Type} -> (nil : Bool) ->
+  (locked, free : Context (state -> Type)) -> (a : state -> Type) -> Type
 InkyParser nil locked free a =
-  Parser InkyKind nil
+  Parser state (WithBounds InkyError) InkyKind nil
     (map (map (False,)) locked)
     (map (map (False,)) free)
     a
 
+%inline
 public export
-record ParseFun (as : SnocList Type) (0 p : Fun as Type) where
-  constructor MkParseFun
-  try : DFun as (chain (lengthOf as) Parser.Result p)
-
-mkVar : ({ctx : _} -> Var ctx -> p ctx) -> WithBounds String -> ParseFun [<SnocList String] p
-mkVar f x =
-  MkParseFun
-    (\ctx => case Var.lookup x.val ctx of
-      Just i => Ok (f i)
-      Nothing => Errs (singleton $ "unbound name \"\{x.val}\"" <$ x))
-
-mkVar3 :
-  ({ctx1 : a} -> {ctx2 : b} -> {ctx3 : SnocList String} ->
-    WithBounds (Var ctx3) ->
-    p ctx1 ctx2 ctx3) ->
-  WithBounds String -> ParseFun [<a, b, SnocList String] p
-mkVar3 f x =
-  MkParseFun
-    (\ctx1, ctx2, ctx3 => case Var.lookup x.val ctx3 of
-      Just i => Ok (f $ i <$ x)
-      Nothing => Errs (singleton $ "unbound name \"\{x.val}\"" <$ x))
-
-public export
-TypeFun : Type
-TypeFun = ParseFun [<SnocList String] Ty
-
-Type'Fun : Type
-Type'Fun = ParseFun [<Mode, SnocList String, SnocList String] (\mode => Ty' mode Bounds)
-
-BoundType'Fun : Type
-BoundType'Fun = ParseFun [<Mode, SnocList String, SnocList String] (\mode => BoundTy' mode Bounds)
-
-public export
-TermFun : Type
-TermFun = ParseFun [<Mode, SnocList String, SnocList String] (\mode => Term mode Bounds)
+TypeParser : SnocList String -> SnocList String -> Type
+TypeParser locked free = InkyParser False (map (:- Ty) locked) (map (:- Ty) free) Ty
 
+%inline
 public export
-TypeParser : SnocList String -> SnocList String -> Type
-TypeParser locked free =
-  InkyParser False (map (:- TypeFun) locked) (map (:- TypeFun) free) TypeFun
+TermParser : SnocList String -> SnocList String -> Type
+TermParser locked free = InkyParser False (map (:- Term') locked) (map (:- Term') free) Term'
+
+mkTyVar : {ctx : _} -> WithBounds String -> Either (WithBounds InkyError) (Ty ctx)
+mkTyVar x =
+  case Var.lookup x.val ctx of
+    Just i => pure (TVar i)
+    Nothing => Left (UnboundTyVar x.val ctx <$ x)
+
+mkTmVar :
+  {state : _} ->
+  WithBounds String ->
+  Either (WithBounds InkyError) (Term' state)
+mkTmVar {state = (mode, tyCtx, tmCtx)} x =
+  case Var.lookup x.val tmCtx of
+    Just i => pure (Var x.bounds i)
+    Nothing => Left (UnboundTmVar x.val tmCtx <$ x)
 
 RowOf :
-  (0 free : Context Type) ->
+  (0 free : Context (state -> Type)) ->
   InkyParser False [<] free a ->
-  InkyParser True [<] free (List $ WithBounds $ Assoc a)
+  InkyParser True [<] free (List . WithBounds . Assoc . a)
 RowOf free p =
-  sepBy (match Semicolon) (WithBounds $ mkAssoc <$> Seq [match TypeIdent, match Colon, p])
-  where
-  mkAssoc : HList [String, (), a] -> Assoc a
-  mkAssoc [x, _, v] = x :- v
-
-parseRow :
-  List (WithBounds $ Assoc (ParseFun [<a] p)) ->
-  ParseFun [<a] (Row . p)
-parseRow xs =
-  MkParseFun (\ctx =>
-    foldlM
-      (\row => extendResult row . map (\(n :- x) => n :- x.try ctx))
-      [<]
-      xs)
-
-parseRow3 :
-  List (WithBounds $ Assoc (ParseFun [<a,b,c] p)) ->
-  ParseFun [<a, b, c] (\ctx1, ctx2, ctx3 => Row $ p ctx1 ctx2 ctx3)
-parseRow3 xs =
-  MkParseFun (\ctx1, ctx2, ctx3 =>
-    foldlM
-      (\row => extendResult row . map (\(n :- x) => n :- x.try ctx1 ctx2 ctx3))
-      [<]
-      xs)
-
-parseList3 :
-  List (ParseFun [<a,b,c] p) ->
-  ParseFun [<a, b, c] (\ctx1, ctx2, ctx3 => List $ p ctx1 ctx2 ctx3)
-parseList3 [] = MkParseFun (\ctx1, ctx2, ctx3 => Ok [])
-parseList3 (x :: xs) =
-  MkParseFun (\ctx1, ctx2, ctx3 =>
-    [| x.try ctx1 ctx2 ctx3 :: (parseList3 xs).try ctx1 ctx2 ctx3 |])
+  sepBy (match Semicolon)
+    (WithBounds $ (\[x, _, v] => x :- v) <$> Seq [match TypeIdent, match Colon, p])
+
+mkRow :
+  List (WithBounds $ Assoc a) ->
+  Either (WithBounds InkyError) (Row a)
+mkRow =
+  foldlM
+    (\row, x => case extend row x.val of
+      Just row => pure row
+      Nothing => Left (DuplicateLabel x.val.name row.names <$ x))
+    [<]
 
 -- Types -----------------------------------------------------------------------
 
 AtomType : TypeParser [<"openType"] [<]
 AtomType =
   OneOf
-    [ mkVar TVar <$> WithBounds (match TypeIdent)
-    , MkParseFun (\_ => Ok TNat) <$ match Nat
-    , mkProd <$> enclose (match AngleOpen) (match AngleClose) row
-    , mkSum <$> enclose (match BracketOpen) (match BracketClose) row
+    [ Map mkTyVar $ WithBounds (match TypeIdent)
+    , TNat <$ match Nat
+    , TProd <$> enclose (match AngleOpen) (match AngleClose) row
+    , TSum <$> enclose (match BracketOpen) (match BracketClose) row
     , enclose (match ParenOpen) (match ParenClose) (Var (%%% "openType"))
     ]
   where
-  row : InkyParser True [<] [<"openType" :- TypeFun] (List $ WithBounds $ Assoc TypeFun)
-  row = RowOf [<"openType" :- TypeFun] $ Var (%%% "openType")
-
-  mkProd : List (WithBounds $ Assoc TypeFun) -> TypeFun
-  mkProd xs = MkParseFun (\ctx => TProd <$> (parseRow xs).try ctx)
-
-  mkSum : List (WithBounds $ Assoc TypeFun) -> TypeFun
-  mkSum xs = MkParseFun (\ctx => TSum <$> (parseRow xs).try ctx)
+  row : InkyParser True [<] [<"openType" :- Ty] (Row . Ty)
+  row = Map mkRow $ RowOf [<"openType" :- Ty] $ Var (%%% "openType")
 
 AppType : TypeParser [<"openType"] [<]
 AppType =
   OneOf
     [ AtomType
-    , match List **> mkList <$> weaken (S Z) AtomType
-    , mkFix <$> Seq
-      [ match Data
-      , match TypeIdent
-      , weaken (S Z) AtomType
-      ]
+    , match List *> TList <$> weaken (S Z) AtomType
+    , match Data *> (\[x, t] => TFix x t) <$>
+        Seq (Update (match TypeIdent) (Just (:<)) [weaken (S Z) AtomType])
     ]
   where
-  mkList : TypeFun -> TypeFun
-  mkList x = MkParseFun (\ctx => TList <$> x.try ctx)
-
-  mkFix : HList [(), String, TypeFun] -> TypeFun
-  mkFix [_, x, a] = MkParseFun (\ctx => TFix x <$> a.try (ctx :< x))
 
 export
 OpenType : TypeParser [<] [<]
 OpenType =
-  Fix "openType" $ mkArrow <$> sepBy1 (match Arrow) AppType
-  where
-  mkArrow : List1 TypeFun -> TypeFun
-  mkArrow =
-    foldr1 {a = TypeFun}
-      (\x, y => MkParseFun (\ctx => [| TArrow (x.try ctx) (y.try ctx) |]))
+  Fix "openType" $ foldr1 TArrow <$> sepBy1 (match Arrow) AppType
 
 export
 [ListSet] Eq a => Set a (List a) where
@@ -462,483 +393,329 @@ OpenTypeWf = Refl
 
 -- Terms -----------------------------------------------------------------------
 
-NoSugarMsg : String
-NoSugarMsg = "sugar is not allowed here"
-
-NoUnquoteMsg : String
-NoUnquoteMsg = "cannot unquote outside of quote"
-
-NoQuoteMsg : String
-NoQuoteMsg = "cannot quote inside of quote"
-
-NoQuoteTypesMsg : String
-NoQuoteTypesMsg = "cannot quote types"
-
-NoLetTyMsg : String
-NoLetTyMsg = "cannot bind type inside of quote"
-
-NoQAbsMsg : String
-NoQAbsMsg = "cannot bind term name inside of quote"
-
-AtomTerm : InkyParser False [<"openTerm" :- TermFun] [<] TermFun
+Type' : (Mode, SnocList String, SnocList String) -> Type
+Type' state = Ty' (fst state) Bounds (fst $ snd state) (snd $ snd state)
+
+BoundType' : (Mode, SnocList String, SnocList String) -> Type
+BoundType' state = BoundTy' (fst state) Bounds (fst $ snd state) (snd $ snd state)
+
+sugarOnly :
+  (0 a, b : (Mode, SnocList String, SnocList String) -> Type) ->
+  ({qtCtx, tyCtx, tmCtx : _} ->
+    WithBounds (a (Sugar qtCtx, tyCtx, tmCtx)) ->
+    b (Sugar qtCtx, tyCtx, tmCtx)) ->
+  {state : _} -> WithBounds (a state) -> Either (WithBounds InkyError) (b state)
+sugarOnly a b f {state = (Sugar qtCtx, tyCtx, tmCtx)} x = pure (f x)
+sugarOnly a b f {state = (mode, tyCtx, tmCtx)} x = Left (NeedsSugar mode <$ x)
+
+quoteOnly :
+  (0 a, b : (Mode, SnocList String, SnocList String) -> Type) ->
+  ({ctx1, ctx2, tmCtx : _} ->
+    WithBounds (a (Quote ctx1 ctx2, [<], tmCtx)) ->
+    b (Quote ctx1 ctx2, [<], tmCtx)) ->
+  {state : _} -> WithBounds (a state) -> Either (WithBounds InkyError) (b state)
+-- HACK: should special case for tyCtx /= [<]. But this case is "impossible", so it doesn't matter
+quoteOnly a b f {state = (Quote ctx1 ctx2, [<], tmCtx)} x = pure (f x)
+quoteOnly a b f {state = (mode, tyCtx, tmCtx)} x = Left (NeedsQuote mode <$ x)
+
+forceQuote :
+  (Mode, SnocList String, SnocList String) -> (Mode, SnocList String, SnocList String)
+forceQuote (Sugar qtCtx, tyCtx, tmCtx) = (Quote tyCtx tmCtx, [<], qtCtx)
+forceQuote state = state
+
+forceSugar :
+  (Mode, SnocList String, SnocList String) -> (Mode, SnocList String, SnocList String)
+forceSugar (Quote ctx1 ctx2, tyCtx, tmCtx) = (Sugar tmCtx, ctx1, ctx2)
+forceSugar state = state
+
+embedType :
+  {state : _} ->
+  WithBounds (Ty (fst $ snd state)) ->
+  Either (WithBounds InkyError) (Type' state)
+embedType {state = (Quote ctx1 ctx2, tyCtx, tmCtx)} t = Left (NoQuotedTypes <$ t)
+embedType {state = (Sugar qtCtx, tyCtx, tmCtx)} t = Right t.val
+embedType {state = (NoSugar, tyCtx, tmCtx)} t = Right t.val
+
+AtomTerm : TermParser [<"openTerm"] [<]
 AtomTerm =
   OneOf
-    [ mkVar3 (\x => Var x.bounds x.val) <$> WithBounds (match TermIdent)
-    , mkStrLit <$> WithBounds (match StringLit)
-    , mkLit <$> WithBounds (match Lit)
-    , mkList <$> WithBounds (
+    [ Map mkTmVar $ WithBounds (match TermIdent)
+    , Map (sugarOnly (const String) Term' (\k => Str k.bounds k.val)) $
+      WithBounds (match StringLit)
+    , Map (sugarOnly (const Nat) Term' (\k => Lit k.bounds k.val)) $
+      WithBounds (match Lit)
+    , Map (sugarOnly (List . Term') Term' (\ts => List ts.bounds ts.val)) $ WithBounds (
         enclose (match BracketOpen) (match BracketClose) $
-        sepBy (match Semicolon) $
-        Var (%%% "openTerm"))
-    , mkTup <$> WithBounds (enclose (match AngleOpen) (match AngleClose) $
-        RowOf [<"openTerm" :- TermFun] (Var (%%% "openTerm")))
+        sepBy (match Semicolon) $ Var (%%% "openTerm"))
+    , (\row => Tup row.bounds row.val) <$> WithBounds (
+        enclose (match AngleOpen) (match AngleClose) $
+        Map mkRow $ RowOf [<"openTerm" :- Term'] (Var (%%% "openTerm")))
     , enclose (match ParenOpen) (match ParenClose) (Var (%%% "openTerm"))
     ]
-  where
-  mkStrLit : WithBounds String -> TermFun
-  mkStrLit k = MkParseFun (\mode, tyCtx, tmCtx =>
-    case mode of
-      NoSugar => Errs (singleton $ NoSugarMsg <$ k)
-      Sugar qtCtx => Ok (Str k.bounds k.val)
-      Quote ctx1 ctx2 => Errs (singleton $ NoSugarMsg <$ k))
-
-  mkLit : WithBounds Nat -> TermFun
-  mkLit k = MkParseFun (\mode, tyCtx, tmCtx =>
-    case mode of
-      NoSugar => Errs (singleton $ NoSugarMsg <$ k)
-      Sugar qtCtx => Ok (Lit k.bounds k.val)
-      Quote ctx1 ctx2 => Errs (singleton $ NoSugarMsg <$ k))
 
-  mkList : WithBounds (List TermFun) -> TermFun
-  mkList xs = MkParseFun (\mode, tyCtx, tmCtx =>
-    case mode of
-      NoSugar => Errs (singleton $ NoSugarMsg <$ xs)
-      Sugar ctx => List xs.bounds <$> (parseList3 xs.val).try (Sugar ctx) tyCtx tmCtx
-      Quote ctx1 ctx2 => Errs (singleton $ NoSugarMsg <$ xs))
-
-  mkTup : WithBounds (List (WithBounds $ Assoc TermFun)) -> TermFun
-  mkTup xs =
-    MkParseFun (\mode, tyCtx, tmCtx =>
-      Tup xs.bounds <$> (parseRow3 xs.val).try mode tyCtx tmCtx)
-
-PrefixTerm : InkyParser False [<"openTerm" :- TermFun] [<] TermFun
+PrefixTerm : TermParser [<"openTerm"] [<]
 PrefixTerm =
   Fix "prefixTerm" $ OneOf
-    [ mkRoll <$> WithBounds (match Tilde **> Var (%%% "prefixTerm"))
-    , mkUnroll <$> WithBounds (match Bang **> Var (%%% "prefixTerm"))
-    , mkQuote <$> WithBounds (match Backtick **> Var (%%% "prefixTerm"))
-    , mkUnquote <$> WithBounds (match Comma **> Var (%%% "prefixTerm"))
+    [ (\t => Roll t.bounds t.val) <$> WithBounds (match Tilde *> Var (%%% "prefixTerm"))
+    , (\t => Unroll t.bounds t.val) <$> WithBounds (match Bang *> Var (%%% "prefixTerm"))
+    , Map (sugarOnly (Term' . forceQuote) Term' (\t => QuasiQuote t.bounds t.val)) $
+        WithBounds $ (\[_, t] => t) <$>
+        Seq (Update (match Backtick) (Just $ const . forceQuote) [Var (%%% "prefixTerm")])
+    , Map (quoteOnly (Term' . forceSugar) Term' (\t => Unquote t.bounds t.val)) $
+        WithBounds $ (\[_, t] => t) <$>
+        Seq (Update (match Comma) (Just $ const . forceSugar) [Var (%%% "prefixTerm")])
     , rename (Drop Id) Id AtomTerm
     ]
-  where
-  mkRoll : WithBounds TermFun -> TermFun
-  mkRoll x = MkParseFun (\mode, tyCtx, tmCtx => Roll x.bounds <$> x.val.try mode tyCtx tmCtx)
-
-  mkUnroll : WithBounds TermFun -> TermFun
-  mkUnroll x = MkParseFun (\mode, tyCtx, tmCtx => Unroll x.bounds <$> x.val.try mode tyCtx tmCtx)
-
-  mkQuote : WithBounds TermFun -> TermFun
-  mkQuote x =
-    MkParseFun (\mode, tyCtx, tmCtx =>
-      case mode of
-        Quote ctx1 ctx2 => Errs (singleton $ NoQuoteMsg <$ x)
-        Sugar ctx => QuasiQuote x.bounds <$> x.val.try (Quote tyCtx tmCtx) [<] ctx
-        NoSugar => Errs (singleton $ NoSugarMsg <$ x))
-
-  mkUnquote : WithBounds TermFun -> TermFun
-  mkUnquote x =
-    MkParseFun (\mode, tyCtx, tmCtx =>
-      case mode of
-        Quote ctx1 ctx2 =>
-          case tyCtx of
-            [<] => Unquote x.bounds <$> x.val.try (Sugar tmCtx) ctx1 ctx2
-            _ => Errs (singleton $ "internal error 0001" <$ x)
-        Sugar ctx => Errs (singleton $ NoUnquoteMsg <$ x)
-        NoSugar => Errs (singleton $ NoSugarMsg <$ x))
-
-SuffixTerm : InkyParser False [<"openTerm" :- TermFun] [<] TermFun
-SuffixTerm = mkSuffix <$> Seq [ PrefixTerm , star (match Dot **> WithBounds (match TypeIdent)) ]
-  where
-  mkSuffix : HList [TermFun, List (WithBounds String)] -> TermFun
-  mkSuffix [t, []] = t
-  mkSuffix [t, prjs] =
-    MkParseFun (\mode, tyCtx, tmCtx =>
-      Ok $ foldl (\acc, l => Prj l.bounds acc l.val) !(t.try mode tyCtx tmCtx) prjs)
 
-SuffixTy' : InkyParser False [<"openTerm" :- TermFun] [<] Type'Fun
+SuffixTerm : TermParser [<"openTerm"] [<]
+SuffixTerm =
+  (\[t, prjs] => foldl (\t, l => Prj l.bounds t l.val) t prjs) <$>
+  Seq [PrefixTerm , star (match Dot *> WithBounds (match TypeIdent)) ]
+
+SuffixTy' : InkyParser False [<"openTerm" :- Term'] [<] Type'
 SuffixTy' =
   OneOf
-    [ mkTy <$> WithBounds (sub [<"openType" :- rename Id (Drop Id) OpenType] [<] AtomType)
-    , mkTm <$> WithBounds (match Comma **> weaken (S Z) PrefixTerm)
+    [ Map embedType $ Forget (fst . snd) $ WithBounds $ sub [<"openType" :- OpenType] [<] AtomType
+    , Map (quoteOnly (Term' . forceSugar) Type' val) $
+        WithBounds $ (\[_, t] => t) <$>
+        Seq (Update (match Comma) (Just $ const . forceSugar) [weaken (S Z) PrefixTerm])
     ]
-  where
-  mkTy : WithBounds TypeFun -> Type'Fun
-  mkTy x =
-    MkParseFun (\mode, tyCtx, tmCtx =>
-      case mode of
-        Quote ctx1 ctx2 => Errs (singleton $ NoQuoteTypesMsg <$ x)
-        Sugar ctx => x.val.try tyCtx
-        NoSugar => x.val.try tyCtx)
-
-  mkTm : WithBounds TermFun -> Type'Fun
-  mkTm x =
-    MkParseFun (\mode, tyCtx, tmCtx =>
-      case mode of
-        Quote ctx1 ctx2 => x.val.try (Sugar tmCtx) ctx1 ctx2
-        Sugar ctx => Errs (singleton $ NoUnquoteMsg <$ x)
-        NoSugar => Errs (singleton $ NoSugarMsg <$ x))
-
-SuffixBoundTy' : InkyParser False [<"openTerm" :- TermFun] [<] BoundType'Fun
+
+SuffixBoundTy' : InkyParser False [<"openTerm" :- Term'] [<] BoundType'
 SuffixBoundTy' =
-  OneOf
-    [ mkTy <$> enclose (match ParenOpen) (match ParenClose) (Seq
-      [ WithBounds (match Backslash)
-      , match TypeIdent
-      , match DoubleArrow
-      , rename Id (Drop Id) OpenType
-      ])
-    , mkTm <$> WithBounds (match Comma **> weaken (S Z) PrefixTerm)
+  OneOf {nils = [False, False]}
+    [ enclose (match ParenOpen) (match ParenClose) $
+      Map embedBoundType $
+      Forget (fst . snd) $
+      WithBounds {a = \ctx => (x ** Ty (ctx :< x))} $
+      (\[n, t] => (n ** t)) <$>
+      Seq (Update (match Backslash *> match TypeIdent <* match DoubleArrow) (Just (:<)) [OpenType])
+    , Map (quoteOnly (Term' . forceSugar) BoundType' val) $
+        WithBounds $ (\[_, t] => t) <$>
+        Seq (Update (match Comma) (Just $ const . forceSugar) [weaken (S Z) PrefixTerm])
     ]
   where
-  mkTy : HList [WithBounds _, String, _, TypeFun] -> BoundType'Fun
-  mkTy [x, n, _, a] =
-    MkParseFun (\mode, tyCtx, tmCtx =>
-      case mode of
-        Quote ctx1 ctx2 => Errs (singleton $ NoQuoteTypesMsg <$ x)
-        Sugar ctx => MkDPair n <$> a.try (tyCtx :< n)
-        NoSugar => MkDPair n <$> a.try (tyCtx :< n))
-
-  mkTm : WithBounds TermFun -> BoundType'Fun
-  mkTm x =
-    MkParseFun (\mode, tyCtx, tmCtx =>
-      case mode of
-        Quote ctx1 ctx2 => x.val.try (Sugar tmCtx) ctx1 ctx2
-        Sugar ctx => Errs (singleton $ NoUnquoteMsg <$ x)
-        NoSugar => Errs (singleton $ NoSugarMsg <$ x))
-
-AppTerm : InkyParser False [<"openTerm" :- TermFun] [<] TermFun
+  embedBoundType :
+    {state : _} ->
+    WithBounds (x ** Ty (fst (snd state) :< x)) ->
+    Either (WithBounds InkyError) (BoundType' state)
+  embedBoundType {state = (Quote ctx1 ctx2, tyCtx, tmCtx)} t = Left (NoQuotedTypes <$ t)
+  embedBoundType {state = (Sugar qtCtx, tyCtx, tmCtx)} t = Right t.val
+  embedBoundType {state = (NoSugar, tyCtx, tmCtx)} t = Right t.val
+
+AppTerm : TermParser [<"openTerm"] [<]
 AppTerm =
   OneOf
-    [ mkInj <$> Seq
-      [ WithBounds (match TypeIdent)
-      , weaken (S Z) SuffixTerm
-      ]
-    , mkSuc <$> Seq
-      [ WithBounds (match Suc)
-      , weaken (S Z) SuffixTerm
-      ]
-    , mkCons <$> Seq
-      [ WithBounds (match Cons)
-      , weaken (S Z) SuffixTerm
-      , weaken (S Z) SuffixTerm
-      ]
-    , mkApp <$> Seq
-      [ OneOf
-        [ WithBounds SuffixTerm
-        , mkMap <$> Seq
-          [ WithBounds (match Map)
-          , weaken (S Z) SuffixBoundTy'
-          , weaken (S Z) SuffixTy'
-          , weaken (S Z) SuffixTy'
+    [ (\lt => Inj lt.bounds (fst lt.val) (snd lt.val)) <$>
+      WithBounds (match TypeIdent <**> weaken (S Z) SuffixTerm)
+    , Map (sugarOnly Term' Term' (\t => Suc t.bounds t.val)) $
+      WithBounds $ match Suc *> weaken (S Z) SuffixTerm
+    , Map (sugarOnly (\s => (Term' s, Term' s)) Term'
+        (\tu => Cons tu.bounds (fst tu.val) (snd tu.val))) $
+      WithBounds $ match Cons *> weaken (S Z) SuffixTerm <**> weaken (S Z) SuffixTerm
+    , (\case
+        [f, []] => f.val
+        [f, args] => App f.bounds f.val args) <$>
+      Seq
+        [ OneOf
+          [ WithBounds SuffixTerm
+          , (\[x, f, a, b] => Map x.bounds f a b <$ x) <$> Seq
+            [ WithBounds (match Map)
+            , weaken (S Z) SuffixBoundTy'
+            , weaken (S Z) SuffixTy'
+            , weaken (S Z) SuffixTy'
+            ]
           ]
+        , star (weaken (S Z) SuffixTerm)
         ]
-      , star (weaken (S Z) SuffixTerm)
-      ]
     ]
-  where
-  mkInj : HList [WithBounds String, TermFun] -> TermFun
-  mkInj [tag, t] =
-    MkParseFun (\mode, tyCtx, tmCtx =>
-      Inj tag.bounds tag.val <$> t.try mode tyCtx tmCtx)
-
-  mkSuc : HList [WithBounds _, TermFun] -> TermFun
-  mkSuc [x, t] =
-    MkParseFun (\mode, tyCtx, tmCtx =>
-      case mode of
-        Quote ctx1 ctx2 => Errs (singleton $ NoSugarMsg <$ x)
-        Sugar ctx => Suc x.bounds <$> t.try (Sugar ctx) tyCtx tmCtx
-        NoSugar => Errs (singleton $ NoSugarMsg <$ x))
-
-  mkCons : HList [WithBounds _, TermFun, TermFun] -> TermFun
-  mkCons [x, t, u] =
-    MkParseFun (\mode, tyCtx, tmCtx =>
-      case mode of
-        Quote ctx1 ctx2 => Errs (singleton $ NoSugarMsg <$ x)
-        Sugar ctx =>
-          [| Cons (pure x.bounds)
-               (t.try (Sugar ctx) tyCtx tmCtx)
-               (u.try (Sugar ctx) tyCtx tmCtx)
-          |]
-        NoSugar => Errs (singleton $ NoSugarMsg <$ x))
-
-  mkMap :
-    HList [WithBounds (), BoundType'Fun, Type'Fun, Type'Fun] ->
-    WithBounds TermFun
-  mkMap [m, a, b, c] =
-    MkParseFun (\mode, tyCtx, tmCtx => do
-      (a, b, c) <-
-        [| (a.try mode tyCtx tmCtx, [|(b.try mode tyCtx tmCtx, c.try mode tyCtx tmCtx)|]) |]
-      Ok $ Map m.bounds a b c)
-    <$ m
-
-  mkApp : HList [WithBounds TermFun, List TermFun] -> TermFun
-  mkApp [t, []] = t.val
-  mkApp [fun, args] =
-    MkParseFun (\mode, tyCtx, tmCtx => do
-      (funVal, args) <-
-        [| (fun.val.try mode tyCtx tmCtx, (parseList3 args).try mode tyCtx tmCtx) |]
-      Ok $ App fun.bounds funVal args)
-
-OpenTy' : InkyParser False [<"openTerm" :- TermFun] [<] Type'Fun
+
+OpenTy' : InkyParser False [<"openTerm" :- Term'] [<] Type'
 OpenTy' =
   OneOf
-    [ mkTy <$> WithBounds (rename (Drop Id) Id OpenType)
-    , mkTm <$> WithBounds (match Comma **> weaken (S Z) PrefixTerm)
-    ]
-  where
-  mkTy : WithBounds TypeFun -> Type'Fun
-  mkTy x =
-    MkParseFun (\mode, tyCtx, tmCtx =>
-      case mode of
-        Quote ctx1 ctx2 => Errs (singleton $ NoQuoteTypesMsg <$ x)
-        Sugar ctx => x.val.try tyCtx
-        NoSugar => x.val.try tyCtx)
-
-  mkTm : WithBounds TermFun -> Type'Fun
-  mkTm x =
-    MkParseFun (\mode, tyCtx, tmCtx =>
-      case mode of
-        Quote ctx1 ctx2 => x.val.try (Sugar tmCtx) ctx1 ctx2
-        Sugar ctx => Errs (singleton $ NoUnquoteMsg <$ x)
-        NoSugar => Errs (singleton $ NoSugarMsg <$ x))
-
-AnnotTerm : InkyParser False [<"openTerm" :- TermFun] [<] TermFun
-AnnotTerm =
-  mkAnnot <$> Seq
-    [ AppTerm
-    , option (match Colon **> WithBounds (weaken (S Z) OpenTy'))
+    [ Map embedType $ Forget (fst . snd) $ WithBounds OpenType
+    , Map (quoteOnly (Term' . forceSugar) Type' val) $
+      WithBounds $ (\[_, t] => t) <$>
+      Seq (Update (match Comma) (Just $ const . forceSugar) [weaken (S Z) PrefixTerm])
     ]
-  where
-  mkAnnot : HList [TermFun, Maybe (WithBounds Type'Fun)] -> TermFun
-  mkAnnot [t, Nothing] = t
-  mkAnnot [t, Just a] = MkParseFun (\mode, tyCtx, tmCtx =>
-    [| Annot (pure a.bounds) (t.try mode tyCtx tmCtx) (a.val.try mode tyCtx tmCtx) |])
 
 -- Open Terms
 
-LetTerm : InkyParser False [<"openTerm" :- TermFun] [<] TermFun
+AnnotTerm : TermParser [<"openTerm"] [<]
+AnnotTerm =
+  (\case
+    (t, Nothing) => t
+    (t, Just a) => Annot a.bounds t a.val) <$>
+  (AppTerm <**> option (WithBounds $ match Colon *> weaken (S Z) OpenTy'))
+
+LetTerm : TermParser [<"openTerm"] [<]
 LetTerm =
-  match Let **>
+  match Let *>
   OneOf
-    [ mkLet <$> Seq
-      [ WithBounds (match TermIdent)
-      , OneOf
-        [ mkAnnot <$> Seq
-          [ star (enclose (match ParenOpen) (match ParenClose) $
-            Seq [ match TermIdent, match Colon, weaken (S Z) OpenTy' ])
-          , WithBounds (match Colon)
-          , weaken (S Z) OpenTy'
-          , match Equal
-          , star (match Comment)
-          , Var (%%% "openTerm")]
-        , mkUnannot <$> Seq [match Equal, star (match Comment) , Var (%%% "openTerm")]
-        ]
-      , match In
-      , Var (%%% "openTerm")
-      ]
-    , mkLetType <$> Seq
-      [ WithBounds (match TypeIdent)
-      , match Equal
-      , star (match Comment)
-      , rename Id (Drop Id) OpenType
-      , match In
-      , Var (%%% "openTerm")
-      ]
+    [ mkLet _ <$> Seq
+      (Update
+        (WithBounds (match TermIdent) <**> OneOf
+          [ mkAnnot _ <$>
+            Seq (Update
+              (Seq
+                [ star (enclose (match ParenOpen) (match ParenClose)
+                  (match TermIdent <* match Colon <**> weaken (S Z) OpenTy'))
+                , WithBounds (match Colon)
+                , weaken (S Z) OpenTy'
+                , match Equal
+                , star (match Comment)
+                ])
+              (Just GetArgs)
+              [Var (%%% "openTerm")])
+          , (\[_, doc, body] => AddDoc body doc) <$>
+            Seq [match Equal, star (match Comment), Var (%%% "openTerm")]
+          ])
+        (Just $ \state, v => mapSnd (mapSnd (:< (fst v).val)) state)
+        [match In *> Var (%%% "openTerm")])
+    , Map (mkLetTy _) $ Seq
+      (Update
+        (WithBounds (match TypeIdent) <**>
+          uncurry (flip AddDoc) <$>
+          (match Equal *> (star (match Comment) <**> Forget (fst . snd) OpenType)))
+        (Just $ \state, v => mapSnd (mapFst (:< (fst v).val)) state)
+        [match In *> Var (%%% "openTerm")])
+
     ]
   where
-  mkLet : HList [WithBounds String, WithDoc TermFun, (), TermFun] -> TermFun
-  mkLet [x, AddDoc e doc, _, t] =
-    MkParseFun (\mode, tyCtx, tmCtx =>
-      [| (\e, t => Let (AddDoc x.bounds doc) e (x.val ** t))
-         (e.try mode tyCtx tmCtx)
-         (t.try mode tyCtx (tmCtx :< x.val))
-      |])
-
-  mkLetType : HList [WithBounds String, (), List String, TypeFun, (), TermFun] -> TermFun
-  mkLetType [x, _, doc, a, _, t] =
-    MkParseFun (\mode, tyCtx, tmCtx =>
-      case mode of
-        Quote ctx1 ctx2 => Errs (singleton $ NoLetTyMsg <$ x)
-        Sugar ctx =>
-          [| (\a, t => LetTy (AddDoc x.bounds doc) a (x.val ** t))
-             (a.try tyCtx)
-             (t.try (Sugar ctx) (tyCtx :< x.val) tmCtx)
-          |]
-        NoSugar =>
-          [| (\a, t => LetTy (AddDoc x.bounds doc) a (x.val ** t))
-             (a.try tyCtx)
-             (t.try NoSugar (tyCtx :< x.val) tmCtx)
-          |])
-
-  mkArrow : (meta : Bounds) -> List Type'Fun -> Type'Fun -> Type'Fun
-  mkArrow meta [] cod = cod
-  mkArrow meta (arg :: args) cod =
-    let
-      arrowTm :
-        Term mode Bounds tyCtx tmCtx ->
-        Term mode Bounds tyCtx tmCtx ->
-        Term mode Bounds tyCtx tmCtx
-      arrowTm =
-        \t, u => Roll meta $ Inj meta "TArrow" $ Tup meta [<"Dom" :- t, "Cod" :- u]
-    in
-    MkParseFun (\mode, tyCtx, tmCtx =>
-      case mode of
-        Quote ctx1 ctx2 =>
-          [| arrowTm
-             (arg.try (Quote ctx1 ctx2) tyCtx tmCtx)
-             ((mkArrow meta args cod).try (Quote ctx1 ctx2) tyCtx tmCtx)
-          |]
-        Sugar ctx =>
-          [| TArrow
-             (arg.try (Sugar ctx) tyCtx tmCtx)
-             ((mkArrow meta args cod).try (Sugar ctx) tyCtx tmCtx)
-          |]
-        NoSugar =>
-          [| TArrow
-             (arg.try NoSugar tyCtx tmCtx)
-             ((mkArrow meta args cod).try NoSugar tyCtx tmCtx)
-          |])
+  AnnotSeq : List (Stage TermState)
+  AnnotSeq = map (\a => MkStage a Nothing)
+    [ (\s => List (String, Type' s))
+    , const (WithBounds ())
+    , Type'
+    , const ()
+    , const (List String)
+    ]
 
-  mkAnnot :
-    HList [List (HList [String, (), Type'Fun]), WithBounds (), Type'Fun, (), List String, TermFun] ->
-    WithDoc TermFun
-  mkAnnot [[], m, cod, _, doc, t] =
-    AddDoc
-      (MkParseFun (\mode, tyCtx, tmCtx =>
-        [| Annot (pure m.bounds) (t.try mode tyCtx tmCtx) (cod.try mode tyCtx tmCtx) |]))
-      doc
-  mkAnnot [args, m, cod, _, doc, t] =
-    let bound = map (\[x, _, a] => x) args in
-    let tys = map (\[x, _, a] => a) args in
-    AddDoc
-      (MkParseFun (\mode, tyCtx, tmCtx =>
-        [| (\t, a => Annot m.bounds (Abs m.bounds (bound ** t)) a)
-           (t.try mode tyCtx (tmCtx <>< bound))
-           ((mkArrow m.bounds tys cod).try mode tyCtx tmCtx)
-        |]))
-      doc
+  LetSeq : List (Stage TermState)
+  LetSeq =
+    [ MkStage (\s => (WithBounds String, WithDoc (Term' s)))
+        (Just $ \s, v => mapSnd (mapSnd (:< (fst v).val)) s)
+    , MkStage Term' Nothing
+    ]
+
+  LetTySeq : List (Stage TermState)
+  LetTySeq =
+    [ MkStage (\s => (WithBounds String, WithDoc (Ty $ fst $ snd s)))
+        (Just $ \s, v => mapSnd (mapFst (:< (fst v).val)) s)
+    , MkStage Term' Nothing
+    ]
+
+  GetArgs : (state : TermState) -> Sequence state AnnotSeq -> TermState
+  GetArgs state [args, _, _, _, _] = mapSnd (mapSnd (<>< map fst args)) state
 
-  mkUnannot : HList [(), List String, TermFun] -> WithDoc TermFun
-  mkUnannot [_, doc, e] = AddDoc e doc
+  MkArrow : (meta : Bounds) -> (state : TermState) -> Type' state -> Type' state -> Type' state
+  MkArrow meta (Quote ctx1 ctx2, _, _) = \dom, cod =>
+    Roll meta $ Inj meta "TArrow" $ Tup meta [<"Dom" :- dom, "Cod" :- cod]
+  MkArrow meta (Sugar qtCtx, _, _) = TArrow
+  MkArrow meta (NoSugar, _, _) = TArrow
 
-AbsTerm : InkyParser False [<"openTerm" :- TermFun] [<] TermFun
+  mkAnnot :
+    (state : TermState) ->
+    Sequence state [MkStage (flip Sequence AnnotSeq) (Just GetArgs), MkStage Term' Nothing] ->
+    WithDoc (Term' state)
+  mkAnnot (_, _, _) [[[], colon, ret, _, docs], body] =
+    AddDoc (Annot colon.bounds body ret) docs
+  mkAnnot (mode, tyCtx, tmCtx) [[(arg :: args), colon, ret, _, docs], body] =
+    AddDoc
+      (Annot colon.bounds
+        (Abs colon.bounds (fst arg :: map fst args ** body))
+        (foldr (MkArrow colon.bounds (mode, tyCtx, tmCtx)) ret (snd arg ::: map snd args)))
+      docs
+
+  mkLet : (state : TermState) -> Sequence state LetSeq -> Term' state
+  mkLet (_, _, _) [(x, body), rest] = Let (AddDoc x.bounds body.doc) body.value (x.val ** rest)
+
+  mkLetTy :
+    (state : TermState) ->
+    Sequence state LetTySeq ->
+    Either (WithBounds InkyError) (Term' state)
+  mkLetTy (Quote ctx1 ctx2, _, _) [(x, ty), rest] = Left (NoQuotedTypes <$ x)
+  mkLetTy (Sugar qtCtx, _, _) [(x, ty), rest] =
+    pure $ LetTy (AddDoc x.bounds ty.doc) ty.value (x.val ** rest)
+  mkLetTy (NoSugar, _, _) [(x, ty), rest] =
+    pure $ LetTy (AddDoc x.bounds ty.doc) ty.value (x.val ** rest)
+
+AbsTerm : TermParser [<"openTerm"] [<]
 AbsTerm =
-  mkAbs <$> Seq
-    [ WithBounds (match Backslash)
-    , sepBy1 (match Comma) (match TermIdent)
-    , (match DoubleArrow <||> match WaveArrow)
-    , Var (%%% "openTerm")
-    ]
+  Map (mkAbs _) $
+  Seq
+    (Update
+      (WithBounds (match Backslash *> sepBy1 (match Comma) (match TermIdent)) <**>
+        (match DoubleArrow <||> match WaveArrow))
+      (Just UpdateCtx)
+      [Var (%%% "openTerm")])
   where
-  mkAbs : HList [WithBounds (), List1 String, Either () (), TermFun] -> TermFun
-  mkAbs [m, args, Left _, body] =
-    MkParseFun (\mode, tyCtx, tmCtx =>
-      [| (\t => Abs m.bounds (forget args ** t))
-         (body.try mode tyCtx (tmCtx <>< forget args))
-      |])
-  mkAbs [m, args, Right _, body] =
-    MkParseFun (\mode, tyCtx, tmCtx =>
-      case mode of
-        Quote ctx1 ctx2 => Errs (singleton $ NoQAbsMsg <$ m)
-        Sugar ctx =>
-          [| (\t => QAbs m.bounds (forget args ** t))
-             (body.try (Sugar (ctx <>< forget args)) tyCtx tmCtx)
-          |]
-        NoSugar => Errs (singleton $ NoSugarMsg <$ m))
-
-CaseTerm : InkyParser False [<"openTerm" :- TermFun] [<] TermFun
+  UpdateCtx : (state : TermState) -> (WithBounds (List1 String), Either () ()) -> TermState
+  UpdateCtx state (args, Left abs) = mapSnd (mapSnd (<>< forget args.val)) state
+  UpdateCtx state (args, Right quot) = case fst state of
+    Sugar qtCtx => (Sugar (qtCtx <>< forget args.val), snd state)
+    _ => state
+
+  mkAbs :
+    (state : TermState) ->
+    Sequence state
+      [ MkStage (const $ (WithBounds (List1 String), Either () ())) (Just UpdateCtx)
+      , MkStage Term' Nothing
+      ] ->
+    Either (WithBounds InkyError) (Term' state)
+  mkAbs (mode, tyCtx, tmCtx) [(args, Left abs), body] = pure (Abs args.bounds (forget args.val ** body))
+  mkAbs (mode, tyCtx, tmCtx) [(args, Right quot), body] =
+    case mode of
+      Sugar qtCtx => pure (QAbs args.bounds (forget args.val ** body))
+      _ => Left (NeedsSugar mode <$ args)
+
+CaseTerm : TermParser [<"openTerm"] [<]
 CaseTerm =
-  (\[f, x] => f x) <$>
-  Seq
-    [ OneOf
-      [ mkCase <$> Seq
-        [ WithBounds (match Case)
-        , Var (%%% "openTerm")
-        , match Of
-        ]
-      , mkFoldCase <$> Seq
-        [ WithBounds (match FoldCase)
-        , Var (%%% "openTerm")
-        , match By
-        ]
-      ]
-    , enclose (match BraceOpen) (match BraceClose) (
-        sepBy (match Semicolon) $
+  Map (uncurry $ mkCase _) $
+      WithBounds (
+         (match Case *> Var (%%% "openTerm") <* match Of) <||>
+         (match FoldCase *> Var (%%% "openTerm") <* match By))
+  <**> Map mkRow
+    (enclose (match BraceOpen) (match BraceClose)
+      (sepBy (match Semicolon) $
         WithBounds $
-        Seq
-          [ match TypeIdent
-          , match TermIdent
-          , match DoubleArrow
-          , Var (%%% "openTerm")
-          ])
-    ]
+        (\[(label, x), body] => label :- (x ** body)) <$>
+        Seq (Update
+          (match TypeIdent <**> match TermIdent <* match DoubleArrow)
+          (Just $ \state, x => mapSnd (mapSnd (:< snd x)) state)
+          [Var (%%% "openTerm")])))
   where
-  Cases : Type
-  Cases = List (WithBounds $ HList [String, String, (), TermFun])
-
-  mkBranch :
-    HList [String, String, (), TermFun] ->
-    Assoc
-      (ParseFun [<Mode, SnocList String, SnocList String] $
-       \mode, tyCtx, tmCtx => (x ** Term mode Bounds tyCtx (tmCtx :< x)))
-  mkBranch [tag, bound, _, branch] =
-    tag :-
-    MkParseFun (\mode, tyCtx, tmCtx =>
-      [| (\t => MkDPair bound t) (branch.try mode tyCtx (tmCtx :< bound)) |])
-
-  mkCase : HList [WithBounds (), TermFun, _] -> Cases -> TermFun
-  mkCase [m, target, _] branches =
-    let branches = map (map mkBranch) branches in
-    MkParseFun (\mode, tyCtx, tmCtx =>
-      [| Case (pure m.bounds)
-           (target.try mode tyCtx tmCtx)
-           ((parseRow3 branches).try mode tyCtx tmCtx)
-      |])
-
-  mkFoldCase : HList [WithBounds (), TermFun, _] -> Cases -> TermFun
-  mkFoldCase [m, target, _] branches =
-    let branches = map (map mkBranch) branches in
-    MkParseFun (\mode, tyCtx, tmCtx =>
-      [| (\t, ts => Fold m.bounds t ("__tmp" ** Case m.bounds (Var m.bounds $ %% "__tmp") ts))
-         (target.try mode tyCtx tmCtx)
-         ((parseRow3 branches).try mode tyCtx (tmCtx :< "__tmp"))
-      |])
-
-FoldTerm : InkyParser False [<"openTerm" :- TermFun] [<] TermFun
+  mkCase :
+    (state : TermState) ->
+    WithBounds (Either (Term' state) (Term' state)) ->
+    Row (x ** Term' (mapSnd (mapSnd (:< x)) state)) ->
+    Either (WithBounds InkyError) (Term' state)
+  mkCase (mode, _, _) x branches = case x.val of
+    Left target => pure $ Case x.bounds target branches
+    Right target => case mode of
+      Sugar _ => pure $ FoldCase x.bounds target branches
+      _ => Left (NeedsSugar mode <$ x)
+
+FoldTerm : TermParser [<"openTerm"] [<]
 FoldTerm =
-  mkFold <$> Seq
-    [ WithBounds (match Fold)
-    , Var (%%% "openTerm")
-    , match By
-    , enclose (match ParenOpen) (match ParenClose) $
-      Seq
-        [ match Backslash
-        , match TermIdent
-        , match DoubleArrow
-        , Var (%%% "openTerm")
-        ]
-    ]
+  mkFold _ <$>
+    ( WithBounds (match Fold *> Var (%%% "openTerm") <* match By)
+    <**>
+      (\[x, u] => (x ** u)) <$>
+      enclose (match ParenOpen) (match ParenClose)
+      (Seq $ Update
+        (match Backslash *> match TermIdent <* match DoubleArrow)
+        (Just $ \state, x => mapSnd (mapSnd (:< x)) state)
+        [Var (%%% "openTerm")]))
   where
-  mkFold : HList [WithBounds (), TermFun, (), HList [(), String, (), TermFun]] -> TermFun
-  mkFold [m, target, _, [_, arg, _, body]] =
-    MkParseFun (\mode, tyCtx, tmCtx =>
-      [| (\e, t => Fold m.bounds e (arg ** t))
-         (target.try mode tyCtx tmCtx)
-         (body.try mode tyCtx (tmCtx :< arg))
-      |])
+  mkFold :
+    (state : TermState) ->
+    (WithBounds (Term' state), (x ** Term' (mapSnd (mapSnd (:< x)) state))) ->
+    Term' state
+  mkFold (_, _, _) (t, rest) = Fold t.bounds t.val rest
 
 export
-OpenTerm : InkyParser False [<] [<] TermFun
+OpenTerm : TermParser [<] [<]
 OpenTerm =
   Fix "openTerm" $ OneOf
     [ LetTerm
diff --git a/src/Inky/Term/Pretty.idr b/src/Inky/Term/Pretty.idr
index fbedab3..041eb42 100644
--- a/src/Inky/Term/Pretty.idr
+++ b/src/Inky/Term/Pretty.idr
@@ -188,14 +188,6 @@ prettyTerm (Roll _ t) d =
   parenthesise (d < Prefix) $ align $ pretty "~" <+> prettyTerm t Prefix
 prettyTerm (Unroll _ e) d =
   parenthesise (d < Prefix) $ align $ pretty "!" <+> prettyTerm e Prefix
-prettyTerm (Fold _ e ("__tmp" ** Case _ (Var _ ((%%) "__tmp" {pos = Here})) (MkRow ts _))) d =
-  let parts = prettyCases ts <>> [] in
-  -- XXX: should check for usage of "__tmp" in ts
-  group $ align $ hang 2 $ parenthesise (d < Open) $
-    (group $ "foldcase" <++> prettyTerm e Open <++> "by") <+> line <+>
-    (braces $ flatAlt
-      (neutral <++> concatWith (surround $ line' <+> ";" <++> neutral) parts <+> line)
-      (concatWith (surround $ ";" <++> neutral) parts))
 prettyTerm (Fold _ e (x ** t)) d =
   group $ align $ hang 2 $ parenthesise (d < Open) $
     (group $ hang (-2) $ "fold" <++> prettyTerm e Open <++> "by") <+> line <+>
@@ -231,3 +223,10 @@ prettyTerm (Cons _ t u) d =
   group $ align $ hang 2 $ parenthesise (d < App) $
     concatWith (surround line) [pretty "cons", prettyTerm t Suffix, prettyTerm u Suffix]
 prettyTerm (Str _ str) d = enclose "\"" "\"" $ pretty str
+prettyTerm (FoldCase _ e (MkRow ts _)) d =
+  let parts = prettyCases ts <>> [] in
+  group $ align $ hang 2 $ parenthesise (d < Open) $
+    (group $ "foldcase" <++> prettyTerm e Open <++> "by") <+> line <+>
+    (braces $ flatAlt
+      (neutral <++> concatWith (surround $ line' <+> ";" <++> neutral) parts <+> line)
+      (concatWith (surround $ ";" <++> neutral) parts))
diff --git a/src/Inky/Term/Rename.idr b/src/Inky/Term/Rename.idr
new file mode 100644
index 0000000..7bbd524
--- /dev/null
+++ b/src/Inky/Term/Rename.idr
@@ -0,0 +1,85 @@
+module Inky.Term.Rename
+
+import Inky.Term
+import Flap.Data.List
+import Flap.Data.SnocList.Thinning
+
+public export
+data Thins : Mode -> Mode -> Type where
+  NoSugar : NoSugar `Thins` NoSugar
+  Sugar : qtCtx1 `Thins` qtCtx2 -> Sugar qtCtx1 `Thins` Sugar qtCtx2
+  Quote : ctx2 `Thins` ctx3 -> Quote ctx1 ctx2 `Thins` Quote ctx1 ctx3
+
+export
+rename :
+  mode `Thins` mode' -> tmCtx `Thins` tmCtx' ->
+  Term mode meta tyCtx tmCtx ->
+  Term mode' meta tyCtx tmCtx'
+renameList :
+  mode `Thins` mode' -> tmCtx `Thins` tmCtx' ->
+  List (Term mode meta tyCtx tmCtx) ->
+  List (Term mode' meta tyCtx tmCtx')
+renameAll :
+  mode `Thins` mode' -> tmCtx `Thins` tmCtx' ->
+  (ts : Context (Term mode meta tyCtx tmCtx)) ->
+  All (Assoc0 $ Term mode' meta tyCtx tmCtx') ts.names
+renameBranches :
+  mode `Thins` mode' -> tmCtx `Thins` tmCtx' ->
+  (ts : Context (x ** Term mode meta tyCtx (tmCtx :< x))) ->
+  All (Assoc0 (x ** Term mode' meta tyCtx (tmCtx' :< x))) ts.names
+renameTy' :
+  mode `Thins` mode' -> tmCtx `Thins` tmCtx' ->
+  Ty' mode meta tyCtx tmCtx ->
+  Ty' mode' meta tyCtx tmCtx'
+renameBoundTy' :
+  mode `Thins` mode' -> tmCtx `Thins` tmCtx' ->
+  BoundTy' mode meta tyCtx tmCtx ->
+  BoundTy' mode' meta tyCtx tmCtx'
+
+rename f g (Annot m e a) = Annot m (rename f g e) (renameTy' f g a)
+rename f g (Var m i) = Var m (index g i)
+rename f g (Let m e (x ** t)) = Let m (rename f g e) (x ** rename f (Keep g) t)
+rename f g (LetTy m a (x ** t)) =
+  case f of
+    NoSugar => LetTy m a (x ** rename f g t)
+    Sugar _ => LetTy m a (x ** rename f g t)
+rename f g (Abs m (bound ** t)) = Abs m (bound ** rename f (g <>< lengthOf bound) t)
+rename f g (App m e ts) = App m (rename f g e) (renameList f g ts)
+rename f g (Tup m (MkRow ts fresh)) = Tup m (fromAll (renameAll f g ts) fresh)
+rename f g (Prj m e l) = Prj m (rename f g e) l
+rename f g (Inj m l t) = Inj m l (rename f g t)
+rename f g (Case m e (MkRow ts fresh)) =
+  Case m (rename f g e) (fromAll (renameBranches f g ts) fresh)
+rename f g (Roll m t) = Roll m (rename f g t)
+rename f g (Unroll m e) = Unroll m (rename f g e)
+rename f g (Fold m e (x ** t)) = Fold m (rename f g e) (x ** rename f (Keep g) t)
+rename f g (Map m a b c) = Map m (renameBoundTy' f g a) (renameTy' f g b) (renameTy' f g c)
+rename (Sugar f) g (QuasiQuote m t) = QuasiQuote m (rename (Quote g) f t)
+rename (Quote f) g (Unquote m t) = Unquote m (rename (Sugar g) f t)
+rename (Sugar f) g (QAbs m (bound ** t)) =
+  QAbs m (bound ** rename (Sugar (f <>< lengthOf bound)) g t)
+rename (Sugar f) g (Lit m k) = Lit m k
+rename (Sugar f) g (Suc m t) = Suc m (rename (Sugar f) g t)
+rename (Sugar f) g (List m ts) = List m (renameList (Sugar f) g ts)
+rename (Sugar f) g (Cons m t u) = Cons m (rename (Sugar f) g t) (rename (Sugar f) g u)
+rename (Sugar f) g (Str m str) = Str m str
+rename (Sugar f) g (FoldCase m e (MkRow ts fresh)) =
+  FoldCase m (rename (Sugar f) g e) (fromAll (renameBranches (Sugar f) g ts) fresh)
+
+renameList f g [] = []
+renameList f g (t :: ts) = rename f g t :: renameList f g ts
+
+renameAll f g [<] = [<]
+renameAll f g (ts :< (x :- t)) = renameAll f g ts :< (x :- rename f g t)
+
+renameBranches f g [<] = [<]
+renameBranches f g (ts :< (l :- (x ** t))) =
+  renameBranches f g ts :< (l :- (x ** rename f (Keep g) t))
+
+renameTy' NoSugar g a = a
+renameTy' (Sugar f) g a = a
+renameTy' (Quote f) g t = rename (Sugar g) f t
+
+renameBoundTy' NoSugar g xa = xa
+renameBoundTy' (Sugar f) g xa = xa
+renameBoundTy' (Quote f) g t = rename (Sugar g) f t