Print type checking errors.

2 files changed, 315 insertions, 92 deletions

diff --git a/src/Inky/Term/Parser.idr b/src/Inky/Term/Parser.idr
index 90b4e08..ee122bb 100644
--- a/src/Inky/Term/Parser.idr
+++ b/src/Inky/Term/Parser.idr
@@ -267,12 +267,12 @@ mkVar f x =
       Nothing => Left "\{x.bounds}: unbound name \"\{x.val}\"")
 
 mkVar2 :
-  ({tyCtx, tmCtx : _} -> Var tmCtx -> p tyCtx tmCtx) ->
+  ({tyCtx, tmCtx : _} -> WithBounds (Var tmCtx) -> p tyCtx tmCtx) ->
   WithBounds String -> ParseFun 2 p
 mkVar2 f x =
   MkParseFun
     (\tyCtx, tmCtx => case Var.lookup x.val tmCtx of
-      Just i => pure (f i)
+      Just i => pure (f $ i <$ x)
       Nothing => Left "\{x.bounds}: unbound name \"\{x.val}\"")
 
 public export
@@ -281,7 +281,7 @@ TypeFun = ParseFun 1 Ty
 
 public export
 TermFun : Type
-TermFun = ParseFun 2 Term
+TermFun = ParseFun 2 (Term Bounds)
 
 public export
 TypeParser : SnocList String -> SnocList String -> Type
@@ -383,57 +383,58 @@ OpenTypeWf = Oh
 AtomTerm : InkyParser False [<"openTerm" :- TermFun] [<] TermFun
 AtomTerm =
   OneOf
