Add quotation to help metaprogramming.

15 files changed, 1068 insertions, 996 deletions

diff --git a/inky.ipkg b/inky.ipkg
index 493dea2..fe90df1 100644
--- a/inky.ipkg
+++ b/inky.ipkg
@@ -22,8 +22,6 @@ modules
   , Inky.Term.Pretty
   , Inky.Term.Pretty.Error
   , Inky.Term.Recompute
-  , Inky.Term.Substitution
-  , Inky.Term.Sugar
   , Inky.Type
   , Inky.Type.Pretty
   , Inky.Type.Substitution
diff --git a/program/reducer.prim b/program/reducer.prim
index 0a0517e..3abbc97 100644
--- a/program/reducer.prim
+++ b/program/reducer.prim
@@ -1,16 +1,16 @@
-let Bool = [T: <>, F: <>] in
+let Bool = [T: <>; F: <>] in
 let or (x : Bool) (y : Bool) : Bool = case x of {T u => T <>; F u => y} in
 let SysT =
   (\T =>
     [ Var: Nat
-    , Zero: <>
-    , Suc: T
-    , Primrec: <Zero: T, Suc: T, Target: T>
-    , Abs: T
-    , App: <Fun: T, Arg: T>
+    ; Zero: <>
+    ; Suc: T
+    ; Primrec: <Zero: T; Suc: T; Target: T>
+    ; Abs: T
+    ; App: <Fun: T; Arg: T>
     ])
 in
-let Stepped = <Term: SysT, Smaller: Bool> in
+let Stepped = <Term: SysT; Smaller: Bool> in
 let lift (f : Nat -> Nat) (n : Nat) : Nat =
   case !n of {Z u => 0; S k => suc (f k)}
 in
@@ -20,9 +20,9 @@ let rename (t : SysT) : (Nat -> Nat) -> SysT =
     ; Zero u => \f => ~(Zero <>)
     ; Suc r => \f => ~(Suc (r f))
     ; Primrec p => \f =>
-      ~(Primrec <Zero: p.Zero f, Suc: p.Suc (lift f), Target: p.Target f>)
+      ~(Primrec <Zero: p.Zero f; Suc: p.Suc (lift f); Target: p.Target f>)
     ; Abs r => \f => ~(Abs (r f))
-    ; App p => \f => ~(App <Fun: p.Fun f, Arg: p.Arg f>)
+    ; App p => \f => ~(App <Fun: p.Fun f; Arg: p.Arg f>)
     }
 in
 let index (xs : List SysT) : Nat -> SysT =
@@ -40,35 +40,35 @@ let sub (t : SysT) : List SysT -> SysT =
     ; Primrec p => \env =>
       ~(Primrec
          < Zero: p.Zero env
-         , Suc: p.Suc (cons ~(Var 0) (shift env))
-         , Target: p.Target env
+         ; Suc: p.Suc (cons ~(Var 0) (shift env))
+         ; Target: p.Target env
          >)
     ; Abs f => \env => ~(Abs (f (cons ~(Var 0) (shift env))))
-    ; App p => \env => ~(App <Fun: p.Fun env, Arg: p.Arg env>)
+    ; App p => \env => ~(App <Fun: p.Fun env; Arg: p.Arg env>)
     }
 in
 let app (fun : SysT) (arg : SysT) (smaller : Bool) : Stepped =
   let default : Stepped =
-    <Term: ~(App <Fun: fun, Arg: arg>), Smaller: smaller>
+    <Term: ~(App <Fun: fun; Arg: arg>); Smaller: smaller>
   in
   case !fun of
     { Var n => default
     ; Zero u => default
     ; Suc t => default
     ; Primrec p => default
-    ; Abs t => <Term: sub t [arg], Smaller: T <>>
+    ; Abs t => <Term: sub t [arg]; Smaller: T <>>
     ; App t => default
     }
 in
 let rec (z : SysT) (s : SysT) (target : SysT) (smaller : Bool) : Stepped =
   let default : Stepped =
