Add dependent products.

7 files changed, 373 insertions, 141 deletions

diff --git a/src/Obs/Abstract.idr b/src/Obs/Abstract.idr
index 1b72965..0915152 100644
--- a/src/Obs/Abstract.idr
+++ b/src/Obs/Abstract.idr
@@ -33,18 +33,29 @@ printErr (Right x) = pure x
 
 export
 abstractSyntax : Context n -> Syntax -> Error (Term n)
-abstractSyntax ctx (Var b str) = do
-  let Just i = lookup str ctx
-    | Nothing => report b "unbound variable: \{str}"
-  pure (Var b i)
-abstractSyntax ctx (Sort b s) = pure (Sort b s)
+abstractSyntax ctx (Var var) = do
+  let Just i = lookup var.val ctx
+    | Nothing => report var.bounds "unbound variable: \{var.val}"
+  pure (Var var i)
+abstractSyntax ctx (Sort bounds s) = pure (Sort bounds s)
+abstractSyntax ctx (Pi bounds var a b) = do
+  a <- abstractSyntax ctx a
+  b <- abstractSyntax (bind ctx var.val) b
+  pure (Pi bounds var.val a b)
+abstractSyntax ctx (Lambda bounds var t) = do
+  t <- abstractSyntax (bind ctx var.val) t
+  pure (Lambda bounds var.val t)
+abstractSyntax ctx (App t u) = do
+  t <- abstractSyntax ctx t
+  u <- abstractSyntax ctx u
+  pure (App t u)
 abstractSyntax ctx (Top b) = pure (Top b)
 abstractSyntax ctx (Point b) = pure (Point b)
 abstractSyntax ctx (Bottom b) = pure (Bottom b)
-abstractSyntax ctx (Absurd b a t) = do
+abstractSyntax ctx (Absurd bounds a t) = do
   a <- abstractSyntax ctx a
   t <- abstractSyntax ctx t
-  pure (Absurd b a t)
+  pure (Absurd bounds a t)
 
 export
 abstractDefinition : Context n -> Definition -> Error (Definition n)
diff --git a/src/Obs/NormalForm.idr b/src/Obs/NormalForm.idr
index 08354b4..8ee3b19 100644
--- a/src/Obs/NormalForm.idr
+++ b/src/Obs/NormalForm.idr
@@ -18,12 +18,15 @@ data NormalForm  : Nat -> Type
 public export
 data Constructor : Nat -> Type where
   Sort   : Sort -> Constructor n
+  Pi     : Sort -> Sort -> NormalForm n -> NormalForm (S n) -> Constructor n
+  Lambda : NormalForm (S n) -> Constructor n
   Top    : Constructor n
   Bottom : Constructor n
 
 public export
 data Neutral : Nat -> Type where
   Var    : Fin n -> Neutral n
+  App    : Neutral n -> NormalForm n -> Neutral n
   Absurd : Neutral n
 
 public export
@@ -35,7 +38,7 @@ data NormalForm : Nat -> Type where
 public export
 record Definition (n : Nat) where
   constructor MkDefinition
-  name   : Maybe String
+  name   : String
   sort   : Sort
   ty     : NormalForm n
   tm     : NormalForm n
