Do a lot.

- Add type aliases.
- Make `suc` a symbol.
- Fix incorrect specification for `IsFunction`.
- Write parser for terms.
- Use `collie` to improve command line experience.

10 files changed, 1005 insertions, 432 deletions

diff --git a/inky.ipkg b/inky.ipkg
index 2301466..8a86c56 100644
--- a/inky.ipkg
+++ b/inky.ipkg
@@ -4,7 +4,7 @@ sourcedir = "src"
 
 options = "--total"
 
-depends = contrib
+depends = collie, contrib
 
 executable = inky
 main = Inky
diff --git a/src/Inky.idr b/src/Inky.idr
index 5c7a821..bd3975f 100644
--- a/src/Inky.idr
+++ b/src/Inky.idr
@@ -1,13 +1,18 @@
 module Inky
 
+import Collie
 import Control.App
 import Control.App.Console
 import Control.App.FileIO
 import Inky.Context
 import Inky.Parser
+import Inky.Term
 import Inky.Term.Parser
+import Inky.Term.Pretty
+import Inky.Thinning
 import Inky.Type
 import Inky.Type.Pretty
+import System.File.Mode
 import System.File.ReadWrite
 import System.File.Virtual
 import Text.Lexer
@@ -16,6 +21,10 @@ import Text.PrettyPrint.Prettyprinter.Render.Terminal
 
 %default partial
 
+%hide Collie.Modifiers.infix.(::=)
+
+-- Actions ---------------------------------------------------------------------
+
 lexInkyString : HasErr String es => String -> App es (List (WithBounds InkyToken))
 lexInkyString file = do
   let (tokens, _, _, "") = lex tokenMap file
@@ -31,37 +40,171 @@ parseType toks = do
     | Left msg => throw msg
   pure a
 
+parseTerm : HasErr String es => List (WithBounds InkyToken) -> App es (CheckTerm [<] [<])
+parseTerm toks = do
+  let Ok res [] _ = parse @{EqI} OpenCheck 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
+
 checkType : HasErr String es => Ty [<] () -> App es ()
 checkType a = do
   let False = illFormed a
     | True => throw "type ill-formed"
   pure ()
 
+checkTerm : HasErr String es => Ty [<] () -> CheckTerm [<] [<] -> App es ()
+checkTerm a t = do
+  let True = checks [<] [<] a t
+    | False => throw "term ill-typed"
+  pure ()
+
 printType :
   PrimIO es => {default defaultLayoutOptions opts : LayoutOptions} ->
   Ty [<] () -> App es ()
 printType a = do
   primIO $ renderIO $ layoutSmart opts $ prettyType a Open
 
-ppType : FileIO es => PrimIO es => HasErr String es => App es ()
-ppType = do
-  file <- fGetStr stdin
-  toks <- lexInkyString file
-  a <- parseType toks
-  checkType a
-  printType a
+printTerm :
+  PrimIO es => {default defaultLayoutOptions opts : LayoutOptions} ->
+  CheckTerm [<] [<] -> App es ()
+printTerm a = do
+  primIO $ renderIO $ layoutSmart opts $ prettyCheck a Open
 
-main : IO ()
-main =
-  run $
-  handle {err = IOError}
-    (handle {err = String} ppType
-      (const $ pure ())
-      printErrLn)
-    (const $ pure ())
-    (printErrLn . show)
+readFile : FileIO es => File -> App es String
+readFile f = do
+  content <- read [<] f
+  pure (fastConcat $ content <>> [])
   where
-  printErrLn : PrimIO es => String -> App es ()
-  printErrLn msg = do
-    primIO $ () <$ fPutStrLn stderr msg
-    pure ()
+  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 -------------------------------------------------------------------
+
+Inky : Command "inky"
+Inky = MkCommand
+  { description = """
+    tool suite for Primrose programs
+    """
+  , subcommands =
+    [ "--help" ::= basic "print this help text" none
+    , "format" ::= MkCommand
+      { description = """
+        pretty print data
+        """
+      , subcommands =
+        [ "type" ::= basic "print a type" filePath
+        , "term" ::= basic "print a term" filePath
+        ]
+      , modifiers = []
+      , arguments = none
+      }
+    , "check" ::= MkCommand
+      { description = """
+        check well-formedness
+        """
+      , subcommands =
+        [ "type" ::= basic "check a type" filePath
+        , "term" ::= MkCommand
+          { description = "check a term"
+          , subcommands = []
+          , modifiers = ["--type" ::= option "type to check against" filePath]
+          , arguments = filePath
+          }
+        ]
+      , modifiers = []
+      , arguments = none
+      }
+    ]
+  , modifiers = []
+  , arguments = none
+  }
+
+-- 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
+  Collie.handle {cmd = ("inky" ** Inky)} args
+    [ const showHelp
+    , "--help" ::= [ const showHelp ]
+    , "format" ::=
+      [ const showHelp
+      , "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
+          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
+          printTerm t
+          pure ()
+        ]
+      ]
+    , "check" ::=
+      [ const showHelp
+      , "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) pure abortErr
+        ]
+      , "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
+          a <-
+            maybe (pure (TArrow TNat TNat))
+              (\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) pure abortErr
+                pure a)
+              type
+          handle {err = String} (checkTerm a t) pure abortErr
+        ]
+      ]
+    ]
diff --git a/src/Inky/Context.idr b/src/Inky/Context.idr
index 2e9af8f..586aae2 100644
--- a/src/Inky/Context.idr
+++ b/src/Inky/Context.idr
@@ -70,6 +70,11 @@ public export
 ctx ++ [<] = ctx
 ctx ++ ctx' :< x = (ctx ++ ctx') :< x
 
+export
+appendLinLeftNeutral : (ctx : Context a) -> [<] ++ ctx = ctx
+appendLinLeftNeutral [<] = Refl
+appendLinLeftNeutral (ctx :< x) = cong (:< x) $ appendLinLeftNeutral ctx
+
 public export
 lengthAppend : Length ctx1 -> Length ctx2 -> Length (ctx1 ++ ctx2)
 lengthAppend len1 Z = len1
@@ -111,6 +116,14 @@ public export
 ThereVar : Var ctx v -> Var (ctx :< x) v
 ThereVar i = toVar (There i.pos)
 
+export
+Show (VarPos ctx x v) where
+  show i = show (toNat i)
+
+export
+Show (Var ctx v) where
+  show i = show i.pos
+
 -- Basic Properties
 
 export
@@ -237,7 +250,7 @@ namespace Quantifier
     Lin : All p [<]
     (:<) :
       All p ctx -> (px : Assoc0 (p x.value)) ->
-      {auto 0 prf : px.name = x.name}->
+      {auto 0 prf : px.name = x.name} ->
       All p (ctx :< x)
 
   %name Quantifier.All env
diff --git a/src/Inky/Parser.idr b/src/Inky/Parser.idr
index c44e7bd..fc553ec 100644
--- a/src/Inky/Parser.idr
+++ b/src/Inky/Parser.idr
@@ -360,6 +360,42 @@ namespace M
     map f (Ok res ys prf) = Ok (f res) ys prf
 
   export