-    <Term: ~(Primrec <Zero: z, Suc: s, Target: target>), Smaller: smaller>
+    <Term: ~(Primrec <Zero: z; Suc: s; Target: target>); Smaller: smaller>
   in
   case !target of
     { Var n => default
-    ; Zero u => <Term: z, Smaller: T <>>
+    ; Zero u => <Term: z; Smaller: T <>>
     ; Suc t =>
-      <Term: sub s [~(Primrec <Zero: z, Suc: s, Target: t>)], Smaller: T <>>
+      <Term: sub s [~(Primrec <Zero: z; Suc: s; Target: t>)]; Smaller: T <>>
     ; Primrec p => default
     ; Abs t => default
     ; App t => default
@@ -76,9 +76,9 @@ let rec (z : SysT) (s : SysT) (target : SysT) (smaller : Bool) : Stepped =
 in
 let step (t : SysT) : Stepped =
   foldcase t by
-    { Var n => <Term: ~(Var n), Smaller: F <>>
-    ; Zero u => <Term: ~(Zero <>), Smaller: F <>>
-    ; Suc t => <Term: ~(Suc t.Term), Smaller: t.Smaller>
+    { Var n => <Term: ~(Var n); Smaller: F <>>
+    ; Zero u => <Term: ~(Zero <>); Smaller: F <>>
+    ; Suc t => <Term: ~(Suc t.Term); Smaller: t.Smaller>
     ; Primrec t =>
       case t.Target.Smaller of
         { F u =>
@@ -91,22 +91,22 @@ let step (t : SysT) : Stepped =
           < Term:
             ~(Primrec
                (map
-                 (\X => <Zero: X, Suc: X, Target: X>)
+                 (\X => <Zero: X; Suc: X; Target: X>)
                  Stepped
                  SysT
                  (\p => p.Term)
                  t))
-          , Smaller: T <>
+          ; Smaller: T <>
           >
         }
-    ; Abs t => <Term: ~(Abs t.Term), Smaller: t.Smaller>
+    ; Abs t => <Term: ~(Abs t.Term); Smaller: t.Smaller>
     ; App t =>
       case t.Arg.Smaller of
         { F u => app t.Fun.Term t.Arg.Term t.Fun.Smaller
         ; T u =>
           < Term:
-            ~(App (map (\X => <Fun: X, Arg: X>) Stepped SysT (\p => p.Term) t))
-          , Smaller: T <>
+            ~(App (map (\X => <Fun: X; Arg: X>) Stepped SysT (\p => p.Term) t))
+          ; Smaller: T <>
           >
         }
     }
diff --git a/program/reducer.pty b/program/reducer.pty
index 996541b..c72b8c6 100644
--- a/program/reducer.pty
+++ b/program/reducer.pty
@@ -1,17 +1,17 @@
 Nat ->
 (\T =>
   [ Var: Nat
-  , Zero: <>
-  , Suc: T
-  , Primrec: <Zero: T, Suc: T, Target: T>
-  , Abs: T
-  , App: <Fun: T, Arg: T>
+  ; Zero: <>
+  ; Suc: T
+  ; Primrec: <Zero: T; Suc: T; Target: T>
+  ; Abs: T
+  ; App: <Fun: T; Arg: T>
   ]) ->
 (\T =>
   [ Var: Nat
-  , Zero: <>
-  , Suc: T
-  , Primrec: <Zero: T, Suc: T, Target: T>
-  , Abs: T
-  , App: <Fun: T, Arg: T>
+  ; Zero: <>
+  ; Suc: T
+  ; Primrec: <Zero: T; Suc: T; Target: T>
+  ; Abs: T
+  ; App: <Fun: T; Arg: T>
   ])
diff --git a/src/Inky.idr b/src/Inky.idr
index ad3a503..3f6b755 100644
--- a/src/Inky.idr
+++ b/src/Inky.idr
@@ -6,6 +6,8 @@ import Control.App
 import Control.App.Console
 import Control.App.FileIO
 
+import Data.String
+
 import Flap.Decidable
 import Flap.Decidable.Maybe
 import Flap.Parser
@@ -35,45 +37,110 @@ record Erased (a : Type) where
   constructor Forget
   0 value : a
 
+record SynthFailed where
+  constructor UhOh
+  term : Term NoSugar Bounds [<] [<]
+  err : NotSynths {m = Bounds} [<] [<] term
+
+Err : Type
+Err = List1 (WithBounds String)
+
+Interpolation Bounds where
+  interpolate b =
+    "\{show (1 + b.startLine)}:\{show (1 + b.startCol)}--\{show (1 + b.endLine)}:\{show (1 + b.endCol)}"
+
+Interpolation a => Interpolation (WithBounds a) where
+  interpolate x =
+    if x.isIrrelevant
+    then "?:?--?:?: \{x.val}"
+    else "\{x.bounds}: \{x.val}"
+
 -- Actions ---------------------------------------------------------------------
 
-lexInkyString : HasErr String es => String -> App es (List (WithBounds InkyToken))
+readFile : FileIO es => File -> App es String
+readFile f = do
+  content <- read [<] f
+  pure (fastConcat $ content <>> [])
+  where
+  read : SnocList String -> File -> App es (SnocList String)
+  read acc f = do
+    False <- fEOF f
+      | True => pure acc
+    str <- fGetStr f
+    read (acc :< str) f
+
+readFileOrStdin : FileIO es => HasErr IOError es => Maybe FilePath -> App es String
+readFileOrStdin Nothing = readFile stdin
+readFileOrStdin (Just path) = withFile path Read throw readFile
+
+lexInkyString : HasErr (WithBounds String) es => String -> App es (List (WithBounds InkyToken))
 lexInkyString file = do
   let (tokens, _, _, "") = lex tokenMap file
-    | (_, line, col, rest) => throw "\{show (1 + line)}:\{show col}: unexpected character"
+    | (_, line, col, rest) => 
+      throw (MkBounded "unexpected character" False (MkBounds line col line col))
   pure (filter (\x => relevant x.val.kind) tokens)
 
-parseType : HasErr String es => List (WithBounds InkyToken) -> App es (Ty [<])
-parseType toks = do
-  let Ok res [] _ = parse @{EqI} OpenType toks
-    | Ok res (x :: _) _ => throw "\{x.bounds}: unexpected token \{x.val.kind}, expected end of input"
-    | Err msg => throw msg
-  let Right a = res.try [<]
-    | Left msg => throw msg
+Interpolation (List InkyKind) where
+  interpolate [t] = interpolate t
+  interpolate ts = "one of " ++ joinBy ", " (map interpolate ts)
+
+doParse :
+  HasErr (WithBounds String) es =>
+  (p : InkyParser False [<] [<] a) ->
+  {auto 0 wf : collectTypeErrs @{ListSet} [<] [<] [<] [<] p = []} ->
+  List (WithBounds InkyToken) ->
+  App es a
+doParse p toks =
+  case parse @{ListSet} p 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
+
+parseType :
+  Has [HasErr (WithBounds String), 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
 
-parseTerm : HasErr String es => List (WithBounds InkyToken) -> App es (Term Sugar Bounds [<] [<])
-parseTerm toks = do
-  let Ok res [] _ = parse @{EqI} OpenTerm toks
-    | Ok res (x :: _) _ => throw "\{x.bounds}: unexpected token \{x.val.kind}, expected end of input"
-    | Err msg => throw msg
-  let Right t = res.try [<] [<]
-    | Left msg => throw msg
-  pure t
+parseTerm :
+  Has [HasErr (WithBounds String), 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
+  -- Annotate with type
+  let Just _ = tyPath
+    | Nothing => pure t
+  a <- parseType tyPath
+  pure (Annot (MkBounds 0 0 0 0) t a)
 
-checkType : HasErr String es => (a : Ty [<]) -> App es (Erased $ WellFormed a)
-checkType a = do
-  let True `Because` wf = wellFormed a
-    | False `Because` bad => throw "type ill-formed"
-  pure (Forget wf)
+checkType : HasErr String es => (a : Ty [<]) -> App es ()
+checkType a =
+  unless (wellFormed a).does $
+    throw "type ill-formed"
 
 synthTerm :
-  (t : Term mode m [<] [<]) ->
-  HasErr (NotSynths [<] [<] t) es =>
+  (t : Term NoSugar Bounds [<] [<]) ->
+  HasErr SynthFailed es =>
   App es (Subset (Ty [<]) (Synths [<] [<] t))
 synthTerm t = do
   let Just a `Because` prf = synths [<] [<] t
-    | Nothing `Because` contra => throw contra
+    | Nothing `Because` contra => throw (UhOh t contra)
   pure (Element a prf)
 
 printType :
@@ -84,23 +151,13 @@ printType a = do
 
 printTerm :
   PrimIO es => {default defaultLayoutOptions opts : LayoutOptions} ->
-  Term mode m [<] [<] -> App es ()
+  {mode : Term.Mode} -> Term mode m [<] [<] -> App es ()
 printTerm a = do
   primIO $ renderIO $ layoutSmart opts $ prettyTerm a Open
 
-printSynthError :
-  PrimIO es => {default defaultLayoutOptions opts : LayoutOptions} ->
-  {t : Term mode Bounds [<] [<]} ->
-  NotSynths [<] [<] t -> App es ()
-printSynthError contra =
-  primIO $ renderIO $ layoutSmart opts $
-  concatWith (surround hardline) $
-  map (\(bounds, msg) => group $ align $ hang 2 $ pretty "\{bounds}:" <+> line <+> msg) $
-  prettyNotSynths contra
-
 compileTerm :
   PrimIO es => {default defaultLayoutOptions opts : LayoutOptions} ->
-  {t : Term mode m [<] [<]} ->
+  {t : Term NoSugar m [<] [<]} ->
   (0 prf : Synths [<] [<] t a) ->
   App es ()
 compileTerm prf =
@@ -108,22 +165,6 @@ compileTerm prf =
   pretty "(use-modules (ice-9 match))" <+> line <+>
   parens (hang 1 $ pretty "define main" <+> line <+> group (compileSynths [<] [<] prf))
 
-readFile : FileIO es => File -> App es String
-readFile f = do
-  content <- read [<] f
-  pure (fastConcat $ content <>> [])
-  where
-  read : SnocList String -> File -> App es (SnocList String)
-  read acc f = do
-    False <- fEOF f
-      | True => pure acc
-    str <- fGetStr f
-    read (acc :< str) f
-
-readFileOrStdin : FileIO es => HasErr IOError es => Maybe FilePath -> App es String
-readFileOrStdin Nothing = readFile stdin
-readFileOrStdin (Just path) = withFile path Read throw readFile
-
 
 -- Arguments -------------------------------------------------------------------
 
@@ -188,27 +229,25 @@ Inky = MkCommand
 
 -- Driver ----------------------------------------------------------------------
 
-parseArgs :
-  (cmd : Command nm) ->
-  App (String :: Init) (ParseTree cmd)
-parseArgs cmd = do
-  Right args <- primIO cmd.parseArgs
-    | Left msg => throw msg
-  let Pure args = ParsedTree.finalising args
-    | Fail errs => throw (show $ the (Error ()) $ Fail errs)
-  pure args
-
-abortErr : PrimIO es => String -> App es a
-abortErr msg = do
-  primIO $ () <$ fPutStrLn stderr msg
-  primIO exitFailure
-
 showHelp : Console es => App es ()
 showHelp = putStrLn "Usage: \{Inky .usage}"
 
-main : IO ()
-main = run {l = MayThrow} $ do
-  args <- handle {err = String} (parseArgs Inky) pure abortErr
+process :
+  Has
+    [ HasErr String
+    , HasErr (WithBounds String)
+    , HasErr (List1 $ WithBounds String)
+    , HasErr (List1 ErrorMsg)
+    , HasErr SynthFailed
+    , FileIO
+    , PrimIO
+    ] es =>
+  App es ()
+process = do
+  Right args <- primIO (Inky).parseArgs
+    | Left msg => throw msg
+  let Pure args = ParsedTree.finalising args
+    | Fail errs => throw errs
   Collie.handle {cmd = ("inky" ** Inky)} args
     [ const showHelp
     , "--help" ::= [ const showHelp ]
@@ -217,24 +256,16 @@ main = run {l = MayThrow} $ do
       , "type" ::=
         [ \cmd => do
           let path = cmd.arguments
-          txt <- handle {err = IOError} (readFileOrStdin path) pure (abortErr . show)
-          toks <- handle {err = String} (lexInkyString txt) pure abortErr
-          a <- handle {err = String} (parseType toks) pure abortErr
+          a <- parseType path
           printType a
-          pure ()
         ]
       , "term" ::=
         [ \cmd => do
           let path = cmd.arguments
-          txt <- handle {err = IOError} (readFileOrStdin path) pure (abortErr . show)
-          toks <- handle {err = String} (lexInkyString txt) pure abortErr
-          t <- handle {err = String} (parseTerm toks) pure abortErr
+          t <- parseTerm path Nothing
           let [noSugar] = cmd.modifiers.content
           case noSugar of
-            True => do
-              let Just t = maybeDesugar t
-                | Nothing => abortErr "failed to desugar term"
-              printTerm t
+            True => printTerm (desugar t)
             False => printTerm t
         ]
       ]
@@ -243,29 +274,18 @@ main = run {l = MayThrow} $ do
       , "type" ::=
         [ \cmd => do
           let path = cmd.arguments
-          txt <- handle {err = IOError} (readFileOrStdin path) pure (abortErr . show)
-          toks <- handle {err = String} (lexInkyString txt) pure abortErr
-          a <- handle {err = String} (parseType toks) pure abortErr
-          handle {err = String} (checkType a) (const $ pure ()) abortErr
+          a <- parseType path
+          _ <- checkType a
+          pure ()
         ]
       , "term" ::=
         [ \cmd => do
           let path = cmd.arguments
-          txt <- handle {err = IOError} (readFileOrStdin path) pure (abortErr . show)
-          toks <- handle {err = String} (lexInkyString txt) pure abortErr
-          t <- handle {err = String} (parseTerm toks) pure abortErr
           let [type] = cmd.modifiers.content
-          t <-
-            maybe (pure t)
-              (\path => do
-                txt <- handle {err = IOError} (readFileOrStdin $ Just path) pure (abortErr . show)
-                toks <- handle {err = String} (lexInkyString txt) pure abortErr
-                a <- handle {err = String} (parseType toks) pure abortErr
-                handle {err = String} (checkType a) (const $ pure ()) abortErr
-                pure (Annot (MkBounds (-1) (-1) (-1) (-1)) t a))
-              type
-          handle {err = NotSynths [<] [<] t} (synthTerm t) (const $ pure ())
-            (\contra => do printSynthError contra; primIO exitFailure)
+          t <- parseTerm path type
+          let t = desugar t
+          _ <- synthTerm t
+          pure ()
         ]
       ]
     , "compile" ::=
@@ -273,23 +293,50 @@ main = run {l = MayThrow} $ do
       , "term" ::=
         [ \cmd => do
           let path = cmd.arguments
-          txt <- handle {err = IOError} (readFileOrStdin path) pure (abortErr . show)
-          toks <- handle {err = String} (lexInkyString txt) pure abortErr
-          t <- handle {err = String} (parseTerm toks) pure abortErr
           let [type] = cmd.modifiers.content
-          t <-
-            maybe (pure t)
-              (\path => do
-                txt <- handle {err = IOError} (readFileOrStdin $ Just path) pure (abortErr . show)
-                toks <- handle {err = String} (lexInkyString txt) pure abortErr
-                a <- handle {err = String} (parseType toks) pure abortErr
-                handle {err = String} (checkType a) (const $ pure ()) abortErr
-                pure (Annot (MkBounds (-1) (-1) (-1) (-1)) t a))
-              type
-          Element _ prf <-
-            handle {err = NotSynths [<] [<] t} (synthTerm t) pure
-              (\contra => do printSynthError contra; primIO exitFailure)
+          t <- parseTerm path type
+          let t = desugar t
+          Element _ prf <- synthTerm t
           compileTerm prf
         ]
       ]
     ]
+
+handleErr : (0 e : Type) -> (forall a. e -> App es a) -> App (e :: es) a -> App es a
+handleErr e handler app = handle app pure handler
+
+printSynthFailed :
+  PrimIO es => {default defaultLayoutOptions opts : LayoutOptions} ->
+  SynthFailed -> App es ()
+printSynthFailed (UhOh t err) =
+  primIO $ renderIO $ layoutSmart opts $
+  concatWith (surround hardline) $
+  map (\(bounds, msg) => group $ align $ hang 2 $ pretty "\{bounds}:" <+> line <+> msg) $
+  prettyNotSynths err
+
+main : IO ()
+main =
+  run {l = MayThrow} $
+  handleErr (List String)
+    (\msgs => do
+      foldlM (\_, msg => primIO $ () <$ fPutStrLn stderr msg) () msgs
+      primIO exitFailure) $
+  handleErr String
+    (throw . List.singleton) $
+  handleErr (List1 ErrorMsg)
+    (throw . map show . forget) $
+  handleErr (List1 $ WithBounds String)
+    (throw . map interpolate . forget) $
+  handleErr (WithBounds String)
+    (throw . (::: [])) $
+  handleErr IOError
+    (throw . show) $
+  handleErr SynthFailed
+    (\err => do
+      printSynthFailed err
+      primIO exitFailure) $
+  process
+
+-- main =
+--   run {l = MayThrow} $
+--   handle
diff --git a/src/Inky/Term.idr b/src/Inky/Term.idr
index 8fd15aa..0f05f59 100644
--- a/src/Inky/Term.idr
+++ b/src/Inky/Term.idr
@@ -16,7 +16,23 @@ import Flap.Decidable.Maybe
 --------------------------------------------------------------------------------
 
 public export
-data Mode = Sugar | NoSugar
+data Mode : Type where
+  Quote : (tyCtx, tmCtx : SnocList String) -> Mode
+  Sugar : (qtCtx : SnocList String) -> Mode
+  NoSugar : Mode
+
+namespace Mode
+  public export
+  NotQuote : Mode -> Type
+  NotQuote (Quote _ _) = Void
+  NotQuote (Sugar _) = So True
+  NotQuote NoSugar = So True
+
+  public export
+  HasSugar : Mode -> Type
+  HasSugar (Quote _ _) = So True
+  HasSugar (Sugar _) = So True
+  HasSugar NoSugar = Void
 
 public export
 record WithDoc (a : Type) where
@@ -25,11 +41,28 @@ record WithDoc (a : Type) where
   doc : List String
 
 public export
-data Term : Mode -> (m : Type) -> (tyCtx, tmCtx : SnocList String) -> Type where
-  Annot : (meta : m) -> Term mode m tyCtx tmCtx -> Ty tyCtx -> Term mode m tyCtx tmCtx
+data Term : Mode -> (m : Type) -> (tyCtx, tmCtx : SnocList String) -> Type
+
+public export
+Ty' : Mode -> (m : Type) -> (tyCtx, tmCtx : SnocList String) -> Type
+Ty' (Quote tyCtx tmCtx) m _ qtCtx = Term (Sugar qtCtx) m tyCtx tmCtx
+Ty' (Sugar qtCtx) m tyCtx tmCtx = Ty tyCtx
+Ty' NoSugar m tyCtx tmCtx = Ty tyCtx
+
+public export
+BoundTy' : Mode -> (m : Type) -> (tyCtx, tmCtx : SnocList String) -> Type
+BoundTy' (Quote tyCtx tmCtx) m _ qtCtx = Term (Sugar qtCtx) m tyCtx tmCtx
+BoundTy' (Sugar qtCtx) m tyCtx tmCtx = (x ** Ty (tyCtx :< x))
+BoundTy' NoSugar m tyCtx tmCtx = (x ** Ty (tyCtx :< x))
+
+data Term where
+  Annot : (meta : m) -> Term mode m tyCtx tmCtx -> Ty' mode m tyCtx tmCtx -> Term mode m tyCtx tmCtx
   Var : (meta : m) -> Var tmCtx -> Term mode m tyCtx tmCtx
   Let : (meta : WithDoc m) -> Term mode m tyCtx tmCtx -> (x ** Term mode m tyCtx (tmCtx :< x)) -> Term mode m tyCtx tmCtx
-  LetTy : (meta : WithDoc m) -> Ty tyCtx -> (x ** Term mode m (tyCtx :< x) tmCtx) -> Term mode m tyCtx tmCtx
+  LetTy :
+    {auto 0 notQuote : NotQuote mode} ->
+    (meta : WithDoc m) -> Ty tyCtx ->
+    (x ** Term mode m (tyCtx :< x) tmCtx) -> Term mode m tyCtx tmCtx
   Abs : (meta : m) -> (bound ** Term mode m tyCtx (tmCtx <>< bound)) -> Term mode m tyCtx tmCtx
   App : (meta : m) -> Term mode m tyCtx tmCtx -> List (Term mode m tyCtx tmCtx) -> Term mode m tyCtx tmCtx
   Tup : (meta : m) -> Row (Term mode m tyCtx tmCtx) -> Term mode m tyCtx tmCtx
@@ -39,7 +72,29 @@ data Term : Mode -> (m : Type) -> (tyCtx, tmCtx : SnocList String) -> Type where
   Roll : (meta : m) -> Term mode m tyCtx tmCtx -> Term mode m tyCtx tmCtx
   Unroll : (meta : m) -> Term mode m tyCtx tmCtx -> Term mode m tyCtx tmCtx
   Fold : (meta : m) -> Term mode m tyCtx tmCtx -> (x ** Term mode m tyCtx (tmCtx :< x)) -> Term mode m tyCtx tmCtx
-  Map : (meta : m) -> (x ** Ty (tyCtx :< x)) -> Ty tyCtx -> Ty tyCtx -> Term Sugar m tyCtx tmCtx
+  Map : (meta : m) -> BoundTy' mode m tyCtx tmCtx -> Ty' mode m tyCtx tmCtx -> Ty' mode m tyCtx tmCtx -> Term mode m tyCtx tmCtx
+  -- Quotation sugar
+  QuasiQuote : (meta : m) -> Term (Quote tyCtx tmCtx) m [<] qtCtx -> Term (Sugar qtCtx) m tyCtx tmCtx
+  Unquote : (meta : m) -> Term (Sugar qtCtx) m tyCtx tmCtx -> Term (Quote tyCtx tmCtx) m [<] qtCtx
+  QAbs : (meta : m) -> (bound ** Term (Sugar (qtCtx <>< bound)) m tyCtx tmCtx) -> Term (Sugar qtCtx) m tyCtx tmCtx
+  -- Other sugar
+  Lit :
+    (meta : m) -> Nat ->
+    Term (Sugar qtCtx) m tyCtx tmCtx
+  Suc :
+    (meta : m) -> Term (Sugar qtCtx) m tyCtx tmCtx ->
+    Term (Sugar qtCtx) m tyCtx tmCtx
+  List :
+    (meta : m) -> List (Term (Sugar qtCtx) m tyCtx tmCtx) ->
+    Term (Sugar qtCtx) m tyCtx tmCtx
+  Cons :
+    (meta : m) ->
+    Term (Sugar qtCtx) m tyCtx tmCtx ->
+    Term (Sugar qtCtx) m tyCtx tmCtx ->
+    Term (Sugar qtCtx) m tyCtx tmCtx
+  Str :
+    (meta : m) -> String ->
+    Term (Sugar qtCtx) m tyCtx tmCtx
 
 %name Term e, f, t, u
 
@@ -59,6 +114,14 @@ export
 (Unroll meta _).meta = meta
 (Fold meta _ _).meta = meta
 (Map meta _ _ _).meta = meta
+(QuasiQuote meta _).meta = meta
+(Unquote meta _).meta = meta
+(QAbs meta _).meta = meta
+(Lit meta _).meta = meta
+(Suc meta _).meta = meta
+(List meta _).meta = meta
+(Cons meta _ _).meta = meta
+(Str meta _).meta = meta
 
 --------------------------------------------------------------------------------
 -- Well Formed -----------------------------------------------------------------
@@ -126,7 +189,7 @@ isFunction (x :: bound) a =
 
 namespace Modes
   public export
-  data SynthsOnly : Term mode m tyCtx tmCtx -> Type where
+  data SynthsOnly : Term NoSugar m tyCtx tmCtx -> Type where
     Annot : SynthsOnly (Annot meta t a)
     Var : SynthsOnly (Var meta i)
     App : SynthsOnly (App meta f ts)
@@ -135,7 +198,7 @@ namespace Modes
     Map : SynthsOnly (Map meta (x ** a) b c)
 
   public export
-  data ChecksOnly : Term mode m tyCtx tmCtx -> Type where
+  data ChecksOnly : Term NoSugar m tyCtx tmCtx -> Type where
     Abs : ChecksOnly (Abs meta (bounds ** t))
     Inj : ChecksOnly (Inj meta l t)
     Case : ChecksOnly (Case meta e ts)
@@ -149,19 +212,19 @@ public export
 data Synths :
   All (Assoc0 $ Ty [<]) tyCtx ->
   All (Assoc0 $ Ty [<]) tmCtx ->
-  Term mode m tyCtx tmCtx -> Ty [<] -> Type
+  Term NoSugar m tyCtx tmCtx -> Ty [<] -> Type
 public export
 data Checks :
   All (Assoc0 $ Ty [<]) tyCtx ->
   All (Assoc0 $ Ty [<]) tmCtx ->
-  Ty [<] -> Term mode m tyCtx tmCtx -> Type
+  Ty [<] -> Term NoSugar m tyCtx tmCtx -> Type
 
 namespace Spine
   public export
   data CheckSpine :
     All (Assoc0 $ Ty [<]) tyCtx ->
     All (Assoc0 $ Ty [<]) tmCtx ->
-    Ty [<] -> List (Term mode m tyCtx tmCtx) -> Ty [<] -> Type
+    Ty [<] -> List (Term NoSugar m tyCtx tmCtx) -> Ty [<] -> Type
     where
     Nil : CheckSpine tyEnv tmEnv a [] a
     (::) :
@@ -176,7 +239,7 @@ namespace Synths
   data AllSynths :
     All (Assoc0 $ Ty [<]) tyCtx ->
     All (Assoc0 $ Ty [<]) tmCtx ->
-    Context (Term mode m tyCtx tmCtx) -> Row (Ty [<]) -> Type
+    Context (Term NoSugar m tyCtx tmCtx) -> Row (Ty [<]) -> Type
     where
     Lin : AllSynths tyEnv tmEnv [<] [<]
     (:<) :
@@ -192,7 +255,7 @@ namespace Checks
   data AllChecks :
     All (Assoc0 $ Ty [<]) tyCtx ->
     All (Assoc0 $ Ty [<]) tmCtx ->
-    Context (Ty [<]) -> Context (Term mode m tyCtx tmCtx) -> Type
+    Context (Ty [<]) -> Context (Term NoSugar m tyCtx tmCtx) -> Type
     where
     Base : AllChecks tyEnv tmEnv [<] [<]
     Step :
@@ -208,7 +271,7 @@ namespace Branches
   data AllBranches :
     All (Assoc0 $ Ty [<]) tyCtx ->
     All (Assoc0 $ Ty [<]) tmCtx ->
-    Context (Ty [<]) -> Ty [<] -> Context (x ** Term mode m tyCtx (tmCtx :< x)) -> Type
+    Context (Ty [<]) -> Ty [<] -> Context (x ** Term NoSugar m tyCtx (tmCtx :< x)) -> Type
     where
     Base : AllBranches tyEnv tmEnv [<] a [<]
     Step :
@@ -233,7 +296,7 @@ data Synths where
   LetTyS :
     WellFormed a ->
     Synths (tyEnv :< (x :- sub tyEnv a)) tmEnv e b ->
-    Synths tyEnv tmEnv (LetTy meta a (x ** e)) b
+    Synths tyEnv tmEnv (LetTy {notQuote} meta a (x ** e)) b
   AppS :
     Synths tyEnv tmEnv f a ->
     CheckSpine tyEnv tmEnv a ts b ->
@@ -263,9 +326,9 @@ data Checks where
     Alpha b c ->
     Checks tyEnv tmEnv c (Annot meta t a)
   VarC :
-    Synths tyEnv tmEnv (Var {mode} meta i) a ->
+    Synths tyEnv tmEnv (Var meta i) a ->
     Alpha a b ->
-    Checks tyEnv tmEnv b (Var {mode} meta i)
+    Checks tyEnv tmEnv b (Var meta i)
   LetC :
     Synths tyEnv tmEnv e a ->
     Checks tyEnv (tmEnv :< (x :- a)) b t ->
@@ -273,7 +336,7 @@ data Checks where
   LetTyC :
     WellFormed a ->
     Checks (tyEnv :< (x :- sub tyEnv a)) tmEnv b t ->
-    Checks tyEnv tmEnv b (LetTy meta a (x ** t))
+    Checks tyEnv tmEnv b (LetTy {notQuote} meta a (x ** t))
   AbsC :
     IsFunction bound a dom cod ->
     Checks tyEnv (tmEnv <>< dom) cod t ->
@@ -334,19 +397,19 @@ public export
 data NotSynths :
   All (Assoc0 $ Ty [<]) tyCtx ->
   All (Assoc0 $ Ty [<]) tmCtx ->
-  Term mode m tyCtx tmCtx -> Type
+  Term NoSugar m tyCtx tmCtx -> Type
 public export
 data NotChecks :
   All (Assoc0 $ Ty [<]) tyCtx ->
   All (Assoc0 $ Ty [<]) tmCtx ->
-  Ty [<] -> Term mode m tyCtx tmCtx -> Type
+  Ty [<] -> Term NoSugar m tyCtx tmCtx -> Type
 
 namespace Spine
   public export
   data NotCheckSpine :
     All (Assoc0 $ Ty [<]) tyCtx ->
     All (Assoc0 $ Ty [<]) tmCtx ->
-    Ty [<] -> List (Term mode m tyCtx tmCtx) -> Type
+    Ty [<] -> List (Term NoSugar m tyCtx tmCtx) -> Type
     where
     Step1 :
       ((b, c : Ty [<]) -> Not (a = TArrow b c)) ->
@@ -362,7 +425,7 @@ namespace Synths
   data AnyNotSynths :
     All (Assoc0 $ Ty [<]) tyCtx ->
     All (Assoc0 $ Ty [<]) tmCtx ->
-    (ts : Context (Term mode m tyCtx tmCtx)) -> Type
+    (ts : Context (Term NoSugar m tyCtx tmCtx)) -> Type
     where
     Step :
       These (NotSynths tyEnv tmEnv t) (AnyNotSynths tyEnv tmEnv ts) ->
@@ -375,7 +438,7 @@ namespace Checks
   data AnyNotChecks :
     All (Assoc0 $ Ty [<]) tyCtx ->
     All (Assoc0 $ Ty [<]) tmCtx ->
-    Context (Ty [<]) -> Context (Term mode m tyCtx tmCtx) -> Type
+    Context (Ty [<]) -> Context (Term NoSugar m tyCtx tmCtx) -> Type
     where
     Base1 : AnyNotChecks tyEnv tmEnv (as :< la) [<]
     Step1 :
@@ -393,7 +456,7 @@ namespace Branches
   data AnyNotBranches :
     All (Assoc0 $ Ty [<]) tyCtx ->
     All (Assoc0 $ Ty [<]) tmCtx ->
-    Context (Ty [<]) -> Ty [<] -> Context (x ** Term mode m tyCtx (tmCtx :< x)) -> Type
+    Context (Ty [<]) -> Ty [<] -> Context (x ** Term NoSugar m tyCtx (tmCtx :< x)) -> Type
     where
     Base1 : AnyNotBranches tyEnv tmEnv (as :< a) b [<]
     Step1 :
@@ -429,7 +492,7 @@ data NotSynths where
     NotSynths tyEnv tmEnv (Let meta e (x ** f))
   LetTyNS :
     These (IllFormed a) (NotSynths (tyEnv :< (x :- sub tyEnv a)) tmEnv e) ->
-    NotSynths tyEnv tmEnv (LetTy meta a (x ** e))
+    NotSynths tyEnv tmEnv (LetTy {notQuote} meta a (x ** e))
   AppNS1 :
     NotSynths tyEnv tmEnv f ->
     NotSynths tyEnv tmEnv (App meta f ts)
@@ -486,7 +549,7 @@ data NotChecks where
     NotChecks tyEnv tmEnv b (Let meta e (x ** t))
   LetTyNC :
     These (IllFormed a) (NotChecks (tyEnv :< (x :- sub tyEnv a)) tmEnv b t) ->
-    NotChecks tyEnv tmEnv b (LetTy meta a (x ** t))
+    NotChecks tyEnv tmEnv b (LetTy {notQuote} meta a (x ** t))
   AbsNC1 :
     NotFunction bound a ->
     NotChecks tyEnv tmEnv a (Abs meta (bound ** t))
diff --git a/src/Inky/Term/Checks.idr b/src/Inky/Term/Checks.idr
index 829561a..0824362 100644
--- a/src/Inky/Term/Checks.idr
+++ b/src/Inky/Term/Checks.idr
@@ -1,13 +1,16 @@
 module Inky.Term.Checks
 
 import Control.Function
+
 import Data.DPair
 import Data.List.Quantifiers
 import Data.Singleton
 import Data.These
+
 import Flap.Data.SnocList.Quantifiers
 import Flap.Decidable
 import Flap.Decidable.Maybe
+
 import Inky.Term
 import Inky.Term.Recompute
 
@@ -208,23 +211,23 @@ export
 synths :
   (tyEnv : All (Assoc0 $ Ty [<]) tyCtx) ->
   (tmEnv : All (Assoc0 $ Ty [<]) tmCtx) ->
-  (e : Term mode m tyCtx tmCtx) ->
+  (e : Term NoSugar m tyCtx tmCtx) ->
   Proof (Ty [<]) (Synths tyEnv tmEnv e) (NotSynths tyEnv tmEnv e)
 export
 checks :
   (tyEnv : All (Assoc0 $ Ty [<]) tyCtx) ->
   (tmEnv : All (Assoc0 $ Ty [<]) tmCtx) ->
-  (a : Ty [<]) -> (t : Term mode m tyCtx tmCtx) ->
+  (a : Ty [<]) -> (t : Term NoSugar m tyCtx tmCtx) ->
   LazyEither (Checks tyEnv tmEnv a t) (NotChecks tyEnv tmEnv a t)
 checkSpine :
   (tyEnv : All (Assoc0 $ Ty [<]) tyCtx) ->
   (tmEnv : All (Assoc0 $ Ty [<]) tmCtx) ->
-  (a : Ty [<]) -> (ts : List (Term mode m tyCtx tmCtx)) ->
+  (a : Ty [<]) -> (ts : List (Term NoSugar m tyCtx tmCtx)) ->
   Proof (Ty [<]) (CheckSpine tyEnv tmEnv a ts) (NotCheckSpine tyEnv tmEnv a ts)
 allSynths :
   (tyEnv : All (Assoc0 $ Ty [<]) tyCtx) ->
   (tmEnv : All (Assoc0 $ Ty [<]) tmCtx) ->
-  (es : Context (Term mode m tyCtx tmCtx)) ->
+  (es : Context (Term NoSugar m tyCtx tmCtx)) ->
   (0 fresh : AllFresh es.names) ->
   Proof (Subset (Row (Ty [<])) (\as => es.names = as.names))
     (AllSynths tyEnv tmEnv es . Subset.fst)
@@ -232,12 +235,13 @@ allSynths :
 allChecks :
   (tyEnv : All (Assoc0 $ Ty [<]) tyCtx) ->
   (tmEnv : All (Assoc0 $ Ty [<]) tmCtx) ->
-  (as : Context (Ty [<])) -> (ts : Context (Term mode m tyCtx tmCtx)) ->
+  (as : Context (Ty [<])) -> (ts : Context (Term NoSugar m tyCtx tmCtx)) ->
   LazyEither (AllChecks tyEnv tmEnv as ts) (AnyNotChecks tyEnv tmEnv as ts)
 allBranches :
   (tyEnv : All (Assoc0 $ Ty [<]) tyCtx) ->
   (tmEnv : All (Assoc0 $ Ty [<]) tmCtx) ->
-  (as : Context (Ty [<])) -> (a : Ty [<]) -> (ts : Context (x ** Term mode m tyCtx (tmCtx :< x))) ->
+  (as : Context (Ty [<])) -> (a : Ty [<]) ->
+  (ts : Context (x ** Term NoSugar m tyCtx (tmCtx :< x))) ->
   LazyEither (AllBranches tyEnv tmEnv as a ts) (AnyNotBranches tyEnv tmEnv as a ts)
 
 synths tyEnv tmEnv (Annot _ t a) =
diff --git a/src/Inky/Term/Compile.idr b/src/Inky/Term/Compile.idr
index 0867cd2..0d42660 100644
--- a/src/Inky/Term/Compile.idr
+++ b/src/Inky/Term/Compile.idr
@@ -149,7 +149,7 @@ compileFold {a} wf prf target bind body =
 export
 compileSynths :
   {tmCtx : SnocList String} ->
-  {t : Term mode m tyCtx tmCtx} ->
+  {t : Term NoSugar m tyCtx tmCtx} ->
   {tyEnv : All (Assoc0 $ Ty [<]) tyCtx} ->
   {tmEnv : All (Assoc0 $ Ty [<]) tmCtx} ->
   (0 tyWf : DAll WellFormed tyEnv) ->
@@ -159,7 +159,7 @@ compileSynths :
 export
 compileChecks :
   {tmCtx : SnocList String} ->
-  {t : Term mode m tyCtx tmCtx} ->
+  {t : Term NoSugar m tyCtx tmCtx} ->
   {tyEnv : All (Assoc0 $ Ty [<]) tyCtx} ->
   {tmEnv : All (Assoc0 $ Ty [<]) tmCtx} ->
   (0 tyWf : DAll WellFormed tyEnv) ->
@@ -170,7 +170,7 @@ compileChecks :
   Doc ann
 compileSpine :
   {tmCtx : SnocList String} ->
-  {ts : List (Term mode m tyCtx tmCtx)} ->
+  {ts : List (Term NoSugar m tyCtx tmCtx)} ->
   {tyEnv : All (Assoc0 $ Ty [<]) tyCtx} ->
   {tmEnv : All (Assoc0 $ Ty [<]) tmCtx} ->
   (0 tyWf : DAll WellFormed tyEnv) ->
@@ -182,7 +182,7 @@ compileSpine :
   Doc ann
 compileAllSynths :
   {tmCtx : SnocList String} ->
-  {ts : Context (Term mode m tyCtx tmCtx)} ->
+  {ts : Context (Term NoSugar m tyCtx tmCtx)} ->
   {tyEnv : All (Assoc0 $ Ty [<]) tyCtx} ->
   {tmEnv : All (Assoc0 $ Ty [<]) tmCtx} ->
   (0 tyWf : DAll WellFormed tyEnv) ->
@@ -191,7 +191,7 @@ compileAllSynths :
   All (Assoc0 $ Doc ann) ts.names
 compileAllChecks :
   {tmCtx : SnocList String} ->
-  {ts : Context (Term mode m tyCtx tmCtx)} ->
+  {ts : Context (Term NoSugar m tyCtx tmCtx)} ->
   {tyEnv : All (Assoc0 $ Ty [<]) tyCtx} ->
   {tmEnv : All (Assoc0 $ Ty [<]) tmCtx} ->
   (0 tyWf : DAll WellFormed tyEnv) ->
@@ -203,7 +203,7 @@ compileAllChecks :
   All (Assoc0 $ Doc ann) ts.names
 compileAllBranches :
   {tmCtx : SnocList String} ->
-  {ts : Context (x ** Term mode m tyCtx (tmCtx :< x))} ->
+  {ts : Context (x ** Term NoSugar m tyCtx (tmCtx :< x))} ->
   {tyEnv : All (Assoc0 $ Ty [<]) tyCtx} ->
   {tmEnv : All (Assoc0 $ Ty [<]) tmCtx} ->
   (0 tyWf : DAll WellFormed tyEnv) ->
diff --git a/src/Inky/Term/Desugar.idr b/src/Inky/Term/Desugar.idr
index 4bf8f05..2ad87c9 100644
--- a/src/Inky/Term/Desugar.idr
+++ b/src/Inky/Term/Desugar.idr
@@ -1,269 +1,226 @@
 module Inky.Term.Desugar
 
-import Data.List.Quantifiers
-import Data.Maybe
-import Flap.Data.List
-import Flap.Decidable
+import Control.Monad.State
+import Data.SortedMap
 import Inky.Term
-import Inky.Term.Substitution
 
--- Desugar map -----------------------------------------------------------------
-
-desugarMap :
-  (meta : m) =>
-  (a : Ty tyCtx) -> (i : Var tyCtx) -> (0 prf : i `StrictlyPositiveIn` a) ->
-  (f : Term mode m tyCtx' tmCtx) ->
-  (t : Term mode m tyCtx' tmCtx) ->
-  Term mode m tyCtx' tmCtx
-desugarMapTuple :
-  (meta : m) =>
-  (as : Context (Ty tyCtx)) ->
-  (0 fresh : AllFresh as.names) ->
-  (i : Var tyCtx) -> (0 prfs : i `StrictlyPositiveInAll` as) ->
-  (f : Term mode m tyCtx' tmCtx) ->
-  (t : Term mode m tyCtx' tmCtx) ->
-  Row (Term mode m tyCtx' tmCtx)
-desugarMapTupleNames :
-  (0 meta : m) =>
-  (as : Context (Ty tyCtx)) ->
-  (0 fresh : AllFresh as.names) ->
-  (0 i : Var tyCtx) -> (0 prfs : i `StrictlyPositiveInAll` as) ->
-  (0 f : Term mode m tyCtx' tmCtx) ->
-  (0 t : Term mode m tyCtx' tmCtx) ->
-  (desugarMapTuple as fresh i prfs f t).names = as.names
-desugarMapCase :
+-- Other Sugar -----------------------------------------------------------------
+
+suc : m -> Term NoSugar m tyCtx tmCtx -> Term NoSugar m tyCtx tmCtx
+suc meta t = Roll meta $ Inj meta "S" t
+
+lit : m -> Nat -> Term NoSugar m tyCtx tmCtx
+lit meta 0 = Roll meta $ Inj meta "Z" $ Tup meta [<]
+lit meta (S k) = suc meta (lit meta k)
+
+cons : m -> Term NoSugar m tyCtx tmCtx -> Term NoSugar m tyCtx tmCtx -> Term NoSugar m tyCtx tmCtx
+cons meta t u = Roll meta $ Inj meta "C" $ Tup meta [<"H" :- t, "T" :- u]
+
+list : m -> List (Term NoSugar m tyCtx tmCtx) -> Term NoSugar m tyCtx tmCtx
+list meta [] = Roll meta $ Inj meta "N" $ Tup meta [<]
+list meta (t :: ts) = cons meta t (list meta ts)
+
+record Cache (a : Type) where
+  constructor MkCache
+  max : Nat
+  vals : SortedMap a Nat
+
+miss : Ord a => a -> Cache a -> (Cache a, Nat)
+miss x cache =
+  let newVals = insert x cache.max cache.vals in
+  let newMax = S cache.max in
+  (MkCache newMax newVals, cache.max)
+
+lookup : Ord a => MonadState (Cache a) m => a -> m Nat
+lookup x = do
+  cache <- get
+  case lookup x cache.vals of
+    Nothing => state (miss x)
+    Just n => pure n
+
+string : MonadState (Cache String) f => m -> String -> f (Term NoSugar m tyCtx tmCtx)
+string meta str = do
+  n <- lookup str
+  pure $ lit meta n
+
+-- Desugar ---------------------------------------------------------------------
+
+desugar' :
+  MonadState (Cache String) f =>
+  Term (Sugar qtCtx) m tyCtx tmCtx -> f (Term NoSugar m tyCtx tmCtx)
+desugarAll :
+  MonadState (Cache String) f =>
+  List (Term (Sugar qtCtx) m tyCtx tmCtx) ->
+  f (List $ Term NoSugar m tyCtx tmCtx)
+desugarCtx :
+  MonadState (Cache String) f =>
+  (ctx : Context (Term (Sugar qtCtx) m tyCtx tmCtx)) ->
+  f (All (Assoc0 $ Term NoSugar m tyCtx tmCtx) ctx.names)
+desugarBranches :
+  MonadState (Cache String) f =>
+  (ctx : Context (x ** Term (Sugar qtCtx) m tyCtx (tmCtx :< x))) ->
+  f (All (Assoc0 (x ** Term NoSugar m tyCtx (tmCtx :< x))) ctx.names)
+
+quote :
+  MonadState (Cache String) f =>
+  Term (Quote tyCtx tmCtx) m [<] qtCtx ->
+  f (Term NoSugar m tyCtx tmCtx)
+quoteAll :
+  MonadState (Cache String) f =>
+  List (Term (Quote tyCtx tmCtx) m [<] qtCtx) ->
+  f (List $ Term NoSugar m tyCtx tmCtx)
+quoteCtx :
+  MonadState (Cache String) f =>
   (meta : m) =>
-  (as : Context (Ty tyCtx)) ->
-  (0 fresh : AllFresh as.names) ->
-  (i : Var tyCtx) -> (0 prfs : i `StrictlyPositiveInAll` as) ->
-  (f : Term mode m tyCtx' tmCtx) ->
-  Row (x ** Term mode m tyCtx' (tmCtx :< x))
-desugarMapCaseNames :
+  Context (Term (Quote tyCtx tmCtx) m [<] qtCtx) ->
+  f (List $ Term NoSugar m tyCtx tmCtx)
+quoteBranches :
+  MonadState (Cache String) f =>
   (meta : m) =>
-  (as : Context (Ty tyCtx)) ->
-  (0 fresh : AllFresh as.names) ->
-  (i : Var tyCtx) -> (0 prfs : i `StrictlyPositiveInAll` as) ->
-  (f : Term mode m tyCtx' tmCtx) ->
-  (desugarMapCase as fresh i prfs f).names = as.names
-
-desugarMap (TVar j) i TVar f t with (i `decEq` j)
-  _ | True `Because` _ = App meta f [t]
-  _ | False `Because` _ = t
-desugarMap (TArrow a b) i (TArrow prf) f t = t
-desugarMap (TProd (MkRow as fresh)) i (TProd prfs) f t =
-  Tup meta (desugarMapTuple as fresh i prfs f t)
-desugarMap (TSum (MkRow as fresh)) i (TSum prfs) f t =
-  Case meta t (desugarMapCase as fresh i prfs f)
-desugarMap (TFix x a) i (TFix prf) f t =
-  Fold meta t ("_eta" ** Roll meta
-    (desugarMap a (ThereVar i) prf (thin (Drop Id) f) (Var meta (%% "_eta"))))
-
-desugarMapTuple [<] [<] i [<] f t = [<]
-desugarMapTuple (as :< (l :- a)) (fresh :< freshIn) i (prfs :< prf) f t =
-  (:<)
-    (desugarMapTuple as fresh i prfs f t)
-    (l :- desugarMap a i prf f (Prj meta t l))
-    @{rewrite desugarMapTupleNames as fresh i prfs f t in freshIn}
-
-desugarMapTupleNames [<] [<] i [<] f t = Refl
-desugarMapTupleNames (as :< (l :- a)) (fresh :< freshIn) i (prfs :< prf) f t =
-  cong (:< l) $ desugarMapTupleNames as fresh i prfs f t
-
-desugarMapCase [<] [<] i [<] f = [<]
-desugarMapCase (as :< (l :- a)) (fresh :< freshIn) i (prfs :< prf) f =
-  (:<)
-    (desugarMapCase as fresh i prfs f)
-    (l :- ("_eta" ** Inj meta l (desugarMap a i prf (thin (Drop Id) f) (Var meta (%% "_eta")))))
-    @{rewrite desugarMapCaseNames as fresh i prfs f in freshIn}
-
-desugarMapCaseNames [<] [<] i [<] f = Refl
-desugarMapCaseNames (as :< (l :- a)) (fresh :< freshIn) i (prfs :< prf) f =
-  cong (:< l) $ desugarMapCaseNames as fresh i prfs f
-
--- Desugar Terms ---------------------------------------------------------------
-
-desugarSynths :
-  (len : LengthOf tyCtx) =>
-  {t : Term Sugar m tyCtx tmCtx} ->
-  (0 _ : Synths tyEnv tmEnv t a) ->
-  Term NoSugar m tyCtx tmCtx
-desugarChecks :
-  LengthOf tyCtx =>
-  {t : Term Sugar m tyCtx tmCtx} ->
-  (0 _ : Checks tyEnv tmEnv a t) ->
-  Term NoSugar m tyCtx tmCtx
-desugarCheckSpine :
-  LengthOf tyCtx =>
-  {ts : List (Term Sugar m tyCtx tmCtx)} ->
-  (0 _ : CheckSpine tyEnv tmEnv a ts b) ->
-  List (Term NoSugar m tyCtx tmCtx)
-desugarAllSynths :
-  LengthOf tyCtx =>
-  {ts : Context (Term Sugar m tyCtx tmCtx)} ->
-  (0 _ : AllSynths tyEnv tmEnv ts as) ->
-  Context (Term NoSugar m tyCtx tmCtx)
-desugarAllChecks :
-  LengthOf tyCtx =>
-  {ts : Context (Term Sugar m tyCtx tmCtx)} ->
-  (0 _ : AllChecks tyEnv tmEnv as ts) ->
-  Context (Term NoSugar m tyCtx tmCtx)
-desugarAllBranches :
-  LengthOf tyCtx =>
-  {ts : Context (x ** Term Sugar m tyCtx (tmCtx :< x))} ->
-  (0 _ : AllBranches tyEnv tmEnv as a ts) ->
-  Context (x ** Term NoSugar m tyCtx (tmCtx :< x))
-desugarAllSynthsNames :
-  (0 len : LengthOf tyCtx) =>
-  {ts : Context (Term Sugar m tyCtx tmCtx)} ->
-  (0 prfs : AllSynths tyEnv tmEnv ts as) ->
-  (desugarAllSynths prfs).names = ts.names
-desugarAllChecksNames :
-  (0 len : LengthOf tyCtx) =>
-  {ts : Context (Term Sugar m tyCtx tmCtx)} ->
-  (0 prfs : AllChecks tyEnv tmEnv as ts) ->
-  (desugarAllChecks prfs).names = ts.names
-desugarAllBranchesNames :
-  (0 len : LengthOf tyCtx) =>
-  {ts : Context (x ** Term Sugar m tyCtx (tmCtx :< x))} ->
-  (0 prfs : AllBranches tyEnv tmEnv as a ts) ->
-  (desugarAllBranches prfs).names = ts.names
-
-desugarSynths (AnnotS {meta, a} wf prf) = Annot meta (desugarChecks prf) a
-desugarSynths (VarS {meta, i}) = Var meta i
-desugarSynths (LetS {meta, x} prf1 prf2) = Let meta (desugarSynths prf1) (x ** desugarSynths prf2)
-desugarSynths (LetTyS {meta, a, x} wf prf) = LetTy meta a (x ** desugarSynths prf)
-desugarSynths (AppS {meta} prf prfs) = App meta (desugarSynths prf) (desugarCheckSpine prfs)
-desugarSynths (TupS {meta, es} prfs) =
-  Tup meta (MkRow (desugarAllSynths prfs) (rewrite desugarAllSynthsNames prfs in es.fresh))
-desugarSynths (PrjS {meta, l} prf i) = Prj meta (desugarSynths prf) l
-desugarSynths (UnrollS {meta} prf) = Unroll meta (desugarSynths prf)
-desugarSynths (MapS {meta, x, a, b, c} (TFix prf1 wf1) wf2 wf3) =
-  Annot meta
-    (Abs meta
-      (["_fun", "_arg"] ** desugarMap a (%% x) prf1 (Var meta (%% "_fun")) (Var meta (%% "_arg"))))
-    (TArrow (TArrow b c) (TArrow
-      (sub (tabulate len (\i => _ :- TVar (toVar i)) :< (x :- b)) a)
-      (sub (tabulate len (\i => _ :- TVar (toVar i)) :< (x :- c)) a)))
-
-desugarChecks (AnnotC prf1 prf2) = desugarSynths prf1
-desugarChecks (VarC prf1 prf2) = desugarSynths prf1
-desugarChecks (LetC {meta, x} prf1 prf2) = Let meta (desugarSynths prf1) (x ** desugarChecks prf2)
-desugarChecks (LetTyC {meta, a, x} wf prf) = LetTy meta a (x ** desugarChecks prf)
-desugarChecks (AbsC {meta, bound} prf1 prf2) = Abs meta (bound ** desugarChecks prf2)
-desugarChecks (AppC prf1 prf2) = desugarSynths prf1
-desugarChecks (TupC {meta, ts} prfs) =
-  Tup meta (MkRow (desugarAllChecks prfs) (rewrite desugarAllChecksNames prfs in ts.fresh))
-desugarChecks (PrjC prf1 prf2) = desugarSynths prf1
-desugarChecks (InjC {meta, l} i prf) = Inj meta l (desugarChecks prf)
-desugarChecks (CaseC {meta, ts} prf prfs) =
-  Case meta (desugarSynths prf)
-    (MkRow (desugarAllBranches prfs) (rewrite desugarAllBranchesNames prfs in ts.fresh))
-desugarChecks (RollC {meta} prf) = Roll meta (desugarChecks prf)
-desugarChecks (UnrollC prf1 prf2) = desugarSynths prf1
-desugarChecks (FoldC {meta, y} prf1 prf2) = Fold meta (desugarSynths prf1) (y ** desugarChecks prf2)
-desugarChecks (MapC prf1 prf2) = desugarSynths prf1
-
-desugarCheckSpine [] = []
-desugarCheckSpine (prf :: prfs) = desugarChecks prf :: desugarCheckSpine prfs
-
-desugarAllSynths [<] = [<]
-desugarAllSynths ((:<) {l} prfs prf) = desugarAllSynths prfs :< (l :- desugarSynths prf)
-
-desugarAllChecks Base = [<]
-desugarAllChecks (Step {l} i prf prfs) = desugarAllChecks prfs :< (l :- desugarChecks prf)
-
-desugarAllBranches Base = [<]
-desugarAllBranches (Step {l, x} i prf prfs) = desugarAllBranches prfs :< (l :- (x ** desugarChecks prf))
-
-desugarAllSynthsNames [<] = Refl
-desugarAllSynthsNames ((:<) {l} prfs prf) = cong (:< l) $ desugarAllSynthsNames prfs
-
-desugarAllChecksNames Base = Refl
-desugarAllChecksNames (Step {l} i prf prfs) = cong (:< l) $ desugarAllChecksNames prfs
-
-desugarAllBranchesNames Base = Refl
-desugarAllBranchesNames (Step {l} i prf prfs) = cong (:< l) $ desugarAllBranchesNames prfs
-
--- Fallibly Desugar Terms ------------------------------------------------------
+  Context (x ** Term (Quote tyCtx tmCtx) m [<] (qtCtx :< x)) ->
+  f (List $ Term NoSugar m tyCtx tmCtx)
+
+desugar' (Annot meta t a) =
+  let f = \t => Annot meta t a in
+  [| f (desugar' t) |]
+desugar' (Var meta i) = pure (Var meta i)
+desugar' (Let meta e (x ** t)) =
+  let f = \e, t => Let meta e (x ** t) in
+  [| f (desugar' e) (desugar' t) |]
+desugar' (LetTy meta a (x ** t)) =
+  let f = \t => LetTy meta a (x ** t) in
+  [| f (desugar' t) |]
+desugar' (Abs meta (bound ** t)) =
+  let f = \t => Abs meta (bound ** t) in
+  [| f (desugar' t) |]
+desugar' (App meta e ts) =
+  let f = \e, ts => App meta e ts in
+  [| f (desugar' e) (desugarAll ts) |]
+desugar' (Tup meta (MkRow ts fresh)) =
+  let f = \ts => Tup meta (fromAll ts fresh) in
+  [| f (desugarCtx ts) |]
+desugar' (Prj meta e l) =
+  let f = \e => Prj meta e l in
+  [| f (desugar' e) |]
+desugar' (Inj meta l t) =
+  let f = Inj meta l in
+  [| f (desugar' t) |]
+desugar' (Case meta e (MkRow ts fresh)) =
+  let f = \e, ts => Case meta e (fromAll ts fresh) in
+  [| f (desugar' e) (desugarBranches ts) |]
+desugar' (Roll meta t) =
+  let f = Roll meta in
+  [| f (desugar' t) |]
+desugar' (Unroll meta e) =
+  let f = Unroll meta in
+  [| f (desugar' e) |]
+desugar' (Fold meta e (x ** t)) =
+  let f = \e, t => Fold meta e (x ** t) in
+  [| f (desugar' e) (desugar' t) |]
+desugar' (Map meta (x ** a) b c) = pure $ Map meta (x ** a) b c
+desugar' (QuasiQuote meta t) = quote t
+desugar' (QAbs meta (bound ** t)) = desugar' t
+desugar' (Lit meta k) = pure $ lit meta k
+desugar' (Suc meta t) =
+  let f = suc meta in
+  [| f (desugar' t) |]
+desugar' (List meta ts) =
+  let f = list meta in
+  [| f (desugarAll ts) |]
+desugar' (Cons meta t u) =
+  let f = cons meta in
+  [| f (desugar' t) (desugar' u) |]
+desugar' (Str meta str) = string meta str
+
+desugarAll [] = pure []
+desugarAll (t :: ts) = [| desugar' t :: desugarAll ts |]
+
+desugarCtx [<] = pure [<]
+desugarCtx (ts :< (l :- t)) =
+  let f = \ts, t => ts :< (l :- t) in
+  [| f (desugarCtx ts) (desugar' t) |]
+
+desugarBranches [<] = pure [<]
+desugarBranches (ts :< (l :- (x ** t))) =
+  let f = \ts, t => ts :< (l :- (x ** t)) in
+  [| f (desugarBranches ts) (desugar' t) |]
+
+quote (Annot meta t a) =
+  let f = \t, a => Roll meta $ Inj meta "Annot" $ Tup meta [<"Body" :- t, "Ty" :- a] in
+  [| f (quote t) (desugar' a) |]
+quote (Var meta i) = pure $ Roll meta $ Inj meta "Var" $ lit meta (elemToNat i.pos)
+quote (Let meta e (x ** t)) =
+  let
+    f = \e, t =>
+      Roll meta.value $ Inj meta.value "Let" $
+      Tup meta.value [<"Value" :- e, "Body" :- t]
+  in
+  [| f (quote e) (quote t) |]
+quote (Abs meta (bound ** t)) =
+  let
+    f = \t => Roll meta $ Inj meta "Abs" $
+    Tup meta [<"Bound" :- lit meta (length bound), "Body" :- t]
+  in
+  [| f (quote t) |]
+quote (App meta e ts) =
+  let
+    f = \e, ts =>
+      Roll meta $ Inj meta "App" $
+      Tup meta [<"Fun" :- e, "Args" :- list meta ts]
+  in
+  [| f (quote e) (quoteAll ts) |]
+quote (Tup meta (MkRow ts _)) =
+  let f = Roll meta . Inj meta "Tup" . list meta in
+  [| f (quoteCtx ts) |]
+quote (Prj meta e l) =
+  let f = \e, l => Roll meta $ Inj meta "Prj" $ Tup meta [<"Target" :- e, "Label" :- l] in
+  [| f (quote e) (string meta l) |]
+quote (Inj meta l t) =
+  let f = \t, l => Roll meta $ Inj meta "Inj" $ Tup meta [<"Value" :- t, "Label" :- l] in
+  [| f (quote t) (string meta l) |]
+quote (Case meta e (MkRow ts _)) =
+  let
+    f = \e, ts =>
+      Roll meta $ Inj meta "Case" $
+      Tup meta [<"Target" :- e, "Branches" :- list meta ts]
+  in
+  [| f (quote e) (quoteBranches ts) |]
+quote (Roll meta t) =
+  let f = Roll meta . Inj meta "Roll" in
+  [| f (quote t) |]
+quote (Unroll meta e) =
+  let f = Roll meta . Inj meta "Unroll" in
+  [| f (quote e) |]
+quote (Fold meta e (x ** t)) =
+  let f = \e, t => Roll meta $ Inj meta "Fold" $ Tup meta [<"Target" :- e, "Body" :- t] in
+  [| f (quote e) (quote t) |]
+quote (Map meta a b c) =
+  let
+    f = \a, b, c =>
+      Roll meta $ Inj meta "Map" $
+      Tup meta [<"Functor" :- a, "Source" :- b, "Target" :- c]
+  in
+  [| f (desugar' a) (desugar' b) (desugar' c) |]
+quote (Unquote meta t) = desugar' t
+
+quoteAll [] = pure []
+quoteAll (t :: ts) = [| quote t :: quoteAll ts |]
+
+quoteCtx [<] = pure []
+quoteCtx (ts :< (l :- t)) =
+  let f = \ts, l, t => Tup meta [<"Label" :- l, "Value" :- t] :: ts in
+  [| f (quoteCtx ts) (string meta l) (quote t) |]
+
+quoteBranches [<] = pure []
+quoteBranches (ts :< (l :- (x ** t))) =
+  let f = \ts, l, t => Tup meta [<"Label" :- l, "Body" :- t] :: ts in
+  [| f (quoteBranches ts) (string meta l) (quote t) |]
 
 export
-maybeDesugar : (len : LengthOf tyCtx) => Term Sugar m tyCtx tmCtx -> Maybe (Term NoSugar m tyCtx tmCtx)
-maybeDesugarList :
-  (len : LengthOf tyCtx) =>
-  List (Term Sugar m tyCtx tmCtx) -> Maybe (List $ Term NoSugar m tyCtx tmCtx)
-maybeDesugarAll :
-  (len : LengthOf tyCtx) =>
-  (ts : Context (Term Sugar m tyCtx tmCtx)) ->
-  Maybe (All (Assoc0 $ Term NoSugar m tyCtx tmCtx) ts.names)
-maybeDesugarBranches :
-  (len : LengthOf tyCtx) =>
-  (ts : Context (x ** Term Sugar m tyCtx (tmCtx :< x))) ->
-  Maybe (All (Assoc0 $ (x ** Term NoSugar m tyCtx (tmCtx :< x))) ts.names)
-
-maybeDesugar (Annot meta t a) = do
-  t <- maybeDesugar t
-  pure (Annot meta t a)
-maybeDesugar (Var meta i) = pure (Var meta i)
-maybeDesugar (Let meta e (x ** t)) = do
-  e <- maybeDesugar e
-  t <- maybeDesugar t
-  pure (Let meta e (x ** t))
-maybeDesugar (LetTy meta a (x ** t)) = do
-  t <- maybeDesugar t
-  pure (LetTy meta a (x ** t))
-maybeDesugar (Abs meta (bound ** t)) = do
-  t <- maybeDesugar t
-  pure (Abs meta (bound ** t))
-maybeDesugar (App meta e ts) = do
-  e <- maybeDesugar e
-  ts <- maybeDesugarList ts
-  pure (App meta e ts)
-maybeDesugar (Tup meta (MkRow ts fresh)) = do
-  ts <- maybeDesugarAll ts
-  pure (Tup meta (fromAll ts fresh))
-maybeDesugar (Prj meta e l) = do
-  e <- maybeDesugar e
-  pure (Prj meta e l)
-maybeDesugar (Inj meta l t) = do
-  t <- maybeDesugar t
-  pure (Inj meta l t)
-maybeDesugar (Case meta e (MkRow ts fresh)) = do
-  e <- maybeDesugar e
-  ts <- maybeDesugarBranches ts
-  pure (Case meta e (fromAll ts fresh))
-maybeDesugar (Roll meta t) = do
-  t <- maybeDesugar t
-  pure (Roll meta t)
-maybeDesugar (Unroll meta e) = do
-  e <- maybeDesugar e
-  pure (Unroll meta e)
-maybeDesugar (Fold meta e (x ** t)) = do
-  e <- maybeDesugar e
-  t <- maybeDesugar t
-  pure (Fold meta e (x ** t))
-maybeDesugar (Map meta (x ** a) b c) =
-  case (%% x `strictlyPositiveIn` a) of
-    False `Because` contra => Nothing
-    True `Because` prf =>
-      pure $
-      Annot meta
-        (Abs meta
-          (["_fun", "_arg"] ** desugarMap a (%% x) prf (Var meta (%% "_fun")) (Var meta (%% "_arg"))))
-        (TArrow (TArrow b c) (TArrow
-          (sub (tabulate len (\i => _ :- TVar (toVar i)) :< (x :- b)) a)
-          (sub (tabulate len (\i => _ :- TVar (toVar i)) :< (x :- c)) a)))
-
-maybeDesugarList [] = pure []
-maybeDesugarList (t :: ts) = [| maybeDesugar t :: maybeDesugarList ts |]
-
-maybeDesugarAll [<] = pure [<]
-maybeDesugarAll (ts :< (l :- t)) = do
-  ts <- maybeDesugarAll ts
-  t <- maybeDesugar t
-  pure (ts :< (l :- t))
-
-maybeDesugarBranches [<] = pure [<]
-maybeDesugarBranches (ts :< (l :- (x ** t))) = do
-  ts <- maybeDesugarBranches ts
-  t <- maybeDesugar t
-  pure (ts :< (l :- (x ** t)))
+desugar : Term (Sugar qtCtx) m tyCtx tmCtx -> Term NoSugar m tyCtx tmCtx
+desugar t =
+  let
+    cache : Cache String
+    cache = MkCache {max = 0, vals = empty}
+  in
+  evalState cache (desugar' t)
diff --git a/src/Inky/Term/Parser.idr b/src/Inky/Term/Parser.idr
index 1f9d983..e977bc2 100644
--- a/src/Inky/Term/Parser.idr
+++ b/src/Inky/Term/Parser.idr
@@ -18,7 +18,6 @@ import Flap.Parser
 
 import Inky.Data.Row
 import Inky.Term
-import Inky.Term.Sugar
 import Inky.Type
 
 import Text.Lexer
@@ -29,6 +28,7 @@ export
 data InkyKind
   = TermIdent
   | TypeIdent
+  | StringLit
   | Lit
   | Let
   | In
@@ -52,8 +52,10 @@ data InkyKind
   | BraceClose
   | Arrow
   | DoubleArrow
+  | WaveArrow
   | Bang
   | Tilde
+  | Backtick
   | Dot
   | Backslash
   | Colon
@@ -64,9 +66,10 @@ data InkyKind
   | Comment
 
 export
-[EqI] Eq InkyKind where
+Eq InkyKind where
   TermIdent == TermIdent = True
   TypeIdent == TypeIdent = True
+  StringLit == StringLit = True
   Lit == Lit = True
   Let == Let = True
   In == In = True
@@ -90,8 +93,10 @@ export
   BraceClose == BraceClose = True
   Arrow == Arrow = True
   DoubleArrow == DoubleArrow = True
+  WaveArrow == WaveArrow = True
   Bang == Bang = True
   Tilde == Tilde = True
+  Backtick == Backtick = True
   Dot == Dot = True
   Backslash == Backslash = True
   Colon == Colon = True
@@ -106,6 +111,7 @@ export
 Interpolation InkyKind where
   interpolate TermIdent = "term name"
   interpolate TypeIdent = "type name"
+  interpolate StringLit = "string"
   interpolate Lit = "number"
   interpolate Let = "'let'"
   interpolate In = "'in'"
@@ -129,8 +135,10 @@ Interpolation InkyKind where
   interpolate BraceClose = "'}'"
   interpolate Arrow = "'->'"
   interpolate DoubleArrow = "'=>'"
+  interpolate WaveArrow = "'~>'"
   interpolate Bang = "'!'"
   interpolate Tilde = "'~'"
+  interpolate Backtick = "'`'"
   interpolate Dot = "'.'"
   interpolate Backslash = "'\\'"
   interpolate Colon = "':'"
@@ -143,12 +151,14 @@ Interpolation InkyKind where
 TokenKind InkyKind where
   TokType TermIdent = String
   TokType TypeIdent = String
+  TokType StringLit = String
   TokType Lit = Nat
   TokType Comment = String
   TokType _ = ()
 
   tokValue TermIdent = id
   tokValue TypeIdent = id
+  tokValue StringLit = \str => substr 1 (length str `minus` 2) str
   tokValue Lit = stringToNatOrZ
   tokValue Let = const ()
   tokValue In = const ()
@@ -172,8 +182,10 @@ TokenKind InkyKind where
   tokValue BraceClose = const ()
   tokValue Arrow = const ()
   tokValue DoubleArrow = const ()
+  tokValue WaveArrow = const ()
   tokValue Bang = const ()
   tokValue Tilde = const ()
+  tokValue Backtick = const ()
   tokValue Dot = const ()
   tokValue Backslash = const ()
   tokValue Colon = const ()
@@ -201,7 +213,7 @@ keywords =
 
 export
 relevant : InkyKind -> Bool
-relevant = (/=) @{EqI} Ignore
+relevant = (/=) Ignore
 
 public export
 InkyToken : Type
@@ -228,7 +240,8 @@ tokenMap =
       Just k => Tok k s
       Nothing => Tok TypeIdent s)] ++
   toTokenMap
-    [ (digits, Lit)
+    [ (quote (is '"') alpha, StringLit)
+    , (digits, Lit)
     , (exact "(", ParenOpen)
     , (exact ")", ParenClose)
     , (exact "[", BracketOpen)
@@ -239,8 +252,10 @@ tokenMap =
     , (exact "}", BraceClose)
     , (exact "->", Arrow)
     , (exact "=>", DoubleArrow)
+    , (exact "~>", WaveArrow)
     , (exact "!", Bang)
     , (exact "~", Tilde)
+    , (exact "`", Backtick)
     , (exact ".", Dot)
     , (exact "\\", Backslash)
     , (exact ":", Colon)
@@ -249,6 +264,43 @@ tokenMap =
     , (exact ",", Comma)
     ]
 
+-- Error Monad -----------------------------------------------------------------
+
+public export
+data Result : (a : Type) -> Type where
+  Ok : a -> Result a
+  Errs : (msgs : List1 (WithBounds String)) -> Result a
+
+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
+
+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 |]
+
 -- Parser ----------------------------------------------------------------------
 
 public export
@@ -260,35 +312,41 @@ InkyParser nil locked free a =
     a
 
 public export
-record ParseFun (0 n : Nat) (0 p : Fun (replicate n $ SnocList String) Type) where
+record ParseFun (as : SnocList Type) (0 p : Fun as Type) where
   constructor MkParseFun
-  try :
-    DFun (replicate n $ SnocList String)
-      (chain (lengthOfReplicate n $ SnocList String) (Either String) p)
+  try : DFun as (chain (lengthOf as) Parser.Result p)
 
-mkVar : ({ctx : _} -> Var ctx -> p ctx) -> WithBounds String -> ParseFun 1 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 => pure (f i)
-      Nothing => Left "\{x.bounds}: unbound name \"\{x.val}\"")
-
-mkVar2 :
-  ({tyCtx, tmCtx : _} -> WithBounds (Var tmCtx) -> p tyCtx tmCtx) ->
-  WithBounds String -> ParseFun 2 p
-mkVar2 f x =
+      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
-    (\tyCtx, tmCtx => case Var.lookup x.val tmCtx of
-      Just i => pure (f $ i <$ x)
-      Nothing => Left "\{x.bounds}: unbound name \"\{x.val}\"")
+    (\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 1 Ty
+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 2 (Term Sugar Bounds)
+TermFun = ParseFun [<Mode, SnocList String, SnocList String] (\mode => Term mode Bounds)
 
 public export
 TypeParser : SnocList String -> SnocList String -> Type
@@ -299,36 +357,41 @@ RowOf :
   (0 free : Context Type) ->
   InkyParser False [<] free a ->
   InkyParser True [<] free (List $ WithBounds $ Assoc a)
-RowOf free p = sepBy (match Comma) (WithBounds $ mkAssoc <$> Seq [match TypeIdent, match Colon, p])
+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
 
-tryRow :
-  List (WithBounds $ Assoc (ParseFun 1 p)) ->
-  (ctx : _) -> Either String (Row $ p ctx)
-tryRow xs ctx =
-  foldlM
-    (\row, xf => do
-      a <- xf.val.value.try ctx
-      let Just row' = extend row (xf.val.name :- a)
-        | Nothing => Left "\{xf.bounds}: duplicate name \"\{xf.val.name}\""
-      pure row')
-    [<]
-    xs
-
-tryRow2 :
-  List (WithBounds $ Assoc (ParseFun 2 p)) ->
-  (tyCtx, tmCtx : _) -> Either String (Row $ p tyCtx tmCtx)
-tryRow2 xs tyCtx tmCtx =
-  foldlM
-    (\row, xf => do
-      a <- xf.val.value.try tyCtx tmCtx
-      let Just row' = extend row (xf.val.name :- a)
-        | Nothing => Left "\{xf.bounds}: duplicate name \"\{xf.val.name}\""
-      pure row')
-    [<]
-    xs
+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 |])
+
+-- Types -----------------------------------------------------------------------
 
 OpenOrFixpointType : TypeParser [<] [<"openType"]
 OpenOrFixpointType =
@@ -339,13 +402,13 @@ OpenOrFixpointType =
     ]
   where
   mkFix : HList [(), String, (), TypeFun] -> TypeFun
-  mkFix [_, x, _, a] = MkParseFun (\ctx => pure $ TFix x !(a.try (ctx :< x)))
+  mkFix [_, x, _, a] = MkParseFun (\ctx => TFix x <$> a.try (ctx :< x))
 
 AtomType : TypeParser [<"openType"] [<]
 AtomType =
   OneOf
     [ mkVar TVar <$> WithBounds (match TypeIdent)
-    , MkParseFun (\_ => pure TNat) <$ match Nat
+    , MkParseFun (\_ => Ok TNat) <$ match Nat
     , mkProd <$> enclose (match AngleOpen) (match AngleClose) row
     , mkSum <$> enclose (match BracketOpen) (match BracketClose) row
     , enclose (match ParenOpen) (match ParenClose) OpenOrFixpointType
@@ -355,10 +418,10 @@ AtomType =
   row = RowOf [<"openType" :- TypeFun] $ Var (%%% "openType")
 
   mkProd : List (WithBounds $ Assoc TypeFun) -> TypeFun
-  mkProd xs = MkParseFun (\ctx => TProd <$> tryRow xs ctx)
+  mkProd xs = MkParseFun (\ctx => TProd <$> (parseRow xs).try ctx)
 
   mkSum : List (WithBounds $ Assoc TypeFun) -> TypeFun
-  mkSum xs = MkParseFun (\ctx => TSum <$> tryRow xs ctx)
+  mkSum xs = MkParseFun (\ctx => TSum <$> (parseRow xs).try ctx)
 
 AppType : TypeParser [<"openType"] [<]
 AppType =
@@ -380,54 +443,116 @@ OpenType =
     foldr1 {a = TypeFun}
       (\x, y => MkParseFun (\ctx => [| TArrow (x.try ctx) (y.try ctx) |]))
 
+export
+[ListSet] Eq a => Set a (List a) where
+  singleton x = [x]
+
+  member x xs = elem x xs
+
+  intersect xs = filter (\x => elem x xs)
+
+  toList = id
+
 %hint
 export
-OpenTypeWf : So (wellTyped EqI [<] [<] [<] [<] OpenType)
-OpenTypeWf = Oh
+OpenTypeWf : collectTypeErrs @{ListSet} [<] [<] [<] [<] OpenType = []
+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
 AtomTerm =
   OneOf
-    [ mkVar2 (\x => Var x.bounds x.val) <$> WithBounds (match TermIdent)
+    [ mkVar3 (\x => Var x.bounds x.val) <$> WithBounds (match TermIdent)
+    , mkStrLit <$> WithBounds (match StringLit)
     , mkLit <$> WithBounds (match Lit)
     , mkList <$> WithBounds (
         enclose (match BracketOpen) (match BracketClose) $
-        sepBy (match Comma) $
+        sepBy (match Semicolon) $
         Var (%%% "openTerm"))
     , mkTup <$> WithBounds (enclose (match AngleOpen) (match AngleClose) $
         RowOf [<"openTerm" :- TermFun] (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 (\tyCtx, tmCtx => pure (Lit k.bounds k.val))
+  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 (\tyCtx, tmCtx =>
-      foldr
-        (\x, ys => pure $ Cons xs.bounds !(x.try tyCtx tmCtx) !ys)
-        (pure $ Nil xs.bounds)
-        xs.val)
+  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 (\tyCtx, tmCtx => Tup xs.bounds <$> tryRow2 xs.val tyCtx tmCtx)
+  mkTup xs =
+    MkParseFun (\mode, tyCtx, tmCtx =>
+      Tup xs.bounds <$> (parseRow3 xs.val).try mode tyCtx tmCtx)
 
 PrefixTerm : InkyParser False [<"openTerm" :- TermFun] [<] TermFun
 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"))
     , rename (Drop Id) Id AtomTerm
     ]
   where
   mkRoll : WithBounds TermFun -> TermFun
-  mkRoll x = MkParseFun (\tyCtx, tmCtx => pure $ Roll x.bounds !(x.val.try tyCtx tmCtx))
+  mkRoll x = MkParseFun (\mode, tyCtx, tmCtx => Roll x.bounds <$> x.val.try mode tyCtx tmCtx)
 
   mkUnroll : WithBounds TermFun -> TermFun
-  mkUnroll x = MkParseFun (\tyCtx, tmCtx => pure $ Unroll x.bounds !(x.val.try tyCtx tmCtx))
+  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)) ]
@@ -435,8 +560,59 @@ SuffixTerm = mkSuffix <$> Seq [ PrefixTerm , star (match Dot **> WithBounds (mat
   mkSuffix : HList [TermFun, List (WithBounds String)] -> TermFun
   mkSuffix [t, []] = t
   mkSuffix [t, prjs] =
-    MkParseFun (\tyCtx, tmCtx =>
-      pure $ foldl (\acc, l => Prj l.bounds acc l.val) !(t.try tyCtx tmCtx) 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
+SuffixTy' =
+  OneOf
+    [ mkTy <$> WithBounds (sub [<"openType" :- rename Id (Drop Id) OpenType] [<] AtomType)
+    , 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))
+
+SuffixBoundTy' : InkyParser False [<"openTerm" :- TermFun] [<] BoundType'Fun
+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)
+    ]
+  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
 AppTerm =
@@ -459,14 +635,9 @@ AppTerm =
         [ WithBounds SuffixTerm
         , mkMap <$> Seq
           [ WithBounds (match Map)
-          , enclose (match ParenOpen) (match ParenClose) $ Seq
-            [ match Backslash
-            , match TypeIdent
-            , match DoubleArrow
-            , rename Id (Drop Id) OpenType
-            ]
-          , sub [<"openType" :- rename Id (Drop Id) OpenType] [<] AtomType
-          , sub [<"openType" :- rename Id (Drop Id) OpenType] [<] AtomType
+          , weaken (S Z) SuffixBoundTy'
+          , weaken (S Z) SuffixTy'
+          , weaken (S Z) SuffixTy'
           ]
         ]
       , star (weaken (S Z) SuffixTerm)
@@ -474,44 +645,82 @@ AppTerm =
     ]
   where
   mkInj : HList [WithBounds String, TermFun] -> TermFun
-  mkInj [tag, t] = MkParseFun (\tyCtx, tmCtx => Inj tag.bounds tag.val <$> t.try tyCtx tmCtx)
+  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 (\tyCtx, tmCtx => Suc x.bounds <$> t.try tyCtx tmCtx)
+  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 (\tyCtx, tmCtx =>
-      pure $ Cons x.bounds !(t.try tyCtx tmCtx) !(u.try tyCtx tmCtx))
-
-  mkMap : HList [WithBounds (), HList [_, String, _, TypeFun], TypeFun, TypeFun] -> WithBounds TermFun
-  mkMap [m, [_, x, _, a], b, c] =
-    MkParseFun (\tyCtx, tmCtx =>
-      pure $ Map m.bounds (x ** !(a.try (tyCtx :< x))) !(b.try tyCtx) !(c.try tyCtx))
+    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, (arg :: args)] =
-    MkParseFun (\tyCtx, tmCtx =>
-      pure $
-      App
-        fun.bounds
-        !(fun.val.try tyCtx tmCtx)
-        (  !(arg.try tyCtx tmCtx)
-        :: (!(foldlM (\acc, arg => pure $ acc :< !(arg.try tyCtx tmCtx)) [<] args) <>> [])))
+  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' =
+  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 (rename Id (Drop Id) OpenType))
+    , option (match Colon **> WithBounds (weaken (S Z) OpenTy'))
     ]
   where
-  mkAnnot : HList [TermFun, Maybe (WithBounds TypeFun)] -> TermFun
+  mkAnnot : HList [TermFun, Maybe (WithBounds Type'Fun)] -> TermFun
   mkAnnot [t, Nothing] = t
-  mkAnnot [t, Just a] = MkParseFun (\tyCtx, tmCtx =>
-    pure $ Annot a.bounds !(t.try tyCtx tmCtx) !(a.val.try tyCtx))
+  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
 
@@ -524,9 +733,9 @@ LetTerm =
       , OneOf
         [ mkAnnot <$> Seq
           [ star (enclose (match ParenOpen) (match ParenClose) $
-            Seq [ match TermIdent, match Colon, rename Id (Drop Id) OpenType ])
+            Seq [ match TermIdent, match Colon, weaken (S Z) OpenTy' ])
           , WithBounds (match Colon)
-          , rename Id (Drop Id) OpenType
+          , weaken (S Z) OpenTy'
           , match Equal
           , star (match Comment)
           , Var (%%% "openTerm")]
@@ -547,38 +756,74 @@ LetTerm =
   where
   mkLet : HList [WithBounds String, WithDoc TermFun, (), TermFun] -> TermFun
   mkLet [x, AddDoc e doc, _, t] =
-    MkParseFun (\tyCtx, tmCtx =>
-      pure $
-      Let (AddDoc x.bounds doc) !(e.try tyCtx tmCtx) (x.val ** !(t.try tyCtx (tmCtx :< x.val))))
+    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 (\tyCtx, tmCtx =>
-      pure $
-      LetTy (AddDoc x.bounds doc) !(a.try tyCtx) (x.val ** !(t.try (tyCtx :< x.val) tmCtx)))
-
-  mkArrow : List TypeFun -> TypeFun -> TypeFun
-  mkArrow [] cod = cod
-  mkArrow (arg :: args) cod =
-    MkParseFun (\ctx => [| TArrow (arg.try ctx) ((mkArrow args cod).try ctx) |])
+    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)
+          |])
 
   mkAnnot :
-    HList [List (HList [String, (), TypeFun]), WithBounds (), TypeFun, (), List String, TermFun] ->
+    HList [List (HList [String, (), Type'Fun]), WithBounds (), Type'Fun, (), List String, TermFun] ->
     WithDoc TermFun
   mkAnnot [[], m, cod, _, doc, t] =
     AddDoc
-      (MkParseFun (\tyCtx, tmCtx =>
-        pure $ Annot m.bounds !(t.try tyCtx tmCtx) !(cod.try tyCtx)))
+      (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 (\tyCtx, tmCtx =>
-        pure $
-        Annot m.bounds
-          (Abs m.bounds (bound ** !(t.try tyCtx (tmCtx <>< bound))))
-          !((mkArrow tys cod).try tyCtx)))
+      (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
 
   mkUnannot : HList [(), List String, TermFun] -> WithDoc TermFun
@@ -589,14 +834,25 @@ AbsTerm =
   mkAbs <$> Seq
     [ WithBounds (match Backslash)
     , sepBy1 (match Comma) (match TermIdent)
-    , match DoubleArrow
+    , (match DoubleArrow <||> match WaveArrow)
     , Var (%%% "openTerm")
     ]
   where
-  mkAbs : HList [WithBounds (), List1 String, (), TermFun] -> TermFun
-  mkAbs [m, args, _, body] =
-    MkParseFun (\tyCtx, tmCtx =>
-      pure $ Abs m.bounds (forget args ** !(body.try tyCtx (tmCtx <>< forget args))))
+  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
 CaseTerm =
@@ -630,25 +886,31 @@ CaseTerm =
 
   mkBranch :
     HList [String, String, (), TermFun] ->
-    Assoc (ParseFun 2 $ \tyCtx, tmCtx => (x ** Term Sugar Bounds tyCtx (tmCtx :< x)))
+    Assoc
+      (ParseFun [<Mode, SnocList String, SnocList String] $
+       \mode, tyCtx, tmCtx => (x ** Term mode Bounds tyCtx (tmCtx :< x)))
   mkBranch [tag, bound, _, branch] =
-    tag :- MkParseFun (\tyCtx, tmCtx => pure (bound ** !(branch.try tyCtx (tmCtx :< bound))))
+    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 (\tyCtx, tmCtx =>
-      pure $ Case m.bounds !(target.try tyCtx tmCtx) !(tryRow2 branches tyCtx tmCtx))
+    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 (\tyCtx, tmCtx =>
-      pure $
-      Fold
-        m.bounds
-        !(target.try tyCtx tmCtx)
-        ("__tmp" ** Case m.bounds (Var m.bounds $ %% "__tmp") !(tryRow2 branches tyCtx (tmCtx :< "__tmp"))))
+    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
 FoldTerm =
@@ -667,8 +929,11 @@ FoldTerm =
   where
   mkFold : HList [WithBounds (), TermFun, (), HList [(), String, (), TermFun]] -> TermFun
   mkFold [m, target, _, [_, arg, _, body]] =
-    MkParseFun (\tyCtx, tmCtx =>
-      pure $ Fold m.bounds !(target.try tyCtx tmCtx) (arg ** !(body.try tyCtx (tmCtx :< arg))))
+    MkParseFun (\mode, tyCtx, tmCtx =>
+      [| (\e, t => Fold m.bounds e (arg ** t))
+         (target.try mode tyCtx tmCtx)
+         (body.try mode tyCtx (tmCtx :< arg))
+      |])
 
 export
 OpenTerm : InkyParser False [<] [<] TermFun
@@ -683,5 +948,5 @@ OpenTerm =
 
 %hint
 export
-OpenTermWf : So (wellTyped EqI [<] [<] [<] [<] OpenTerm)
-OpenTermWf = Oh
+OpenTermWf : collectTypeErrs @{ListSet} [<] [<] [<] [<] OpenTerm = []
+OpenTermWf = Refl
diff --git a/src/Inky/Term/Pretty.idr b/src/Inky/Term/Pretty.idr
index 0523362..fbedab3 100644
--- a/src/Inky/Term/Pretty.idr
+++ b/src/Inky/Term/Pretty.idr
@@ -5,81 +5,34 @@ import Data.String
 
 import Inky.Term
 import Inky.Type.Pretty
-import Inky.Term.Sugar
 
 import Text.Bounded
 import Text.PrettyPrint.Prettyprinter
 
-public export
-data TermPrec = Atom | Prefix | Suffix | App | Annot | Open
-
-%name TermPrec d
-
-Eq TermPrec where
-  Atom == Atom = True
-  Prefix == Prefix = True
-  Suffix == Suffix = True
-  App == App = True
-  Annot == Annot = True
-  Open == Open = True
-  _ == _ = False
-
-Ord TermPrec where
-  compare Atom Atom = EQ
-  compare Atom d2 = LT
-  compare Prefix Atom = GT
-  compare Prefix Prefix = EQ
-  compare Prefix d2 = LT
-  compare Suffix Atom = GT
-  compare Suffix Prefix = GT
-  compare Suffix Suffix = EQ
-  compare Suffix d2 = LT
-  compare App App = EQ
-  compare App Annot = LT
-  compare App Open = LT
-  compare App d2 = GT
-  compare Annot Annot = EQ
-  compare Annot Open = LT
-  compare Annot d2 = GT
-  compare Open Open = EQ
-  compare Open d2 = GT
-
 export
-prettyTerm : {tyCtx, tmCtx : SnocList String} -> Term mode m tyCtx tmCtx -> TermPrec -> Doc ann
-prettyAllTerm : {tyCtx, tmCtx : SnocList String} -> List (Term mode m tyCtx tmCtx) -> TermPrec -> List (Doc ann)
-prettyTermCtx : {tyCtx, tmCtx : SnocList String} -> Context (Term mode m tyCtx tmCtx) -> SnocList (Doc ann)
-prettyCases : {tyCtx, tmCtx : SnocList String} -> Context (x ** Term mode m tyCtx (tmCtx :< x)) -> SnocList (Doc ann)
+prettyTerm :
+  {mode : Mode} -> {tyCtx, tmCtx : SnocList String} ->
+  Term mode m tyCtx tmCtx -> InkyPrec -> Doc ann
+prettyAllTerm :
+  {mode : Mode} -> {tyCtx, tmCtx : SnocList String} ->
+  List (Term mode m tyCtx tmCtx) -> InkyPrec -> List (Doc ann)
+prettyTermCtx :
+  {mode : Mode} -> {tyCtx, tmCtx : SnocList String} ->
+  Context (Term mode m tyCtx tmCtx) -> SnocList (Doc ann)
+prettyCases :
+  {mode : Mode} -> {tyCtx, tmCtx : SnocList String} ->
+  Context (x ** Term mode m tyCtx (tmCtx :< x)) -> SnocList (Doc ann)
 prettyLet :
   (eqLine : Doc ann) ->
   (doc : List String) ->
   (bound, body : Doc ann) ->
   Doc ann
-lessPrettyTerm : {tyCtx, tmCtx : SnocList String} -> Term mode m tyCtx tmCtx -> TermPrec -> Doc ann
-
-prettyTerm t d =
-  case isLit t of
-    Just k => pretty k
-    Nothing =>
-      case isSuc t of
-        Just u =>
-          group $ align $ hang 2 $ parenthesise (d < App) $
-            concatWith (surround line) [pretty "suc", prettyTerm (assert_smaller t u) Suffix]
-        Nothing => case isList t of
-          Just ts =>
-            let ts = prettyAllTerm (assert_smaller t ts) Open in
-            group $ align $ flatAlt
-              (enclose ("[" <++> neutral) (line <+> "]") $
-                concatWith (surround $ line <+> "," <++> neutral) ts)
-              (enclose "[" "]" $ concatWith (surround $ "," <++> neutral) ts)
-          Nothing => case isCons t of
-            Just (hd, tl) =>
-              group $ align $ hang 2 $ parenthesise (d < App) $
-                concatWith (surround line)
-                  [ pretty "cons"
-                  , prettyTerm (assert_smaller t hd) Suffix
-                  , prettyTerm (assert_smaller t tl) Suffix
-                  ]
-            Nothing => lessPrettyTerm t d
+prettyType' :
+  (mode : Mode) -> {tyCtx, tmCtx : SnocList String} ->
+  Ty' mode m tyCtx tmCtx -> InkyPrec -> Doc ann
+prettyBoundType' :
+  (mode : Mode) -> {tyCtx, tmCtx : SnocList String} ->
+  BoundTy' mode m tyCtx tmCtx -> InkyPrec -> Doc ann
 
 prettyAllTerm [] d = []
 prettyAllTerm (t :: ts) d = prettyTerm t d :: prettyAllTerm ts d
@@ -91,6 +44,12 @@ prettyTermCtx (ts :< (l :- Abs _ (bound ** t))) =
    pretty l <+> ":" <++>
      "\\" <+> concatWith (surround $ "," <++> neutral) (map pretty bound) <++> "=>" <+> line <+>
    prettyTerm t Open)
+prettyTermCtx (ts :< (l :- QAbs _ (bound ** t))) =
+ prettyTermCtx ts :<
+ (group $ align $
+   pretty l <+> ":" <++>
+     "\\" <+> concatWith (surround $ "," <++> neutral) (map pretty bound) <++> "~>" <+> line <+>
+   prettyTerm t Open)
 prettyTermCtx (ts :< (l :- t)) =
   prettyTermCtx ts :<
   (group $ align $ pretty l <+> ":" <+> line <+> prettyTerm t Open)
@@ -109,30 +68,42 @@ prettyCases (ts :< (l :- (x ** t))) =
     prettyTerm t Open)
 
 prettyLet eqLine [] bound body =
-  group $
-  (group $
-    hang 2
-      (group (pretty "let" <++> eqLine) <+> line <+>
-       group bound) <+> line <+>
-    "in") <+> line <+>
-  group body
+  group $ align $
+    (group $
+      hang 2
+        (group (pretty "let" <++> eqLine) <+> line <+>
+         group bound) <+> line <+>
+      "in") <+> line <+>
+    group body
 prettyLet eqLine doc bound body  =
-  (hang 2 $
-    group (pretty "let" <++> eqLine) <+> hardline <+>
-    concatMap (enclose "--" hardline . pretty) doc <+>
-    group bound) <+> hardline <+>
-  "in" <+> line <+>
-  group body
+  align $
+    (hang 2 $
+      group (pretty "let" <++> eqLine) <+> hardline <+>
+      concatMap (enclose "--" hardline . pretty) doc <+>
+      group bound) <+> hardline <+>
+    "in" <+> line <+>
+    group body
 
-lessPrettyTerm (Annot _ t a) d =
+prettyType' (Quote tyCtx tmCtx) a d = parenthesise (d < Prefix) $ align $ "," <+> prettyTerm a Prefix
+prettyType' (Sugar qtCtx) a d = prettyType a d
+prettyType' NoSugar a d = prettyType a d
+
+prettyBoundType' (Quote tyCtx tmCtx) a d = parenthesise (d < Prefix) $ align $ "," <+> prettyTerm a Prefix
+prettyBoundType' (Sugar qtCtx) (x ** a) d =
+  parens $ group $ align $ hang 2 $ "\\" <+> pretty x <++> "=>" <+> line <+> prettyType a Open
+prettyBoundType' NoSugar (x ** a) d =
+  parens $ group $ align $ hang 2 $ "\\" <+> pretty x <++> "=>" <+> line <+> prettyType a Open
+
+prettyTerm (Annot _ t a) d =
   group $ align $ parenthesise (d < Annot) $
     prettyTerm t App <+> line <+>
-    ":" <++> prettyType a Open
-lessPrettyTerm (Var _ i) d = pretty (unVal $ nameOf i)
-lessPrettyTerm (Let meta (Annot _ (Abs _ (bound ** e)) a) (x ** t)) d =
+    ":" <++> prettyType' mode a Open
+prettyTerm (Var _ i) d = pretty (unVal $ nameOf i)
+prettyTerm {mode = Sugar _} (Let meta (Annot _ (Abs _ (bound ** e)) a) (x ** t)) d =
   let (binds, cod, rest) = groupBinds bound a in
   let binds = map (\x => parens (pretty x.name <++> ":" <++> prettyType x.value Open)) binds in
-  group $ align $ parenthesise (d < Open) $
+  -- NOTE: group breaks comments
+  align $ parenthesise (d < Open) $
   prettyLet
    (group $ hang 2 $ flatAlt
         ( pretty x <+> line <+>
@@ -155,85 +126,108 @@ lessPrettyTerm (Let meta (Annot _ (Abs _ (bound ** e)) a) (x ** t)) d =
     let (binds, cod, rest) = groupBinds xs b in
     ((x :- a) :: binds, cod, rest)
   groupBinds xs a = ([], a, xs)
-lessPrettyTerm (Let meta (Annot _ e a) (x ** t)) d =
-  group $ align $ parenthesise (d < Open) $
+prettyTerm (Let meta (Annot _ e a) (x ** t)) d =
+  -- NOTE: group breaks comments
+  align $ parenthesise (d < Open) $
   prettyLet
-    (pretty x <+> line <+> ":" <++> prettyType a Open <++> "=")
+    (pretty x <+> line <+> ":" <++> prettyType' mode a Open <++> "=")
     meta.doc
     (prettyTerm e Open)
     (prettyTerm t Open)
-lessPrettyTerm (Let meta e (x ** t)) d =
-  group $ align $ parenthesise (d < Open) $
+prettyTerm (Let meta e (x ** t)) d =
+  -- NOTE: group breaks comments
+  align $ parenthesise (d < Open) $
   prettyLet
     (pretty x <++> "=")
     meta.doc
     (prettyTerm e Open)
     (prettyTerm t Open)
-lessPrettyTerm (LetTy meta a (x ** t)) d =
-  group $ align $ parenthesise (d < Open) $
+prettyTerm (LetTy meta a (x ** t)) d =
+  -- NOTE: group breaks comments
+  align $ parenthesise (d < Open) $
   prettyLet
     (pretty x <++> "=")
     meta.doc
     (prettyType a Open)
     (prettyTerm t Open)
-lessPrettyTerm (Abs _ (bound ** t)) d =
+prettyTerm (Abs _ (bound ** t)) d =
   group $ hang 2 $ parenthesise (d < Open) $
     "\\" <+> concatWith (surround $ "," <++> neutral) (map pretty bound) <++> "=>" <+> line <+>
     prettyTerm t Open
-lessPrettyTerm (App _ (Map _ (x ** a) b c) ts) d =
+prettyTerm (App _ (Map _ a b c) ts) d =
   group $ align $ hang 2 $ parenthesise (d < App) $
     concatWith (surround line)
       (  pretty "map"
-      :: parens (group $ align $ hang 2 $ "\\" <+> pretty x <++> "=>" <+> line <+> prettyType a Open)
-      :: prettyType b Atom
-      :: prettyType c Atom
+      :: prettyBoundType' mode a Suffix
+      :: prettyType' mode b Suffix
+      :: prettyType' mode c Suffix
       :: prettyAllTerm ts Suffix)
-lessPrettyTerm (App _ f ts) d =
+prettyTerm (App _ f ts) d =
   group $ align $ hang 2 $ parenthesise (d < App) $
-    concatWith (surround line) (prettyTerm f Suffix :: prettyAllTerm ts Suffix)
-lessPrettyTerm (Tup _ (MkRow ts _)) d =
+    concatWith (surround line) (prettyTerm f App :: prettyAllTerm ts Suffix)
+prettyTerm (Tup _ (MkRow ts _)) d =
   let parts = prettyTermCtx ts <>> [] in
   group $ align $ enclose "<" ">" $
     flatAlt
-      (neutral <++> concatWith (surround $ line' <+> "," <++> neutral) parts <+> line)
-      (concatWith (surround $ "," <++> neutral) parts)
-lessPrettyTerm (Prj _ e l) d =
+      (neutral <++> concatWith (surround $ line' <+> ";" <++> neutral) parts <+> line)
+      (concatWith (surround $ ";" <++> neutral) parts)
+prettyTerm (Prj _ e l) d =
   group $ align $ hang 2 $ parenthesise (d < Suffix) $
     prettyTerm e Suffix <+> line' <+> "." <+> pretty l
-lessPrettyTerm (Inj _ l t) d =
+prettyTerm (Inj _ l t) d =
   group $ align $ hang 2 $ parenthesise (d < App) $
     pretty l <+> line <+> prettyTerm t Suffix
-lessPrettyTerm (Case _ e (MkRow ts _)) d =
+prettyTerm (Case _ e (MkRow ts _)) d =
   let parts = prettyCases ts <>> [] in
   group $ align $ hang 2 $ parenthesise (d < Open) $
     (group $ "case" <++> prettyTerm e Open <++> "of") <+> line <+>
     (braces $ flatAlt
       (neutral <++> concatWith (surround $ line' <+> ";" <++> neutral) parts <+> line)
       (concatWith (surround $ ";" <++> neutral) parts))
-lessPrettyTerm (Roll _ t) d =
-  pretty "~" <+>
-  parenthesise (d < Prefix) (group $ align $ hang 2 $ prettyTerm t Prefix)
-lessPrettyTerm (Unroll _ e) d =
-  pretty "!" <+>
-  parenthesise (d < Prefix) (group $ align $ hang 2 $ prettyTerm e Prefix)
-lessPrettyTerm (Fold _ e ("__tmp" ** Case _ (Var _ ((%%) "__tmp" {pos = Here})) (MkRow ts _))) d =
+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 $ hang (-2) $ "foldcase" <++> prettyTerm e Open <+> line <+> "by") <+> line <+>
+    (group $ "foldcase" <++> prettyTerm e Open <++> "by") <+> line <+>
     (braces $ flatAlt
       (neutral <++> concatWith (surround $ line' <+> ";" <++> neutral) parts <+> line)
       (concatWith (surround $ ";" <++> neutral) parts))
-lessPrettyTerm (Fold _ e (x ** t)) d =
+prettyTerm (Fold _ e (x ** t)) d =
   group $ align $ hang 2 $ parenthesise (d < Open) $
     (group $ hang (-2) $ "fold" <++> prettyTerm e Open <++> "by") <+> line <+>
     (group $ align $ hang 2 $ parens $
       "\\" <+> pretty x <++> "=>" <+> line <+> prettyTerm t Open)
-lessPrettyTerm (Map _ (x ** a) b c) d =
+prettyTerm (Map _ a b c) d =
   group $ align $ hang 2 $ parenthesise (d < App) $
     concatWith (surround line)
       [ pretty "map"
-      , group (align $ hang 2 $ parens $  "\\" <+> pretty x <++> "=>" <+> line <+> prettyType a Open)
-      , prettyType b Atom
-      , prettyType c Atom
+      , prettyBoundType' mode a Suffix
+      , prettyType' mode  b Suffix
+      , prettyType' mode  c Suffix
       ]
+prettyTerm (QuasiQuote _ t) d =
+  parenthesise (d < Prefix) $ align $ pretty "`" <+> prettyTerm t Prefix
+prettyTerm (Unquote _ t) d =
+  parenthesise (d < Prefix) $ align $ pretty "," <+> prettyTerm t Prefix
+prettyTerm (QAbs _ (bound ** t)) d =
+  group $ hang 2 $ parenthesise (d < Open) $
+    "\\" <+> concatWith (surround $ "," <++> neutral) (map pretty bound) <++> "~>" <+> line <+>
+    prettyTerm t Open
+prettyTerm (Lit _ k) d = pretty k
+prettyTerm (Suc _ t) d =
+  group $ align $ hang 2 $ parenthesise (d < App) $
+    concatWith (surround line) [pretty "suc", prettyTerm t Suffix]
+prettyTerm (List _ ts) d =
+  let parts = prettyAllTerm ts Open in
+  group $ align $ enclose "[" "]" $
+    flatAlt
+      (neutral <++> concatWith (surround $ line' <+> ";" <++> neutral) parts <+> line)
+      (concatWith (surround $ ";" <++> neutral) parts)
+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
diff --git a/src/Inky/Term/Pretty/Error.idr b/src/Inky/Term/Pretty/Error.idr
index d87178f..ee0f28a 100644
--- a/src/Inky/Term/Pretty/Error.idr
+++ b/src/Inky/Term/Pretty/Error.idr
@@ -25,7 +25,7 @@ Pretty (ChecksOnly t) where
 export
 prettyNotSynths :
   {tyCtx, tmCtx : SnocList String} ->
-  {e : Term mode m tyCtx tmCtx} ->
+  {e : Term NoSugar m tyCtx tmCtx} ->
   {tyEnv : _} -> {tmEnv : _} ->
   NotSynths tyEnv tmEnv e ->
   List (m, Doc ann)
@@ -33,33 +33,33 @@ export
 prettyNotChecks :
   {tyCtx, tmCtx : SnocList String} ->
   {a : Ty [<]} ->
-  {t : Term mode m tyCtx tmCtx} ->
+  {t : Term NoSugar m tyCtx tmCtx} ->
   {tyEnv : _} -> {tmEnv : _} ->
   NotChecks tyEnv tmEnv a t ->
   List (m, Doc ann)
 prettyNotCheckSpine :
   {tyCtx, tmCtx : SnocList String} ->
   {a : Ty [<]} ->
-  {ts : List (Term mode m tyCtx tmCtx)} ->
+  {ts : List (Term NoSugar m tyCtx tmCtx)} ->
   {tyEnv : _} -> {tmEnv : _} ->
   NotCheckSpine tyEnv tmEnv a ts ->
   List (m, Doc ann)
 prettyAnyNotSynths :
   {tyCtx, tmCtx : SnocList String} ->
-  {es : Context (Term mode m tyCtx tmCtx)} ->
+  {es : Context (Term NoSugar m tyCtx tmCtx)} ->
   {tyEnv : _} -> {tmEnv : _} ->
   AnyNotSynths tyEnv tmEnv es ->
   List (m, Doc ann)
 prettyAnyNotChecks :
   {tyCtx, tmCtx : SnocList String} ->
-  {ts : Context (Term mode m tyCtx tmCtx)} ->
+  {ts : Context (Term NoSugar m tyCtx tmCtx)} ->
   {tyEnv : _} -> {tmEnv : _} -> {as : Context _} ->
   (meta : m) ->
   AnyNotChecks tyEnv tmEnv as ts ->
   List (m, Doc ann)
 prettyAnyNotBranches :
   {tyCtx, tmCtx : SnocList String} ->
-  {ts : Context (x ** Term mode m tyCtx (tmCtx :< x))} ->
+  {ts : Context (x ** Term NoSugar m tyCtx (tmCtx :< x))} ->
   {tyEnv : _} -> {tmEnv : _} -> {as : Context _} -> {a : _} ->
   (meta : m) ->
   AnyNotBranches tyEnv tmEnv as a ts ->
diff --git a/src/Inky/Term/Recompute.idr b/src/Inky/Term/Recompute.idr
index dd0e809..71ba6b9 100644
--- a/src/Inky/Term/Recompute.idr
+++ b/src/Inky/Term/Recompute.idr
@@ -76,7 +76,7 @@ dropAllWellFormed (wfs :< wf) (There i) = dropAllWellFormed wfs i :< wf
 
 export
 synthsWf :
-  {e : Term mode m tyCtx tmCtx} ->
+  {e : Term NoSugar m tyCtx tmCtx} ->
   {tyEnv : All (Assoc0 $ Ty [<]) tyCtx} ->
   {tmEnv : All (Assoc0 $ Ty [<]) tmCtx} ->
   DAll WellFormed tyEnv -> DAll WellFormed tmEnv ->
@@ -85,7 +85,7 @@ checkSpineWf :
   CheckSpine tyEnv tmEnv a ts b ->
   WellFormed a -> WellFormed b
 allSynthsWf :
-  {es : Context (Term mode m tyCtx tmCtx)} ->
+  {es : Context (Term NoSugar m tyCtx tmCtx)} ->
   {tyEnv : All (Assoc0 $ Ty [<]) tyCtx} ->
   {tmEnv : All (Assoc0 $ Ty [<]) tmCtx} ->
   DAll WellFormed tyEnv -> DAll WellFormed tmEnv ->
diff --git a/src/Inky/Term/Substitution.idr b/src/Inky/Term/Substitution.idr
deleted file mode 100644
index c99f5e6..0000000
--- a/src/Inky/Term/Substitution.idr
+++ /dev/null
@@ -1,197 +0,0 @@
-module Inky.Term.Substitution
-
-import Data.List.Quantifiers
-import Flap.Data.List
-import Inky.Term
-
-public export
-thin : ctx1 `Thins` ctx2 -> Term mode m tyCtx ctx1 -> Term mode m tyCtx ctx2
-public export
-thinList : ctx1 `Thins` ctx2 -> List (Term mode m tyCtx ctx1) -> List (Term mode m tyCtx ctx2)
-public export
-thinAll : ctx1 `Thins` ctx2 -> Context (Term mode m tyCtx ctx1) -> Context (Term mode m tyCtx ctx2)
-public export
-thinAllNames :
-  (f : ctx1 `Thins` ctx2) -> (ts : Context (Term mode m tyCtx ctx1)) ->
-  (thinAll f ts).names = ts.names
-public export
-thinBranches :
-  ctx1 `Thins` ctx2 ->
-  Context (x ** Term mode m tyCtx (ctx1 :< x)) ->
-  Context (x ** Term mode m tyCtx (ctx2 :< x))
-public export
-thinBranchesNames :
-  (f : ctx1 `Thins` ctx2) -> (ts : Context (x ** Term mode m tyCtx (ctx1 :< x))) ->
-  (thinBranches f ts).names = ts.names
-
-thin f (Annot meta t a) = Annot meta (thin f t) a
-thin f (Var meta i) = Var meta (index f i)
-thin f (Let meta e (x ** t)) = Let meta (thin f e) (x ** thin (Keep f) t)
-thin f (LetTy meta a (x ** t)) = LetTy meta a (x ** thin f t)
-thin f (Abs meta (bound ** t)) = Abs meta (bound ** thin (f <>< lengthOf bound) t)
-thin f (App meta e ts) = App meta (thin f e) (thinList f ts)
-thin f (Tup meta (MkRow ts fresh)) =
-  Tup meta (MkRow (thinAll f ts) (rewrite thinAllNames f ts in fresh))
-thin f (Prj meta e l) = Prj meta (thin f e) l
-thin f (Inj meta l t) = Inj meta l (thin f t)
-thin f (Case meta t (MkRow ts fresh)) =
-  Case meta (thin f t) (MkRow (thinBranches f ts) (rewrite thinBranchesNames f ts in fresh))
-thin f (Roll meta t) = Roll meta (thin f t)
-thin f (Unroll meta e) = Unroll meta (thin f e)
-thin f (Fold meta e (x ** t)) = Fold meta (thin f e) (x ** thin (Keep f) t)
-thin f (Map meta (x ** a) b c) = Map meta (x ** a) b c
-
-thinList f [] = []
-thinList f (t :: ts) = thin f t :: thinList f ts
-
-thinAll f [<] = [<]
-thinAll f (ts :< (l :- t)) = thinAll f ts :< (l :- thin f t)
-
-thinAllNames f [<] = Refl
-thinAllNames f (ts :< (l :- t)) = cong (:< l) $ thinAllNames f ts
-
-thinBranches f [<] = [<]
-thinBranches f (ts :< (l :- (x ** t))) = thinBranches f ts :< (l :- (x ** thin (Keep f) t))
-
-thinBranchesNames f [<] = Refl
-thinBranchesNames f (ts :< (l :- (x ** t))) = cong (:< l) $ thinBranchesNames f ts
-
-public export
-thinTy : ctx1 `Thins` ctx2 -> Term mode m ctx1 tmCtx -> Term mode m ctx2 tmCtx
-public export
-thinTyList : ctx1 `Thins` ctx2 -> List (Term mode m ctx1 tmCtx) -> List (Term mode m ctx2 tmCtx)
-public export
-thinTyAll : ctx1 `Thins` ctx2 -> Context (Term mode m ctx1 tmCtx) -> Context (Term mode m ctx2 tmCtx)
-public export
-thinTyAllNames :
-  (f : ctx1 `Thins` ctx2) -> (ts : Context (Term mode m ctx1 tmCtx)) ->
-  (thinTyAll f ts).names = ts.names
-public export
-thinTyBranches :
-  ctx1 `Thins` ctx2 ->
-  Context (x ** Term mode m ctx1 (tmCtx :< x)) ->
-  Context (x ** Term mode m ctx2 (tmCtx :< x))
-public export
-thinTyBranchesNames :
-  (f : ctx1 `Thins` ctx2) -> (ts : Context (x ** Term mode m ctx1 (tmCtx :< x))) ->
-  (thinTyBranches f ts).names = ts.names
-
-thinTy f (Annot meta t a) = Annot meta (thinTy f t) (rename f a)
-thinTy f (Var meta i) = Var meta i
-thinTy f (Let meta e (x ** t)) = Let meta (thinTy f e) (x ** thinTy f t)
-thinTy f (LetTy meta a (x ** t)) = LetTy meta (rename f a) (x ** thinTy (Keep f) t)
-thinTy f (Abs meta (bound ** t)) = Abs meta (bound ** thinTy f t)
-thinTy f (App meta e ts) = App meta (thinTy f e) (thinTyList f ts)
-thinTy f (Tup meta (MkRow ts fresh)) =
-  Tup meta (MkRow (thinTyAll f ts) (rewrite thinTyAllNames f ts in fresh))
-thinTy f (Prj meta e l) = Prj meta (thinTy f e) l
-thinTy f (Inj meta l t) = Inj meta l (thinTy f t)
-thinTy f (Case meta t (MkRow ts fresh)) =
-  Case meta (thinTy f t) (MkRow (thinTyBranches f ts) (rewrite thinTyBranchesNames f ts in fresh))
-thinTy f (Roll meta t) = Roll meta (thinTy f t)
-thinTy f (Unroll meta e) = Unroll meta (thinTy f e)
-thinTy f (Fold meta e (x ** t)) = Fold meta (thinTy f e) (x ** thinTy f t)
-thinTy f (Map meta (x ** a) b c) = Map meta (x ** rename (Keep f) a) (rename f b) (rename f c)
-
-thinTyList f [] = []
-thinTyList f (t :: ts) = thinTy f t :: thinTyList f ts
-
-thinTyAll f [<] = [<]
-thinTyAll f (ts :< (l :- t)) = thinTyAll f ts :< (l :- thinTy f t)
-
-thinTyAllNames f [<] = Refl
-thinTyAllNames f (ts :< (l :- t)) = cong (:< l) $ thinTyAllNames f ts
-
-thinTyBranches f [<] = [<]
-thinTyBranches f (ts :< (l :- (x ** t))) = thinTyBranches f ts :< (l :- (x ** thinTy f t))
-
-thinTyBranchesNames f [<] = Refl
-thinTyBranchesNames f (ts :< (l :- (x ** t))) = cong (:< l) $ thinTyBranchesNames f ts
-
-public export
-Env : Mode -> Type -> SnocList String -> SnocList String -> SnocList String -> Type
-Env mode m tyCtx ctx1 ctx2 = All (Assoc0 $ Either (Var ctx2) (Term mode m tyCtx ctx2)) ctx1
-
-public export
-Env' : Mode -> Type -> SnocList String -> List String -> SnocList String -> Type
-Env' mode m tyCtx ctx1 ctx2 = All (Assoc0 $ Either (Var ctx2) (Term mode m tyCtx ctx2)) ctx1
-
-public export
-thinEnv :
-  ctx2 `Thins` ctx3 ->
-  Env mode m tyCtx ctx1 ctx2 ->
-  Env mode m tyCtx ctx1 ctx3
-thinEnv f = mapProperty (map $ bimap (index f) (thin $ f))
-
-public export
-lift :
-  Env mode m tyCtx ctx1 ctx2 ->
-  Env mode m tyCtx (ctx1 :< x) (ctx2 :< x)
-lift f = thinEnv (Drop Id) f :< (x :- Left (%% x))
-
-public export
-sub :
-  Env mode m tyCtx ctx1 ctx2 ->
-  Term mode m tyCtx ctx1 -> Term mode m tyCtx ctx2
-public export
-subList :
-  Env mode m tyCtx ctx1 ctx2 ->
-  List (Term mode m tyCtx ctx1) -> List (Term mode m tyCtx ctx2)
-public export
-subAll :
-  Env mode m tyCtx ctx1 ctx2 ->
-  Context (Term mode m tyCtx ctx1) -> Context (Term mode m tyCtx ctx2)
-public export
-subAllNames :
-  (f : Env mode m tyCtx ctx1 ctx2) ->
-  (ts : Context (Term mode m tyCtx ctx1)) -> (subAll f ts).names = ts.names
-public export
-subBranches :
-  Env mode m tyCtx ctx1 ctx2 ->
-  Context (x ** Term mode m tyCtx (ctx1 :< x)) ->
-  Context (x ** Term mode m tyCtx (ctx2 :< x))
-public export
-subBranchesNames :
-  (f : Env mode m tyCtx ctx1 ctx2) ->
-  (ts : Context (x ** Term mode m tyCtx (ctx1 :< x))) -> (subBranches f ts).names = ts.names
-
-public export
-keepBound :
-  forall ctx. {0 bound : List String} ->
-  LengthOf bound -> Env' mode m tyCtx bound (ctx <>< bound)
-keepBound Z = []
-keepBound (S len) = (_ :- Left (index (dropFish Id len) (toVar Here))) :: keepBound len
-
-sub f (Annot meta t a) = Annot meta (sub f t) a
-sub f (Var meta i) = either (Var meta) id (indexAll i.pos f).value
-sub f (Let meta e (x ** t)) = Let meta (sub f e) (x ** sub (lift f) t)
-sub f (LetTy meta a (x ** t)) = LetTy meta a (x ** sub (mapProperty (map $ map $ thinTy (Drop Id)) f) t)
-sub f (Abs meta (bound ** t)) =
-  let len = lengthOf bound in
-  Abs meta (bound ** sub (thinEnv (dropFish Id len) f <>< keepBound len) t)
-sub f (App meta e ts) = App meta (sub f e) (subList f ts)
-sub f (Tup meta (MkRow ts fresh)) =
-  Tup meta (MkRow (subAll f ts) (rewrite subAllNames f ts in fresh))
-sub f (Prj meta e l) = Prj meta (sub f e) l
-sub f (Inj meta l t) = Inj meta l (sub f t)
-sub f (Case meta t (MkRow ts fresh)) =
-  Case meta (sub f t) (MkRow (subBranches f ts) (rewrite subBranchesNames f ts in fresh))
-sub f (Roll meta t) = Roll meta (sub f t)
-sub f (Unroll meta e) = Unroll meta (sub f e)
-sub f (Fold meta e (x ** t)) = Fold meta (sub f e) (x ** sub (lift f) t)
-sub f (Map meta (x ** a) b c) = Map meta (x ** a) b c
-
-subList f [] = []
-subList f (t :: ts) = sub f t :: subList f ts
-
-subAll f [<] = [<]
-subAll f (ts :< (l :- t)) = subAll f ts :< (l :- sub f t)
-
-subAllNames f [<] = Refl
-subAllNames f (ts :< (l :- t)) = cong (:< l) $ subAllNames f ts
-
-subBranches f [<] = [<]
-subBranches f (ts :< (l :- (x ** t))) = subBranches f ts :< (l :- (x ** sub (lift f) t))
-
-subBranchesNames f [<] = Refl
-subBranchesNames f (ts :< (l :- (x ** t))) = cong (:< l) $ subBranchesNames f ts
diff --git a/src/Inky/Term/Sugar.idr b/src/Inky/Term/Sugar.idr
deleted file mode 100644
index 477df5e..0000000
--- a/src/Inky/Term/Sugar.idr
+++ /dev/null
@@ -1,73 +0,0 @@
-module Inky.Term.Sugar
-
-import Flap.Decidable
-import Inky.Term
-
--- Naturals --------------------------------------------------------------------
-
-export
-Zero : m -> Term mode m tyCtx tmCtx
-Zero meta = Roll meta (Inj meta "Z" $ Tup meta [<])
-
-export
-Suc : m -> Term mode m tyCtx tmCtx -> Term mode m tyCtx tmCtx
-Suc meta t = Roll meta (Inj meta "S" t)
-
-export
-isZero : Term mode m tyCtx tmCtx -> Bool
-isZero (Roll _ (Inj _ "Z" $ Tup _ $ MkRow [<] _)) = True
-isZero _ = False
-
-export
-isSuc : Term mode m tyCtx tmCtx -> Maybe (Term mode m tyCtx tmCtx)
-isSuc (Roll _ (Inj _ "S" t)) = Just t
-isSuc _ = Nothing
-
-export
-Lit : m -> Nat -> Term mode m tyCtx tmCtx
-Lit meta 0 = Roll meta (Inj meta "Z" $ Tup meta [<])
-Lit meta (S n) = Suc meta (Lit meta n)
-
-export
-isLit : Term mode m tyCtx tmCtx -> Maybe Nat
-isLit t =
-  if isZero t then Just 0
-  else do
-    u <- isSuc t
-    k <- isLit (assert_smaller t u)
-    pure (S k)
-
--- Lists -----------------------------------------------------------------------
-
-export
-Nil : m -> Term mode m tyCtx tmCtx
-Nil meta = Roll meta (Inj meta "N" $ Tup meta [<])
-
-export
-Cons : m -> Term mode m tyCtx tmCtx -> Term mode m tyCtx tmCtx -> Term mode m tyCtx tmCtx
-Cons meta t ts = Roll meta (Inj meta "C" $ Tup meta [<"H" :- t, "T" :- ts])
-
-export
-fromList : m -> List (Term mode m tyCtx tmCtx) -> Term mode m tyCtx tmCtx
-fromList meta [] = Nil meta
-fromList meta (t :: ts) = Cons meta t (fromList meta ts)
-
-export
-isNil : Term mode m tyCtx tmCtx -> Bool
-isNil (Roll _ (Inj _ "N" $ Tup _ $ MkRow [<] _)) = True
-isNil _ = False
-
-export
-isCons : Term mode m tyCtx tmCtx -> Maybe (Term mode m tyCtx tmCtx, Term mode m tyCtx tmCtx)
-isCons (Roll _ (Inj _ "C" $ Tup meta $ MkRow [<"H" :- t, "T" :- ts] _)) = Just (t, ts)
-isCons (Roll _ (Inj _ "C" $ Tup meta $ MkRow [<"T" :- ts, "H" :- t] _)) = Just (t, ts)
-isCons _ = Nothing
-
-export
-isList : Term mode m tyCtx tmCtx -> Maybe (List $ Term mode m tyCtx tmCtx)
-isList t =
-  if isNil t then Just []
-  else do
-    (hd, tl) <- isCons t
-    tl <- isList (assert_smaller t tl)
-    pure (hd :: tl)
diff --git a/src/Inky/Type/Pretty.idr b/src/Inky/Type/Pretty.idr
index 91b28ba..03b9964 100644
--- a/src/Inky/Type/Pretty.idr
+++ b/src/Inky/Type/Pretty.idr
@@ -6,31 +6,45 @@ import Inky.Type
 import Text.PrettyPrint.Prettyprinter
 
 public export
-data TyPrec = Atom | App | Open
+data InkyPrec = Atom | Prefix | Suffix | App | Annot | Open
 
-%name TyPrec d
+%name InkyPrec d
 
-Eq TyPrec where
+export
+Eq InkyPrec where
   Atom == Atom = True
+  Prefix == Prefix = True
+  Suffix == Suffix = True
   App == App = True
+  Annot == Annot = True
   Open == Open = True
   _ == _ = False
 
-Ord TyPrec where
+export
+Ord InkyPrec where
   compare Atom Atom = EQ
-  compare Atom App = LT
-  compare Atom Open = LT
-  compare App Atom = GT
+  compare Atom d2 = LT
+  compare Prefix Atom = GT
+  compare Prefix Prefix = EQ
+  compare Prefix d2 = LT
+  compare Suffix Atom = GT
+  compare Suffix Prefix = GT
+  compare Suffix Suffix = EQ
+  compare Suffix d2 = LT
   compare App App = EQ
+  compare App Annot = LT
   compare App Open = LT
-  compare Open Atom = GT
-  compare Open App = GT
+  compare App d2 = GT
+  compare Annot Annot = EQ
+  compare Annot Open = LT
+  compare Annot d2 = GT
   compare Open Open = EQ
+  compare Open d2 = GT
 
 export
-prettyType : {ctx : SnocList String} -> Ty ctx -> TyPrec -> Doc ann
-lessPrettyType : {ctx : SnocList String} -> Ty ctx -> TyPrec -> Doc ann
-lessPrettyTypeCtx : {ctx : SnocList String} -> Context (Ty ctx) -> TyPrec -> SnocList (Doc ann)
+prettyType : {ctx : SnocList String} -> Ty ctx -> InkyPrec -> Doc ann
+lessPrettyType : {ctx : SnocList String} -> Ty ctx -> InkyPrec -> Doc ann
+lessPrettyTypeCtx : {ctx : SnocList String} -> Context (Ty ctx) -> InkyPrec -> SnocList (Doc ann)
 
 prettyType a d =
   if does (alpha {ctx2 = [<]} a TNat)
@@ -55,14 +69,14 @@ lessPrettyType (TProd (MkRow as _)) d =
   let parts = lessPrettyTypeCtx as Open <>> [] in
   group $ align $ enclose "<" ">" $
     flatAlt
-      (neutral <++> concatWith (surround $ line <+> "," <++> neutral) parts <+> line)
-      (concatWith (surround $ "," <++> neutral) parts)
+      (neutral <++> concatWith (surround $ line <+> ";" <++> neutral) parts <+> line)
+      (concatWith (surround $ ";" <++> neutral) parts)
 lessPrettyType (TSum (MkRow as _)) d =
   let parts = lessPrettyTypeCtx as Open <>> [] in
   group $ align $ enclose "[" "]" $
     flatAlt
-      (neutral <++> concatWith (surround $ line <+> "," <++> neutral) parts <+> line)
-      (concatWith (surround $ "," <++> neutral) parts)
+      (neutral <++> concatWith (surround $ line <+> ";" <++> neutral) parts <+> line)
+      (concatWith (surround $ ";" <++> neutral) parts)
 lessPrettyType (TFix x a) d =
   group $ align $ hang 2 $ parens $
     "\\" <+> pretty x <++> "=>" <+> line <+>