Add more program structure to abstract terms.

Add more program structure to type inference and checking.

8 files changed, 478 insertions, 368 deletions

diff --git a/obs.ipkg b/obs.ipkg
index df5db66..0679395 100644
--- a/obs.ipkg
+++ b/obs.ipkg
@@ -14,6 +14,7 @@ modules
   , Obs.NormalForm
   , Obs.NormalForm.Normalise
   , Obs.Parser
+  , Obs.Pretty
   , Obs.Substitution
   , Obs.Syntax
   , Obs.Term
diff --git a/src/Obs/Abstract.idr b/src/Obs/Abstract.idr
index f91be66..039f60e 100644
--- a/src/Obs/Abstract.idr
+++ b/src/Obs/Abstract.idr
@@ -24,74 +24,75 @@ abstractSyntaxBounds : Context n -> WithBounds Syntax -> Logging ann (WithBounds
 abstractSyntax ctx (Var {var}) = do
   let Just i = lookup var ctx
     | Nothing => inScope "unbound variable" $ fatal var
-  pure (Var var i)
-abstractSyntax ctx (Universe {s}) = pure (Universe s)
+  pure (Var {var, i})
+abstractSyntax ctx (Universe {s}) = pure (Universe {s})
 abstractSyntax ctx (Pi {var, domain, codomain}) = do
-  a <- abstractSyntaxBounds ctx domain
-  b <- abstractSyntaxBounds (bind ctx var.val) codomain
-  pure (Pi var a b)
+  domain <- abstractSyntaxBounds ctx domain
+  codomain <- abstractSyntaxBounds (bind ctx var.val) codomain
+  pure (Pi {var, domain, codomain})
 abstractSyntax ctx (Lambda {var, body}) = do
-  t <- abstractSyntaxBounds (bind ctx var.val) body
-  pure (Lambda var t)
+  body <- abstractSyntaxBounds (bind ctx var.val) body
+  pure (Lambda {var, body})
 abstractSyntax ctx (App {fun, arg}) = do
-  t <- abstractSyntaxBounds ctx fun
-  u <- abstractSyntaxBounds ctx arg
-  pure (App t u)
+  fun <- abstractSyntaxBounds ctx fun
+  arg <- abstractSyntaxBounds ctx arg
+  pure (App {fun, arg})
 abstractSyntax ctx (Sigma {var, index, element}) = do
-  a <- abstractSyntaxBounds ctx index
-  b <- abstractSyntaxBounds (bind ctx var.val) element
-  pure (Sigma var a b)
+  index <- abstractSyntaxBounds ctx index
+  element <- abstractSyntaxBounds (bind ctx var.val) element
+  pure (Sigma {var, index, element})
 abstractSyntax ctx (Pair {first, second}) = do
-  t <- abstractSyntaxBounds ctx first
-  u <- abstractSyntaxBounds ctx second
-  pure (Pair t u)
+  first <- abstractSyntaxBounds ctx first
+  second <- abstractSyntaxBounds ctx second
+  pure (Pair {first, second})
 abstractSyntax ctx (First {arg}) = do
-  t <- abstractSyntaxBounds ctx arg
-  pure (Fst t)
+  arg <- abstractSyntaxBounds ctx arg
+  pure (First {arg})
 abstractSyntax ctx (Second {arg}) = do
-  t <- abstractSyntaxBounds ctx arg
-  pure (Snd t)
+  arg <- abstractSyntaxBounds ctx arg
+  pure (Second {arg})
 abstractSyntax ctx Bool = pure Bool
 abstractSyntax ctx True = pure True
 abstractSyntax ctx False = pure False
 abstractSyntax ctx (If {var, returnType, discriminant, true, false}) = do
-  a <- abstractSyntaxBounds (bind ctx var.val) returnType
-  t <- abstractSyntaxBounds ctx discriminant
-  f <- abstractSyntaxBounds ctx true
-  g <- abstractSyntaxBounds ctx false
-  pure (If var a t f g)
+  returnType <- abstractSyntaxBounds (bind ctx var.val) returnType
+  discriminant <- abstractSyntaxBounds ctx discriminant
+  true <- abstractSyntaxBounds ctx true
+  false <- abstractSyntaxBounds ctx false
+  pure (If {var, returnType, discriminant, true, false})
 abstractSyntax ctx Top = pure Top
 abstractSyntax ctx Point = pure Point
 abstractSyntax ctx Bottom = pure Bottom
 abstractSyntax ctx (Absurd {contradiction}) = do
-  t <- abstractSyntaxBounds ctx contradiction
-  pure (Absurd t)
+  contradiction <- abstractSyntaxBounds ctx contradiction
+  pure (Absurd {contradiction})
 abstractSyntax ctx (Equal {left, right}) = do
-  t <- abstractSyntaxBounds ctx left
-  u <- abstractSyntaxBounds ctx right
-  pure (Equal t u)
+  left <- abstractSyntaxBounds ctx left
+  right <- abstractSyntaxBounds ctx right
+  pure (Equal {left, right})
 abstractSyntax ctx (Refl {value}) = do
-  t <- abstractSyntaxBounds ctx value
-  pure (Refl t)
+  value <- abstractSyntaxBounds ctx value
+  pure (Refl {value})
 abstractSyntax ctx (Transp {indexedType, oldIndex, value, newIndex, equality}) = do
-  a <- abstractSyntaxBounds ctx indexedType
-  t <- abstractSyntaxBounds ctx oldIndex
-  u <- abstractSyntaxBounds ctx value
-  t' <- abstractSyntaxBounds ctx newIndex
-  e <- abstractSyntaxBounds ctx equality
-  pure (Transp a t u t' e)
+  indexedType <- abstractSyntaxBounds ctx indexedType
+  oldIndex <- abstractSyntaxBounds ctx oldIndex
+  value <- abstractSyntaxBounds ctx value
+  newIndex <- abstractSyntaxBounds ctx newIndex
+  equality <- abstractSyntaxBounds ctx equality
+  pure (Transp {indexedType, oldIndex, value, newIndex, equality})
 abstractSyntax ctx (Cast {oldType, newType, equality, value}) = do
-  a <- abstractSyntaxBounds ctx oldType
-  b <- abstractSyntaxBounds ctx newType
-  e <- abstractSyntaxBounds ctx equality
-  t <- abstractSyntaxBounds ctx value
-  pure (Cast a b e t)
+  oldType <- abstractSyntaxBounds ctx oldType
+  newType <- abstractSyntaxBounds ctx newType
+  equality <- abstractSyntaxBounds ctx equality
+  value <- abstractSyntaxBounds ctx value
+  pure (Cast {oldType, newType, equality, value})
 abstractSyntax ctx (CastId {value}) = do
-  t <- abstractSyntaxBounds ctx value
-  pure (CastId t)
+  value <- abstractSyntaxBounds ctx value
+  pure (CastId {value})
 
-abstractSyntaxBounds ctx (MkBounded v irrel bnds) =
-  pure $ MkBounded !(abstractSyntax ctx v) irrel bnds
+abstractSyntaxBounds ctx val@(MkBounded v irrel bnds) = do
+  term <- inBounds $ (MkBounded (abstractSyntax ctx v) irrel bnds)
+  pure $ map (const term) val
 
 abstractDefinition : Context n -> Definition -> Logging ann (Definition n)
 abstractDefinition ctx def = pure $ MkDefinition
diff --git a/src/Obs/Logging.idr b/src/Obs/Logging.idr
index ef0bae6..5666001 100644
--- a/src/Obs/Logging.idr
+++ b/src/Obs/Logging.idr
@@ -126,8 +126,11 @@ inScope : (tag : String) -> Logging ann a -> Logging ann a
 inScope tag = mapMsg {tags $= (tag ::)}
 
 export
-inBounds : Bounds -> Logging ann a -> Logging ann a
-inBounds bounds = mapMsg {bounds $= maybe (Just bounds) Just}
+inBounds : WithBounds (Logging ann a) -> Logging ann a
+inBounds msg =
+  let map : Logging ann a -> Logging ann a
+      map = if msg.isIrrelevant then id else mapMsg {bounds $= maybe (Just msg.bounds) Just}
+  in map msg.val
 
 public export
 interface Loggable (0 ann, ty : Type) where
diff --git a/src/Obs/Parser.idr b/src/Obs/Parser.idr
index 8eea42c..68591ee 100644
--- a/src/Obs/Parser.idr
+++ b/src/Obs/Parser.idr
@@ -424,7 +424,8 @@ castErr : Either (List1 (ParsingError tok)) a -> Logging ann a
 castErr (Right x) = pure x
 castErr (Left errs) = do
   for_ {b = ()} errs
-    (\(Error msg bounds) => maybe id inBounds bounds $ error msg)
+    (\(Error msg bounds) =>
+      inBounds $ map error $ maybe (irrelevantBounds msg) (MkBounded msg True) bounds)
   abort
 
 partial
diff --git a/src/Obs/Pretty.idr b/src/Obs/Pretty.idr
new file mode 100644
index 0000000..52a358c
--- /dev/null
+++ b/src/Obs/Pretty.idr
@@ -0,0 +1,42 @@
+module Obs.Pretty
+
+import public Text.PrettyPrint.Prettyprinter
+
+-- ty is rendered Open
+export
+prettyDecl : (name : String) -> (ty : Doc ann) -> Doc ann
+prettyDecl name ty = parens $ group (pretty name <++> colon <+> line <+> align ty)
+
+-- ty and tail are rendered Open
+export
+prettyDeclForm : (prec : Prec) ->
+  (name : String) ->
+  (ty : Doc ann) ->
+  (sep : String) ->
+  (tail : Doc ann) ->
+  Doc ann
+prettyDeclForm d name ty sep tail =
+  parenthesise (d > Open) $ group $ vsep $ [prettyDecl name ty <++> pretty sep, align tail]
+
+-- body is rendered Open
+export
+prettyLambda : (prec : Prec) -> (name : String) -> (body : Doc ann) -> Doc ann
+prettyLambda d name body =
+  parenthesise (d >= App) $ group $ vsep [backslash <+> pretty name <++> pretty "=>", align body]
+
+-- head is rendered Open, tail are rendered App
+export
+prettyApp : (prec : Prec) -> (head : Doc ann) -> (tail : List (Doc ann)) -> Doc ann
+prettyApp d head tail = parenthesise (d >= App) $ group $ vsep (align head :: map (hang 2) tail)
+
+-- first and second are rendered Open
+export
+prettyPair : (first, second : Doc ann) -> Doc ann
+prettyPair first second =
+  angles $ group (neutral <++> align first <+> comma <+> line <+> align second <++> neutral)
+
+-- left and right are rendered Equal
+export
+prettyEqual : (prec : Prec) -> (left, right : Doc ann) -> Doc ann
+prettyEqual d left right =
+  parenthesise (d >= Equal) $ group $ vsep [align left <++> pretty "~", align right]
diff --git a/src/Obs/Syntax.idr b/src/Obs/Syntax.idr
index a8a468c..a141d28 100644
--- a/src/Obs/Syntax.idr
+++ b/src/Obs/Syntax.idr
@@ -1,10 +1,10 @@
 ||| Raw syntax for terms. This is before eliminating names.
 module Obs.Syntax
 
+import Obs.Pretty
 import Obs.Universe
 
 import Text.Bounded
-import Text.PrettyPrint.Prettyprinter
 
 %default total
 
@@ -53,33 +53,9 @@ record Definition where
 
 -- Pretty Print ----------------------------------------------------------------
 
-prettyDecl : (name : String) -> (ty : Doc ann) -> Doc ann
-prettyDecl name ty = parens $ group (pretty name <++> colon <+> line <+> align ty)
-
-prettyDeclForm : (prec : Prec) ->
-  (name : String) ->
-  (ty : Doc ann) ->
-  (sep : String) ->
-  (tail : Doc ann) ->
-  Doc ann
-prettyDeclForm d name ty sep tail =
-  parenthesise (d > Open) $
-  group $
-  vsep $
-  [prettyDecl name ty <++> pretty sep, align tail]
-
-prettyLambda : (prec : Prec) -> (name : String) -> (body : Doc ann) -> Doc ann
-prettyLambda d name body =
-  parenthesise (d >= App) $
-  group $
-  backslash <+> pretty name <++> pretty "=>" <+> line <+> align body
-
-prettyApp : (prec : Prec) -> (head : Doc ann) -> (tail : List (Doc ann)) -> Doc ann
-prettyApp d head tail = parenthesise (d >= App) $ group $ vsep (align head :: map (hang 2) tail)
-
-prettyPrec : Prec -> Syntax -> Doc ann
 prettyPrecBounds : Prec -> WithBounds Syntax -> Doc ann
 
+prettyPrec : Prec -> Syntax -> Doc ann
 prettyPrec d (Var {var}) = pretty var
 prettyPrec d (Universe {s}) = prettyPrec d s
 prettyPrec d (Pi {var, domain, codomain}) =
@@ -89,14 +65,7 @@ prettyPrec d (App {fun, arg}) = prettyApp d (prettyPrecBounds Open fun) [prettyP
 prettyPrec d (Sigma {var, index, element}) =
   prettyDeclForm d var.val (prettyPrecBounds Open index) "**" (prettyPrecBounds Open element)
 prettyPrec d (Pair {first, second}) =
-  angles $
-  group $
-  neutral <++>
-  align (prettyPrecBounds Open first) <+>
-  comma <+>
-  line <+>
-  align (prettyPrecBounds Open second) <++>
-  neutral
+  prettyPair (prettyPrecBounds Open first) (prettyPrecBounds Open second)
 prettyPrec d (First {arg}) = prettyApp d (pretty "fst") [prettyPrecBounds App arg]
 prettyPrec d (Second {arg}) = prettyApp d (pretty "snd") [prettyPrecBounds App arg]
 prettyPrec d Bool = pretty "Bool"
@@ -115,12 +84,7 @@ prettyPrec d Bottom = pretty "Void"
 prettyPrec d (Absurd {contradiction}) =
   prettyApp d (pretty "absurd") [prettyPrecBounds App contradiction]
 prettyPrec d (Equal {left, right}) =
-  parenthesise (d >= Equal) $
-  group $
-  align (prettyPrecBounds Equal left) <++>
-  pretty "~" <+>
-  line <+>
-  align (prettyPrecBounds Equal right)
+  prettyEqual d (prettyPrecBounds Equal left) (prettyPrecBounds Equal right)
 prettyPrec d (Refl {value}) = prettyApp d (pretty "refl") [prettyPrecBounds App value]
 prettyPrec d (Transp {indexedType, oldIndex, value, newIndex, equality}) =
   prettyApp d (pretty "transp") $
diff --git a/src/Obs/Term.idr b/src/Obs/Term.idr
index c4d9e40..95ed08b 100644
--- a/src/Obs/Term.idr
+++ b/src/Obs/Term.idr
@@ -2,9 +2,11 @@
 module Obs.Term
 
 import Data.Fin
+
+import Obs.Pretty
 import Obs.Universe
+
 import Text.Bounded
-import Text.PrettyPrint.Prettyprinter
 
 %default total
 
@@ -12,56 +14,51 @@ import Text.PrettyPrint.Prettyprinter
 
 public export
 data Term : Nat -> Type where
-  Var : String -> Fin n -> Term n
+  Var : (var : String) -> (i : Fin n) -> Term n
   -- Universes
-  Universe : Universe -> Term n
+  Universe : (s : Universe) -> Term n
   -- Dependent Product
-  Pi : WithBounds String -> WithBounds (Term n) -> WithBounds (Term (S n)) -> Term n
-  Lambda : WithBounds String -> WithBounds (Term (S n)) -> Term n
-  App : WithBounds (Term n) -> WithBounds (Term n) -> Term n
+  Pi : (var : WithBounds String) ->
+    (domain : WithBounds (Term n)) ->
+    (codomain : WithBounds (Term (S n))) ->
+    Term n
+  Lambda : (var : WithBounds String) -> (body : WithBounds (Term (S n))) -> Term n
+  App : (fun, arg : WithBounds (Term n)) -> Term n
   -- Dependent Sums
-  Sigma : WithBounds String -> WithBounds (Term n) -> WithBounds (Term (S n)) -> Term n
-  Pair : WithBounds (Term n) -> WithBounds (Term n) -> Term n
-  Fst : WithBounds (Term n) -> Term n
-  Snd : WithBounds (Term n) -> Term n
+  Sigma : (var : WithBounds String) ->
+    (index : WithBounds (Term n)) ->
+    (element : WithBounds (Term (S n))) ->
+    Term n
+  Pair : (first, second : WithBounds (Term n)) -> Term n
+  First : (arg : WithBounds (Term n)) -> Term n
+  Second : (arg : WithBounds (Term n)) -> Term n
   -- Booleans
   Bool : Term n
   True : Term n
   False : Term n
-  If : WithBounds String ->
-    WithBounds (Term (S n)) ->
-    WithBounds (Term n) ->
-    WithBounds (Term n) ->
-    WithBounds (Term n) ->
+  If : (var : WithBounds String) ->
+    (returnType : WithBounds (Term (S n))) ->
+    (discriminant, true, false : WithBounds (Term n)) ->
     Term n
   -- True
   Top : Term n
   Point : Term n
   -- False
   Bottom : Term n
-  Absurd : WithBounds (Term n) -> Term n
+  Absurd : (contradiction : WithBounds (Term n)) -> Term n
   -- Equality
-  Equal : WithBounds (Term n) -> WithBounds (Term n) -> Term n
-  Refl : WithBounds (Term n) -> Term n
-  Transp : WithBounds (Term n) ->
-    WithBounds (Term n) ->
-    WithBounds (Term n) ->
-    WithBounds (Term n) ->
-    WithBounds (Term n) ->
-    Term n
-  Cast : WithBounds (Term n) ->
-    WithBounds (Term n) ->
-    WithBounds (Term n) ->
-    WithBounds (Term n) ->
-    Term n
-  CastId : WithBounds (Term n) -> Term n
+  Equal : (left, right : WithBounds (Term n)) -> Term n
+  Refl : (value : WithBounds (Term n)) -> Term n
+  Transp : (indexedType, oldIndex, value, newIndex, equality : WithBounds (Term n)) -> Term n
+  Cast : (oldType, newType, equality, value : WithBounds (Term n)) -> Term n
+  CastId : (value : WithBounds (Term n)) -> Term n
 
 public export
 record Definition (n : Nat) where
   constructor MkDefinition
-  name   : WithBounds String
-  ty     : WithBounds (Term n)
-  tm     : WithBounds (Term n)
+  name : WithBounds String
+  ty   : WithBounds (Term n)
+  tm   : WithBounds (Term n)
 
 public export
 data Block : Nat -> Type where
@@ -70,102 +67,55 @@ data Block : Nat -> Type where
 
 -- Pretty Print ----------------------------------------------------------------
 
-prettyPrec : Prec -> Term n -> Doc ann
 prettyPrecBounds : Prec -> WithBounds (Term n) -> Doc ann
 
-prettyPrec d (Var var _) = pretty var
-prettyPrec d (Universe s) = prettyPrec d s
-prettyPrec d (Pi var a b) =
-  parenthesise (d > Open) $
-  group $
-  parens (pretty var.val <++> colon <+> softline <+> align (prettyPrecBounds Open a)) <++>
-  pretty "->" <+> line <+>
-  align (prettyPrecBounds Open b)
-prettyPrec d (Lambda var t) =
-  parenthesise (d > Open) $
-  group $
-  backslash <+> pretty var.val <++>
-  pretty "=>" <+> line <+>
-  align (prettyPrecBounds Open t)
-prettyPrec d (App t u) =
-  parenthesise (d >= App) $
-  group $
-  vsep [prettyPrecBounds Open t, prettyPrecBounds App u]
-prettyPrec d (Sigma var a b) =
-  parenthesise (d >= App) $
-  group $
-  parens (pretty var.val <++> colon <+> softline <+> align (prettyPrecBounds Open a)) <++>
-  pretty "**" <+> line <+>
-  align (prettyPrecBounds Open b)
-prettyPrec d (Pair t u) =
-  angles $
-  group $
-  neutral <++> prettyPrecBounds Open t <+> comma <+> line <+> prettyPrecBounds Open u <++> neutral
-prettyPrec d (Fst t) =
-  parenthesise (d >= App) $
-  group $
-  vsep [pretty "fst", prettyPrecBounds App t]
-prettyPrec d (Snd t) =
-  parenthesise (d >= App) $
-  group $
-  vsep [pretty "snd", prettyPrecBounds App t]
+prettyPrec : Prec -> Term n -> Doc ann
+prettyPrec d (Var {var, i}) = pretty var
+prettyPrec d (Universe {s}) = prettyPrec d s
+prettyPrec d (Pi {var, domain, codomain}) =
+  prettyDeclForm d var.val (prettyPrecBounds Open domain) "->" (prettyPrecBounds Open codomain)
+prettyPrec d (Lambda {var, body}) = prettyLambda d var.val (prettyPrecBounds Open body)
+prettyPrec d (App {fun, arg}) = prettyApp d (prettyPrecBounds Open fun) [prettyPrecBounds App arg]
+prettyPrec d (Sigma {var, index, element}) =
+  prettyDeclForm d var.val (prettyPrecBounds Open index) "**" (prettyPrecBounds Open element)
+prettyPrec d (Pair {first, second}) =
+  prettyPair (prettyPrecBounds Open first) (prettyPrecBounds Open second)
+prettyPrec d (First {arg}) = prettyApp d (pretty "fst") [prettyPrecBounds App arg]
+prettyPrec d (Second {arg}) = prettyApp d (pretty "snd") [prettyPrecBounds App arg]
 prettyPrec d Bool = pretty "Bool"
 prettyPrec d True = pretty "True"
 prettyPrec d False = pretty "False"
-prettyPrec d (If var a t f g) =
-  parenthesise (d >= App) $
-  group $
-  vsep $
-  [ pretty "if"
-  , parens $
-    group $
-    backslash <+> pretty var.val <++>
-    pretty "=>" <+> line <+>
-    align (prettyPrecBounds Open a)
-  , prettyPrecBounds App t
-  , prettyPrecBounds App f
-  , prettyPrecBounds App g
+prettyPrec d (If {var, returnType, discriminant, true, false}) =
+  prettyApp d (pretty "if") $
+  [ prettyLambda App var.val (prettyPrecBounds Open returnType)
+  , prettyPrecBounds App discriminant
+  , prettyPrecBounds App true
+  , prettyPrecBounds App false
   ]
 prettyPrec d Top = pretty "()"
 prettyPrec d Point = pretty "tt"
 prettyPrec d Bottom = pretty "Void"
-prettyPrec d (Absurd t) =
-  parenthesise (d > Open) $
-  group $
-  vsep [pretty "absurd", prettyPrecBounds App t]
-prettyPrec d (Equal t u) =
-  parenthesise (d >= Equal) $
-  group $
-  prettyPrecBounds Equal t <++> pretty "~" <+> line <+> prettyPrecBounds Equal u
-prettyPrec d (Refl t) =
-  parenthesise (d >= App) $
-  group $
-  vsep [pretty "refl", prettyPrecBounds App t]
-prettyPrec d (Transp a t u t' e) =
-  parenthesise (d >= App) $
-  group $
-  vsep $
-  [ pretty "transp"
-  , prettyPrecBounds App a
-  , prettyPrecBounds App t
-  , prettyPrecBounds App u
-  , prettyPrecBounds App t'
-  , prettyPrecBounds App e
+prettyPrec d (Absurd {contradiction}) =
+  prettyApp d (pretty "absurd") [prettyPrecBounds App contradiction]
+prettyPrec d (Equal {left, right}) =
+  prettyEqual d (prettyPrecBounds Equal left) (prettyPrecBounds Equal right)
+prettyPrec d (Refl {value}) = prettyApp d (pretty "refl") [prettyPrecBounds App value]
+prettyPrec d (Transp {indexedType, oldIndex, value, newIndex, equality}) =
+  prettyApp d (pretty "transp") $
+  [ prettyPrecBounds App indexedType
+  , prettyPrecBounds App oldIndex
+  , prettyPrecBounds App value
+  , prettyPrecBounds App newIndex
+  , prettyPrecBounds App equality
   ]
-prettyPrec d (Cast a b e t) =
-  parenthesise (d >= App) $
-  group $
-  vsep $
-  [ pretty "cast"
-  , prettyPrecBounds App a
-  , prettyPrecBounds App b
-  , prettyPrecBounds App e
-  , prettyPrecBounds App t
+prettyPrec d (Cast {oldType, newType, equality, value}) =
+  prettyApp d (pretty "cast") $
+  [ prettyPrecBounds App oldType
+  , prettyPrecBounds App newType
+  , prettyPrecBounds App equality
+  , prettyPrecBounds App value
   ]
-prettyPrec d (CastId t) =
-  parenthesise (d >= App) $
-  group $
-  vsep [pretty "castRefl", prettyPrecBounds App t]
+prettyPrec d (CastId {value}) = prettyApp d (pretty "castRefl") [prettyPrecBounds App value]
 
 prettyPrecBounds d (MkBounded v _ _) = prettyPrec d v
 
diff --git a/src/Obs/Typing.idr b/src/Obs/Typing.idr
index 7bb5deb..b3762cf 100644
--- a/src/Obs/Typing.idr
+++ b/src/Obs/Typing.idr
@@ -48,11 +48,31 @@ MkPair s@(Set _) s' t u = Cnstr $ Pair s s' Set t u
 
 -- Checking and Inference ------------------------------------------------------
 
+check' : (tyCtx : TyContext ctx)
+  -> (s : Universe)
+  -> TypeNormalForm ctx
+  -> Term (length ctx)
+  -> Logging ann (NormalForm (relevance s) ctx)
+
+infer' : (tyCtx : TyContext ctx)
+  -> Term (length ctx)
+  -> Logging ann (s ** (TypeNormalForm ctx, NormalForm (relevance s) ctx))
+
+inferType' : {default typeMismatch tag : forall a . Doc ann -> Doc ann -> Logging ann a}
+  -> (tyCtx : TyContext ctx)
+  -> Term (length ctx)
+  -> Logging ann (Universe, TypeNormalForm ctx)
+inferType' ctx t = do
+  (Set _ ** (Cnstr (Universe s), a)) <- infer' ctx t
+    | (_ ** (type, a)) => tag (pretty "sort") (pretty type)
+  pure (s, a)
+
 check : (tyCtx : TyContext ctx)
   -> (s : Universe)
   -> TypeNormalForm ctx
   -> WithBounds (Term (length ctx))
   -> Logging ann (NormalForm (relevance s) ctx)
+check ctx s a (MkBounded t irrel bounds) = inBounds (MkBounded (check' ctx s a t) irrel bounds)
 
 checkType : (tyCtx : TyContext ctx)
   -> (s : Universe)
@@ -63,212 +83,340 @@ checkType ctx s tm = check ctx (succ s) (cast s) tm
 infer : (tyCtx : TyContext ctx)
   -> WithBounds (Term (length ctx))
   -> Logging ann (s ** (TypeNormalForm ctx, NormalForm (relevance s) ctx))
+infer ctx (MkBounded t irrel bounds) = inBounds (MkBounded (infer' ctx t) irrel bounds)
 
 inferType : {default typeMismatch tag : forall a . Doc ann -> Doc ann -> Logging ann a}
   -> (tyCtx : TyContext ctx)
   -> WithBounds (Term (length ctx))
   -> Logging ann (Universe, TypeNormalForm ctx)
-inferType ctx tm = inBounds tm.bounds $ do
-  (Set _ ** (Cnstr (Universe s), a)) <- infer ctx tm
-    | (_ ** (a, t)) => tag (pretty "universe") (pretty a)
-  pure (s, a)
+inferType ctx (MkBounded t irrel bounds) = inBounds (MkBounded (inferType' ctx t) irrel bounds)
+
+check' ctx sort (Cnstr (Pi domainSort codomainSort _ domain codomain)) (Lambda {var, body}) = do
+  info "encountered lambda"
+
+  let Yes Refl = decEq sort (domainSort ~> codomainSort)
+    | No _ => fatal "internal universe mismatch"
+
+  let bodyCtx = ctx ::< MkFreeVar domainSort domain var.val
+
+  trace $ pretty {ann} "checking body has type" <++> pretty codomainSort
+  body <- check bodyCtx codomainSort codomain body
+
+  pure $ case codomainSort of
+    Prop => Irrel
+    Set _ => Cnstr (Lambda domainSort var.val body)
+
+check' ctx sort type (Lambda {var, body}) = typeMismatch (pretty "function") (pretty type)
+
+check' ctx sort (Cnstr (Sigma indexSort elementSort var index element)) (Pair {first, second}) = do
+  info "encountered pair"
+
+  let Yes Refl = decEq sort (max indexSort elementSort)
+    | No _ => fatal "internal universe mismatch"
+
+  trace $ pretty {ann} "checking first has type" <++> pretty index
+  first <- check ctx indexSort index first
+
+  element <- subst1 first element
+  trace $ pretty {ann} "checking second has type" <++> pretty element
+  second <- check ctx elementSort element second
+
+  pure $ MkPair indexSort elementSort first second
+
+check' ctx sort type (Pair {first, second}) = typeMismatch (pretty "pair type") (pretty type)
+
+check' ctx sort type (Absurd {contradiction}) = do
+  info "encountered absurd"
+
+  trace "checking proof of contradiction"
+  Irrel <- check ctx Prop (Cnstr Bottom) contradiction
+
+  pure $ doAbsurd _
+
+check' ctx sort type t = do
+  info "falling through to inference"
+
+  (inferredSort ** (inferredType, value)) <- infer' ctx t
+  trace $ pretty {ann} "inferred type is" <++> pretty inferredType
+
+  let Yes Refl = decEq sort inferredSort
+    | No _ => typeMismatch (pretty type) (pretty inferredType)
+
+  expandedType <- subst type (reduce ctx)
+  expandedInferredType <- subst inferredType (reduce ctx)
+
+  Just _ <- inScope "convert" $ runMaybeT $ convert (succ sort) (cast sort) expandedType expandedInferredType
+  | Nothing => inScope "conversion failed" $ mismatch (pretty type) (pretty inferredType)
+
+  pure value
+
+
+infer' ctx tm@(Var {var, i}) = do
+    info $ pretty {ann} "encountered variable" <++> pretty tm
 
-check ctx s ty tm = inBounds tm.bounds $ case (ty, tm.val) of
-  (Cnstr (Pi l l' _ a b), Lambda var t) => do
-    info "encountered lambda"
-    trace $ pretty {ann} "checking body has type" <++> pretty b
-    t <- check (ctx ::< MkFreeVar l a var.val) l' b (assert_smaller tm t)
-    let Yes Refl = decEq s (l ~> l')
-      | No _ => fatal "internal universe mismatch"
-    pure $ case l' of
-      Prop => Irrel
-      Set _ => Cnstr (Lambda l var.val t)
-  (_, Lambda var t) => typeMismatch (pretty "function") (pretty ty)
-  (Cnstr (Sigma l l' var a b), Pair t u) => do
-    info "encountered pair"
-    trace $ pretty {ann} "checking first has type" <++> pretty a
-    t <- check ctx l a (assert_smaller tm t)
-    b <- subst1 t b
-    trace $ pretty {ann} "checking second has type" <++> pretty b
-    u <- check ctx l' b (assert_smaller tm u)
-    let Yes Refl = decEq s (max l l')
-      | No _ => fatal "internal universe mismatch"
-    pure $ MkPair l l' t u
-  (_, Pair t u) => typeMismatch (pretty "pair type") (pretty ty)
-  (_, Absurd t) => do
-    info "encountered absurd"
-    trace "checking proof of contradiction"
-    Irrel <- check ctx Prop (Cnstr Bottom) (assert_smaller tm t)
-    pure $ doAbsurd _
-  (a, t) => do
-    info "falling through to inference"
-    (l ** (b, t)) <- infer ctx tm
-    trace $ pretty {ann} "inferred type is" <++> pretty b
-    let Yes Refl = decEq s l
-      | No _ => typeMismatch (pretty a) (pretty b)
-    a' <- subst a (reduce ctx)
-    b' <- subst b (reduce ctx)
-    Just _ <- inScope "convert" $ runMaybeT $ convert (succ s) (cast s) a' b'
-    | Nothing => inScope "conversion failed" $ mismatch (pretty a) (pretty b)
-    pure t
-
-infer ctx tm = inBounds tm.bounds $ case tm.val of
-  (Var var i) => do
-    info $ pretty {ann} "encountered variable" <++> pretty tm.val
     let def = index' ctx i
     pure (def.sort ** (def.ty, def.tm))
-  (Universe s) => do
-    info $ pretty {ann} "encountered universe" <++> pretty tm.val
+
+infer' ctx (Universe {s}) = do
+    info $ pretty {ann} "encountered universe" <++> pretty s
+
     pure (succ (succ s) ** (cast (succ s), cast s))
-  (Pi var a b) => do
+
+infer' ctx (Pi {var, domain, codomain}) = do
     info "encountered pi"
-    (s, a) <- inferType ctx (assert_smaller tm a)
-    trace $ pretty {ann} "domain type is" <++> pretty a
-    (s', b) <- inferType (ctx ::< MkFreeVar s a var.val) (assert_smaller tm b)
-    trace $ pretty {ann} "codomain type is" <++> pretty b
-    pure (succ (s ~> s') ** (cast (s ~> s'), Cnstr (Pi s s' var.val a b)))
-  (Lambda var t) => fatal "cannot infer type of lambda"
-  (App t u) => do
+
+    (domainSort, domain) <- inferType ctx domain
+    trace $ pretty {ann} "domain type is" <++> pretty domain
+
+    let domainVar = MkFreeVar domainSort domain var.val
+    let codomainCtx = ctx ::< domainVar
+
+    (codomainSort, codomain) <- inferType codomainCtx codomain
+    trace $ pretty {ann} "codomain type is" <++> pretty codomain
+
+    let piSort = domainVar.sort ~> codomainSort
+    let term = Cnstr (Pi domainVar.sort codomainSort var.val domain codomain)
+    pure (succ piSort ** (cast piSort, term))
+
+infer' ctx (Lambda {var, body}) = fatal "cannot infer type of lambda"
+
+infer' ctx (App {fun, arg}) = do
     info "encountered application"
-    (s ** (ty@(Cnstr (Pi l l' _ a b)), t)) <- infer ctx (assert_smaller tm t)
-      | (_ ** (ty, _)) => inBounds t.bounds $ typeMismatch (pretty "function") (pretty ty)
-    trace $ pretty {ann} "function has type" <++> pretty ty
-    trace $ pretty {ann} "checking argument has type" <++> pretty a
-    u <- check ctx l a (assert_smaller tm u)
-    trace $ pretty {ann} "argument is well typed"
-    let Yes Refl = decEq s (l ~> l')
+
+    (piSort ** (funType, funValue)) <- infer ctx fun
+    trace $ pretty {ann} "function has type" <++> pretty funType
+
+    let Cnstr (Pi domainSort codomainSort _ domain codomain) = funType
+      | _ => inBounds $ map (const $ typeMismatch (pretty "function") (pretty funType)) fun
+
+    let Yes Refl = decEq piSort (domainSort ~> codomainSort)
       | No _ => fatal "internal universe mismatch"
-    ty <- subst1 u b
-    tm <- doApp t u
-    pure (l' ** (ty, rewrite sym $ functionRelevance l l' in tm))
-  (Sigma var a b) => do
+
+    let fun = funValue
+
+    trace $ pretty {ann} "checking argument has type" <++> pretty domain
+    arg <- check ctx domainSort domain arg
+    trace $ pretty {ann} "argument is well typed"
+
+    returnType <- subst1 arg codomain
+    returnValue <- doApp fun arg
+
+    let returnValue = rewrite sym $ functionRelevance domainSort codomainSort in returnValue
+
+    pure (codomainSort ** (returnType, returnValue))
+
+infer' ctx (Sigma {var, index, element}) = do
     info "encountered sigma"
-    (s, a) <- inferType ctx (assert_smaller tm a)
-    trace $ pretty {ann} "first type is" <++> pretty a
-    (s', b) <- inferType (ctx ::< MkFreeVar s a var.val) (assert_smaller tm b)
-    trace $ pretty {ann} "second type is" <++> pretty b
-    pure (succ (max s s') ** (cast (max s s'), Cnstr (Sigma s s' var.val a b)))
-  (Pair t u) => fatal "cannot infer type of pair"
-  (Fst t) => do
+
+    (indexSort, index) <- inferType ctx index
+    trace $ pretty {ann} "index type is" <++> pretty index
+
+    let indexVar = MkFreeVar indexSort index var.val
+    let elementCtx = ctx ::< indexVar
+
+    (elementSort, element) <- inferType elementCtx element
+    trace $ pretty {ann} "element type is" <++> pretty element
+
+    let sigmaSort = max indexVar.sort elementSort
+    let term = Cnstr (Sigma indexVar.sort elementSort var.val index element)
+    pure (succ sigmaSort ** (cast sigmaSort, term))
+
+infer' ctx (Pair {first, second}) = fatal "cannot infer type of pair"
+
+infer' ctx (First {arg}) = do
     info "encountered first"
-    (s ** (ty@(Cnstr (Sigma l l' _ a b)), t)) <- infer ctx (assert_smaller tm t)
-      | (_ ** (ty, _)) => inBounds t.bounds $ typeMismatch (pretty "pair type") (pretty ty)
-    trace $ pretty {ann} "pair has type" <++> pretty ty
-    let Yes Refl = decEq s (max l l')
+
+    (sigmaSort ** (argType, argValue)) <- infer ctx arg
+    trace $ pretty {ann} "pair has type" <++> pretty argType
+
+    let Cnstr (Sigma indexSort elementSort _ index element) = argType
+      | _ => inBounds $ map (const $ typeMismatch (pretty "pair type") (pretty argType)) arg
+
+    let Yes Refl = decEq sigmaSort (max indexSort elementSort)
       | No _ => fatal "internal universe mismatch"
-    let ty = a
-    tm <- doFst (relevance l) (relevance l') (rewrite sym $ pairRelevance l l' in t)
-    pure (l ** (ty, tm))
-  (Snd t) => do
+
+    let argValue = rewrite sym $ pairRelevance indexSort elementSort in argValue
+
+    let returnType = index
+    returnValue <- doFst (relevance indexSort) (relevance elementSort) argValue
+
+    pure (indexSort ** (returnType, returnValue))
+
+infer' ctx (Second {arg}) = do
     info "encountered second"
-    (s ** (ty@(Cnstr (Sigma l l' _ a b)), t)) <- infer ctx (assert_smaller tm t)
-      | (_ ** (ty, _)) => inBounds t.bounds $ typeMismatch (pretty "pair type") (pretty ty)
-    trace $ pretty {ann} "pair has type" <++> pretty ty
-    let Yes Refl = decEq s (max l l')
+
+    (sigmaSort ** (argType, argValue)) <- infer ctx arg
+    trace $ pretty {ann} "pair has type" <++> pretty argType
+
+    let Cnstr (Sigma indexSort elementSort _ index element) = argType
+      | _ => inBounds $ map (const $ typeMismatch (pretty "pair type") (pretty argType)) arg
+
+    let Yes Refl = decEq sigmaSort (max indexSort elementSort)
       | No _ => fatal "internal universe mismatch"
-    let t = rewrite sym $ pairRelevance l l' in t
-    fst <- doFst (relevance l) (relevance l') t
-    ty <- subst1 fst b
-    tm <- doSnd (relevance l) (relevance l') t
-    pure (l' ** (ty, tm))
-  Bool => do
+
+    let argValue = rewrite sym $ pairRelevance indexSort elementSort in argValue
+
+    indexValue <- doFst (relevance indexSort) (relevance elementSort) argValue
+    returnType <- subst1 indexValue element
+    returnValue <- doSnd (relevance indexSort) (relevance elementSort) argValue
+
+    pure (elementSort ** (returnType, returnValue))
+
+infer' ctx Bool = do
     info "encountered bool"
     pure (Set 1 ** (cast (Set 0), Cnstr Bool))
-  True => do
+
+infer' ctx True = do
     info "encountered true"
     pure (Set 0 ** (Cnstr Bool, Cnstr True))
-  False => do
+
+infer' ctx False = do
     info "encountered false"
     pure (Set 0 ** (Cnstr Bool, Cnstr False))
-  (If var a t u v) => do
+
+infer' ctx (If {var, returnType, discriminant, true, false}) = do
     info "encountered if"
     trace "checking discriminant is bool"
-    t <- check ctx (Set 0) (Cnstr Bool) (assert_smaller tm t)
+
+    discriminant <- check ctx (Set 0) (Cnstr Bool) discriminant
     trace "discriminant is well typed"
-    (s, a) <- inferType (ctx ::< MkFreeVar (Set 0) (Cnstr Bool) var.val) (assert_smaller tm a)
-    ty <- subst1 (Cnstr True) a
-    trace $ pretty {ann} "checking true branch has type" <++> pretty ty
-    u <- check ctx s ty (assert_smaller tm u)
-    ty <- subst1 (Cnstr False) a
-    trace $ pretty {ann} "checking false branch has type" <++> pretty ty
-    v <- check ctx s ty (assert_smaller tm v)
-    ty <- subst1 t a
-    tm <- doIf t u v
-    pure (s ** (ty, tm))
-  Top => do
+
+    let returnTypeCtx = ctx ::< MkFreeVar (Set 0) (Cnstr Bool) var.val
+
+    (returnSort, returnType) <- inferType returnTypeCtx returnType
+    trace $ pretty {ann} "result is an index of type" <++> pretty returnType
+
+    trueType <- subst1 (Cnstr True) returnType
+    trace $ pretty {ann} "checking true branch has type" <++> pretty trueType
+    true <- check ctx returnSort trueType true
+    trace "true branch is well typed"
+
+    falseType <- subst1 (Cnstr False) returnType
+    trace $ pretty {ann} "checking false branch has type" <++> pretty falseType
+    false <- check ctx returnSort falseType false
+    trace "false branch is well typed"
+
+    returnType <- subst1 discriminant returnType
+    returnValue <- doIf discriminant true false
+
+    pure (returnSort ** (returnType, returnValue))
+
+infer' ctx Top = do
     info "encountered top"
     pure (Set 0 ** (Cnstr (Universe Prop), Cnstr Top))
-  Point => do
+
+infer' ctx Point = do
     info "encountered point"
     pure (Prop ** (Cnstr Top, Irrel))
-  Bottom => do
+
+infer' ctx Bottom = do
     info "encountered bottom"
     pure (Set 0 ** (Cnstr (Universe Prop), Cnstr Bottom))
-  (Absurd t) => fatal "cannot infer type of absurd"
-  (Equal t u) => do
+
+infer' ctx (Absurd {contradiction}) = fatal "cannot infer type of absurd"
+
+infer' ctx (Equal {left, right}) = do
     info "encountered equal"
-    (s ** (a, t)) <- infer ctx (assert_smaller tm t)
-    trace $ pretty {ann} "left side has type" <++> pretty a
-    u <- check ctx s a (assert_smaller tm u)
+
+    (sort ** (type, left)) <- infer ctx left
+    trace $ pretty {ann} "left side has type" <++> pretty type
+
+    right <- check ctx sort type right
     trace "right side is well typed"
-    eq <- doEqual (relevance s) a t u
-    pure (Set 0 ** (Cnstr (Universe Prop), eq))
-  (Refl t) => do
+
+    let equalitySort = Prop
+    equalityType <- doEqual (relevance sort) type left right
+
+    pure (succ equalitySort ** (cast equalitySort, equalityType))
+
+infer' ctx (Refl {value}) = do
     info "encountered refl"
-    (s ** (a, t)) <- infer ctx (assert_smaller tm t)
-    trace "argument is well typed"
-    eq <- doEqual (relevance s) a t t
-    pure (Prop ** (eq, Irrel))
-  (Transp b t u t' e) => do
+
+    (sort ** (type, value)) <- infer ctx value
+    trace $ pretty {ann} "value has type" <++> pretty type
+
+    equalityType <- doEqual (relevance sort) type value value
+
+    pure (Prop ** (equalityType, Irrel))
+
+infer' ctx (Transp {indexedType, oldIndex, value, newIndex, equality}) = do
     info "encountered transp"
-    (s ** (a, t)) <- infer ctx (assert_smaller tm t)
-    trace $ pretty {ann} "index type is" <++> pretty a
-    t' <- check ctx s a (assert_smaller tm t')
+
+    (indexSort ** (indexType, oldIndex)) <- infer ctx oldIndex
+    trace $ pretty {ann} "index type is" <++> pretty indexType
+
+    newIndex <- check ctx indexSort indexType newIndex
     trace "new index is well typed"
-    b <- check ctx (s ~> Set 0) (Cnstr $ Pi s (Set 0) "" a (Cnstr (Universe Prop))) (assert_smaller tm b)
-    trace "transporting in Prop"
-    oldB <- doApp b t
-    u <- check ctx Prop oldB (assert_smaller tm u)
-    trace "old-indexed proposition is well typed"
-    eq <- doEqual (relevance s) a t t'
-    trace $ pretty {ann} "checking equality has type" <++> pretty eq
-    e <- check ctx Prop eq (assert_smaller tm e)
+
+    let indexedTypeShape = Cnstr $ Pi indexSort (Set 0) "" indexType (Cnstr (Universe Prop))
+    indexedType <- check ctx (indexSort ~> Set 0) indexedTypeShape indexedType
+    trace $ pretty {ann} "result is an index of type" <++> pretty indexedType
+
+    oldType <- doApp indexedType oldIndex
+    trace $ pretty {ann} "checking value has type" <++> pretty oldType
+    Irrel <- check ctx Prop oldType value
+    trace "value is well typed"
+
+    equalityType <- doEqual (relevance indexSort) indexType oldIndex newIndex
+    trace $ pretty {ann} "checking equality has type" <++> pretty equalityType
+    equality <- check ctx Prop equalityType equality
     trace "equality is well typed"
-    newB <- doApp b t'
-    pure (Prop ** (newB, Irrel))
-  (Cast a b e t) => do
+
+    returnType <- doApp indexedType newIndex
+
+    pure (Prop ** (returnType, Irrel))
+
+infer' ctx (Cast {oldType, newType, equality, value}) = do
     info "encountered cast"
-    (s, a) <- inferType ctx (assert_smaller tm a)
-    trace $ pretty {ann} "old type is" <++> pretty a
-    b <- checkType ctx s (assert_smaller tm b)
-    trace $ pretty {ann} "new type is" <++> pretty b
-    eq <- doEqual Relevant (cast s) a b
-    e <- check ctx Prop eq (assert_smaller tm e)
+
+    (sort, oldType) <- inferType ctx oldType
+    trace $ pretty {ann} "old type is" <++> pretty oldType
+
+    newType <- checkType ctx sort newType
+    trace $ pretty {ann} "new type is" <++> pretty newType
+
+    equalityType <- doEqual Relevant (cast sort) oldType newType
+    trace $ pretty {ann} "checking equality has type" <++> pretty equalityType
+    equality <- check ctx Prop equalityType equality
     trace "equality is well typed"
-    t <- check ctx s a (assert_smaller tm t)
+
+    trace $ pretty {ann} "checking value has type" <++> pretty oldType
+    value <- check ctx sort oldType value
     trace "value is well typed"
-    tm <- doCast (relevance s) a b t
-    pure (s ** (b, tm))
-  (CastId t) => do
+
+    returnValue <- doCast (relevance sort) oldType newType value
+
+    pure (sort ** (newType, returnValue))
+
+infer' ctx (CastId {value}) = do
     info "encountered castRefl"
-    (s ** (a, t)) <- infer ctx (assert_smaller tm t)
-    trace $ pretty {ann} "argument has type" <++> pretty a
-    lhs <- doCast (relevance s) a a t
-    ret <- doEqual (relevance s) a lhs t
-    pure (Prop ** (ret, Irrel))
+
+    (sort ** (type, value)) <- infer ctx value
+    trace $ pretty {ann} "value has type" <++> pretty value
+
+    castRefl <- doCast (relevance sort) type type value
+
+    returnType <- doEqual (relevance sort) type castRefl value
+
+    pure (Prop ** (returnType, Irrel))
 
 -- Checking Definitions and Blocks ---------------------------------------------
 
 checkDef : Context ctx -> Term.Definition (length ctx) -> Logging ann (NormalForm.Definition ctx)
-checkDef ctx def = inBounds def.name.bounds $ inScope "check" $ do
-  debug $ "inferring type of \{def.name.val}"
-  (sort, ty) <-
-    inferType {tag = \lhs, rhs => inScope "invalid declaration" $ mismatch lhs rhs}
-      (fromContext ctx) def.ty
-  debug $ pretty {ann} "\{def.name.val} has type" <++> pretty ty
-  tm <- check (fromContext ctx) sort ty def.tm
-  debug $ pretty {ann} "\{def.name.val} is well typed with value" <++> pretty tm
-  pure $ MkDefinition {name = def.name, ty, tm, sort}
+checkDef ctx def =
+  let block = do
+    debug $ "inferring type of \{def.name.val}"
+    (sort, ty) <-
+      inferType {tag = \lhs, rhs => inScope "invalid declaration" $ mismatch lhs rhs}
+        (fromContext ctx) def.ty
+    debug $ pretty {ann} "\{def.name.val} has type" <++> pretty ty
+
+    tm <- check (fromContext ctx) sort ty def.tm
+    debug $ pretty {ann} "\{def.name.val} is well typed with value" <++> pretty tm
+
+    pure $ MkDefinition {name = def.name, ty, tm, sort}
+
+  in inBounds $ map (const $ inScope "check" block) def.name
 
 export
 checkBlock : Block n -> Logging ann (ctx ** (Context ctx, length ctx = n))