+  pure : {xs : List a} -> (x : b) -> M xs True b
+  pure x = Ok x xs (Lax reflexive)
+
+  export
+  (>>=) :
+    M xs nil b ->
+    (b -> {ys : List a} -> {auto 0 prf : SmallerX nil ys xs} -> M ys nil' c) ->
+    M xs (nil && nil') c
+  Err str >>= f = Err str
+  Ok res ys prf >>= f =
+    case f {ys, prf} res of
+      Err str => Err str
+      Ok res' zs prf' => Ok res' zs (rewrite andCommutative nil nil' in transX prf' prf)
+
+  export
+  take :
+    Eq a =>
+    Interpolation a =>
+    (toks : List a) ->
+    (xs : List (WithBounds (Token a))) ->
+    M xs False String
+  take [tok] [] = Err "expected \{tok}; got end of input"
+  take toks [] = Err "expected one of: \{join ", " $ map (\k => "\{k}") toks}; got end of input"
+  take toks (x :: xs) =
+    if x.val.kind `elem` toks
+    then Ok x.val.text xs (Strict reflexive)
+    else case toks of
+      [tok] => Err "\{x.bounds}: expected \{tok}; got \{x.val.kind}"
+      toks => Err "\{x.bounds}: expected one of: \{join ", " $ map (\k => "\{k}") toks}; got \{x.val.kind}"
+
+  export
+  bounds : (xs : List (WithBounds a)) -> M xs True (Bool, Bounds)
+  bounds [] = Ok (True, MkBounds (-1) (-1) (-1) (-1)) [] (Lax reflexive)
+  bounds (x :: xs) = Ok (x.isIrrelevant, x.bounds) (x :: xs) (Lax reflexive)
+
+  export
   wknL : M xs b1 a -> (b2 : Bool) -> M xs (b1 || b2) a
   wknL (Err msg) b2 = Err msg
   wknL (Ok res ys prf) b2 = Ok res ys (wknSmallerL prf b2)
@@ -381,30 +417,34 @@ namespace M
 
 -- The Big Function
 
-data FirstNil : List Bool -> Type where
-  Here : FirstNil (True :: bs)
-  There : FirstNil bs -> FirstNil (False :: bs)
-
-findNil : (nils : List Bool) -> Maybe (FirstNil nils)
-findNil [] = Nothing
-findNil (False :: bs) = There <$> findNil bs
-findNil (True :: bs) = Just Here
-
-memberOf : Eq a => (x : a) -> All.All (const $ List a) xs -> Maybe (Any (const ()) xs)
-memberOf x [] = Nothing
-memberOf x (xs :: xss) =
-  if x `elem` xs
-  then Just (Here ())
-  else There <$> (x `memberOf` xss)
+||| Searches `sets` for the first occurence of `x`.
+||| On failure, returns the index for the nil element, if it exists.
+|||
+||| # Unsafe Invariants
+||| * `nils` has at most one `True` element
+||| * `sets` are disjoint
+lookahead :
+  Eq a =>
+  (x : Maybe a) ->
+  (nils : List Bool) ->
+  (sets : Lazy (All (const $ List a) nils)) ->
+  Maybe (Any (const ()) nils)
+lookahead x [] [] = Nothing
+lookahead x (nil :: nils) (set :: sets) =
+  (do
+    x <- x
+    if x `elem` set then Just (Here ()) else Nothing)
+  <|> There <$> lookahead x nils sets
+  <|> (if nil then Just (Here ()) else Nothing)
 
 parser :
   (e : Eq i) => Interpolation i =>
   (p : Parser i nil locked free a) ->
-  (penv1 : _) ->
-  (penv2 : _) ->
-  (fenv1 : _) ->
-  (fenv2 : _) ->
-  {auto 0 wf : So (wellTyped e penv1 penv2 fenv1 fenv2 p)} ->
+  {penv1 : _} ->
+  {penv2 : _} ->
+  {0 fenv1 : _} ->
+  {0 fenv2 : _} ->
+  (0 wf : So (wellTyped e penv1 penv2 fenv1 fenv2 p)) ->
   (xs : List (WithBounds (Token i))) ->
   All (\x => (ys : List (WithBounds (Token i))) -> (0 _ : SmallerX False ys xs) -> uncurry (M ys) x) locked ->
   All (\x => (ys : List (WithBounds (Token i))) -> (0 _ : SmallerX True ys xs) -> uncurry (M ys) x) free ->
@@ -412,140 +452,96 @@ parser :
 parserChain :
   (e : Eq i) => Interpolation i =>
   (ps : ParserChain i nil locked free as) ->
-  (penv1 : _) ->
-  (penv2 : _) ->
-  (fenv1 : _) ->
-  (fenv2 : _) ->
-  {auto 0 wf : So (wellTypedChain e penv1 penv2 fenv1 fenv2 ps)} ->
+  {penv1 : _} ->
+  {penv2 : _} ->
+  {0 fenv1 : _} ->
+  {0 fenv2 : _} ->
+  (0 wf : So (wellTypedChain e penv1 penv2 fenv1 fenv2 ps)) ->
   (xs : List (WithBounds (Token i))) ->
   All (\x => (ys : List (WithBounds (Token i))) -> (0 _ : SmallerX False ys xs) -> uncurry (M ys) x) locked ->
   All (\x => (ys : List (WithBounds (Token i))) -> (0 _ : SmallerX True ys xs) -> uncurry (M ys) x) free ->
   M xs nil (HList as)
-parserNil :
+parserOneOf :
   (e : Eq i) => Interpolation i =>
-  (at : FirstNil nils) ->
+  {nils : List Bool} ->
+  (at : Any (const ()) nils) ->
   (ps : All (\nil => Parser i nil locked free a) nils) ->
-  (penv1 : _) ->
-  (penv2 : _) ->
-  (fenv1 : _) ->
-  (fenv2 : _) ->
-  {auto 0 wf : So (allWellTyped e penv1 penv2 fenv1 fenv2 ps)} ->
+  {penv1 : _} ->
+  {penv2 : _} ->
+  {0 fenv1 : _} ->
+  {0 fenv2 : _} ->
+  (0 wf : So (allWellTyped e penv1 penv2 fenv1 fenv2 ps)) ->
   (xs : List (WithBounds (Token i))) ->
   All (\x => (ys : List (WithBounds (Token i))) -> (0 _ : SmallerX False ys xs) -> uncurry (M ys) x) locked ->
   All (\x => (ys : List (WithBounds (Token i))) -> (0 _ : SmallerX True ys xs) -> uncurry (M ys) x) free ->
   M xs (any Basics.id nils) a
-parserOneOf :
-  (e : Eq i) => Interpolation i =>
-  {nils : List Bool} ->
-  (at : Any (const ()) nils) ->
-  (ps : All (\nil => Parser i nil locked free a) nils) ->
-  (penv1 : _) ->
-  (penv2 : _) ->
-  (fenv1 : _) ->
-  (fenv2 : _) ->
-  {auto 0 wf : So (allWellTyped e penv1 penv2 fenv1 fenv2 ps)} ->
-  (xs : List1 (WithBounds (Token i))) ->
-  All (\x => (ys : List (WithBounds (Token i))) -> (0 _ : SmallerX False ys (forget xs)) -> uncurry (M ys) x) locked ->
-  All (\x => (ys : List (WithBounds (Token i))) -> (0 _ : SmallerX True ys (forget xs)) -> uncurry (M ys) x) free ->
-  M (forget xs) (any Basics.id nils) a
-
-parser (Var x) penv1 penv2 fenv1 fenv2 xs env1 env2 =
+
+parser (Var x) wf xs env1 env2 =
   indexAll x env2 xs (Lax reflexive)
-parser (Lit text) penv1 penv2 fenv1 fenv2 xs env1 env2 =
-  case xs of
-    [] => Err "expected \{text}, got end of file"
-    y :: ys =>
-      if y.val.kind == text
-      then Ok y.val.text ys (Strict reflexive)
-      else Err "\{y.bounds}: expected \{text}, got \{y.val.kind}"
-parser (Seq ps) penv1 penv2 fenv1 fenv2 xs env1 env2 =
-  parserChain ps penv1 penv2 fenv1 fenv2 xs env1 env2
-parser (OneOf {nils} ps) penv1 penv2 fenv1 fenv2 [] env1 env2 {wf} =
+parser (Lit text) wf xs env1 env2 = take [text] xs
+parser (Seq ps) wf xs env1 env2 =
+  parserChain ps wf xs env1 env2
+parser (OneOf {nils} ps) wf [] env1 env2 =
   let 0 wfs = soAnd {a = disjoint (forget $ peekAll penv2 ps)} wf in
-  case findNil nils of
+  let sets = peekAll penv2 ps in
+  case lookahead Nothing nils sets of
     Nothing => Err "unexpected end of input"
-    Just at => parserNil at ps penv1 penv2 fenv1 fenv2 [] env1 env2
-parser (OneOf {nils} ps) penv1 penv2 fenv1 fenv2 (x :: xs) env1 env2 {wf = wf} =
+    Just at => parserOneOf at ps (snd wfs) [] env1 env2
+parser (OneOf {nils} ps) wf (x :: xs) env1 env2 =
   let 0 wfs = soAnd {a = disjoint (forget $ peekAll penv2 ps)} wf in
   let sets = peekAll penv2 ps in
-  case x.val.kind `memberOf` sets of
-    Just at => parserOneOf at ps penv1 penv2 fenv1 fenv2 (x ::: xs) env1 env2
-    Nothing => case findNil nils of
-      Nothing =>
-        Err
-          "\{x.bounds}: expected one of: \{join ", " $ map (\k => "\{k}") $ concat $ forget sets}; got \{x.val.kind}"
-      Just at => parserNil at ps penv1 penv2 fenv1 fenv2 (x :: xs) env1 env2
-parser (Fix {a, nil} x p) penv1 penv2 fenv1 fenv2 xs env1 env2 =
-  let f = parser p _ _ _ _ {wf} in
-  let
-    res : M xs nil a
-    res =
-      sizeInd {P = \ys => (0 prf : SmallerX True ys xs) -> M ys nil a}
-        (\ys, rec, lte =>
-          f ys
-            (  mapProperty (\f, zs, 0 prf => f zs $ transX prf lte) env1
-            :< (x :- (\zs, prf => rec zs (toSmaller prf) (forget $ transX prf lte)))
-            )
-            (mapProperty (\f, zs, prf => f zs $ transX prf lte) env2))
-        xs
-        (Lax reflexive)
-  in
-  res
-parser (Map f p) penv1 penv2 fenv1 fenv2 xs env1 env2 =
-  f <$> parser p penv1 penv2 fenv1 fenv2 xs env1 env2
-parser (WithBounds p) penv1 penv2 fenv1 fenv2 xs env1 env2 =
-  case xs of
-    [] => irrelevantBounds <$> parser p penv1 penv2 fenv1 fenv2 [] env1 env2
-    (x :: xs) =>
-      (\y => MkBounded y x.isIrrelevant x.bounds) <$>
-      parser p penv1 penv2 fenv1 fenv2 (x :: xs) env1 env2
-
-parserChain [] penv1 penv2 fenv1 fenv2 xs env1 env2 = Ok [] xs (Lax reflexive)
-parserChain ((::) {nil1 = False, nil2} p ps) penv1 penv2 fenv1 fenv2 xs env1 env2 =
+  case lookahead (Just x.val.kind) nils sets of
+    Nothing => Err "\{x.bounds}: expected one of: \{join ", " $ map (\k => "\{k}") $ concat $ forget sets}; got \{x.val.kind}"
+    Just at => parserOneOf at ps (snd wfs) (x :: xs) env1 env2
+parser (Fix {a, nil} x p) wf xs env1 env2 =
+  let f = parser p wf in
+  sizeInd {P = \ys => (0 prf : SmallerX True ys xs) -> M ys nil a}
+    (\ys, rec, lte =>
+      f ys
+        (  mapProperty (\f, zs, 0 prf => f zs $ transX prf lte) env1
+        :< (x :- (\zs, prf => rec zs (toSmaller prf) (forget $ transX prf lte)))
+        )
+        (mapProperty (\f, zs, prf => f zs $ transX prf lte) env2))
+    xs (Lax reflexive)
+parser (Map f p) wf xs env1 env2 =
+  f <$> parser p wf xs env1 env2
+parser (WithBounds p) wf xs env1 env2 = do
+  (irrel, bounds) <- bounds xs
+  rewrite sym $ andTrueNeutral nil
+  x <- parser p wf _
+         (mapProperty (\f, zs, 0 prf => f zs $ transX {b2 = True} prf %search) env1)
+         (mapProperty (\f, zs, 0 prf => f zs $ transX prf %search) env2)
+  pure (MkBounded x irrel bounds)
+
+parserChain [] wf xs env1 env2 = Ok [] xs (Lax reflexive)
+parserChain ((::) {nil1 = False, nil2} p ps) wf xs env1 env2 =
   let 0 wfs = soAnd wf in
-  let 0 wfs' = soAnd (snd wfs) in
-  case parser p penv1 penv2 fenv1 fenv2 xs env1 env2 of
-    Err msg => Err msg
-    Ok x ys lt =>
-      case
-        parserChain ps [<] (penv2 ++ penv1) [<] (fenv2 ++ fenv1)
-          ys
+  let 0 wfs' = soAnd (snd wfs) in do
+    x <- parser p (fst wfs') xs env1 env2
+    y <- parserChain ps (snd wfs')
+          _
           [<]
-          (  mapProperty (\f, zs, 0 prf => f zs $ forget $ transX prf lt) env2
-          ++ mapProperty (\f, zs, 0 prf => f zs $ transX prf lt) env1
+          (  mapProperty (\f, zs, 0 prf => f zs $ forget $ transX {b2 = False} prf %search) env2
+          ++ mapProperty (\f, zs, 0 prf => f zs $ transX prf %search) env1
           )
-      of
-        Err msg => Err msg
-        Ok y zs prf => Ok (x :: y) zs (rewrite sym $ andFalseFalse nil2 in transX prf lt)
-parserChain ((::) {nil1 = True, nil2} p ps) penv1 penv2 fenv1 fenv2 xs env1 env2 =
-  let 0 wfs = soAnd wf in
-  let 0 wfs' = soAnd (snd wfs) in
-  case parser p penv1 penv2 fenv1 fenv2 xs env1 env2 of
-    Err msg => Err msg
-    Ok x ys lte =>
-      case
-        parserChain ps penv1 penv2 fenv1 fenv2
-          ys
-          (mapProperty (\f, zs, prf => f zs $ transX prf lte) env1)
-          (mapProperty (\f, zs, prf => f zs $ transX prf lte) env2)
-      of
-        Err msg => Err msg
-        Ok y zs prf => Ok (x :: y) zs (rewrite sym $ andTrueNeutral nil2 in transX prf lte)
-
-parserNil {nils = True :: nils} Here (p :: ps) penv1 penv2 fenv1 fenv2 xs env1 env2 =
+    pure (x :: y)
+parserChain ((::) {nil1 = True, nil2} p ps) wf xs env1 env2 =
   let 0 wfs = soAnd wf in
-  rewrite anyTrue nils in
-  parser p penv1 penv2 fenv1 fenv2 xs env1 env2
-parserNil (There at) (p :: ps) penv1 penv2 fenv1 fenv2 xs env1 env2 =
-  let 0 wfs = soAnd {a = wellTyped e penv1 penv2 fenv1 fenv2 p} wf in
-  parserNil at ps penv1 penv2 fenv1 fenv2 xs env1 env2
-
-parserOneOf {nils = nil :: nils} (Here ()) (p :: ps) penv1 penv2 fenv1 fenv2 xs env1 env2 =
+  let 0 wfs' = soAnd (snd wfs) in do
+    x <- parser p (fst wfs') xs env1 env2
+    rewrite sym $ andTrueNeutral nil2
+    y <- parserChain ps (snd wfs')
+           _
+           (mapProperty (\f, zs, prf => f zs $ transX {b2 = True} prf %search) env1)
+           (mapProperty (\f, zs, prf => f zs $ transX prf %search) env2)
+    pure (x :: y)
+
+parserOneOf {nils = nil :: nils} (Here ()) (p :: ps) wf xs env1 env2 =
   let 0 wfs = soAnd wf in
-  anyR nils (parser p penv1 penv2 fenv1 fenv2 (forget xs) env1 env2)
-parserOneOf {nils = nil :: nils} (There at) (p :: ps) penv1 penv2 fenv1 fenv2 xs env1 env2 =
+  anyR nils (parser p (fst wfs) xs env1 env2)
+parserOneOf {nils = nil :: nils} (There at) (p :: ps) wf xs env1 env2 =
   let 0 wfs = soAnd {a = wellTyped e penv1 penv2 fenv1 fenv2 p} wf in
-  anyL nil (parserOneOf at ps penv1 penv2 fenv1 fenv2 xs env1 env2)
+  anyL nil (parserOneOf at ps (snd wfs) xs env1 env2)
 
 export
 parse :
@@ -553,7 +549,7 @@ parse :
   (p : Parser i nil [<] [<] a) ->
   {auto 0 wf : So (wellTyped e [<] [<] [<] [<] p)} ->
   (xs : List (WithBounds (Token i))) -> M xs nil a
-parse p xs = parser p [<] [<] [<] [<] xs [<] [<]
+parse p xs = parser p wf xs [<] [<]
 
 -- Functor ---------------------------------------------------------------------
 
diff --git a/src/Inky/Term.idr b/src/Inky/Term.idr
index 807b3e3..54e51ae 100644
--- a/src/Inky/Term.idr
+++ b/src/Inky/Term.idr
@@ -20,17 +20,21 @@ data CheckTerm : (tyCtx, tmCtx : Context ()) -> Type
 data SynthTerm where
   Var : Var tmCtx v -> SynthTerm tyCtx tmCtx
   Lit : Nat -> SynthTerm tyCtx tmCtx
-  Suc : CheckTerm tyCtx tmCtx -> SynthTerm tyCtx tmCtx
+  Suc : SynthTerm tyCtx tmCtx
   App :
     SynthTerm tyCtx tmCtx ->
     (args : List (CheckTerm tyCtx tmCtx)) ->
-    {auto 0 _ : NonEmpty args} ->
+    {auto 0 prf : NonEmpty args} ->
     SynthTerm tyCtx tmCtx
   Prj : SynthTerm tyCtx tmCtx -> String -> SynthTerm tyCtx tmCtx
   Expand : SynthTerm tyCtx tmCtx -> SynthTerm tyCtx tmCtx
   Annot : CheckTerm tyCtx tmCtx -> Ty tyCtx () -> SynthTerm tyCtx tmCtx
 
 data CheckTerm where
+  LetTy :
+    (x : String) -> Ty tyCtx () ->
+    CheckTerm (tyCtx :< (x :- ())) tmCtx ->
+    CheckTerm tyCtx tmCtx
   Let :
     (x : String) -> SynthTerm tyCtx tmCtx ->
     CheckTerm tyCtx (tmCtx :< (x :- ())) ->
@@ -178,32 +182,31 @@ IsFunction :
   Type
 IsFunction [<] fun dom cod = (dom = [<], cod = fun)
 IsFunction (bound :< (x :- ())) fun dom cod =
-  ( b ** c **
-  ( IsArrow fun b c
-  , ( dom' **
-    ( dom = dom' :< (x :- b)
-    , IsFunction bound c dom' cod
+  ( dom' ** cod' **
+  ( IsFunction bound fun dom' cod'
+  , ( b **
+    ( IsArrow cod' b cod
+    , dom = dom' :< (x :- b)
     ))
   ))
 
-
 isFunctionUnique :
   (bound : Context ()) -> (a : Ty tyCtx ()) ->
   forall dom1, dom2, cod1, cod2.
   IsFunction bound a dom1 cod1 -> IsFunction bound a dom2 cod2 -> (dom1 = dom2, cod1 = cod2)
 isFunctionUnique [<] a (Refl, Refl) (Refl, Refl) = (Refl, Refl)
 isFunctionUnique (bound :< (x :- ())) a
-  (b1 ** c1 ** (isArrow1, (dom1' ** (Refl, isFunc1))))
-  (b2 ** c2 ** (isArrow2, (dom2' ** (Refl, isFunc2))))
-  with (isArrowUnique a isArrow1 isArrow2)
+  (dom1 ** cod1 ** (isFunc1, (b1 ** (isArrow1, eq1))))
+  (dom2 ** cod2 ** (isFunc2, (b2 ** (isArrow2, eq2))))
+  with (isFunctionUnique bound a isFunc1 isFunc2)
   isFunctionUnique (bound :< (x :- ())) a
-    (b ** c ** (_, (dom1' ** (Refl, isFunc1))))
-    (b ** c ** (_, (dom2' ** (Refl, isFunc2))))
+    (dom ** cod ** (_, (b1 ** (isArrow1, eq1))))
+    (dom ** cod ** (_, (b2 ** (isArrow2, eq2))))
     | (Refl, Refl)
-    with (isFunctionUnique bound c isFunc1 isFunc2)
+    with (isArrowUnique cod isArrow1 isArrow2)
     isFunctionUnique (bound :< (x :- ())) a
-      (b ** c ** (_, (dom' ** (Refl, _))))
-      (b ** c ** (_, (dom' ** (Refl, _))))
+      (dom ** cod ** (_, (b ** (isArrow1, Refl))))
+      (dom ** cod ** (_, (b ** (isArrow2, Refl))))
       | (Refl, Refl) | (Refl, Refl) = (Refl, Refl)
 
 isFunction :
@@ -211,154 +214,168 @@ isFunction :
   Maybe (All (const $ Ty tyCtx ()) bound, Ty tyCtx ())
 isFunction [<] a = Just ([<], a)
 isFunction (bound :< (x :- ())) a = do
-  (b, c) <- isArrow a
-  (dom, cod) <- isFunction bound c
+  (dom, cod) <- isFunction bound a
+  (b, cod) <- isArrow cod
   Just (dom :< (x :- b), cod)
 
 reflectIsFunction :
   (bound : Context ()) -> (a : Ty tyCtx ()) ->
   uncurry (IsFunction bound a) `OnlyWhen` isFunction bound a
 reflectIsFunction [<] a = RJust (Refl, Refl)
-reflectIsFunction (bound :< (x :- ())) a with (reflectIsArrow a) | (isArrow a)
-  _ | RJust isArrow | Just (b, c) with (reflectIsFunction bound c) | (isFunction bound c)
-    _ | RJust isFunc | Just (dom, cod) = RJust (b ** c ** (isArrow , (dom ** (Refl, isFunc))))
-    _ | RNothing notFunc | _ =
-      RNothing (\(dom :< (x :- b'), cod), (b' ** c' ** (isArrow', (dom ** (Refl, isFunc)))) =>
-        let (eq1, eq2) = isArrowUnique a {b, c, d = b', e = c'} isArrow isArrow' in
-        let isFunc = rewrite eq2 in isFunc in
-        notFunc (dom, cod) isFunc)
-  _ | RNothing notArrow | _ =
-    RNothing (\(dom, cod), (b ** c ** (isArrow, _)) => notArrow (b, c) isArrow)
+reflectIsFunction (bound :< (x :- ())) a with (reflectIsFunction bound a) | (isFunction bound a)
+  _ | RJust isFunc | Just (dom', cod') with (reflectIsArrow cod') | (isArrow cod')
+    _ | RJust isArrow | Just (b, cod) = RJust (dom' ** cod' ** (isFunc , (b ** (isArrow, Refl))))
+    _ | RNothing notArrow | _ =
+      RNothing (\(dom :< (x :- b), cod), (dom ** cod'' ** (isFunc', (b ** (isArrow, Refl)))) =>
+        let (eq1, eq2) = isFunctionUnique bound a {dom1 = dom', dom2 = dom, cod1 = cod', cod2 = cod''} isFunc isFunc' in
+        let isArrow = rewrite eq2 in isArrow in
+        notArrow (b, cod) isArrow)
+  _ | RNothing notFunc | _ =
+    RNothing (\(dom, cod), (dom' ** cod' ** (isFunc, _)) => notFunc (dom', cod') isFunc)
 
 -- Full type checking and synthesis --------------------------------------------
 
 Synths :
-  {tyCtx, tmCtx : Context ()} -> (env : All (const (Ty tyCtx ())) tmCtx) ->
-  SynthTerm tyCtx tmCtx -> Ty tyCtx () -> Type
+  {tmCtx : Context ()} ->
+  (tyEnv : DEnv Ty tyCtx) ->
+  (env : All (const $ Ty [<] ()) tmCtx) ->
+  SynthTerm tyCtx tmCtx -> Ty [<] () -> Type
 Checks :
-  {tyCtx, tmCtx : Context ()} -> (env : All (const (Ty tyCtx ())) tmCtx) ->
-  Ty tyCtx () -> CheckTerm tyCtx tmCtx -> Type
+  {tmCtx : Context ()} ->
+  (tyEnv : DEnv Ty tyCtx) ->
+  (env : All (const $ Ty [<] ()) tmCtx) ->
+  Ty [<] () -> CheckTerm tyCtx tmCtx -> Type
 CheckSpine :
-  {tyCtx, tmCtx : Context ()} -> (env : All (const (Ty tyCtx ())) tmCtx) ->
-  (fun : Ty tyCtx ()) -> List (CheckTerm tyCtx tmCtx) -> (res : Ty tyCtx ()) -> Type
+  {tmCtx : Context ()} ->
+  (tyEnv : DEnv Ty tyCtx) ->
+  (env : All (const $ Ty [<] ()) tmCtx) ->
+  (fun : Ty [<] ()) -> List (CheckTerm tyCtx tmCtx) -> (res : Ty [<] ()) -> Type
 AllCheck :
-  {tyCtx, tmCtx : Context ()} -> (env : All (const (Ty tyCtx ())) tmCtx) ->
-  Row (Ty tyCtx ()) -> Row (CheckTerm tyCtx tmCtx) -> Type
+  {tmCtx : Context ()} ->
+  (tyEnv : DEnv Ty tyCtx) ->
+  (env : All (const $ Ty [<] ()) tmCtx) ->
+  Row (Ty [<] ()) -> Row (CheckTerm tyCtx tmCtx) -> Type
 AllCheckBinding :
-  {tyCtx, tmCtx : Context ()} -> (env : All (const (Ty tyCtx ())) tmCtx) ->
-  Row (Ty tyCtx ()) -> Ty tyCtx () ->
+  {tmCtx : Context ()} ->
+  (tyEnv : DEnv Ty tyCtx) ->
+  (env : All (const $ Ty [<] ()) tmCtx) ->
+  Row (Ty [<] ()) -> Ty [<] () ->
   Row (x : String ** CheckTerm tyCtx (tmCtx :< (x :- ()))) ->
   Type
 
-Synths env (Var i) a = (a = indexAll i env)
-Synths env (Lit k) a = (a = TNat)
-Synths env (Suc t) a = (Checks env TNat t, a = TNat)
-Synths env (App e ts) a =
+Synths tyEnv env (Var i) a = (a = indexAll i env)
+Synths tyEnv env (Lit k) a = (a = TNat)
+Synths tyEnv env Suc a = (a = TArrow TNat TNat)
+Synths tyEnv env (App e ts) a =
   ( fun **
-  ( Synths env e fun
-  , CheckSpine env fun ts a
+  ( Synths tyEnv env e fun
+  , CheckSpine tyEnv env fun ts a
   ))
-Synths env (Prj e x) a =
+Synths tyEnv env (Prj e x) a =
   ( b **
-  ( Synths env e b
+  ( Synths tyEnv env e b
   , ( as **
     ( IsProduct b as
     , GetAt x as a
     ))
   ))
-Synths env (Expand e) a =
+Synths tyEnv env (Expand e) a =
   ( b **
-  ( Synths env e b
+  ( Synths tyEnv env e b
   , ( xc **
     ( IsFixpoint b xc
     , a = sub (Base Id :< (fst xc :- b)) (snd xc)
     ))
   ))
-Synths env (Annot t a) b =
+Synths tyEnv env (Annot t a) b =
   ( Not (IllFormed a)
-  , Checks env a t
-  , a = b
+  , Checks tyEnv env (expand tyEnv a) t
+  , expand tyEnv a = b
   )
 
-Checks env a (Let x e t) =
+Checks tyEnv env a (LetTy x b t) =
+  ( Not (IllFormed b)
+  , Checks (tyEnv :< (x :- b)) env a t
+  )
+Checks tyEnv env a (Let x e t) =
   ( b **
-  ( Synths env e b
-  , Checks (env :< (x :- b)) a t
+  ( Synths tyEnv env e b
+  , Checks tyEnv (env :< (x :- b)) a t
   ))
-Checks env a (Abs bound t) =
+Checks tyEnv env a (Abs bound t) =
   ( as ** b **
   ( IsFunction bound a as b
-  , Checks (env ++ as) b t
+  , Checks tyEnv (env ++ as) b t
   ))
-Checks env a (Inj x t) =
+Checks tyEnv env a (Inj x t) =
   ( as **
   ( IsSum a as
   , ( b **
     ( GetAt x as b
-    , Checks env b t
+    , Checks tyEnv env b t
     ))
   ))
-Checks env a (Tup ts) =
+Checks tyEnv env a (Tup ts) =
   ( as **
   ( IsProduct a as
-  , AllCheck env as ts
+  , AllCheck tyEnv env as ts
   ))
-Checks env a (Case e ts) =
+Checks tyEnv env a (Case e ts) =
   ( b **
-  ( Synths env e b
+  ( Synths tyEnv env e b
   , ( as **
     ( IsSum b as
-    , AllCheckBinding env as a ts
+    , AllCheckBinding tyEnv env as a ts
     ))
   ))
-Checks env a (Contract t) =
+Checks tyEnv env a (Contract t) =
   ( xb **
   ( IsFixpoint a xb
-  , Checks env (sub (Base Id :< (fst xb :- a)) (snd xb)) t
+  , Checks tyEnv env (sub (Base Id :< (fst xb :- a)) (snd xb)) t
   ))
-Checks env a (Fold e x t) =
+Checks tyEnv env a (Fold e x t) =
   ( b **
-  ( Synths env e b
+  ( Synths tyEnv env e b
   , ( yc **
     ( IsFixpoint b yc
-    , Checks (env :< (x :- sub (Base Id :< (fst yc :- a)) (snd yc))) a t
+    , Checks tyEnv (env :< (x :- sub (Base Id :< (fst yc :- a)) (snd yc))) a t
     ))
   ))
-Checks env a (Embed e) =
+Checks tyEnv env a (Embed e) =
   ( b **
-  ( Synths env e b
+  ( Synths tyEnv env e b
   , a `Eq` b
   ))
 
-CheckSpine env fun [] res = fun = res
-CheckSpine env fun (t :: ts) res =
+CheckSpine tyEnv env fun [] res = fun = res
+CheckSpine tyEnv env fun (t :: ts) res =
   ( a ** b **
   ( IsArrow fun a b
-  , Checks env a t
-  , CheckSpine env b ts res
+  , Checks tyEnv env a t
+  , CheckSpine tyEnv env b ts res
   ))
 
-AllCheck env as [<] = (as = [<])
-AllCheck env as (ts :< (x :- t)) =
+AllCheck tyEnv env as [<] = (as = [<])
+AllCheck tyEnv env as (ts :< (x :- t)) =
   ( a ** bs **
   ( Remove x as a bs
-  , Checks env a t
-  , AllCheck env bs ts
+  , Checks tyEnv env a t
+  , AllCheck tyEnv env bs ts
   ))
 
-AllCheckBinding env as a [<] = (as = [<])
-AllCheckBinding env as a (ts :< (x :- (y ** t))) =
+AllCheckBinding tyEnv env as a [<] = (as = [<])
+AllCheckBinding tyEnv env as a (ts :< (x :- (y ** t))) =
   ( b ** bs **
   ( Remove x as b bs
-  , Checks (env :< (y :- b)) a t
-  , AllCheckBinding env bs a ts
+  , Checks tyEnv (env :< (y :- b)) a t
+  , AllCheckBinding tyEnv env bs a ts
   ))
 
 -- Reordering
 
 allCheckReorder :
   as <~> bs -> (ts : Row (CheckTerm tyCtx tmCtx)) ->
-  AllCheck env as ts -> AllCheck env bs ts
+  AllCheck tyEnv env as ts -> AllCheck tyEnv env bs ts
 allCheckReorder [] [<] Refl = Refl
 allCheckReorder (_ :: _) [<] Refl impossible
 allCheckReorder prf (ts :< (x :- t)) (a ** bs ** (prf1, prf2, prf3)) =
@@ -366,7 +383,7 @@ allCheckReorder prf (ts :< (x :- t)) (a ** bs ** (prf1, prf2, prf3)) =
 
 allCheckBindingReorder :
   as <~> bs -> (ts : Row (x ** CheckTerm tyCtx (tmCtx :< (x :- ())))) ->
-  AllCheckBinding env as a ts -> AllCheckBinding env bs a ts
+  AllCheckBinding tyEnv env as a ts -> AllCheckBinding tyEnv env bs a ts
 allCheckBindingReorder [] [<] Refl = Refl
 allCheckBindingReorder (_ :: _) [<] Refl impossible
 allCheckBindingReorder prf (ts :< (x :- (y ** t))) (b ** bs ** (prf1, prf2, prf3)) =
@@ -375,139 +392,153 @@ allCheckBindingReorder prf (ts :< (x :- (y ** t))) (b ** bs ** (prf1, prf2, prf3
 -- Uniqueness
 
 synthsUnique :
-  (0 env : All (const $ Ty tyCtx ()) tmCtx) -> (e : SynthTerm tyCtx tmCtx) ->
-  Synths env e a -> Synths env e b -> a = b
+  (0 tyEnv : DEnv Ty tyCtx) ->
+  (0 env : All (const $ Ty [<] ()) tmCtx) ->
+  (e : SynthTerm tyCtx tmCtx) ->
+  Synths tyEnv env e a -> Synths tyEnv env e b -> a = b
 checkSpineUnique :
-  (0 env : All (const $ Ty tyCtx ()) tmCtx) ->
-  (fun : Ty tyCtx ()) -> (ts : List (CheckTerm tyCtx tmCtx)) ->
-  CheckSpine env fun ts a -> CheckSpine env fun ts b -> a = b
-
-synthsUnique env (Var i) prf1 prf2 = trans prf1 (sym prf2)
-synthsUnique env (Lit k) prf1 prf2 = trans prf1 (sym prf2)
-synthsUnique env (Suc t) (_, prf1) (_, prf2) = trans prf1 (sym prf2)
-synthsUnique env (App e ts) (fun1 ** (prf11, prf12)) (fun2 ** (prf21, prf22))
-  with (synthsUnique env e prf11 prf21)
-  synthsUnique env (App e ts) (fun ** (prf11, prf12)) (fun ** (prf21, prf22)) | Refl =
-    checkSpineUnique env fun ts prf12 prf22
-synthsUnique env (Prj e k) (a ** (prf11, prf12)) (b ** (prf21, prf22))
-  with (synthsUnique env e prf11 prf21)
-  synthsUnique env (Prj e k) (a ** (_, (as ** (prf11, prf12)))) (a ** (_, (bs ** (prf21, prf22)))) | Refl
+  (0 tyEnv : DEnv Ty tyCtx) ->
+  (0 env : All (const $ Ty [<] ()) tmCtx) ->
+  (fun : Ty [<] ()) -> (ts : List (CheckTerm tyCtx tmCtx)) ->
+  CheckSpine tyEnv env fun ts a -> CheckSpine tyEnv env fun ts b -> a = b
+
+synthsUnique tyEnv env (Var i) prf1 prf2 = trans prf1 (sym prf2)
+synthsUnique tyEnv env (Lit k) prf1 prf2 = trans prf1 (sym prf2)
+synthsUnique tyEnv env Suc prf1 prf2 = trans prf1 (sym prf2)
+synthsUnique tyEnv env (App e ts) (fun1 ** (prf11, prf12)) (fun2 ** (prf21, prf22))
+  with (synthsUnique tyEnv env e prf11 prf21)
+  synthsUnique tyEnv env (App e ts) (fun ** (prf11, prf12)) (fun ** (prf21, prf22)) | Refl =
+    checkSpineUnique tyEnv env fun ts prf12 prf22
+synthsUnique tyEnv env (Prj e k) (a ** (prf11, prf12)) (b ** (prf21, prf22))
+  with (synthsUnique tyEnv env e prf11 prf21)
+  synthsUnique tyEnv env (Prj e k) (a ** (_, (as ** (prf11, prf12)))) (a ** (_, (bs ** (prf21, prf22)))) | Refl
     with (isProductUnique a prf11 prf21)
-    synthsUnique env (Prj e k) (a ** (_, (as ** (_, prf1)))) (a ** (_, (as ** (_, prf2)))) | Refl | Refl =
+    synthsUnique tyEnv env (Prj e k) (a ** (_, (as ** (_, prf1)))) (a ** (_, (as ** (_, prf2)))) | Refl | Refl =
       getAtUnique k as prf1 prf2
-synthsUnique env (Expand e) (a ** (prf11, prf12)) (b ** (prf21, prf22))
-  with (synthsUnique env e prf11 prf21)
-  synthsUnique env (Expand e) (a ** (_, (b ** (prf11, prf12)))) (a ** (_, (c ** (prf21, prf22)))) | Refl
+synthsUnique tyEnv env (Expand e) (a ** (prf11, prf12)) (b ** (prf21, prf22))
+  with (synthsUnique tyEnv env e prf11 prf21)
+  synthsUnique tyEnv env (Expand e) (a ** (_, (b ** (prf11, prf12)))) (a ** (_, (c ** (prf21, prf22)))) | Refl
     with (isFixpointUnique a prf11 prf21)
-    synthsUnique env (Expand e) (a ** (_, (b ** (_, prf1)))) (a ** (_, (b ** (_, prf2)))) | Refl | Refl =
+    synthsUnique tyEnv env (Expand e) (a ** (_, (b ** (_, prf1)))) (a ** (_, (b ** (_, prf2)))) | Refl | Refl =
       trans prf1 (sym prf2)
-synthsUnique env (Annot t c) prf1 prf2 = trans (sym $ snd $ snd prf1) (snd $ snd prf2)
+synthsUnique tyEnv env (Annot t c) prf1 prf2 = trans (sym $ snd $ snd prf1) (snd $ snd prf2)
 
-checkSpineUnique env fun [] prf1 prf2 = trans (sym prf1) prf2
-checkSpineUnique env fun (t :: ts) (a ** b ** (prf11, _ , prf12)) (c ** d ** (prf21, _ , prf22))
+checkSpineUnique tyEnv env fun [] prf1 prf2 = trans (sym prf1) prf2
+checkSpineUnique tyEnv env fun (t :: ts) (a ** b ** (prf11, _ , prf12)) (c ** d ** (prf21, _ , prf22))
   with (isArrowUnique fun prf11 prf21)
-  checkSpineUnique env fun (t :: ts) (a ** b ** (_, _ , prf1)) (a ** b ** (_, _ , prf2)) | (Refl, Refl) =
-    checkSpineUnique env b ts prf1 prf2
+  checkSpineUnique tyEnv env fun (t :: ts) (a ** b ** (_, _ , prf1)) (a ** b ** (_, _ , prf2)) | (Refl, Refl) =
+    checkSpineUnique tyEnv env b ts prf1 prf2
 
 -- Decision
 
 synths :
-  (env : All (const (Ty tyCtx ())) tmCtx) ->
-  SynthTerm tyCtx tmCtx -> Maybe (Ty tyCtx ())
+  (tyEnv : DEnv Ty tyCtx) ->
+  (env : All (const $ Ty [<] ()) tmCtx) ->
+  SynthTerm tyCtx tmCtx -> Maybe (Ty [<] ())
+export
 checks :
-  (env : All (const (Ty tyCtx ())) tmCtx) ->
-  Ty tyCtx () -> CheckTerm tyCtx tmCtx -> Bool
+  (tyEnv : DEnv Ty tyCtx) ->
+  (env : All (const $ Ty [<] ()) tmCtx) ->
+  Ty [<] () -> CheckTerm tyCtx tmCtx -> Bool
 checkSpine :
-  (env : All (const (Ty tyCtx ())) tmCtx) ->
-  (fun : Ty tyCtx ()) -> List (CheckTerm tyCtx tmCtx) -> Maybe (Ty tyCtx ())
+  (tyEnv : DEnv Ty tyCtx) ->
+  (env : All (const $ Ty [<] ()) tmCtx) ->
+  (fun : Ty [<] ()) -> List (CheckTerm tyCtx tmCtx) -> Maybe (Ty [<] ())
 allCheck :
-  (env : All (const (Ty tyCtx ())) tmCtx) ->
-  Row (Ty tyCtx ()) -> Row (CheckTerm tyCtx tmCtx) -> Bool
+  (tyEnv : DEnv Ty tyCtx) ->
+  (env : All (const $ Ty [<] ()) tmCtx) ->
+  Row (Ty [<] ()) -> Row (CheckTerm tyCtx tmCtx) -> Bool
 allCheckBinding :
-  (env : All (const (Ty tyCtx ())) tmCtx) ->
-  Row (Ty tyCtx ()) -> Ty tyCtx () ->
+  (tyEnv : DEnv Ty tyCtx) ->
+  (env : All (const $ Ty [<] ()) tmCtx) ->
+  Row (Ty [<] ()) -> Ty [<] () ->
   Row (x ** CheckTerm tyCtx (tmCtx :< (x :- ()))) ->
   Bool
 
-synths env (Var i) = Just (indexAll i env)
-synths env (Lit k) = Just TNat
-synths env (Suc t) = do
-  guard (checks env TNat t)
-  Just TNat
-synths env (App e ts) = do
-  a <- synths env e
-  checkSpine env a ts
-synths env (Prj e k) = do
-  a <- synths env e
+synths tyEnv env (Var i) = do
+  pure (indexAll i env)
+synths tyEnv env (Lit k) = do
+  pure TNat
+synths tyEnv env Suc = do
+  pure (TArrow TNat TNat)
+synths tyEnv env (App e ts) = do
+  a <- synths tyEnv env e
+  checkSpine tyEnv env a ts
+synths tyEnv env (Prj e k) = do
+  a <- synths tyEnv env e
   as <- isProduct a
   getAt k as
-synths env (Expand e) = do
-  a <- synths env e
+synths tyEnv env (Expand e) = do
+  a <- synths tyEnv env e
   (x ** b) <- isFixpoint a
   Just (sub (Base Id :< (x :- a)) b)
-synths env (Annot t a) = do
+synths tyEnv env (Annot t a) = do
   guard (not $ illFormed a)
-  guard (checks env a t)
-  Just a
-
-checks env a (Let x e t) =
-  case synths env e of
-    Just b => checks (env :< (x :- b)) a t
+  guard (checks tyEnv env (expand tyEnv a) t)
+  Just (expand tyEnv a)
+
+checks tyEnv env a (LetTy x b t) =
+  not (illFormed b) &&
+  checks (tyEnv :< (x :- b)) env a t
+checks tyEnv env a (Let x e t) =
+  case synths tyEnv env e of
+    Just b => checks tyEnv (env :< (x :- b)) a t
     Nothing => False
-checks env a (Abs bound t) =
+checks tyEnv env a (Abs bound t) =
   case isFunction bound a of
-    Just (dom, cod) => checks (env ++ dom) cod t
+    Just (dom, cod) => checks tyEnv (env ++ dom) cod t
     Nothing => False
-checks env a (Inj k t) =
+checks tyEnv env a (Inj k t) =
   case isSum a of
     Just as =>
       case getAt k as of
-        Just b => checks env b t
+        Just b => checks tyEnv env b t
         Nothing => False
     Nothing => False
-checks env a (Tup ts) =
+checks tyEnv env a (Tup ts) =
   case isProduct a of
-    Just as => allCheck env as ts
+    Just as => allCheck tyEnv env as ts
     Nothing => False
-checks env a (Case e ts) =
-  case synths env e of
+checks tyEnv env a (Case e ts) =
+  case synths tyEnv env e of
     Just b =>
       case isSum b of
-        Just as => allCheckBinding env as a ts
+        Just as => allCheckBinding tyEnv env as a ts
         Nothing => False
     Nothing => False
-checks env a (Contract t) =
+checks tyEnv env a (Contract t) =
   case isFixpoint a of
-    Just (x ** b) => checks env (sub (Base Id :< (x :- a)) b) t
+    Just (x ** b) => checks tyEnv env (sub (Base Id :< (x :- a)) b) t
     Nothing => False
-checks env a (Fold e x t) =
-  case synths env e of
+checks tyEnv env a (Fold e x t) =
+  case synths tyEnv env e of
     Just b =>
       case isFixpoint b of
-        Just (y ** c) => checks (env :< (x :- sub (Base Id :< (y :- a)) c)) a t
+        Just (y ** c) => checks tyEnv (env :< (x :- sub (Base Id :< (y :- a)) c)) a t
         Nothing => False
     Nothing => False
-checks env a (Embed e) =
-  case synths env e of
+checks tyEnv env a (Embed e) =
+  case synths tyEnv env e of
     Just b => a == b
     Nothing => False
 
-checkSpine env a [] = Just a
-checkSpine env a (t :: ts) = do
+checkSpine tyEnv env a [] = do
+  pure a
+checkSpine tyEnv env a (t :: ts) = do
   (dom, cod) <- isArrow a
-  guard (checks env dom t)
-  checkSpine env cod ts
+  guard (checks tyEnv env dom t)
+  checkSpine tyEnv env cod ts
 
-allCheck env as [<] = null as
-allCheck env as (ts :< (x :- t)) =
+allCheck tyEnv env as [<] = null as
+allCheck tyEnv env as (ts :< (x :- t)) =
   case remove' x as of
-    Just (a, bs) => checks env a t && allCheck env bs ts
+    Just (a, bs) => checks tyEnv env a t && allCheck tyEnv env bs ts
     Nothing => False
 
-allCheckBinding env as a [<] = null as
-allCheckBinding env as a (ts :< (x :- (y ** t))) =
+allCheckBinding tyEnv env as a [<] = null as
+allCheckBinding tyEnv env as a (ts :< (x :- (y ** t))) =
   case remove' x as of
-    Just (b, bs) => checks (env :< (y :- b)) a t && allCheckBinding env bs a ts
+    Just (b, bs) => checks tyEnv (env :< (y :- b)) a t && allCheckBinding tyEnv env bs a ts
     Nothing => False
 
 -- Proof
@@ -516,84 +547,92 @@ allCheckBinding env as a (ts :< (x :- (y ** t))) =
 
 partial
 0 reflectSynths :
-  (env : All (const $ Ty tyCtx ()) tmCtx) ->
+  (tyEnv : DEnv Ty tyCtx) ->
+  (env : All (const $ Ty [<] ()) tmCtx) ->
   (e : SynthTerm tyCtx tmCtx) ->
-  Synths env e `OnlyWhen` synths env e
+  Synths tyEnv env e `OnlyWhen` synths tyEnv env e
 partial
 0 reflectChecks :
-  (env : All (const $ Ty tyCtx ()) tmCtx) ->
-  (a : Ty tyCtx ()) -> (t : CheckTerm tyCtx tmCtx) ->
-  Checks env a t `Reflects` checks env a t
+  (tyEnv : DEnv Ty tyCtx) ->
+  (env : All (const $ Ty [<] ()) tmCtx) ->
+  (a : Ty [<] ()) -> (t : CheckTerm tyCtx tmCtx) ->
+  Checks tyEnv env a t `Reflects` checks tyEnv env a t
 partial
 0 reflectCheckSpine :
-  (env : All (const $ Ty tyCtx ()) tmCtx) ->
-  (fun : Ty tyCtx ()) -> (ts : List (CheckTerm tyCtx tmCtx)) ->
-  CheckSpine env fun ts `OnlyWhen` checkSpine env fun ts
+  (tyEnv : DEnv Ty tyCtx) ->
+  (env : All (const $ Ty [<] ()) tmCtx) ->
+  (fun : Ty [<] ()) -> (ts : List (CheckTerm tyCtx tmCtx)) ->
+  CheckSpine tyEnv env fun ts `OnlyWhen` checkSpine tyEnv env fun ts
 partial
 0 reflectAllCheck :
-  (env : All (const $ Ty tyCtx ()) tmCtx) ->
-  (as : Row (Ty tyCtx ())) -> (ts : Row (CheckTerm tyCtx tmCtx)) ->
-  AllCheck env as ts `Reflects` allCheck env as ts
+  (tyEnv : DEnv Ty tyCtx) ->
+  (env : All (const $ Ty [<] ()) tmCtx) ->
+  (as : Row (Ty [<] ())) -> (ts : Row (CheckTerm tyCtx tmCtx)) ->
+  AllCheck tyEnv env as ts `Reflects` allCheck tyEnv env as ts
 partial
 0 reflectAllCheckBinding :
-  (env : All (const $ Ty tyCtx ()) tmCtx) ->
-  (as : Row (Ty tyCtx ())) -> (a : Ty tyCtx ()) ->
+  (tyEnv : DEnv Ty tyCtx) ->
+  (env : All (const $ Ty [<] ()) tmCtx) ->
+  (as : Row (Ty [<] ())) -> (a : Ty [<] ()) ->
   (ts : Row (x ** CheckTerm tyCtx (tmCtx :< (x :- ())))) ->
-  AllCheckBinding env as a ts `Reflects` allCheckBinding env as a ts
-
-reflectSynths env (Var i) = RJust Refl
-reflectSynths env (Lit k) = RJust Refl
-reflectSynths env (Suc t) with (reflectChecks env TNat t) | (checks env TNat t)
-  _ | RTrue tNat | _ = RJust (tNat, Refl)
-  _ | RFalse tNotNat | _ = RNothing (\_, (tNat, _) => tNotNat tNat)
-reflectSynths env (App e ts) with (reflectSynths env e) | (synths env e)
-  _ | RJust eTy | Just a with (reflectCheckSpine env a ts) | (checkSpine env a ts)
+  AllCheckBinding tyEnv env as a ts `Reflects` allCheckBinding tyEnv env as a ts
+
+reflectSynths tyEnv env (Var i) = RJust Refl
+reflectSynths tyEnv env (Lit k) = RJust Refl
+reflectSynths tyEnv env Suc = RJust Refl
+reflectSynths tyEnv env (App e ts) with (reflectSynths tyEnv env e) | (synths tyEnv env e)
+  _ | RJust eTy | Just a with (reflectCheckSpine tyEnv env a ts) | (checkSpine tyEnv env a ts)
     _ | RJust tsSpine | Just b = RJust (a ** (eTy, tsSpine))
     _ | RNothing tsBad | _ =
       RNothing
         (\c, (b ** (eTy', tsSpine)) =>
-          let tsSpine = rewrite synthsUnique env e {a, b} eTy eTy' in tsSpine in
+          let tsSpine = rewrite synthsUnique tyEnv env e {a, b} eTy eTy' in tsSpine in
           tsBad c tsSpine)
   _ | RNothing eBad | _ =
     RNothing (\c, (b ** (eTy, _)) => eBad b eTy)
-reflectSynths env (Prj e x) with (reflectSynths env e) | (synths env e)
+reflectSynths tyEnv env (Prj e x) with (reflectSynths tyEnv env e) | (synths tyEnv env e)
   _ | RJust eTy | Just a with (reflectIsProduct a) | (isProduct a)
     _ | RJust prf | Just as with (reflectGetAt x as) | (getAt x as)
       _ | RJust got | Just b = RJust (a ** (eTy, (as ** (prf, got))))
       _ | RNothing not | _ =
         RNothing (\x, (a' ** (eTy', (as' ** (prf', got)))) =>
-          let prf' = rewrite synthsUnique env e {a, b = a'} eTy eTy' in prf' in
+          let prf' = rewrite synthsUnique tyEnv env e {a, b = a'} eTy eTy' in prf' in
           let got = rewrite isProductUnique a {as, bs = as'} prf prf' in got in
           not x got)
     _ | RNothing nprf | _ =
       RNothing (\x, (a' ** (eTy', (as' ** (prf, _)))) =>
-        let prf = rewrite synthsUnique env e {a, b = a'} eTy eTy' in prf in
+        let prf = rewrite synthsUnique tyEnv env e {a, b = a'} eTy eTy' in prf in
         nprf as' prf)
   _ | RNothing eBad | _ = RNothing (\x, (a' ** (eTy, _)) => eBad a' eTy)
-reflectSynths env (Expand e) with (reflectSynths env e) | (synths env e)
+reflectSynths tyEnv env (Expand e) with (reflectSynths tyEnv env e) | (synths tyEnv env e)
   _ | RJust eTy | Just a with (reflectIsFixpoint a) | (isFixpoint a)
     _ | RJust prf | Just (x ** b) = RJust (a ** (eTy, ((x ** b) ** (prf, Refl))))
     _ | RNothing nprf | _ =
       RNothing (\x, (a' ** (eTy', (b ** (prf, eq)))) =>
-        let prf = rewrite synthsUnique env e {a, b = a'} eTy eTy' in prf in
+        let prf = rewrite synthsUnique tyEnv env e {a, b = a'} eTy eTy' in prf in
         nprf b prf)
   _ | RNothing eBad | _ = RNothing (\x, (a ** (eTy, _)) => eBad a eTy)
-reflectSynths env (Annot t a) with (reflectIllFormed a) | (illFormed a)
-  _ | RFalse wf | _ with (reflectChecks env a t) | (checks env a t)
+reflectSynths tyEnv env (Annot t a) with (reflectIllFormed a) | (illFormed a)
+  _ | RFalse wf | _ with (reflectChecks tyEnv env (expand tyEnv a) t) | (checks tyEnv env (expand tyEnv a) t)
     _ | RTrue tTy | _ = RJust (wf, tTy, Refl)
     _ | RFalse tBad | _ = RNothing (\x, (_, tTy, Refl) => tBad tTy)
   _ | RTrue notWf | _ = RNothing (\x, (wf, _) => wf notWf)
 
-reflectChecks env a (Let x e t) with (reflectSynths env e) | (synths env e)
-  _ | RJust eTy | Just b with (reflectChecks (env :< (x :- b)) a t) | (checks (env :< (x :- b)) a t)
+reflectChecks tyEnv env a (LetTy x b t) with (reflectIllFormed b) | (illFormed b)
+  _ | RFalse wf | _ with (reflectChecks (tyEnv :< (x :- b)) env a t) | (checks (tyEnv :< (x :- b)) env a t)
+    _ | RTrue tTy | _ = RTrue (wf, tTy)
+    _ | RFalse tBad | _ = RFalse (tBad . snd)
+  _ | RTrue notWf | _ = RFalse (\(wf, _) => wf notWf)
+reflectChecks tyEnv env a (Let x e t) with (reflectSynths tyEnv env e) | (synths tyEnv env e)
+  _ | RJust eTy | Just b with (reflectChecks tyEnv (env :< (x :- b)) a t) | (checks tyEnv (env :< (x :- b)) a t)
     _ | RTrue tTy | _ = RTrue (b ** (eTy, tTy))
     _ | RFalse tBad | _ =
       RFalse (\(b' ** (eTy', tTy)) =>
-        let tTy = rewrite synthsUnique env e {a = b, b = b'} eTy eTy' in tTy in
+        let tTy = rewrite synthsUnique tyEnv env e {a = b, b = b'} eTy eTy' in tTy in
         tBad tTy)
   _ | RNothing eBad | Nothing = RFalse (\(b ** (eTy, _)) => eBad b eTy)
-reflectChecks env a (Abs bound t) with (reflectIsFunction bound a) | (isFunction bound a)
-  _ | RJust prf | Just (as, b) with (reflectChecks (env ++ as) b t) | (checks (env ++ as) b t)
+reflectChecks tyEnv env a (Abs bound t) with (reflectIsFunction bound a) | (isFunction bound a)
+  _ | RJust prf | Just (as, b) with (reflectChecks tyEnv (env ++ as) b t) | (checks tyEnv (env ++ as) b t)
     _ | RTrue tTy | _ = RTrue (as ** b ** (prf, tTy))
     _ | RFalse tBad | _ =
       RFalse (\(as' ** b' ** (prf', tTy)) =>
@@ -606,9 +645,9 @@ reflectChecks env a (Abs bound t) with (reflectIsFunction bound a) | (isFunction
         in
         tBad tTy)
   _ | RNothing nprf | _ = RFalse (\(as ** b ** (prf, _)) => nprf (as, b) prf)
-reflectChecks env a (Inj k t) with (reflectIsSum a) | (isSum a)
+reflectChecks tyEnv env a (Inj k t) with (reflectIsSum a) | (isSum a)
   _ | RJust prf | Just as with (reflectGetAt k as) | (getAt k as)
-    _ | RJust got | Just b with (reflectChecks env b t) | (checks env b t)
+    _ | RJust got | Just b with (reflectChecks tyEnv env b t) | (checks tyEnv env b t)
       _ | RTrue tTy | _ = RTrue (as ** (prf, (b ** (got, tTy))))
       _ | RFalse tBad | _ =
         RFalse (\(as' ** (prf', (b' ** (got', tTy)))) =>
@@ -621,74 +660,74 @@ reflectChecks env a (Inj k t) with (reflectIsSum a) | (isSum a)
         let got = rewrite isSumUnique a {as, bs = as'} prf prf' in got in
         not b got)
   _ | RNothing nprf | _ = RFalse (\(as ** (prf, _)) => nprf as prf)
-reflectChecks env a (Tup ts) with (reflectIsProduct a) | (isProduct a)
-  _ | RJust prf | Just as with (reflectAllCheck env as ts) | (allCheck env as ts)
+reflectChecks tyEnv env a (Tup ts) with (reflectIsProduct a) | (isProduct a)
+  _ | RJust prf | Just as with (reflectAllCheck tyEnv env as ts) | (allCheck tyEnv env as ts)
     _ | RTrue tsTy | _ = RTrue (as ** (prf, tsTy))
     _ | RFalse tsBad | _ =
       RFalse (\(as' ** (prf', tsTy)) =>
         let tsTy = rewrite isProductUnique a {as, bs = as'} prf prf' in tsTy in
         tsBad tsTy)
   _ | RNothing nprf | _ = RFalse (\(as ** (prf, _)) => nprf as prf)
-reflectChecks env a (Case e ts) with (reflectSynths env e) | (synths env e)
+reflectChecks tyEnv env a (Case e ts) with (reflectSynths tyEnv env e) | (synths tyEnv env e)
   _ | RJust eTy | Just b with (reflectIsSum b) | (isSum b)
-    _ | RJust prf | Just as with (reflectAllCheckBinding env as a ts) | (allCheckBinding env as a ts)
+    _ | RJust prf | Just as with (reflectAllCheckBinding tyEnv env as a ts) | (allCheckBinding tyEnv env as a ts)
       _ | RTrue tsTy | _ = RTrue (b ** (eTy, (as ** (prf, tsTy))))
       _ | RFalse tsBad | _ =
         RFalse
           (\(b' ** (eTy', (as' ** (prf', tsTy)))) =>
-            let prf' = rewrite synthsUnique env e {a = b, b = b'} eTy eTy' in prf' in
+            let prf' = rewrite synthsUnique tyEnv env e {a = b, b = b'} eTy eTy' in prf' in
             let tsTy = rewrite isSumUnique b {as, bs = as'} prf prf' in tsTy in
             tsBad tsTy)
     _ | RNothing nprf | _ =
       RFalse (\(b' ** (eTy', (as ** (prf, _)))) =>
-        let prf = rewrite synthsUnique env e {a = b, b = b'} eTy eTy' in prf in
+        let prf = rewrite synthsUnique tyEnv env e {a = b, b = b'} eTy eTy' in prf in
         nprf as prf)
   _ | RNothing eBad | _ = RFalse (\(b ** (eTy, _)) => eBad b eTy)
-reflectChecks env a (Contract t) with (reflectIsFixpoint a) | (isFixpoint a)
-  _ | RJust prf | Just (x ** b) with (reflectChecks env (sub (Base Id :< (x :- a)) b) t) | (checks env (sub (Base Id :< (x :- a)) b) t)
+reflectChecks tyEnv env a (Contract t) with (reflectIsFixpoint a) | (isFixpoint a)
+  _ | RJust prf | Just (x ** b) with (reflectChecks tyEnv env (sub (Base Id :< (x :- a)) b) t) | (checks tyEnv env (sub (Base Id :< (x :- a)) b) t)
     _ | RTrue tTy | _ = RTrue ((x ** b) ** (prf, tTy))
     _ | RFalse tBad | _ =
       RFalse (\(b' ** (prf', tTy)) =>
         let
           eq = isFixpointUnique a {xb = (x ** b), yc = b'} prf prf'
           tTy =
-            replace {p = \xb => Checks env (sub (Base Id :< (xb.fst :- a)) xb.snd) t}
+            replace {p = \xb => Checks tyEnv env (sub (Base Id :< (xb.fst :- a)) xb.snd) t}
               (sym eq) tTy
         in
         tBad tTy)
   _ | RNothing nprf | _ = RFalse (\(b ** (prf, _)) => nprf b prf)
-reflectChecks env a (Fold e x t) with (reflectSynths env e) | (synths env e)
+reflectChecks tyEnv env a (Fold e x t) with (reflectSynths tyEnv env e) | (synths tyEnv env e)
   _ | RJust eTy | Just b with (reflectIsFixpoint b) | (isFixpoint b)
-    _ | RJust prf | Just (y ** c) with (reflectChecks (env :< (x :- sub (Base Id :< (y :- a)) c)) a t) | (checks (env :< (x :- sub (Base Id :< (y :- a)) c)) a t)
+    _ | RJust prf | Just (y ** c) with (reflectChecks tyEnv (env :< (x :- sub (Base Id :< (y :- a)) c)) a t) | (checks tyEnv (env :< (x :- sub (Base Id :< (y :- a)) c)) a t)
       _ | RTrue tTy | _ = RTrue (b ** (eTy, ((y ** c) ** (prf, tTy))))
       _ | RFalse tBad | _ =
         RFalse (\(b' ** (eTy', (c' ** (prf', tTy)))) =>
           let
-            prf' = rewrite synthsUnique env e {a = b, b = b'} eTy eTy' in prf'
+            prf' = rewrite synthsUnique tyEnv env e {a = b, b = b'} eTy eTy' in prf'
             eq = isFixpointUnique b {xb = (y ** c), yc = c'} prf prf'
             tTy =
-              replace {p = \yc => Checks (env :< (x :- sub (Base Id :< (yc.fst :- a)) yc.snd)) a t}
+              replace {p = \yc => Checks tyEnv (env :< (x :- sub (Base Id :< (yc.fst :- a)) yc.snd)) a t}
                 (sym eq) tTy
           in
           tBad tTy)
     _ | RNothing nprf | _ =
       RFalse (\(b' ** (eTy', (c ** (prf, _)))) =>
-        let prf = rewrite synthsUnique env e {a = b, b = b'} eTy eTy' in prf in
+        let prf = rewrite synthsUnique tyEnv env e {a = b, b = b'} eTy eTy' in prf in
         nprf c prf)
   _ | RNothing eBad | _ = RFalse (\(b ** (eTy, _)) => eBad b eTy)
-reflectChecks env a (Embed e) with (reflectSynths env e) | (synths env e)
+reflectChecks tyEnv env a (Embed e) with (reflectSynths tyEnv env e) | (synths tyEnv env e)
   _ | RJust eTy | Just b with (reflectEq a b) | (a == b)
     _ | RTrue eq | _ = RTrue (b ** (eTy, eq))
     _ | RFalse neq | _ =
       RFalse (\(b' ** (eTy', eq)) =>
-        let eq = rewrite synthsUnique env e {a = b, b = b'} eTy eTy' in eq in
+        let eq = rewrite synthsUnique tyEnv env e {a = b, b = b'} eTy eTy' in eq in
         neq eq)
   _ | RNothing eBad | _ = RFalse (\(b ** (eTy, _)) => eBad b eTy)
 
-reflectCheckSpine env a [] = RJust Refl
-reflectCheckSpine env a (t :: ts) with (reflectIsArrow a) | (isArrow a)
-  _ | RJust prf | Just (b, c) with (reflectChecks env b t) | (checks env b t)
-    _ | RTrue tTy | _ with (reflectCheckSpine env c ts) | (checkSpine env c ts)
+reflectCheckSpine tyEnv env a [] = RJust Refl
+reflectCheckSpine tyEnv env a (t :: ts) with (reflectIsArrow a) | (isArrow a)
+  _ | RJust prf | Just (b, c) with (reflectChecks tyEnv env b t) | (checks tyEnv env b t)
+    _ | RTrue tTy | _ with (reflectCheckSpine tyEnv env c ts) | (checkSpine tyEnv env c ts)
       _ | RJust tsTy | Just d = RJust (b ** c ** (prf, tTy, tsTy))
       _ | RNothing tsBad | _ =
         RNothing (\d, (_ ** c' ** (prf', _, tsTy)) =>
@@ -702,10 +741,10 @@ reflectCheckSpine env a (t :: ts) with (reflectIsArrow a) | (isArrow a)
         tBad tTy)
   _ | RNothing nprf | _ = RNothing (\d, (b ** c ** (prf, _)) => nprf (b, c) prf)
 
-reflectAllCheck env [<] [<] = RTrue Refl
-reflectAllCheck env (_ :< _) [<] = RFalse (\case Refl impossible)
-reflectAllCheck env as (ts :< (x :- t)) with (reflectRemove x as) | (remove' x as)
-  _ | RJust prf | Just (a, bs) with (reflectAnd (reflectChecks env a t) (reflectAllCheck env bs ts)) | (checks env a t && allCheck env bs ts)
+reflectAllCheck tyEnv env [<] [<] = RTrue Refl
+reflectAllCheck tyEnv env (_ :< _) [<] = RFalse (\case Refl impossible)
+reflectAllCheck tyEnv env as (ts :< (x :- t)) with (reflectRemove x as) | (remove' x as)
+  _ | RJust prf | Just (a, bs) with (reflectAnd (reflectChecks tyEnv env a t) (reflectAllCheck tyEnv env bs ts)) | (checks tyEnv env a t && allCheck tyEnv env bs ts)
     _ | RTrue checks | _ = RTrue (a ** bs ** (prf, checks))
     _ | RFalse notChecks | _ =
       RFalse (\(a' ** bs' ** (prf', checks)) =>
@@ -714,10 +753,10 @@ reflectAllCheck env as (ts :< (x :- t)) with (reflectRemove x as) | (remove' x a
         bimap (\x => rewrite eq in x) (allCheckReorder (sym reorder) ts) checks)
   _ | RNothing nprf | _ = RFalse (\(a ** bs ** (prf, _)) => nprf (a, bs) prf)
 
-reflectAllCheckBinding env [<] a [<] = RTrue Refl
-reflectAllCheckBinding env (_ :< _) a [<] = RFalse (\case Refl impossible)
-reflectAllCheckBinding env as a (ts :< (x :- (y ** t))) with (reflectRemove x as) | (remove' x as)
-  _ | RJust prf | Just (b, bs) with (reflectAnd (reflectChecks (env :< (y :- b)) a t) (reflectAllCheckBinding env bs a ts)) | (checks (env :< (y :- b)) a t && allCheckBinding env bs a ts)
+reflectAllCheckBinding tyEnv env [<] a [<] = RTrue Refl
+reflectAllCheckBinding tyEnv env (_ :< _) a [<] = RFalse (\case Refl impossible)
+reflectAllCheckBinding tyEnv env as a (ts :< (x :- (y ** t))) with (reflectRemove x as) | (remove' x as)
+  _ | RJust prf | Just (b, bs) with (reflectAnd (reflectChecks tyEnv (env :< (y :- b)) a t) (reflectAllCheckBinding tyEnv env bs a ts)) | (checks tyEnv (env :< (y :- b)) a t && allCheckBinding tyEnv env bs a ts)
     _ | RTrue checks | _ = RTrue (b ** bs ** (prf, checks))
     _ | RFalse notChecks | _ =
       RFalse (\(b' ** bs' ** (prf', checks)) =>
diff --git a/src/Inky/Term/Parser.idr b/src/Inky/Term/Parser.idr
index 7a67441..6913bf8 100644
--- a/src/Inky/Term/Parser.idr
+++ b/src/Inky/Term/Parser.idr
@@ -1,5 +1,7 @@
 module Inky.Term.Parser
 
+import public Data.Fun
+
 import Data.List1
 import Data.String
 import Inky.Context
@@ -21,6 +23,7 @@ data InkyKind
   | In
   | Case
   | Of
+  | FoldCase
   | Fold
   | By
   | Nat
@@ -36,8 +39,10 @@ data InkyKind
   | DoubleArrow
   | Bang
   | Tilde
+  | Dot
   | Backslash
   | Colon
+  | Semicolon
   | Equal
   | Comma
   | Ignore
@@ -52,6 +57,7 @@ export
   In == In = True
   Case == Case = True
   Of == Of = True
+  FoldCase == FoldCase = True
   Fold == Fold = True
   By == By = True
   Nat == Nat = True
@@ -67,8 +73,10 @@ export
   DoubleArrow == DoubleArrow = True
   Bang == Bang = True
   Tilde == Tilde = True
+  Dot == Dot = True
   Backslash == Backslash = True
   Colon == Colon = True
+  Semicolon == Semicolon = True
   Equal == Equal = True
   Comma == Comma = True
   Ignore == Ignore = True
@@ -84,6 +92,7 @@ Interpolation InkyKind where
   interpolate In = "'in'"
   interpolate Case = "'case'"
   interpolate Of = "'of'"
+  interpolate FoldCase = "'foldcase'"
   interpolate Fold = "'fold'"
   interpolate By = "'by'"
   interpolate Nat = "'Nat'"
@@ -99,8 +108,10 @@ Interpolation InkyKind where
   interpolate DoubleArrow = "'=>'"
   interpolate Bang = "'!'"
   interpolate Tilde = "'~'"
+  interpolate Dot = "'.'"
   interpolate Backslash = "'\\'"
   interpolate Colon = "':'"
+  interpolate Semicolon = "';'"
   interpolate Equal = "'='"
   interpolate Comma = "','"
   interpolate Ignore = ""
@@ -119,6 +130,7 @@ TokenKind InkyKind where
   tokValue In = const ()
   tokValue Case = const ()
   tokValue Of = const ()
+  tokValue FoldCase = const ()
   tokValue Fold = const ()
   tokValue By = const ()
   tokValue Nat = const ()
@@ -134,8 +146,10 @@ TokenKind InkyKind where
   tokValue DoubleArrow = const ()
   tokValue Bang = const ()
   tokValue Tilde = const ()
+  tokValue Dot = const ()
   tokValue Backslash = const ()
   tokValue Colon = const ()
+  tokValue Semicolon = const ()
   tokValue Equal = const ()
   tokValue Comma = const ()
   tokValue Ignore = const ()
@@ -147,6 +161,7 @@ keywords =
   , ("in", In)
   , ("case", Case)
   , ("of", Of)
+  , ("foldcase", FoldCase)
   , ("fold", Fold)
   , ("by", By)
   , ("Nat", Nat)
@@ -169,7 +184,10 @@ typeIdentifier = upper <+> many (alphaNum <|> exact "_")
 export
 tokenMap : TokenMap InkyToken
 tokenMap =
-  toTokenMap [(spaces, Ignore)] ++
+  toTokenMap
+    [ (spaces, Ignore)
+    , (lineComment $ exact "--", Ignore)
+    ] ++
   [(termIdentifier, \s =>
     case lookup s keywords of
       Just k => Tok k s
@@ -192,8 +210,10 @@ tokenMap =
     , (exact "=>", DoubleArrow)
     , (exact "!", Bang)
     , (exact "~", Tilde)
+    , (exact ".", Dot)
     , (exact "\\", Backslash)
     , (exact ":", Colon)
+    , (exact ";", Semicolon)
     , (exact "=", Equal)
     , (exact ",", Comma)
     ]
@@ -201,6 +221,16 @@ tokenMap =
 -- Parser ----------------------------------------------------------------------
 
 public export
+DFun : (ts : Vect n Type) -> Fun ts Type -> Type
+DFun [] r = r
+DFun (t :: ts) r = (x : t) -> DFun ts (r x)
+
+public export
+DIFun : (ts : Vect n Type) -> Fun ts Type -> Type
+DIFun [] r = r
+DIFun (t :: ts) r = {x : t} -> DIFun ts (r x)
+
+public export
 InkyParser : Bool -> Context Type -> Context Type -> (a : Type) -> Type
 InkyParser nil locked free a =
   Parser InkyKind nil
@@ -209,33 +239,74 @@ InkyParser nil locked free a =
     a
 
 public export
-record TypeFun where
-  constructor MkTypeFun
-  try : (ctx : Context ()) -> Either String (Ty ctx ())
+record ParseFun (0 tys: Vect n Type) (0 p : Fun (map Context tys) Type) where
+  constructor MkParseFun
+  try : DFun (map Context tys) (chain {ts = map Context tys} (Either String) p)
+
+mkVar : ({ctx : Context ()} -> Var ctx () -> p ctx) -> WithBounds String -> ParseFun [()] p
+mkVar f x =
+  MkParseFun
+    (\ctx => case lookup x.val ctx of
+      Just (() ** i) => pure (f i)
+      Nothing => Left "\{x.bounds}: unbound name \"\{x.val}\"")
+
+mkVar2 :
+  ({tyCtx, tmCtx : Context ()} -> Var tmCtx () -> p tyCtx tmCtx) ->
+  WithBounds String -> ParseFun [(), ()] p
+mkVar2 f x =
+  MkParseFun
+    (\tyCtx, tmCtx => case lookup x.val tmCtx of
+      Just (() ** i) => pure (f i)
+      Nothing => Left "\{x.bounds}: unbound name \"\{x.val}\"")
+
+public export
+TypeFun : Type
+TypeFun = ParseFun [()] (\ctx => Ty ctx ())
+
+public export
+SynthFun : Type
+SynthFun = ParseFun [(), ()] SynthTerm
+
+public export
+CheckFun : Type
+CheckFun = ParseFun [(), ()] CheckTerm
 
 public export
 TypeParser : Context () -> Context () -> Type
 TypeParser locked free =
   InkyParser False (map (const TypeFun) locked) (map (const TypeFun) free) TypeFun
 
-Row : InkyParser True [<] [<"openType" :- TypeFun] (List $ Assoc TypeFun)
-Row =
-  sepBy (match Comma)
-    (mkAssoc <$> Seq [match TypeIdent, match Colon, Var (%% "openType")])
+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])
   where
-  mkAssoc : HList [String, (), TypeFun] -> Assoc TypeFun
+  mkAssoc : HList [String, (), a] -> Assoc a
   mkAssoc [x, _, v] = x :- v
 
-tryRow : WithBounds (List $ Assoc TypeFun) -> (ctx : Context ()) -> Either String (Row (Ty ctx ()))
+tryRow :
+  List (WithBounds $ Assoc (ParseFun [()] p)) ->
+  (ctx : Context ()) -> Either String (Row $ p ctx)
 tryRow xs ctx =
   foldlM
     (\row, xf => do
-      a <- xf.value.try ctx
-      let Just row' = extend row (xf.name :- a)
-        | Nothing => Left "\{xs.bounds}: duplicate name \"\{xf.name}\""
+      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 [(), ()] p)) ->
+  (tyCtx, tmCtx : Context ()) -> 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.val
+    xs
 
 OpenOrFixpointType : TypeParser [<] [<"openType" :- ()]
 OpenOrFixpointType =
@@ -246,31 +317,26 @@ OpenOrFixpointType =
     ]
   where
   mkFix : HList [(), String, (), TypeFun] -> TypeFun
-  mkFix [_, x, _, a] = MkTypeFun (\ctx => pure $ TFix x !(a.try (ctx :< (x :- ()))))
+  mkFix [_, x, _, a] = MkParseFun (\ctx => pure $ TFix x !(a.try (ctx :< (x :- ()))))
 
 AtomType : TypeParser [<"openType" :- ()] [<]
 AtomType =
   OneOf
-    [
-      mkVar <$> WithBounds (match TypeIdent)
-    , MkTypeFun (\_ => pure TNat) <$ match Nat
-    , mkProd <$> enclose (match AngleOpen) (match AngleClose) (WithBounds Row)
-    , mkSum <$> enclose (match BracketOpen) (match BracketClose) (WithBounds Row)
+    [ mkVar TVar <$> WithBounds (match TypeIdent)
+    , MkParseFun (\_ => pure TNat) <$ match Nat
+    , mkProd <$> enclose (match AngleOpen) (match AngleClose) Row
+    , mkSum <$> enclose (match BracketOpen) (match BracketClose) Row
     , enclose (match ParenOpen) (match ParenClose) OpenOrFixpointType
     ]
   where
-  mkVar : WithBounds String -> TypeFun
-  mkVar x =
-    MkTypeFun
-      (\ctx => case lookup x.val ctx of
-        Just (() ** i) => pure (TVar i)
-        Nothing => Left "\{x.bounds}: unbound name \"\{x.val}\"")
+  Row : InkyParser True [<] [<"openType" :- TypeFun] (List $ WithBounds $ Assoc TypeFun)
+  Row = RowOf [<"openType" :- TypeFun] $ Var (%% "openType")
 
-  mkProd : WithBounds (List $ Assoc TypeFun) -> TypeFun
-  mkProd xs = MkTypeFun (\ctx => TProd <$> tryRow xs ctx)
+  mkProd : List (WithBounds $ Assoc TypeFun) -> TypeFun
+  mkProd xs = MkParseFun (\ctx => TProd <$> tryRow xs ctx)
 
-  mkSum : WithBounds (List $ Assoc TypeFun) -> TypeFun
-  mkSum xs = MkTypeFun (\ctx => TSum <$> tryRow xs ctx)
+  mkSum : List (WithBounds $ Assoc TypeFun) -> TypeFun
+  mkSum xs = MkParseFun (\ctx => TSum <$> tryRow xs ctx)
 
 export
 OpenType : TypeParser [<] [<]
@@ -278,9 +344,250 @@ OpenType =
   Fix "openType" $ mkArrow <$> sepBy1 (match Arrow) AtomType
   where
   mkArrow : List1 TypeFun -> TypeFun
-  mkArrow = foldr1 (\x, y => MkTypeFun (\ctx => [| TArrow (x.try ctx) (y.try ctx) |]))
+  mkArrow = foldr1 (\x, y => MkParseFun (\ctx => [| TArrow (x.try ctx) (y.try ctx) |]))
 
 %hint
 export
 OpenTypeWf : So (wellTyped EqI [<] [<] [<] [<] OpenType)
 OpenTypeWf = Oh
+
+-- Terms -----------------------------------------------------------------------
+
+embed : SynthFun -> CheckFun
+embed x = MkParseFun (\tyCtx, tmCtx => Embed <$> x.try tyCtx tmCtx)
+
+unembed : WithBounds CheckFun -> SynthFun
+unembed x =
+  MkParseFun (\tyCtx, tmCtx => do
+    t <- x.val.try tyCtx tmCtx
+    case t of
+      Embed e => pure e
+      _ => Left "\{x.bounds}: cannot synthesise type")
+
+AtomCheck : InkyParser False [<"openCheck" :- CheckFun] [<] CheckFun
+AtomCheck =
+  OneOf
+    [ embed <$> mkVar2 Var <$> WithBounds (match TermIdent)
+    , embed <$> mkLit <$> match Lit
+    , embed <$> MkParseFun (\_, _ => pure Suc) <$ match Suc
+    , mkTup <$> (enclose (match AngleOpen) (match AngleClose) $
+        RowOf [<"openCheck" :- CheckFun] (Var (%% "openCheck")))
+    , enclose (match ParenOpen) (match ParenClose) (Var (%% "openCheck"))
+    ]
+  where
+  mkLit : Nat -> SynthFun
+  mkLit k = MkParseFun (\_, _ => pure (Lit k))
+
+  mkTup : List (WithBounds $ Assoc CheckFun) -> CheckFun
+  mkTup xs = MkParseFun (\tyCtx, tmCtx => Tup <$> tryRow2 xs tyCtx tmCtx)
+
+PrefixCheck : InkyParser False [<"openCheck" :- CheckFun] [<] CheckFun
+PrefixCheck =
+  Fix "prefixCheck" $ OneOf
+    [ embed <$> mkExpand <$> unembed <$> (match Bang **> WithBounds (Var $ %% "prefixCheck"))
+    , mkContract <$> (match Tilde **> Var (%% "prefixCheck"))
+    , rename (Drop Id) Id AtomCheck
+    ]
+  where
+  mkExpand : SynthFun -> SynthFun
+  mkExpand x = MkParseFun (\tyCtx, tmCtx => [| Expand (x.try tyCtx tmCtx) |])
+
+  mkContract : CheckFun -> CheckFun
+  mkContract x = MkParseFun (\tyCtx, tmCtx => [| Contract (x.try tyCtx tmCtx) |])
+
+SuffixCheck : InkyParser False [<"openCheck" :- CheckFun] [<] CheckFun
+SuffixCheck = mkSuffix <$> Seq [ WithBounds PrefixCheck , star (match Dot **> match TypeIdent) ]
+  where
+  mkSuffix : HList [WithBounds CheckFun, List String] -> CheckFun
+  mkSuffix [t, []] = t.val
+  mkSuffix [t, prjs] =
+    embed $
+    MkParseFun (\tyCtx, tmCtx => pure $ foldl Prj !((unembed t).try tyCtx tmCtx) prjs)
+
+AppCheck : InkyParser False [<"openCheck" :- CheckFun] [<] CheckFun
+AppCheck =
+  OneOf
+    [ mkInj <$> Seq
+      [ match TypeIdent
+      , weaken (S Z) SuffixCheck
+      ]
+    , mkApp <$> Seq [ WithBounds SuffixCheck , star (weaken (S Z) SuffixCheck) ]
+    ]
+  where
+  mkInj : HList [String, CheckFun] -> CheckFun
+  mkInj [tag, t] = MkParseFun (\tyCtx, tmCtx => Inj tag <$> t.try tyCtx tmCtx)
+
+  mkApp : HList [WithBounds CheckFun, List CheckFun] -> CheckFun
+  mkApp [t, []] = t.val
+  mkApp [fun, (arg :: args)] =
+    MkParseFun (\tyCtx, tmCtx =>
+      pure $ Embed $
+      App
+        !((unembed fun).try tyCtx tmCtx)
+        (  !(arg.try tyCtx tmCtx)
+        :: (!(foldlM (\acc, arg => pure $ acc :< !(arg.try tyCtx tmCtx)) [<] args) <>> [])))
+
+AnnotCheck : InkyParser False [<"openCheck" :- CheckFun] [<] CheckFun
+AnnotCheck =
+  mkAnnot <$> Seq
+    [ AppCheck
+    , option (match Colon **> rename Id (Drop Id) OpenType)
+    ]
+  where
+  mkAnnot : HList [CheckFun, Maybe TypeFun] -> CheckFun
+  mkAnnot [t, Nothing] = t
+  mkAnnot [t, Just a] = embed $ MkParseFun (\tyCtx, tmCtx => [| Annot (t.try tyCtx tmCtx) (a.try tyCtx) |])
+
+-- Open Terms
+
+LetCheck : InkyParser False [<"openCheck" :- CheckFun] [<] CheckFun
+LetCheck =
+  match Let **>
+  OneOf
+    [ mkLet <$> Seq
+      [ match TermIdent
+      , OneOf
+        [ mkBound <$> Seq
+          [ star (enclose (match ParenOpen) (match ParenClose) $
+            Seq [ match TermIdent, match Colon, rename Id (Drop Id) OpenType ])
+          , match Colon
+          , rename Id (Drop Id) OpenType
+          , match Equal
+          , Var (%% "openCheck")]
+        , match Equal **> unembed <$> WithBounds (Var (%% "openCheck"))
+        ]
+      , match In
+      , Var (%% "openCheck")
+      ]
+    , mkLetType <$> Seq
+      [ match TypeIdent
+      , match Equal
+      , rename Id (Drop Id) OpenType
+      , match In
+      , Var (%% "openCheck")
+      ]
+    ]
+  where
+  mkLet : HList [String, SynthFun, (), CheckFun] -> CheckFun
+  mkLet [x, e, _, t] = MkParseFun (\tyCtx, tmCtx => pure $ Let x !(e.try tyCtx tmCtx) !(t.try tyCtx (tmCtx :< (x :- ()))))
+
+  mkLetType : HList [String, (), TypeFun, (), CheckFun] -> CheckFun
+  mkLetType [x, _, a, _, t] =
+    MkParseFun (\tyCtx, tmCtx => pure $ LetTy x !(a.try tyCtx) !(t.try (tyCtx :< (x :- ())) tmCtx))
+
+  mkArrow : List TypeFun -> TypeFun -> TypeFun
+  mkArrow [] cod = cod
+  mkArrow (arg :: args) cod =
+    MkParseFun (\ctx => [| TArrow (arg.try ctx) ((mkArrow args cod).try ctx) |])
+
+  mkBound : HList [List (HList [String, (), TypeFun]), (), TypeFun, (), CheckFun] -> SynthFun
+  mkBound [[], _, cod, _, t] =
+    MkParseFun (\tyCtx, tmCtx =>
+      pure $
+      Annot !(t.try tyCtx tmCtx) !(cod.try tyCtx))
+  mkBound [args, _, cod, _, t] =
+    let dom = foldl (\dom, [x, _, a] => dom :< (x :- ())) [<] args in
+    MkParseFun (\tyCtx, tmCtx =>
+      pure $
+      Annot (Abs dom !(t.try tyCtx (tmCtx ++ dom))) !((mkArrow (map (\[x, _, a] => a) args) cod).try tyCtx))
+
+AbsCheck : InkyParser False [<"openCheck" :- CheckFun] [<] CheckFun
+AbsCheck =
+  mkAbs <$> Seq
+    [ match Backslash
+    , sepBy1 (match Comma) (match TermIdent)
+    , match DoubleArrow
+    , Var (%% "openCheck")
+    ]
+  where
+  mkAbs : HList [(), List1 String, (), CheckFun] -> CheckFun
+  mkAbs [_, args, _, body] =
+    let args = foldl (\args, x => args :< (x :- ())) [<] args in
+    MkParseFun (\tyCtx, tmCtx => Abs args <$> body.try tyCtx (tmCtx ++ args))
+
+CaseCheck : InkyParser False [<"openCheck" :- CheckFun] [<] CheckFun
+CaseCheck =
+  (\[f, x] => f x) <$>
+  Seq
+    [ OneOf
+      [ mkCase <$> Seq
+        [ match Case
+        , unembed <$> WithBounds (Var $ %% "openCheck")
+        , match Of
+        ]
+      , mkFoldCase <$> Seq
+        [ match FoldCase
+        , unembed <$> WithBounds (Var $ %% "openCheck")
+        , match By
+        ]
+      ]
+    , enclose (match BraceOpen) (match BraceClose) (
+        sepBy (match Semicolon) $
+        WithBounds $
+        Seq
+          [ match TypeIdent
+          , match TermIdent
+          , match DoubleArrow
+          , Var (%% "openCheck")
+          ])
+    ]
+  where
+  Cases : Type
+  Cases = List (WithBounds $ HList [String, String, (), CheckFun])
+
+  mkBranch :
+    HList [String, String, (), CheckFun] ->
+    Assoc (ParseFun [(), ()] $ \tyCtx, tmCtx => (x ** CheckTerm tyCtx (tmCtx :< (x :- ()))))
+  mkBranch [tag, bound, _, branch] =
+    tag :- MkParseFun (\tyCtx, tmCtx => pure (bound ** !(branch.try tyCtx (tmCtx :< (bound :- ())))))
+
+  mkCase : HList [_, SynthFun, _] -> Cases -> CheckFun
+  mkCase [_, target, _] branches =
+    let branches = map (map mkBranch) branches in
+    MkParseFun (\tyCtx, tmCtx =>
+      [| Case (target.try tyCtx tmCtx) (tryRow2 branches tyCtx tmCtx) |])
+
+  mkFoldCase : HList [_, SynthFun, _] -> Cases -> CheckFun
+  mkFoldCase [_, target, _] branches =
+    let branches = map (map mkBranch) branches in
+    MkParseFun (\tyCtx, tmCtx =>
+      pure $
+      Fold
+        !(target.try tyCtx tmCtx)
+        "__tmp"
+        (Case (Var $ %% "__tmp") !(tryRow2 branches tyCtx (tmCtx :< ("__tmp" :- ())))))
+
+FoldCheck : InkyParser False [<"openCheck" :- CheckFun] [<] CheckFun
+FoldCheck =
+  mkFold <$> Seq
+    [ match Fold
+    , unembed <$> WithBounds (Var (%% "openCheck"))
+    , match By
+    , enclose (match ParenOpen) (match ParenClose) $
+      Seq
+        [ match Backslash
+        , match TermIdent
+        , match DoubleArrow
+        , Var (%% "openCheck")
+        ]
+    ]
+  where
+  mkFold : HList [(), SynthFun, (), HList [(), String, (), CheckFun]] -> CheckFun
+  mkFold [_, target, _, [_, arg, _, body]] =
+    MkParseFun (\tyCtx, tmCtx => pure $ Fold !(target.try tyCtx tmCtx) arg !(body.try tyCtx (tmCtx :< (arg :- ()))))
+
+export
+OpenCheck : InkyParser False [<] [<] CheckFun
+OpenCheck =
+  Fix "openCheck" $ OneOf
+    [ LetCheck
+    , AbsCheck
+    , CaseCheck
+    , FoldCheck
+    , AnnotCheck
+    ]
+
+%hint
+export
+OpenCheckWf : So (wellTyped EqI [<] [<] [<] [<] OpenCheck)
+OpenCheckWf = ?d -- Oh
diff --git a/src/Inky/Term/Pretty.idr b/src/Inky/Term/Pretty.idr
index 7c5ee4d..3bed88b 100644
--- a/src/Inky/Term/Pretty.idr
+++ b/src/Inky/Term/Pretty.idr
@@ -23,6 +23,7 @@ export
 prettySynth :
   {tyCtx, tmCtx : Context ()} ->
   SynthTerm tyCtx tmCtx -> Prec -> Doc ann
+export
 prettyCheck :
   {tyCtx, tmCtx : Context ()} ->
   CheckTerm tyCtx tmCtx -> Prec -> Doc ann
@@ -38,15 +39,13 @@ prettyCheckCtxBinding :
 
 prettySynth (Var i) d = pretty (unVal $ nameOf i)
 prettySynth (Lit k) d = pretty k
-prettySynth (Suc t) d =
-  parenthesise (d >= appPrec) $ group $ align $ hang 2 $
-    "suc" <+> line <+> prettyCheck t appPrec
+prettySynth Suc d = pretty "suc"
 prettySynth (App e ts) d =
   parenthesise (d >= appPrec) $ group $ align $ hang 2 $
     concatWith (surround line) (prettySynth e appPrec :: prettyAllCheck ts appPrec)
 prettySynth (Prj e x) d =
   parenthesise (d > prjPrec) $ group $ align $ hang 2 $
-    prettySynth e prjPrec <+> "." <+> pretty x
+    prettySynth e prjPrec <+> line' <+> "." <+> pretty x
 prettySynth (Expand e) d =
   "!" <+>
   (parenthesise (d > expandPrec) $ group $ align $ hang 2 $
@@ -55,17 +54,25 @@ prettySynth (Annot t a) d =
   parenthesise (d > annotPrec) $ group $ align $ hang 2 $
     prettyCheck t annotPrec <++> ":" <+> line <+> prettyType a annotPrec
 
+prettyCheck (LetTy x a t) d =
+  parenthesise (d > letPrec) $ group $ align $
+    "let" <++>
+    (group $ align $ hang 2 $
+      pretty x <++> "=" <+> line <+> prettyType a letPrec
+    ) <+> line <+>
+    "in" <+> line <+>
+    prettyCheck t letPrec
 prettyCheck (Let x e t) d =
-  parenthesise (d > letPrec) $ group $ align $ hang 2 $
+  parenthesise (d > letPrec) $ group $ align $
     "let" <++>
     (group $ align $ hang 2 $
       pretty x <++> "=" <+> line <+> prettySynth e letPrec
-    ) <++>
+    ) <+> line <+>
     "in" <+> line <+>
     prettyCheck t letPrec
 prettyCheck (Abs bound t) d =
   parenthesise (d > absPrec) $ group $ align $ hang 2 $
-    "\\" <+> concatWith (surround ",") (bindings bound <>> []) <++> "=>" <+> line <+>
+    "\\" <+> concatWith (surround $ "," <+> line) (bindings bound <>> []) <++> "=>" <+> line <+>
     prettyCheck t absPrec
   where
   bindings : Context () -> SnocList (Doc ann)
@@ -73,16 +80,15 @@ prettyCheck (Abs bound t) d =
   bindings (bound :< (x :- ())) = bindings bound :< pretty x
 prettyCheck (Inj k t) d =
   parenthesise (d > injPrec) $ group $ align $ hang 2 $
-    "<" <+> line' <+> pretty k <+> line' <+> ">" <+> prettyCheck t injPrec
+    pretty k <+> line <+> prettyCheck t injPrec
 prettyCheck (Tup ts) d =
-  parens $ group $ align $ hang 2 $
+  enclose "<" ">" $ group $ align $ hang 2 $
     concatWith (surround $ "," <+> line) (prettyCheckCtx ts tupPrec)
 prettyCheck (Case e ts) d =
   parenthesise (d > casePrec) $ group $ align $ hang 2 $
     "case" <++> prettySynth e casePrec <++> "of" <+> line <+>
-    (braces $ align $ hang 2 $
-      concatWith (surround hardline) $
-      map parens $
+    (braces $ group $ align $ hang 2 $
+      concatWith (surround $ ";" <+> line) $
       prettyCheckCtxBinding ts casePrec)
 prettyCheck (Contract t) d =
   "~" <+>
@@ -106,5 +112,5 @@ prettyCheckCtx (ts :< (x :- t)) d =
 prettyCheckCtxBinding [<] d = []
 prettyCheckCtxBinding (ts :< (x :- (y ** t))) d =
   (group $ align $ hang 2 $
-    "\\" <+> pretty x <++> pretty y <++> "=>" <+> line <+> prettyCheck t d) ::
+    pretty x <++> pretty y <++> "=>" <+> line <+> prettyCheck t d) ::
   prettyCheckCtxBinding ts d
diff --git a/src/Inky/Thinning.idr b/src/Inky/Thinning.idr
index 87640e2..1627307 100644
--- a/src/Inky/Thinning.idr
+++ b/src/Inky/Thinning.idr
@@ -2,9 +2,10 @@ module Inky.Thinning
 
 import public Inky.Context
 
+import Control.Function
+import Control.WellFounded
 import Data.DPair
 import Data.Nat
-import Control.Function
 
 --------------------------------------------------------------------------------
 -- Thinnings -------------------------------------------------------------------
@@ -252,3 +253,58 @@ lookupLift :
   (f : ctx2 `Thins` ctx3) -> (env : Env ctx1 ctx2 (t ctx2)) -> (i : Var ctx1 v) ->
   lookup (lift f env) i = bimap (index f) (rename f) (lookup env i)
 lookupLift f env i = lookupPosLift f env i.pos
+
+-- Well Founded ----------------------------------------------------------------
+
+export
+Sized (Context a) where
+  size [<] = 0
+  size (ctx :< x) = S (size ctx)
+
+-- Environments ------------------------------------------------------
+
+namespace DEnv
+  public export
+  data DEnv : (0 p : Context a -> a -> Type) -> Context a -> Type where
+    Lin : DEnv p [<]
+    (:<) :
+      DEnv p ctx -> (px : Assoc0 (p ctx x.value)) ->
+      {auto 0 prf : px.name = x.name} ->
+      DEnv p (ctx :< x)
+
+  %name DEnv.DEnv env
+
+  export
+  length : DEnv p ctx -> Length ctx
+  length [<] = Z
+  length (env :< px) = S (length env)
+
+  public export
+  record Entry (p : Context a -> a -> Type) (ctx : Context a) (v : a) where
+    constructor MkEntry
+    {0 support : Context a}
+    0 prf : support `Smaller` ctx
+    thins : support `Thins` ctx
+    value : p support v
+
+  export
+  indexDEnvPos : VarPos ctx x v -> DEnv p ctx -> Entry p ctx v
+  indexDEnvPos Here (env :< px) = MkEntry reflexive (Drop Id) px.value
+  indexDEnvPos (There pos) (env :< px) =
+    let MkEntry prf thins value = indexDEnvPos pos env in
+    MkEntry (lteSuccRight prf) (Drop thins) value
+
+  export
+  indexDEnv' : Var ctx v -> DEnv p ctx -> Entry p ctx v
+  indexDEnv' i env = indexDEnvPos i.pos env
+
+  export
+  indexDEnv : Rename a p => Var ctx v -> DEnv p ctx -> p ctx v
+  indexDEnv i env =
+    let MkEntry _ f x = indexDEnv' i env in
+    rename f x
+
+  export
+  mapProperty : ({0 ctx : Context a} -> {0 v : a} -> p ctx v -> q ctx v) -> DEnv p ctx -> DEnv q ctx
+  mapProperty f [<] = [<]
+  mapProperty f (env :< (x :- px)) = mapProperty f env :< (x :- f px)
diff --git a/src/Inky/Type.idr b/src/Inky/Type.idr
index 9cfc1f7..26f3c0f 100644
--- a/src/Inky/Type.idr
+++ b/src/Inky/Type.idr
@@ -406,3 +406,16 @@ subAll env ((:<) as (x :- a) {fresh}) =
 
 subAllFresh env x [<] = id
 subAllFresh env x (as :< (y :- a)) = andSo . mapSnd (subAllFresh env x as) . soAnd
+
+-- Expansion -------------------------------------------------------------------
+
+export
+expandEnv : DEnv Ty ctx -> Env ctx [<] (Ty [<])
+expandEnv [<] = Base Id
+expandEnv {ctx = ctx :< (x :- v)} (env :< (y :- a)) =
+  let env' = expandEnv env in
+  expandEnv env :< (x :- sub env' a)
+
+export
+expand : DEnv Ty ctx -> Ty ctx v -> Ty [<] v
+expand = sub . expandEnv
diff --git a/src/Inky/Type/Pretty.idr b/src/Inky/Type/Pretty.idr
index 1f2d35b..83253b4 100644
--- a/src/Inky/Type/Pretty.idr
+++ b/src/Inky/Type/Pretty.idr
@@ -19,7 +19,7 @@ prettyType TNat d = pretty "Nat"
 prettyType (TArrow a b) d =
   parenthesise (d > arrowPrec) $ group $ align $ hang 2 $
     let parts = stripArrow b in
-    concatWith (surround $ "->" <+> line) (prettyType a arrowPrec :: parts)
+    concatWith (surround $ neutral <++> "->" <+> line) (prettyType a arrowPrec :: parts)
   where
   stripArrow : Ty ctx () -> List (Doc ann)
   stripArrow (TArrow a b) = prettyType a arrowPrec :: stripArrow b