@@ -53,12 +56,15 @@ eqNtrl  : Neutral n -> Neutral n -> Bool
 eqWhnf  : NormalForm n -> NormalForm n -> Bool
 
 eqCnstr (Sort s) (Sort s') = s == s'
-eqCnstr Top      Top       = True
-eqCnstr Bottom   Bottom    = True
+eqCnstr (Pi s s' a b) (Pi l l' a' b') = s == l && s' == l' && eqWhnf a a' && eqWhnf b b'
+eqCnstr (Lambda t) (Lambda u) = eqWhnf t u
+eqCnstr Top Top = True
+eqCnstr Bottom Bottom = True
 eqCnstr _ _ = False
 
 eqNtrl (Var i) (Var j) = i == j
-eqNtrl Absurd  Absurd  = True
+eqNtrl (App t u) (App t' u') = eqNtrl t t' && eqWhnf u u'
+eqNtrl Absurd Absurd = True
 eqNtrl _ _ = False
 
 eqWhnf (Ntrl t)  (Ntrl u)  = eqNtrl t u
@@ -78,6 +84,14 @@ export
 Eq (NormalForm n) where
   t == u = eqWhnf t u
 
+export
+Cast Sort (Constructor n) where
+  cast = Sort
+
+export
+Cast Sort (NormalForm n) where
+  cast = Cnstr . cast
+
 -- Pretty Print ----------------------------------------------------------------
 
 prettyPrecCnstr : Prec -> Constructor n -> Doc ann
@@ -85,10 +99,24 @@ prettyPrecNtrl  : Prec -> Neutral n -> Doc ann
 prettyPrecWhnf  : Prec -> NormalForm n -> Doc ann
 
 prettyPrecCnstr d (Sort s) = prettyPrec d s
+prettyPrecCnstr d (Pi _ _ a b) =
+  parenthesise (d > Open) $
+  group $
+  parens (prettyPrecWhnf Open a) <++>
+  pretty "->" <+> softline <+>
+  prettyPrecWhnf Open b
+prettyPrecCnstr d (Lambda t) =
+  parenthesise (d > Open) $
+  group $
+  backslash <+> softline <+> prettyPrecWhnf Open t
 prettyPrecCnstr d Top = pretty "()"
 prettyPrecCnstr d Bottom = pretty "Void"
 
 prettyPrecNtrl d (Var i) = pretty "$\{show i}"
+prettyPrecNtrl d (App t u) =
+  parenthesise (d >= App) $
+  group $
+  fillSep [prettyPrecNtrl Open t, prettyPrecWhnf App u]
 prettyPrecNtrl d Absurd = pretty "absurd"
 
 prettyPrecWhnf d (Ntrl t)  = prettyPrecNtrl d t
@@ -128,11 +156,14 @@ renameNtrl  : Neutral n -> (Fin n -> Fin m) -> Neutral m
 renameWhnf  : NormalForm n -> (Fin n -> Fin m) -> NormalForm m
 
 renameCnstr (Sort s) f = Sort s
-renameCnstr Top      f = Top
-renameCnstr Bottom   f = Bottom
+renameCnstr (Pi s s' a b) f = Pi s s' (renameWhnf a f) (renameWhnf b $ lift 1 f)
+renameCnstr (Lambda t) f = Lambda (renameWhnf t $ lift 1 f)
+renameCnstr Top f = Top
+renameCnstr Bottom f = Bottom
 
 renameNtrl (Var i) f = Var (f i)
-renameNtrl Absurd  f = Absurd
+renameNtrl (App t u) f = App (renameNtrl t f) (renameWhnf u f)
+renameNtrl Absurd f = Absurd
 
 renameWhnf (Ntrl t)  f = Ntrl $ renameNtrl t f
 renameWhnf (Cnstr t) f = Cnstr $ renameCnstr t f
@@ -150,31 +181,10 @@ export
 Rename NormalForm where
   rename = renameWhnf
 
--- Substitution
-
-substCnstr : Constructor n -> (Fin n -> NormalForm m) -> Constructor m
-substNtrl  : Neutral n -> (Fin n -> NormalForm m) -> NormalForm m
-substWhnf  : NormalForm n -> (Fin n -> NormalForm m) -> NormalForm m
-
-substCnstr (Sort s) f = Sort s
-substCnstr Top      f = Top
-substCnstr Bottom   f = Bottom
-
-substNtrl (Var i) f = f i
-substNtrl Absurd  f = Ntrl Absurd
-
-substWhnf (Ntrl t)  f = substNtrl t f
-substWhnf (Cnstr t) f = Cnstr $ substCnstr t f
-substWhnf Irrel     f = Irrel
-
-export
-Subst Constructor NormalForm Constructor where
-  subst = substCnstr
-
 export
-Subst Neutral NormalForm NormalForm where
-  subst = substNtrl
+PointedRename Neutral where
+  point = Var
 
 export
-Subst NormalForm NormalForm NormalForm where
-  subst = substWhnf
+PointedRename NormalForm where
+  point = Ntrl . point
diff --git a/src/Obs/Parser.idr b/src/Obs/Parser.idr
index 67446bf..c9705fb 100644
--- a/src/Obs/Parser.idr
+++ b/src/Obs/Parser.idr
@@ -36,25 +36,31 @@ data ObsTokenKind
   | OTPOpen
   | OTPClose
   -- Definition characters
+  | OTBackslash
+  | OTThinArrow
+  | OTFatArrow
   | OTEqual
   | OTColon
 
 Eq ObsTokenKind where
   OTNewline == OTNewline = True
-  OTIgnore  == OTIgnore  = True
-  OTIdent   == OTIdent   = True
-  OTProp    == OTProp    = True
-  OTSet     == OTSet     = True
-  OTNat     == OTNat     = True
-  OTUnit    == OTUnit    = True
-  OTPoint   == OTPoint   = True
-  OTVoid    == OTVoid    = True
-  OTAbsurd  == OTAbsurd  = True
-  OTPOpen   == OTPOpen   = True
-  OTPClose  == OTPClose  = True
-  OTEqual   == OTEqual   = True
-  OTColon   == OTColon   = True
-  _         == _         = False
+  OTIgnore == OTIgnore = True
+  OTIdent == OTIdent = True
+  OTProp == OTProp = True
+  OTSet == OTSet = True
+  OTNat == OTNat = True
+  OTUnit == OTUnit = True
+  OTPoint == OTPoint = True
+  OTVoid == OTVoid = True
+  OTAbsurd == OTAbsurd = True
+  OTPOpen == OTPOpen = True
+  OTPClose == OTPClose = True
+  OTBackslash == OTBackslash = True
+  OTThinArrow == OTThinArrow = True
+  OTFatArrow == OTFatArrow = True
+  OTEqual == OTEqual = True
+  OTColon == OTColon = True
+  _ == _ = False
 
 TokenKind ObsTokenKind where
   TokType OTIdent = String
@@ -62,19 +68,22 @@ TokenKind ObsTokenKind where
   TokType _     = ()
 
   tokValue OTNewline s = ()
-  tokValue OTIgnore  s = ()
-  tokValue OTIdent   s = s
-  tokValue OTProp    s = ()
-  tokValue OTSet     s = ()
-  tokValue OTNat     s = stringToNatOrZ s
-  tokValue OTUnit    s = ()
-  tokValue OTPoint   s = ()
-  tokValue OTVoid    s = ()
-  tokValue OTAbsurd  s = ()
-  tokValue OTPOpen   s = ()
-  tokValue OTPClose  s = ()
-  tokValue OTEqual   s = ()
-  tokValue OTColon   s = ()
+  tokValue OTIgnore s = ()
+  tokValue OTIdent s = s
+  tokValue OTProp s = ()
+  tokValue OTSet s = ()
+  tokValue OTNat s = stringToNatOrZ s
+  tokValue OTUnit s = ()
+  tokValue OTPoint s = ()
+  tokValue OTVoid s = ()
+  tokValue OTAbsurd s = ()
+  tokValue OTPOpen s = ()
+  tokValue OTPClose s = ()
+  tokValue OTBackslash s = ()
+  tokValue OTThinArrow s = ()
+  tokValue OTFatArrow s = ()
+  tokValue OTEqual s = ()
+  tokValue OTColon s = ()
 
 ObsToken : Type
 ObsToken = Token ObsTokenKind
@@ -105,6 +114,9 @@ obsTokenMap = toTokenMap [(newline, OTNewline), (spaces, OTIgnore)] ++
   , (exact "*", OTPoint)
   , (exact "(", OTPOpen)
   , (exact ")", OTPClose)
+  , (exact "=>", OTFatArrow)
+  , (exact "->", OTThinArrow)
+  , (exact "\\", OTBackslash)
   , (exact "=", OTEqual)
   , (exact ":", OTColon)
   ]
@@ -121,9 +133,7 @@ ident : Grammar state ObsToken True (WithBounds String)
 ident = bounds $ match OTIdent
 
 var : Grammar state ObsToken True Syntax
-var = do
-  id <- ident <* commit
-  pure (Var id.bounds id.val)
+var = [| Var (ident <* commit) |]
 
 prop : Grammar state ObsToken True Syntax
 prop = do
@@ -161,6 +171,11 @@ set = do
   i <- [| mergeBounds (bounds $ match OTSet) (bounds $ map Set $ option 0 $ match OTNat) |] <* commit
   pure (Sort i.bounds i.val)
 
+lambda : Grammar state ObsToken True (Syntax -> Syntax)
+lambda = do
+  name <- bounds $ match OTBackslash *> commit *> ident <* match OTFatArrow
+  pure (Lambda name.bounds name.val)
+
 botElim : Grammar state ObsToken True (Syntax -> Syntax -> Syntax)
 botElim = do
   absurd <- bounds $ match OTAbsurd <* commit
@@ -168,21 +183,27 @@ botElim = do
 
 -- NOTE: these functions are all total.
 partial
+pi : Grammar state ObsToken True (Syntax -> Syntax)
+partial
 term : Grammar state ObsToken True Syntax
-
 partial
 precGteApp : Grammar state ObsToken True Syntax
-
+partial
+exp' : Grammar state ObsToken True Syntax
 partial
 exp : Grammar state ObsToken True Syntax
+partial
+decl : Grammar state ObsToken True (WithBounds String, Syntax)
+
+pi = do
+  decl <- bounds $ parens decl <* match OTThinArrow <* commit
+  pure (uncurry (Pi decl.bounds) decl.val)
 
 term = atomic <|> parens exp
 precGteApp = atomicNoSet <|> set <|> parens exp
-exp = precGteApp <|> (botElim <*> term <*> term)
-
-partial
-decl : Grammar state ObsToken True (WithBounds String, Syntax)
-decl = [| MkPair ident (commit *> match OTColon *> exp) |]
+exp' = precGteApp <|> (botElim <*> term <*> term)
+exp = (pi <*> exp) <|> (lambda <*> exp) <|> (map (\(t, ts) => foldl1 App (t :: ts)) [| MkPair exp' (many term) |])
+decl = [| MkPair ident (match OTColon *> commit *> exp) |]
 
 partial
 def : Grammar state ObsToken True (WithBounds String, Syntax)
diff --git a/src/Obs/Substitution.idr b/src/Obs/Substitution.idr
index 54df355..340afff 100644
--- a/src/Obs/Substitution.idr
+++ b/src/Obs/Substitution.idr
@@ -5,9 +5,39 @@ import Data.Fin
 %default total
 
 public export
-interface Rename (x : Nat -> Type) where
+interface Rename (0 x : Nat -> Type) where
   rename : forall m, n . x n -> (Fin n -> Fin m) -> x m
 
 public export
-interface Subst (x, y, z : Nat -> Type) where
+interface Rename x => PointedRename x where
+  point : forall n . Fin n -> x n
+
+public export
+interface Subst (0 x, y, z : Nat -> Type) where
   subst : forall m, n . x n -> (Fin n -> y m) -> z m
+
+public export
+Rename x => Subst x Fin x where
+  subst = rename
+
+public export
+Rename Fin where
+  rename i f = f i
+
+public export
+PointedRename Fin where
+  point = id
+
+public export
+add : (0 x : _) -> x n -> (Fin m -> x n) -> Fin (S m) -> x n
+add x v f FZ     = v
+add x v f (FS i) = f i
+
+public export
+lift : PointedRename x => (k : _) -> (Fin m -> x n) -> Fin (k + m) -> x (k + n)
+lift 0     f = f
+lift (S k) f = add x (point FZ) (\i => rename (lift k f i) FS)
+
+public export
+weaken : Rename x => (m : _) -> x n -> x (m + n)
+weaken m t = rename t (shift m)
diff --git a/src/Obs/Syntax.idr b/src/Obs/Syntax.idr
index 6b95910..4a7ee0c 100644
--- a/src/Obs/Syntax.idr
+++ b/src/Obs/Syntax.idr
@@ -11,9 +11,13 @@ import Text.PrettyPrint.Prettyprinter
 
 public export
 data Syntax : Type where
-  Var    : Bounds -> String -> Syntax
+  Var    : WithBounds String -> Syntax
   -- Sorts
   Sort   : Bounds -> Sort -> Syntax
+  -- Dependent Products
+  Pi     : Bounds -> WithBounds String -> Syntax -> Syntax -> Syntax
+  Lambda : Bounds -> WithBounds String -> Syntax -> Syntax
+  App    : Syntax -> Syntax -> Syntax
   -- True
   Top    : Bounds -> Syntax
   Point  : Bounds -> Syntax
@@ -33,14 +37,30 @@ record Definition where
 
 export
 Pretty Syntax where
-  prettyPrec d (Var x str) = pretty str
-  prettyPrec d (Sort x s) = prettyPrec d s
-  prettyPrec d (Top x) = pretty "()"
-  prettyPrec d (Point x) = pretty "*"
-  prettyPrec d (Bottom x) = pretty "Void"
-  prettyPrec d (Absurd x a t) =
+  prettyPrec d (Var var) = pretty var.val
+  prettyPrec d (Sort _ s) = prettyPrec d s
+  prettyPrec d (Pi _ var a b) =
     parenthesise (d > Open) $
     group $
+    parens (pretty var.val <++> colon <+> softline <+> prettyPrec Open a) <++>
+    pretty "->" <+> softline <+>
+    prettyPrec Open b
+  prettyPrec d (Lambda _ var t) =
+    parenthesise (d > Open) $
+    group $
+    backslash <+> pretty var.val <++>
+    pretty "=>" <+> softline <+>
+    prettyPrec Open t
+  prettyPrec d (App t u) =
+    parenthesise (d >= App) $
+    group $
+    fillSep [prettyPrec Open t, prettyPrec App u]
+  prettyPrec d (Top _) = pretty "()"
+  prettyPrec d (Point _) = pretty "*"
+  prettyPrec d (Bottom _) = pretty "Void"
+  prettyPrec d (Absurd _ a t) =
+    parenthesise (d >= App) $
+    group $
     fillSep [pretty "absurd", prettyPrec App a, prettyPrec App t]
 
 export
diff --git a/src/Obs/Term.idr b/src/Obs/Term.idr
index 05b9a7f..366a4b7 100644
--- a/src/Obs/Term.idr
+++ b/src/Obs/Term.idr
@@ -12,9 +12,13 @@ import Text.PrettyPrint.Prettyprinter
 
 public export
 data Term : Nat -> Type where
-  Var    : Bounds -> Fin n -> Term n
+  Var    : WithBounds String -> Fin n -> Term n
   -- Sorts
   Sort   : Bounds -> Sort -> Term n
+  -- Dependent Product
+  Pi     : Bounds -> String -> Term n -> Term (S n) -> Term n
+  Lambda : Bounds -> String -> Term (S n) -> Term n
+  App    : Term n -> Term n -> Term n
   -- True
   Top    : Bounds -> Term n
   Point  : Bounds -> Term n
@@ -39,23 +43,42 @@ data Block : Nat -> Type where
 
 export
 fullBounds : Term n -> WithBounds (Term n)
-fullBounds tm@(Var x i)      = MkBounded tm False x
-fullBounds tm@(Sort x s)     = MkBounded tm False x
-fullBounds tm@(Top x)        = MkBounded tm False x
-fullBounds tm@(Point x)      = MkBounded tm False x
-fullBounds tm@(Bottom x)     = MkBounded tm False x
+fullBounds tm@(Var var i) = map (\_ => tm) var
+fullBounds tm@(Sort x s) = MkBounded tm False x
+fullBounds tm@(Pi x var a b) = mergeBounds (mergeBounds (fullBounds a) (fullBounds b)) (MkBounded tm False x)
+fullBounds tm@(Lambda x var t) = mergeBounds (fullBounds t) (MkBounded tm False x)
+fullBounds tm@(App t u) = map (\_ => tm) (mergeBounds (fullBounds t) (fullBounds u))
+fullBounds tm@(Top x) = MkBounded tm False x
+fullBounds tm@(Point x) = MkBounded tm False x
+fullBounds tm@(Bottom x) = MkBounded tm False x
 fullBounds tm@(Absurd x a t) = mergeBounds (mergeBounds (fullBounds a) (fullBounds t)) (MkBounded tm False x)
 
 -- Pretty Print ----------------------------------------------------------------
 
 export
 Pretty (Term n) where
-  prettyPrec d (Var x i) = pretty "$\{show i}"
-  prettyPrec d (Sort x s) = prettyPrec d s
-  prettyPrec d (Top x) = pretty "()"
-  prettyPrec d (Point x) = pretty "*"
-  prettyPrec d (Bottom x) = pretty "Void"
-  prettyPrec d (Absurd x a t) =
+  prettyPrec d (Var var _) = pretty var.val
+  prettyPrec d (Sort _ s) = prettyPrec d s
+  prettyPrec d (Pi _ var a b) =
+    parenthesise (d > Open) $
+    group $
+    parens (pretty var <++> colon <+> softline <+> prettyPrec Open a) <++>
+    pretty "->" <+> softline <+>
+    prettyPrec Open b
+  prettyPrec d (Lambda _ var t) =
+    parenthesise (d > Open) $
+    group $
+    backslash <+> pretty var <++>
+    pretty "=>" <+> softline <+>
+    prettyPrec Open t
+  prettyPrec d (App t u) =
+    parenthesise (d >= App) $
+    group $
+    fillSep [prettyPrec Open t, prettyPrec App u]
+  prettyPrec d (Top _) = pretty "()"
+  prettyPrec d (Point _) = pretty "*"
+  prettyPrec d (Bottom _) = pretty "Void"
+  prettyPrec d (Absurd _ a t) =
     parenthesise (d > Open) $
     group $
     fillSep [pretty "absurd", prettyPrec App a, prettyPrec App t]
diff --git a/src/Obs/Typing.idr b/src/Obs/Typing.idr
index e59de5d..e23a9a2 100644
--- a/src/Obs/Typing.idr
+++ b/src/Obs/Typing.idr
@@ -15,91 +15,208 @@ import Text.PrettyPrint.Prettyprinter.Render.Terminal
 
 %default total
 
+-- Errors ----------------------------------------------------------------------
+
+export
+Error : Type -> Type -> Type
+Error ann = Either (Maybe Bounds, Doc ann)
+
+export
+printErr : Error ? a -> IO a
+printErr (Left (Just b, p)) = do
+  () <- putDoc (pretty "typing: \{show b.startLine}:\{show b.startCol}-\{show b.endLine}:\{show b.endCol}:" <+> softline <+> p)
+  exitFailure
+printErr (Left (Nothing, p)) = do
+  () <- putDoc (pretty "typing:" <+> softline <+> p)
+  exitFailure
+printErr (Right x) = pure x
+
+report : Bounds -> Doc ann -> Error ann a
+report = curry Left . Just
+
+internal : Doc ann -> Error ann a
+internal = Left . (Nothing, )
+
+Rename (Error ann . NormalForm) where
+  rename t f = pure $ rename !t f
+
+PointedRename (Error ann . NormalForm) where
+  point = pure . point
+
+-- Substitution ----------------------------------------------------------------
+
+wkn : (k : _) -> (Fin n -> Error ann (NormalForm m)) -> Fin (k + n) -> Error ann (NormalForm (k + m))
+wkn = lift {x = Error ann . NormalForm}
+
+covering partial
+substCnstr : Constructor n -> (Fin n -> Error ann (NormalForm m)) -> Error ann (Constructor m)
+covering partial
+substNtrl  : Neutral n -> (Fin n -> Error ann (NormalForm m)) -> Error ann (NormalForm m)
+covering partial
+subst      : NormalForm n -> (Fin n -> Error ann (NormalForm m)) -> Error ann (NormalForm m)
+covering partial
+doApp      : NormalForm n -> NormalForm n -> Error ann (NormalForm n)
+
+substCnstr (Sort s) f = pure $ Sort s
+substCnstr (Pi s s' a b) f = do
+  a <- subst a f
+  b <- subst b (wkn 1 f)
+  pure (Pi s s' a b)
+substCnstr (Lambda t) f = do
+  t <- subst t (wkn 1 f)
+  pure (Lambda t)
+substCnstr Top f = pure $ Top
+substCnstr Bottom  f = pure $ Bottom
+
+substNtrl (Var i) f = f i
+substNtrl (App t u) f = do
+  t <- substNtrl t f
+  u <- subst u f
+  doApp t u
+substNtrl Absurd f = pure $ Ntrl Absurd
+
+subst (Ntrl t)  f = substNtrl t f
+subst (Cnstr t) f = map Cnstr $ substCnstr t f
+subst Irrel     f = pure Irrel
+
+doApp (Ntrl t) u = pure $ Ntrl (App t u)
+doApp Irrel u = pure $ Irrel
+doApp (Cnstr (Lambda t)) u = subst t (add (Error ann . NormalForm) (pure u) (pure . point))
+doApp (Cnstr t) u = internal (pretty "wrong constructor in apply:" <++> pretty t)
+
+partial
+subst1 : NormalForm n -> NormalForm (S n) -> Error ann (NormalForm n)
+subst1 t u = subst u (add (Error ann . NormalForm) (pure t) (pure . point))
+
 -- Conversion ------------------------------------------------------------------
 
 -- invariant: all definitions fully expanded
 -- invariant: m |- t, u <- a : s
-convert : (t, u, a : NormalForm n) -> Sort -> Bool
+covering partial
+convert : (t, u, a : NormalForm n) -> Sort -> Error ann Bool
 -- In sort Prop
-convert Irrel Irrel a Prop = True
+convert Irrel Irrel a Prop = pure True
 -- In unknown type in set
-convert t u (Ntrl _) (Set k) = t == u
+convert t u (Ntrl _) (Set k) = pure $ t == u
 -- In type Set
-convert (Cnstr (Sort s')) (Cnstr (Sort s'')) (Cnstr (Sort _)) (Set _) = s' == s''
-convert (Cnstr Top) (Cnstr Top) (Cnstr (Sort _)) (Set _) = True
-convert (Cnstr Bottom) (Cnstr Bottom) (Cnstr (Sort _)) (Set _) = True
-convert (Ntrl t) u (Cnstr (Sort s)) (Set k) = Ntrl t == u
-convert t (Ntrl u) (Cnstr (Sort s)) (Set k) = t == Ntrl u
+convert (Cnstr (Sort s')) (Cnstr (Sort s'')) (Cnstr (Sort _)) (Set _) = pure $ s' == s''
+convert (Cnstr (Pi s s' a b)) (Cnstr (Pi l l' a' b')) (Cnstr (Sort _)) (Set _) =
+  pure $
+  s == l && s' == l' && !(convert a a' (cast s) (suc s)) && !(convert b b' (cast s') (suc s'))
+convert (Cnstr Top) (Cnstr Top) (Cnstr (Sort _)) (Set _) = pure True
+convert (Cnstr Bottom) (Cnstr Bottom) (Cnstr (Sort _)) (Set _) = pure True
+convert (Ntrl t) u (Cnstr (Sort s)) (Set k) = pure $ Ntrl t == u
+convert t (Ntrl u) (Cnstr (Sort s)) (Set k) = pure $ t == Ntrl u
+convert t u (Cnstr (Sort s)) (Set k) = pure $ False
+-- In type Pi
+convert t u (Cnstr (Pi s s' a b)) (Set k) = do
+  t <- doApp (weaken 1 t) (point FZ)
+  u <- doApp (weaken 1 u) (point FZ)
+  convert t u b s'
 -- Default
-convert _ _ _ _ = False
+convert t u a s = internal $ fillSep ["invalid convert:", prettyPrec App t, prettyPrec App u, prettyPrec App a, prettyPrec App s]
+
 
 -- Typing Contexts -------------------------------------------------------------
 
-weaken : (m : _) -> NormalForm n -> NormalForm (m + n)
-weaken m t = rename t (shift m)
+infix 5 ::<
 
-index : Context n -> Fin n -> (NormalForm n, NormalForm n, Sort)
-index (ctx :< def) FZ     = bimap (weaken 1) (mapFst (weaken 1)) (def.tm, def.ty, def.sort)
-index (ctx :< def) (FS i) = bimap (weaken 1) (mapFst (weaken 1)) $ index ctx i
+data TyContext : Nat -> Nat -> Type where
+  Nil   : TyContext 0 0
+  (:<)  : TyContext m n -> NormalForm.Definition n -> TyContext m (S n)
+  (::<) : TyContext m n -> (String, NormalForm n, Sort) -> TyContext (S m) (S n)
 
-asSubst : Context n -> Fin n -> NormalForm 0
-asSubst (ctx :< def) FZ     = subst def.tm (asSubst ctx)
-asSubst (ctx :< def) (FS i) = asSubst ctx i
+fromContext : Context n -> TyContext 0 n
+fromContext []           = []
+fromContext (ctx :< def) = fromContext ctx :< def
 
--- Checking and Inference ------------------------------------------------------
+countVars : TyContext m n -> Fin (S n)
+countVars []          = FZ
+countVars (ctx :< y)  = weaken $ countVars ctx
+countVars (ctx ::< y) = FS $ countVars ctx
 
-export
-Error : Type -> Type -> Type
-Error ann = Either (Bounds, Doc ann)
+index : TyContext m n -> Fin n -> (NormalForm n, NormalForm n, Sort)
+index (ctx :< def)         FZ     = (weaken 1 def.tm, weaken 1 def.ty, def.sort)
+index (ctx ::< (_, ty, s)) FZ     = (point FZ, weaken 1 ty, s)
+index (ctx :< _)           (FS i) = bimap (weaken 1) (mapFst (weaken 1)) $ index ctx i
+index (ctx ::< _)          (FS i) = bimap (weaken 1) (mapFst (weaken 1)) $ index ctx i
 
-export
-printErr : Error ? a -> IO a
-printErr (Left (b, p)) = do
-  () <- putDoc (pretty "typing: \{show b.startLine}:\{show b.startCol}-\{show b.endLine}:\{show b.endCol}:" <+> softline <+> p)
-  exitFailure
-printErr (Right x) = pure x
+covering partial
+asSubst : (ctx : TyContext m n) -> Fin n -> Error ann (NormalForm m)
+asSubst (ctx :< def) FZ     = subst def.tm (asSubst ctx)
+asSubst (ctx ::< _)  FZ     = pure $ point FZ
+asSubst (ctx :< def) (FS i) = asSubst ctx i
+asSubst (ctx ::< _)  (FS i) = map (weaken 1) (asSubst ctx i)
 
-report : Bounds -> Doc ann -> Error ann a
-report = curry Left
-  
-check : Context n -> Term n -> NormalForm n -> Sort -> Error ann (NormalForm n)
-infer : Context n -> Term n -> Error ann (NormalForm n, NormalForm n, Sort)
+-- Checking and Inference ------------------------------------------------------
 
+covering partial
+check : TyContext m n -> Term n -> NormalForm n -> Sort -> Error ann (NormalForm n)
+covering partial
+infer : TyContext m n -> Term n -> Error ann (NormalForm n, NormalForm n, Sort)
+covering partial
+inferSort : {default "type mismatch" tag : String}
+  -> TyContext m n -> Term n -> Error ann (NormalForm n, Sort)
+
+check ctx (Lambda _ var t) (Cnstr (Pi s s' a b)) _ = do
+  t <- check (ctx ::< (var, a, s)) t b s'
+  pure (Cnstr $ Lambda t)
+check ctx tm@(Lambda _ _ _) ty _ =
+  report (fullBounds tm).bounds
+    (pretty "type mismatch: expected pi" <+> comma <+> softline <+> "got" <++> pretty ty)
 check ctx tm ty s = do
   let bounds = (fullBounds tm).bounds
   (tm, ty', s') <- infer ctx tm
   let True = s == s'
     | False => report bounds
       (pretty "sort mismatch: expected" <++> pretty s <+> comma <+> softline <+> "got" <++> pretty s')
-  let True = convert (subst ty $ asSubst ctx) (subst ty' $ asSubst ctx) (Cnstr (Sort s)) (suc s)
+  True <- convert !(subst ty $ asSubst ctx) !(subst ty' $ asSubst ctx) (cast s) (suc s)
     | False => report bounds
       (pretty "type mismatch: expected" <++> pretty ty <+> comma <+> softline <+> "got" <++> pretty ty')
   pure tm
 
 infer ctx (Var b i) = pure $ index ctx i
-infer ctx (Sort b s) = pure $ (Cnstr (Sort s), Cnstr (Sort (suc s)), suc (suc s))
-infer ctx (Top b) = pure $ (Cnstr Top, Cnstr (Sort Prop), Set 0)
+infer ctx (Sort b s) = pure $ (cast s, cast (suc s), suc (suc s))
+infer ctx (Pi _ var a b) = do
+  (a, s) <- inferSort ctx a
+  let aDef = MkDefinition {name = var, sort = suc s, ty = cast s, tm = a}
+  (b, s') <- inferSort (ctx :< aDef) b
+  pure (Cnstr (Pi s s' a b), cast (s ~> s'), suc (s ~> s'))
+infer ctx tm@(Lambda _ _ _) = report (fullBounds tm).bounds (pretty "cannot infer type:" <+> softline <+> pretty tm)
+infer ctx (App t u) = do
+  let bounds = (fullBounds t).bounds
+  (t, Cnstr (Pi s s' a b), _) <- infer ctx t
+    | (_, t, _) => report bounds (pretty "wrong type to apply:" <+> softline <+> pretty t)
+  u <- check ctx u a s
+  res <- doApp t u
+  ty <- subst1 t b
+  pure (res, ty, s')
+infer ctx (Top b) = pure $ (Cnstr Top, cast Prop, Set 0)
 infer ctx (Point b) = pure $ (Irrel, Cnstr Top, Prop)
-infer ctx (Bottom b) = pure $ (Cnstr Bottom, Cnstr (Sort Prop), Set 0)
+infer ctx (Bottom b) = pure $ (Cnstr Bottom, cast Prop, Set 0)
 infer ctx (Absurd b a t) = do
-  (a, Cnstr (Sort s), _) <- infer ctx a
-    | (_, ty, _) => report (fullBounds a).bounds
-      (pretty "type mismatch: expected sort" <+> comma <+> softline <+> "got" <++> pretty ty)
+  (a, s) <- inferSort ctx a
   _ <- check ctx t (Cnstr Bottom) Prop
   pure (Ntrl Absurd, a, s)
 
+inferSort ctx a = do
+  (a, Cnstr (Sort s), _) <- infer ctx a
+    | (_, ty, _) => report (fullBounds a).bounds
+      (pretty "\{tag}: expected sort" <+> comma <+> softline <+> "got" <++> pretty ty)
+  pure (a, s)
+
 -- Checking Definitions and Blocks ---------------------------------------------
 
+covering partial
 checkDef : Context n -> Term.Definition n -> Error ann (NormalForm.Definition n)
 checkDef ctx def = do
   let tyBounds = (fullBounds def.ty).bounds
   let tmBounds = (fullBounds def.tm).bounds
-  (ty, Cnstr (Sort sort), _) <- infer ctx def.ty
-    | (_, a, _) => report tyBounds
-      (pretty "invalid declaration: expected sort" <+> comma <+> softline <+> "got" <++> pretty a)
-  tm <- check ctx def.tm ty sort
-  pure $ MkDefinition {name = Just def.name, ty, tm, sort}
+  (ty, sort) <- inferSort {tag = "invalid declaration"} (fromContext ctx) def.ty
+  tm <- check (fromContext ctx) def.tm ty sort
+  pure $ MkDefinition {name = def.name, ty, tm, sort}
 
+covering partial
 export
 checkBlock : Block n -> Error ann (Context n)
 checkBlock [] = pure []