-    [ mkVar2 Var <$> WithBounds (match TermIdent)
-    , mkLit <$> match Lit
-    , mkSuc <$ match Suc
-    , mkTup <$> (enclose (match AngleOpen) (match AngleClose) $
+    [ mkVar2 (\x => Var x.bounds x.val) <$> WithBounds (match TermIdent)
+    , mkLit <$> WithBounds (match Lit)
+    , mkSuc <$> WithBounds (match Suc)
+    , mkTup <$> WithBounds (enclose (match AngleOpen) (match AngleClose) $
         RowOf [<"openTerm" :- TermFun] (Var (%%% "openTerm")))
     , enclose (match ParenOpen) (match ParenClose) (Var (%%% "openTerm"))
     ]
   where
-  mkLit : Nat -> TermFun
-  mkLit k = MkParseFun (\tyCtx, tmCtx => pure (Lit k))
+  mkLit : WithBounds Nat -> TermFun
+  mkLit k = MkParseFun (\tyCtx, tmCtx => pure (Lit k.bounds k.val))
 
-  mkSuc : TermFun
-  mkSuc = MkParseFun (\_, _ => pure Suc)
+  mkSuc : WithBounds () -> TermFun
+  mkSuc x = MkParseFun (\_, _ => pure (Suc x.bounds))
 
-  mkTup : List (WithBounds $ Assoc TermFun) -> TermFun
-  mkTup xs = MkParseFun (\tyCtx, tmCtx => Tup <$> tryRow2 xs tyCtx tmCtx)
+  mkTup : WithBounds (List (WithBounds $ Assoc TermFun)) -> TermFun
+  mkTup xs = MkParseFun (\tyCtx, tmCtx => Tup xs.bounds <$> tryRow2 xs.val tyCtx tmCtx)
 
 PrefixTerm : InkyParser False [<"openTerm" :- TermFun] [<] TermFun
 PrefixTerm =
   Fix "prefixTerm" $ OneOf
-    [ match Tilde **> (mkRoll <$> Var (%%% "prefixTerm"))
-    , match Bang **> mkUnroll <$> Var (%%% "prefixTerm")
+    [ mkRoll <$> WithBounds (match Tilde **> Var (%%% "prefixTerm"))
+    , mkUnroll <$> WithBounds (match Bang **> Var (%%% "prefixTerm"))
     , rename (Drop Id) Id AtomTerm
     ]
   where
-  mkRoll : TermFun -> TermFun
-  mkRoll x = MkParseFun (\tyCtx, tmCtx => [| Roll (x.try tyCtx tmCtx) |])
+  mkRoll : WithBounds TermFun -> TermFun
+  mkRoll x = MkParseFun (\tyCtx, tmCtx => pure $ Roll x.bounds !(x.val.try tyCtx tmCtx))
 
-  mkUnroll : TermFun -> TermFun
-  mkUnroll x = MkParseFun (\tyCtx, tmCtx => [| Unroll (x.try tyCtx tmCtx) |])
+  mkUnroll : WithBounds TermFun -> TermFun
+  mkUnroll x = MkParseFun (\tyCtx, tmCtx => pure $ Unroll x.bounds !(x.val.try tyCtx tmCtx))
 
 SuffixTerm : InkyParser False [<"openTerm" :- TermFun] [<] TermFun
-SuffixTerm = mkSuffix <$> Seq [ PrefixTerm , star (match Dot **> match TypeIdent) ]
+SuffixTerm = mkSuffix <$> Seq [ PrefixTerm , star (match Dot **> WithBounds (match TypeIdent)) ]
   where
-  mkSuffix : HList [TermFun, List String] -> TermFun
+  mkSuffix : HList [TermFun, List (WithBounds String)] -> TermFun
   mkSuffix [t, []] = t
   mkSuffix [t, prjs] =
-    MkParseFun (\tyCtx, tmCtx => pure $ foldl Prj !(t.try tyCtx tmCtx) prjs)
+    MkParseFun (\tyCtx, tmCtx =>
+      pure $ foldl (\acc, l => Prj l.bounds acc l.val) !(t.try tyCtx tmCtx) prjs)
 
 AppTerm : InkyParser False [<"openTerm" :- TermFun] [<] TermFun
 AppTerm =
   OneOf
     [ mkInj <$> Seq
-      [ match TypeIdent
+      [ WithBounds (match TypeIdent)
       , weaken (S Z) SuffixTerm
       ]
     , mkApp <$> Seq
       [ OneOf {nils = [False, False, False]}
-        [ SuffixTerm
+        [ WithBounds SuffixTerm
         , mkMap <$> Seq
-          [ match Map
+          [ WithBounds (match Map)
           , enclose (match ParenOpen) (match ParenClose) $ Seq
             [ match Backslash
             , match TypeIdent
@@ -444,7 +445,7 @@ AppTerm =
           , sub [<"openType" :- rename Id (Drop Id) OpenType] [<] AtomType
           ]
         , mkGetChildren <$> Seq
-          [ match GetChildren
+          [ WithBounds (match GetChildren)
           , enclose (match ParenOpen) (match ParenClose) $ Seq
             [ match Backslash
             , match TypeIdent
@@ -458,26 +459,29 @@ AppTerm =
       ]
     ]
   where
-  mkInj : HList [String, TermFun] -> TermFun
-  mkInj [tag, t] = MkParseFun (\tyCtx, tmCtx => Inj tag <$> t.try tyCtx tmCtx)
+  mkInj : HList [WithBounds String, TermFun] -> TermFun
+  mkInj [tag, t] = MkParseFun (\tyCtx, tmCtx => Inj tag.bounds tag.val <$> t.try tyCtx tmCtx)
 
-  mkMap : HList [_, HList [_, String, _, TypeFun], TypeFun, TypeFun] -> TermFun
-  mkMap [_, [_, x, _, a], b, c] =
+  mkMap : HList [WithBounds (), HList [_, String, _, TypeFun], TypeFun, TypeFun] -> WithBounds TermFun
+  mkMap [m, [_, x, _, a], b, c] =
     MkParseFun (\tyCtx, tmCtx =>
-      pure $ Map (x ** !(a.try (tyCtx :< x))) !(b.try tyCtx) !(c.try tyCtx))
+      pure $ Map m.bounds (x ** !(a.try (tyCtx :< x))) !(b.try tyCtx) !(c.try tyCtx))
+    <$ m
 
-  mkGetChildren : HList [_, HList [_, String, _, TypeFun], TypeFun] -> TermFun
-  mkGetChildren [_, [_, x, _, a], b] =
+  mkGetChildren : HList [WithBounds (), HList [_, String, _, TypeFun], TypeFun] -> WithBounds TermFun
+  mkGetChildren [m, [_, x, _, a], b] =
     MkParseFun (\tyCtx, tmCtx =>
-      pure $ GetChildren (x ** !(a.try (tyCtx :< x))) !(b.try tyCtx))
+      pure $ GetChildren m.bounds (x ** !(a.try (tyCtx :< x))) !(b.try tyCtx))
+    <$ m
 
-  mkApp : HList [TermFun, List TermFun] -> TermFun
-  mkApp [t, []] = t
+  mkApp : HList [WithBounds TermFun, List TermFun] -> TermFun
+  mkApp [t, []] = t.val
   mkApp [fun, (arg :: args)] =
     MkParseFun (\tyCtx, tmCtx =>
       pure $
       App
-        !(fun.try tyCtx tmCtx)
+        fun.bounds
+        !(fun.val.try tyCtx tmCtx)
         (  !(arg.try tyCtx tmCtx)
         :: (!(foldlM (\acc, arg => pure $ acc :< !(arg.try tyCtx tmCtx)) [<] args) <>> [])))
 
@@ -485,12 +489,13 @@ AnnotTerm : InkyParser False [<"openTerm" :- TermFun] [<] TermFun
 AnnotTerm =
   mkAnnot <$> Seq
     [ AppTerm
-    , option (match Colon **> rename Id (Drop Id) OpenType)
+    , option (match Colon **> WithBounds (rename Id (Drop Id) OpenType))
     ]
   where
-  mkAnnot : HList [TermFun, Maybe TypeFun] -> TermFun
+  mkAnnot : HList [TermFun, Maybe (WithBounds TypeFun)] -> TermFun
   mkAnnot [t, Nothing] = t
-  mkAnnot [t, Just a] = MkParseFun (\tyCtx, tmCtx => [| Annot (t.try tyCtx tmCtx) (a.try tyCtx) |])
+  mkAnnot [t, Just a] = MkParseFun (\tyCtx, tmCtx =>
+    pure $ Annot a.bounds !(t.try tyCtx tmCtx) !(a.val.try tyCtx))
 
 -- Open Terms
 
@@ -499,12 +504,12 @@ LetTerm =
   match Let **>
   OneOf
     [ mkLet <$> Seq
-      [ match TermIdent
+      [ WithBounds (match TermIdent)
       , OneOf
         [ mkBound <$> Seq
           [ star (enclose (match ParenOpen) (match ParenClose) $
             Seq [ match TermIdent, match Colon, rename Id (Drop Id) OpenType ])
-          , match Colon
+          , WithBounds (match Colon)
           , rename Id (Drop Id) OpenType
           , match Equal
           , Var (%%% "openTerm")]
@@ -514,7 +519,7 @@ LetTerm =
       , Var (%%% "openTerm")
       ]
     , mkLetType <$> Seq
-      [ match TypeIdent
+      [ WithBounds (match TypeIdent)
       , match Equal
       , rename Id (Drop Id) OpenType
       , match In
@@ -522,43 +527,46 @@ LetTerm =
       ]
     ]
   where
-  mkLet : HList [String, TermFun, (), TermFun] -> TermFun
-  mkLet [x, e, _, t] = MkParseFun (\tyCtx, tmCtx => pure $ Let !(e.try tyCtx tmCtx) (x ** !(t.try tyCtx (tmCtx :< x))))
+  mkLet : HList [WithBounds String, TermFun, (), TermFun] -> TermFun
+  mkLet [x, e, _, t] =
+    MkParseFun (\tyCtx, tmCtx =>
+      pure $ Let x.bounds !(e.try tyCtx tmCtx) (x.val ** !(t.try tyCtx (tmCtx :< x.val))))
 
-  mkLetType : HList [String, (), TypeFun, (), TermFun] -> TermFun
+  mkLetType : HList [WithBounds String, (), TypeFun, (), TermFun] -> TermFun
   mkLetType [x, _, a, _, t] =
-    MkParseFun (\tyCtx, tmCtx => pure $ LetTy !(a.try tyCtx) (x ** !(t.try (tyCtx :< x) tmCtx)))
+    MkParseFun (\tyCtx, tmCtx =>
+      pure $ LetTy x.bounds !(a.try tyCtx) (x.val ** !(t.try (tyCtx :< x.val) tmCtx)))
 
   mkArrow : List TypeFun -> TypeFun -> TypeFun
   mkArrow [] cod = cod
   mkArrow (arg :: args) cod =
     MkParseFun (\ctx => [| TArrow (arg.try ctx) ((mkArrow args cod).try ctx) |])
 
-  mkBound : HList [List (HList [String, (), TypeFun]), (), TypeFun, (), TermFun] -> TermFun
-  mkBound [[], _, cod, _, t] =
+  mkBound : HList [List (HList [String, (), TypeFun]), WithBounds (), TypeFun, (), TermFun] -> TermFun
+  mkBound [[], m, cod, _, t] =
     MkParseFun (\tyCtx, tmCtx =>
       pure $
-      Annot !(t.try tyCtx tmCtx) !(cod.try tyCtx))
-  mkBound [args, _, cod, _, t] =
+      Annot m.bounds !(t.try tyCtx tmCtx) !(cod.try tyCtx))
+  mkBound [args, m, cod, _, t] =
     let bound = map (\[x, _, a] => x) args in
     let tys = map (\[x, _, a] => a) args in
     MkParseFun (\tyCtx, tmCtx =>
       pure $
-      Annot (Abs (bound ** !(t.try tyCtx (tmCtx <>< bound)))) !((mkArrow tys cod).try tyCtx))
+      Annot m.bounds (Abs m.bounds (bound ** !(t.try tyCtx (tmCtx <>< bound)))) !((mkArrow tys cod).try tyCtx))
 
 AbsTerm : InkyParser False [<"openTerm" :- TermFun] [<] TermFun
 AbsTerm =
   mkAbs <$> Seq
-    [ match Backslash
+    [ WithBounds (match Backslash)
     , sepBy1 (match Comma) (match TermIdent)
     , match DoubleArrow
     , Var (%%% "openTerm")
     ]
   where
-  mkAbs : HList [(), List1 String, (), TermFun] -> TermFun
-  mkAbs [_, args, _, body] =
+  mkAbs : HList [WithBounds (), List1 String, (), TermFun] -> TermFun
+  mkAbs [m, args, _, body] =
     MkParseFun (\tyCtx, tmCtx =>
-      pure $ Abs (forget args ** !(body.try tyCtx (tmCtx <>< forget args))))
+      pure $ Abs m.bounds (forget args ** !(body.try tyCtx (tmCtx <>< forget args))))
 
 CaseTerm : InkyParser False [<"openTerm" :- TermFun] [<] TermFun
 CaseTerm =
@@ -566,12 +574,12 @@ CaseTerm =
   Seq
     [ OneOf
       [ mkCase <$> Seq
-        [ match Case
+        [ WithBounds (match Case)
         , Var (%%% "openTerm")
         , match Of
         ]
       , mkFoldCase <$> Seq
-        [ match FoldCase
+        [ WithBounds (match FoldCase)
         , Var (%%% "openTerm")
         , match By
         ]
@@ -592,29 +600,30 @@ CaseTerm =
 
   mkBranch :
     HList [String, String, (), TermFun] ->
-    Assoc (ParseFun 2 $ \tyCtx, tmCtx => (x ** Term tyCtx (tmCtx :< x)))
+    Assoc (ParseFun 2 $ \tyCtx, tmCtx => (x ** Term Bounds tyCtx (tmCtx :< x)))
   mkBranch [tag, bound, _, branch] =
     tag :- MkParseFun (\tyCtx, tmCtx => pure (bound ** !(branch.try tyCtx (tmCtx :< bound))))
 
-  mkCase : HList [_, TermFun, _] -> Cases -> TermFun
-  mkCase [_, target, _] branches =
+  mkCase : HList [WithBounds (), TermFun, _] -> Cases -> TermFun
+  mkCase [m, target, _] branches =
     let branches = map (map mkBranch) branches in
     MkParseFun (\tyCtx, tmCtx =>
-      [| Case (target.try tyCtx tmCtx) (tryRow2 branches tyCtx tmCtx) |])
+      pure $ Case m.bounds !(target.try tyCtx tmCtx) !(tryRow2 branches tyCtx tmCtx))
 
-  mkFoldCase : HList [_, TermFun, _] -> Cases -> TermFun
-  mkFoldCase [_, target, _] branches =
+  mkFoldCase : HList [WithBounds (), TermFun, _] -> Cases -> TermFun
+  mkFoldCase [m, target, _] branches =
     let branches = map (map mkBranch) branches in
     MkParseFun (\tyCtx, tmCtx =>
       pure $
       Fold
+        m.bounds
         !(target.try tyCtx tmCtx)
-        ("__tmp" ** Case (Var $ %% "__tmp") !(tryRow2 branches tyCtx (tmCtx :< "__tmp"))))
+        ("__tmp" ** Case m.bounds (Var m.bounds $ %% "__tmp") !(tryRow2 branches tyCtx (tmCtx :< "__tmp"))))
 
 FoldTerm : InkyParser False [<"openTerm" :- TermFun] [<] TermFun
 FoldTerm =
   mkFold <$> Seq
-    [ match Fold
+    [ WithBounds (match Fold)
     , Var (%%% "openTerm")
     , match By
     , enclose (match ParenOpen) (match ParenClose) $
@@ -626,10 +635,10 @@ FoldTerm =
         ]
     ]
   where
-  mkFold : HList [(), TermFun, (), HList [(), String, (), TermFun]] -> TermFun
-  mkFold [_, target, _, [_, arg, _, body]] =
+  mkFold : HList [WithBounds (), TermFun, (), HList [(), String, (), TermFun]] -> TermFun
+  mkFold [m, target, _, [_, arg, _, body]] =
     MkParseFun (\tyCtx, tmCtx =>
-      pure $ Fold !(target.try tyCtx tmCtx) (arg ** !(body.try tyCtx (tmCtx :< arg))))
+      pure $ Fold m.bounds !(target.try tyCtx tmCtx) (arg ** !(body.try tyCtx (tmCtx :< arg))))
 
 export
 OpenTerm : InkyParser False [<] [<] TermFun
diff --git a/src/Inky/Term/Pretty.idr b/src/Inky/Term/Pretty.idr
index 91a42b8..79e8f6c 100644
--- a/src/Inky/Term/Pretty.idr
+++ b/src/Inky/Term/Pretty.idr
@@ -1,11 +1,15 @@
 module Inky.Term.Pretty
 
+import Data.List.Quantifiers
 import Data.Singleton
 import Data.String
+import Data.These
 
 import Inky.Decidable.Maybe
 import Inky.Term
 import Inky.Type.Pretty
+
+import Text.Bounded
 import Text.PrettyPrint.Prettyprinter
 
 public export
@@ -43,12 +47,12 @@ Ord TermPrec where
   compare Open d2 = GT
 
 export
-prettyTerm : {tyCtx, tmCtx : SnocList String} -> Term tyCtx tmCtx -> TermPrec -> Doc ann
-prettyAllTerm : {tyCtx, tmCtx : SnocList String} -> List (Term tyCtx tmCtx) -> TermPrec -> List (Doc ann)
-prettyTermCtx : {tyCtx, tmCtx : SnocList String} -> Context (Term tyCtx tmCtx) -> TermPrec -> SnocList (Doc ann)
-prettyCases : {tyCtx, tmCtx : SnocList String} -> Context (x ** Term tyCtx (tmCtx :< x)) -> SnocList (Doc ann)
+prettyTerm : {tyCtx, tmCtx : SnocList String} -> Term m tyCtx tmCtx -> TermPrec -> Doc ann
+prettyAllTerm : {tyCtx, tmCtx : SnocList String} -> List (Term m tyCtx tmCtx) -> TermPrec -> List (Doc ann)
+prettyTermCtx : {tyCtx, tmCtx : SnocList String} -> Context (Term m tyCtx tmCtx) -> TermPrec -> SnocList (Doc ann)
+prettyCases : {tyCtx, tmCtx : SnocList String} -> Context (x ** Term m tyCtx (tmCtx :< x)) -> SnocList (Doc ann)
 prettyLet : Doc ann -> Doc ann -> Doc ann
-lessPrettyTerm : {tyCtx, tmCtx : SnocList String} -> Term tyCtx tmCtx -> TermPrec -> Doc ann
+lessPrettyTerm : {tyCtx, tmCtx : SnocList String} -> Term m tyCtx tmCtx -> TermPrec -> Doc ann
 
 prettyTerm t d =
   case isLit t <|> isCheckLit t of
@@ -65,7 +69,7 @@ prettyTermCtx [<] d = [<]
 prettyTermCtx (ts :< (l :- t)) d = prettyTermCtx ts d :< (pretty l <+> ":" <++> prettyTerm t d)
 
 prettyCases [<] = [<]
-prettyCases (ts :< (l :- (x ** Abs (bound ** t)))) =
+prettyCases (ts :< (l :- (x ** Abs _ (bound ** t)))) =
   prettyCases ts :<
   (group $ align $
     pretty l <++> pretty x <++> "=>" <++>
@@ -84,26 +88,26 @@ prettyLet binding term =
     "in") <+> line <+>
   term
 
-lessPrettyTerm (Annot t a) d =
+lessPrettyTerm (Annot _ t a) d =
   group $ align $ hang 2 $ parenthesise (d < Annot) $
     prettyTerm t App <++> ":" <+> line <+> prettyType a Open
-lessPrettyTerm (Var i) d = pretty (unVal $ nameOf i)
-lessPrettyTerm (Let e (x ** t)) d =
+lessPrettyTerm (Var _ i) d = pretty (unVal $ nameOf i)
+lessPrettyTerm (Let _ e (x ** t)) d =
   -- TODO: pretty print annotated abstraction
   group $ align $ parenthesise (d < Open) $
   prettyLet
     (pretty x <++> "=" <+> line <+> prettyTerm e Open)
     (prettyTerm t Open)
-lessPrettyTerm (LetTy a (x ** t)) d =
+lessPrettyTerm (LetTy _ a (x ** t)) d =
   group $ align $ parenthesise (d < Open) $
   prettyLet
     (pretty x <++> "=" <+> line <+> prettyType a Open)
     (prettyTerm t Open)
-lessPrettyTerm (Abs (bound ** t)) d =
+lessPrettyTerm (Abs _ (bound ** t)) d =
   group $ hang 2 $ parenthesise (d < Open) $
     "\\" <+> concatWith (surround $ "," <+> line) (map pretty bound) <++> "=>" <+> line <+>
     prettyTerm t Open
-lessPrettyTerm (App (Map (x ** a) b c) ts) d =
+lessPrettyTerm (App _ (Map _ (x ** a) b c) ts) d =
   group $ align $ hang 2 $ parenthesise (d < App) $
     concatWith (surround line)
       (  pretty "map"
@@ -111,29 +115,29 @@ lessPrettyTerm (App (Map (x ** a) b c) ts) d =
       :: prettyType b Atom
       :: prettyType c Atom
       :: prettyAllTerm ts Suffix)
-lessPrettyTerm (App (GetChildren (x ** a) b) ts) d =
+lessPrettyTerm (App _ (GetChildren _ (x ** a) b) ts) d =
   group $ align $ hang 2 $ parenthesise (d < App) $
     concatWith (surround line)
       (  pretty "getChildren"
       :: parens (group $ align $ hang 2 $ "\\" <+> pretty x <++> "=>" <+> line <+> prettyType a Open)
       :: prettyType b Atom
       :: prettyAllTerm ts Suffix)
-lessPrettyTerm (App f ts) d =
+lessPrettyTerm (App _ f ts) d =
   group $ align $ hang 2 $ parenthesise (d < App) $
     concatWith (surround line) (prettyTerm f Suffix :: prettyAllTerm ts Suffix)
-lessPrettyTerm (Tup (MkRow ts _)) d =
+lessPrettyTerm (Tup _ (MkRow ts _)) d =
   let parts = prettyTermCtx ts Open <>> [] in
   group $ align $ enclose "<" ">" $
     flatAlt
       (neutral <++> concatWith (surround $ line' <+> "," <++> neutral) parts <+> line)
       (concatWith (surround $ "," <++> neutral) parts)
-lessPrettyTerm (Prj e l) d =
+lessPrettyTerm (Prj _ e l) d =
   group $ align $ hang 2 $ parenthesise (d < Suffix) $
     prettyTerm e Suffix <+> line' <+> "." <+> pretty l
-lessPrettyTerm (Inj l t) d =
+lessPrettyTerm (Inj _ l t) d =
   group $ align $ hang 2 $ parenthesise (d < App) $
     pretty l <+> line <+> prettyTerm t Suffix
-lessPrettyTerm (Case e (MkRow ts _)) d =
+lessPrettyTerm (Case _ e (MkRow ts _)) d =
   let parts = prettyCases ts <>> [] in
   group $ align $ hang 2 $ parenthesise (d < Open) $
     (group $ hang (-2) $ "case" <++> prettyTerm e Open <+> line <+> "of") <+> line <+>
@@ -141,19 +145,19 @@ lessPrettyTerm (Case e (MkRow ts _)) d =
       flatAlt
         (neutral <++> concatWith (surround $ line' <+> ";" <++> neutral) parts <+> line)
         (concatWith (surround $ ";" <++> neutral) parts))
-lessPrettyTerm (Roll t) d =
+lessPrettyTerm (Roll _ t) d =
   pretty "~" <+>
   parenthesise (d < Prefix) (group $ align $ hang 2 $ prettyTerm t Prefix)
-lessPrettyTerm (Unroll e) d =
+lessPrettyTerm (Unroll _ e) d =
   pretty "!" <+>
   parenthesise (d > Prefix) (group $ align $ hang 2 $ prettyTerm e Prefix)
-lessPrettyTerm (Fold e (x ** t)) d =
+lessPrettyTerm (Fold _ e (x ** t)) d =
   -- TODO: foldcase
   group $ align $ hang 2 $ parenthesise (d < Open) $
     "fold" <++> prettyTerm e Open <++> "by" <+> hardline <+>
     (group $ align $ hang 2 $ parens $
       "\\" <+> pretty x <++> "=>" <+> line <+> prettyTerm t Open)
-lessPrettyTerm (Map (x ** a) b c) d =
+lessPrettyTerm (Map _ (x ** a) b c) d =
   group $ align $ hang 2 $ parenthesise (d < App) $
     concatWith (surround line)
       [ pretty "map"
@@ -161,10 +165,220 @@ lessPrettyTerm (Map (x ** a) b c) d =
       , prettyType b Atom
       , prettyType c Atom
       ]
-lessPrettyTerm (GetChildren (x ** a) b) d =
+lessPrettyTerm (GetChildren _ (x ** a) b) d =
   group $ align $ hang 2 $ parenthesise (d < App) $
     concatWith (surround line)
       [ pretty "getChildren"
       , group (align $ hang 2 $ parens $  "\\" <+> pretty x <++> "=>" <+> line <+> prettyType a Open)
       , prettyType b Atom
       ]
+
+-- Typing Errors ---------------------------------------------------------------
+
+Pretty (ChecksOnly t) where
+  pretty Abs = "abstraction"
+  pretty Inj = "injection"
+  pretty Case = "case split"
+  pretty Roll = "rolling"
+  pretty Fold = "fold"
+
+prettyNotSynths :
+  {tyCtx, tmCtx : SnocList String} ->
+  {e : Term m tyCtx tmCtx} ->
+  {tyEnv : _} -> {tmEnv : _} ->
+  NotSynths tyEnv tmEnv e ->
+  List (m, Doc ann)
+export
+prettyNotChecks :
+  {tyCtx, tmCtx : SnocList String} ->
+  {a : Ty [<]} ->
+  {t : Term m tyCtx tmCtx} ->
+  {tyEnv : _} -> {tmEnv : _} ->
+  NotChecks tyEnv tmEnv a t ->
+  List (m, Doc ann)
+prettyNotCheckSpine :
+  {tyCtx, tmCtx : SnocList String} ->
+  {a : Ty [<]} ->
+  {ts : List (Term m tyCtx tmCtx)} ->
+  {tyEnv : _} -> {tmEnv : _} ->
+  NotCheckSpine tyEnv tmEnv a ts ->
+  List (m, Doc ann)
+prettyAnyNotSynths :
+  {tyCtx, tmCtx : SnocList String} ->
+  {es : Context (Term m tyCtx tmCtx)} ->
+  {tyEnv : _} -> {tmEnv : _} ->
+  AnyNotSynths tyEnv tmEnv es ->
+  List (m, Doc ann)
+prettyAnyNotChecks :
+  {tyCtx, tmCtx : SnocList String} ->
+  {ts : Context (Term m tyCtx tmCtx)} ->
+  {tyEnv : _} -> {tmEnv : _} -> {as : Context _} ->
+  (meta : m) ->
+  AnyNotChecks tyEnv tmEnv as ts ->
+  List (m, Doc ann)
+prettyAnyNotBranches :
+  {tyCtx, tmCtx : SnocList String} ->
+  {ts : Context (x ** Term m tyCtx (tmCtx :< x))} ->
+  {tyEnv : _} -> {tmEnv : _} -> {as : Context _} -> {a : _} ->
+  (meta : m) ->
+  AnyNotBranches tyEnv tmEnv as a ts ->
+  List (m, Doc ann)
+
+prettyNotSynths (ChecksNS shape) =
+  [(e.meta, pretty "cannot synthesise type of" <++> pretty shape)]
+prettyNotSynths (AnnotNS {a} (This contra)) =
+  [(e.meta, pretty "ill-formed type" <+> line <+> prettyType a Open)]
+prettyNotSynths (AnnotNS (That contra)) = prettyNotChecks contra
+prettyNotSynths (AnnotNS {a} (Both contra1 contra2)) =
+  (e.meta, pretty "ill-formed type" <+> line <+> prettyType a Open) ::
+  prettyNotChecks contra2
+prettyNotSynths (LetNS1 contra) = prettyNotSynths contra
+prettyNotSynths (LetNS2 prf contra) =
+  case synthsRecompute prf of
+    Val a => prettyNotSynths contra
+prettyNotSynths (LetTyNS {a} (This contra)) =
+  [(e.meta, pretty "ill-formed type" <+> line <+> prettyType a Open)]
+prettyNotSynths (LetTyNS (That contra)) = prettyNotSynths contra
+prettyNotSynths (LetTyNS {a} (Both contra1 contra2)) =
+  (e.meta, pretty "ill-formed type" <+> line <+> prettyType a Open)
+  :: prettyNotSynths contra2
+prettyNotSynths (AppNS1 contra) = prettyNotSynths contra
+prettyNotSynths (AppNS2 prf contras) =
+  case synthsRecompute prf of
+    Val a => prettyNotCheckSpine contras
+prettyNotSynths (TupNS contras) = prettyAnyNotSynths contras
+prettyNotSynths (PrjNS1 contra) = prettyNotSynths contra
+prettyNotSynths (PrjNS2 prf f) =
+  case synthsRecompute prf of
+    Val a =>
+      [(e.meta
+      , pretty "cannot project non-product type" <+> line <+>
+        prettyType a Open
+      )]
+prettyNotSynths (PrjNS3 {l, as} prf contra) =
+  case synthsRecompute prf of
+    Val (TProd as) =>
+      [(e.meta
+      , pretty "unknown label" <++> enclose "'" "'" (pretty l) <+> line <+>
+        pretty "in product type" <+> line <+>
+        prettyType (TProd as) Open
+      )]
+prettyNotSynths (UnrollNS1 contra) = prettyNotSynths contra
+prettyNotSynths (UnrollNS2 prf contra) =
+  case synthsRecompute prf of
+    Val a =>
+      [(e.meta
+      , pretty "cannot unroll non-inductive type" <+> line <+>
+        prettyType a Open
+      )]
+prettyNotSynths (MapNS {a} {b} {c} contras) =
+  bifoldMap
+    (const [(e.meta, pretty "ill-formed functor" <+> line <+> prettyType a Open)])
+    (bifoldMap
+      (const [(e.meta, pretty "ill-formed source" <+> line <+> prettyType b Open)])
+      (const [(e.meta, pretty "ill-formed target" <+> line <+> prettyType c Open)]))
+    contras
+prettyNotSynths (GetChildrenNS {a} {b}  contras) =
+  bifoldMap
+    (const [(e.meta, pretty "ill-formed functor" <+> line <+> prettyType a Open)])
+    (const [(e.meta, pretty "ill-formed contents" <+> line <+> prettyType b Open)])
+    contras
+
+prettyNotChecks (EmbedNC1 _ contra) = prettyNotSynths contra
+prettyNotChecks (EmbedNC2 _ prf contra) =
+  case synthsRecompute prf of
+    Val b =>
+      [(t.meta
+      , pretty "cannot unify" <+> line <+>
+        prettyType a Open <+> line <+>
+        pretty "and" <+> line <+>
+        prettyType b Open
+      )]
+prettyNotChecks (LetNC1 contra) = prettyNotSynths contra
+prettyNotChecks (LetNC2 prf contra) =
+  case synthsRecompute prf of
+    Val _ => prettyNotChecks contra
+prettyNotChecks (LetTyNC {a} (This contra)) =
+  [(t.meta, pretty "ill-formed type" <+> line <+> prettyType a Open)]
+prettyNotChecks (LetTyNC (That contra)) = prettyNotChecks contra
+prettyNotChecks (LetTyNC (Both contra1 contra2)) =
+  (t.meta, pretty "ill-formed type" <+> line <+> prettyType a Open) ::
+  prettyNotChecks contra2
+prettyNotChecks (AbsNC1 contra) =
+  [(t.meta, pretty "cannot abstract to construct type" <+> line <+> prettyType a Open)]
+prettyNotChecks (AbsNC2 prf contra) =
+  case isFunctionRecompute prf of
+    (Val _, Val _) => prettyNotChecks contra
+prettyNotChecks (TupNC1 contra) =
+  [(t.meta, pretty "cannot tuple to construct type" <+> line <+> prettyType a Open)]
+prettyNotChecks (TupNC2 contras) = prettyAnyNotChecks t.meta contras
+prettyNotChecks (InjNC1 contra) =
+  [(t.meta, pretty "cannot inject to construct type" <+> line <+> prettyType a Open)]
+prettyNotChecks (InjNC2 {l} contra) =
+  [(t.meta
+  , pretty "unknown label" <++> enclose "'" "'" (pretty l) <+> line <+>
+    pretty "in sum type" <+> line <+>
+    prettyType a Open
+  )]
+prettyNotChecks (InjNC3 i contra) =
+  case [| (nameOf i).value |] of
+    Val _ => prettyNotChecks contra
+prettyNotChecks (CaseNC1 contra) = prettyNotSynths contra
+prettyNotChecks (CaseNC2 prf contra) =
+  case synthsRecompute prf of
+    Val a => [(t.meta, pretty "cannot case split on type" <+> line <+> prettyType a Open)]
+prettyNotChecks (CaseNC3 prf contras) =
+  case synthsRecompute prf of
+    Val _ => prettyAnyNotBranches t.meta contras
+prettyNotChecks (RollNC1 contra) =
+  [(t.meta, pretty "cannot roll to construct type" <+> line <+> prettyType a Open)]
+prettyNotChecks (RollNC2 contra) = prettyNotChecks contra
+prettyNotChecks (FoldNC1 contra) = prettyNotSynths contra
+prettyNotChecks (FoldNC2 prf contra) =
+  case synthsRecompute prf of
+    Val a => [(t.meta, pretty "cannot fold over type" <+> line <+> prettyType a Open)]
+prettyNotChecks (FoldNC3 prf contra) =
+  case synthsRecompute prf of
+    Val _ => prettyNotChecks contra
+
+prettyNotCheckSpine (Step1 {t} contra) =
+  [(t.meta, pretty "cannot apply non-function type" <+> line <+> prettyType a Open)]
+prettyNotCheckSpine (Step2 (This contra)) = prettyNotChecks contra
+prettyNotCheckSpine (Step2 (That contra)) = prettyNotCheckSpine contra
+prettyNotCheckSpine (Step2 (Both contra1 contra2)) =
+  prettyNotChecks contra1 ++ prettyNotCheckSpine contra2
+
+prettyAnyNotSynths (Step (This contra)) = prettyNotSynths contra
+prettyAnyNotSynths (Step (That contra)) = prettyAnyNotSynths contra
+prettyAnyNotSynths (Step (Both contra1 contra2)) =
+  prettyNotSynths contra1 ++ prettyAnyNotSynths contra2
+
+prettyAnyNotChecks meta Base1 =
+  [(meta
+  , pretty "missing components" <+> line <+>
+    concatWith (surround $ "," <++> neutral) (map pretty as.names <>> [])
+  )]
+prettyAnyNotChecks meta (Step1 {t, l} contra) =
+  [(t.meta , pretty "unknown label" <++> enclose "'" "'" (pretty l))]
+prettyAnyNotChecks meta (Step2 i (This contra)) =
+  case [| (nameOf i).value |] of
+    Val _ => prettyNotChecks contra
+prettyAnyNotChecks meta (Step2 i (That contra)) = prettyAnyNotChecks meta contra
+prettyAnyNotChecks meta (Step2 i (Both contra1 contra2)) =
+  case [| (nameOf i).value |] of
+    Val _ => prettyNotChecks contra1 ++ prettyAnyNotChecks meta contra2
+
+prettyAnyNotBranches meta Base1 =
+  [(meta
+  , pretty "missing cases" <+> line <+>
+    concatWith (surround $ "," <++> neutral) (map pretty as.names <>> [])
+  )]
+prettyAnyNotBranches meta (Step1 {t, l} contra) =
+  [(t.meta , pretty "unknown label" <++> enclose "'" "'" (pretty l))]
+prettyAnyNotBranches meta (Step2 i (This contra)) =
+  case [| (nameOf i).value |] of
+    Val _ => prettyNotChecks contra
+prettyAnyNotBranches meta (Step2 i (That contra)) = prettyAnyNotBranches meta contra
+prettyAnyNotBranches meta (Step2 i (Both contra1 contra2)) =
+  case [| (nameOf i).value |] of
+    Val _ => prettyNotChecks contra1 ++ prettyAnyNotBranches meta contra2