{-# LANGUAGE DeriveDataTypeable #-}
{-# LANGUAGE OverloadedStrings  #-}
{-# LANGUAGE RankNTypes         #-}
{-# LANGUAGE RecordWildCards    #-}
{-# OPTIONS_GHC -Wall #-}

-- | This module contains the logic for type checking Dhall code

module Dhall.TypeCheck (
    -- * Type-checking
      typeWith
    , typeOf
    , typeWithA
    , checkContext

    -- * Types
    , Typer
    , X
    , absurd
    , TypeError(..)
    , DetailedTypeError(..)
    , TypeMessage(..)
    ) where

import Data.Void (Void, absurd)
import Control.Exception (Exception)
import Control.Monad.Trans.Class (lift)
import Control.Monad.Trans.Writer.Strict (execWriterT, tell)
import Data.Functor (void)
import Data.Monoid (Endo(..), First(..))
import Data.Sequence (Seq, ViewL(..))
import Data.Semigroup (Max(..), Semigroup(..))
import Data.Set (Set)
import Data.Text (Text)
import Data.Text.Prettyprint.Doc (Doc, Pretty(..))
import Data.Typeable (Typeable)
import Dhall.Binary (ToTerm(..))
import Dhall.Core (Binding(..), Const(..), Chunks(..), Expr(..), Var(..))
import Dhall.Context (Context)
import Dhall.Pretty (Ann, layoutOpts)

import qualified Data.Foldable
import qualified Data.Map
import qualified Data.Sequence
import qualified Data.Set
import qualified Data.Text                               as Text
import qualified Data.Text.Prettyprint.Doc               as Pretty
import qualified Data.Text.Prettyprint.Doc.Render.String as Pretty
import qualified Dhall.Context
import qualified Dhall.Core
import qualified Dhall.Diff
import qualified Dhall.Map
import qualified Dhall.Set
import qualified Dhall.Pretty.Internal
import qualified Dhall.Util

type X = Void

traverseWithIndex_ :: Applicative f => (Int -> a -> f b) -> Seq a -> f ()
traverseWithIndex_ k xs =
    Data.Foldable.sequenceA_ (Data.Sequence.mapWithIndex k xs)

axiom :: Const -> Either (TypeError s a) Const
axiom Type = return Kind
axiom Kind = return Sort
axiom Sort = Left (TypeError Dhall.Context.empty (Const Sort) Untyped)

rule :: Const -> Const -> Const
rule Type Type = Type
rule Kind Type = Type
rule Sort Type = Type
rule Type Kind = Kind
rule Kind Kind = Kind
rule Sort Kind = Sort
rule Type Sort = Sort
rule Kind Sort = Sort
rule Sort Sort = Sort

{-| Type-check an expression and return the expression's type if type-checking
    succeeds or an error if type-checking fails

    `typeWith` does not necessarily normalize the type since full normalization
    is not necessary for just type-checking.  If you actually care about the
    returned type then you may want to `Dhall.Core.normalize` it afterwards.

    The supplied `Context` records the types of the names in scope. If
    these are ill-typed, the return value may be ill-typed.
-}
typeWith :: Context (Expr s X) -> Expr s X -> Either (TypeError s X) (Expr s X)
typeWith ctx expr = do
    checkContext ctx
    typeWithA absurd ctx expr

{-| Function that converts the value inside an `Embed` constructor into a new
    expression
-}
type Typer a = forall s. a -> Expr s a

{-| Generalization of `typeWith` that allows type-checking the `Embed`
    constructor with custom logic
-}
typeWithA
    :: (Eq a, Pretty a)
    => Typer a
    -> Context (Expr s a)
    -> Expr s a
    -> Either (TypeError s a) (Expr s a)
typeWithA tpa = loop
  where
    loop _     (Const c         ) = do
        fmap Const (axiom c)
    loop ctx e@(Var (V x n)     ) = do
        case Dhall.Context.lookup x n ctx of
            Nothing -> Left (TypeError ctx e (UnboundVariable x))
            Just a  -> do
                -- Note: no need to typecheck the value we're
                -- returning; that is done at insertion time.
                return a
    loop ctx   (Lam x _A  b     ) = do
        _ <- loop ctx _A
        let ctx' = fmap (Dhall.Core.shift 1 (V x 0)) (Dhall.Context.insert x (Dhall.Core.normalize _A) ctx)
        _B <- loop ctx' b
        let p = Pi x _A _B
        _t <- loop ctx p
        return p
    loop ctx e@(Pi  x _A _B     ) = do
        tA <- fmap Dhall.Core.normalize (loop ctx _A)
        kA <- case tA of
            Const k -> return k
            _       -> Left (TypeError ctx e (InvalidInputType _A))

        let ctx' = fmap (Dhall.Core.shift 1 (V x 0)) (Dhall.Context.insert x (Dhall.Core.normalize _A) ctx)
        tB <- fmap Dhall.Core.normalize (loop ctx' _B)
        kB <- case tB of
            Const k -> return k
            _       -> Left (TypeError ctx' e (InvalidOutputType _B))

        return (Const (rule kA kB))
    loop ctx e@(App f a         ) = do
        tf <- fmap Dhall.Core.normalize (loop ctx f)
        (x, _A, _B) <- case tf of
            Pi x _A _B -> return (x, _A, _B)
            _          -> Left (TypeError ctx e (NotAFunction f tf))
        _A' <- loop ctx a
        if Dhall.Core.judgmentallyEqual _A _A'
            then do
                let a'   = Dhall.Core.shift   1  (V x 0) a
                let _B'  = Dhall.Core.subst (V x 0) a' _B
                let _B'' = Dhall.Core.shift (-1) (V x 0) _B'
                return _B''
            else do
                let nf_A  = Dhall.Core.normalize _A
                let nf_A' = Dhall.Core.normalize _A'
                Left (TypeError ctx e (TypeMismatch f nf_A a nf_A'))
    loop ctx e@(Let (Binding _ x _ mA _ a0) b0) = do
        _A1 <- loop ctx a0
        case mA of
            Just (_, _A0) -> do
                _ <- loop ctx _A0
                let nf_A0 = Dhall.Core.normalize _A0
                let nf_A1 = Dhall.Core.normalize _A1
                if Dhall.Core.judgmentallyEqual _A0 _A1
                    then return ()
                    else Left (TypeError ctx e (AnnotMismatch a0 nf_A0 nf_A1))
            Nothing -> return ()

        let a1 = Dhall.Core.normalize a0
        let a2 = Dhall.Core.shift 1 (V x 0) a1

        let b1 = Dhall.Core.subst (V x 0) a2 b0
        let b2 = Dhall.Core.shift (-1) (V x 0) b1
        loop ctx b2

    loop ctx e@(Annot x t       ) = do
        case Dhall.Core.denote t of
            Const _ -> return ()
            _       -> void (loop ctx t)

        t' <- loop ctx x
        if Dhall.Core.judgmentallyEqual t t'
            then do
                return t
            else do
                let nf_t  = Dhall.Core.normalize t
                let nf_t' = Dhall.Core.normalize t'
                Left (TypeError ctx e (AnnotMismatch x nf_t nf_t'))
    loop _      Bool              = do
        return (Const Type)
    loop _     (BoolLit _       ) = do
        return Bool
    loop ctx e@(BoolAnd l r     ) = do
        tl <- fmap Dhall.Core.normalize (loop ctx l)
        case tl of
            Bool -> return ()
            _    -> Left (TypeError ctx e (CantAnd l tl))

        tr <- fmap Dhall.Core.normalize (loop ctx r)
        case tr of
            Bool -> return ()
            _    -> Left (TypeError ctx e (CantAnd r tr))

        return Bool
    loop ctx e@(BoolOr  l r     ) = do
        tl <- fmap Dhall.Core.normalize (loop ctx l)
        case tl of
            Bool -> return ()
            _    -> Left (TypeError ctx e (CantOr l tl))

        tr <- fmap Dhall.Core.normalize (loop ctx r)
        case tr of
            Bool -> return ()
            _    -> Left (TypeError ctx e (CantOr r tr))

        return Bool
    loop ctx e@(BoolEQ  l r     ) = do
        tl <- fmap Dhall.Core.normalize (loop ctx l)
        case tl of
            Bool -> return ()
            _    -> Left (TypeError ctx e (CantEQ l tl))

        tr <- fmap Dhall.Core.normalize (loop ctx r)
        case tr of
            Bool -> return ()
            _    -> Left (TypeError ctx e (CantEQ r tr))

        return Bool
    loop ctx e@(BoolNE  l r     ) = do
        tl <- fmap Dhall.Core.normalize (loop ctx l)
        case tl of
            Bool -> return ()
            _    -> Left (TypeError ctx e (CantNE l tl))

        tr <- fmap Dhall.Core.normalize (loop ctx r)
        case tr of
            Bool -> return ()
            _    -> Left (TypeError ctx e (CantNE r tr))

        return Bool
    loop ctx e@(BoolIf x y z    ) = do
        tx <- fmap Dhall.Core.normalize (loop ctx x)
        case tx of
            Bool -> return ()
            _    -> Left (TypeError ctx e (InvalidPredicate x tx))
        ty  <- fmap Dhall.Core.normalize (loop ctx y )
        tty <- fmap Dhall.Core.normalize (loop ctx ty)
        case tty of
            Const Type -> return ()
            _          -> Left (TypeError ctx e (IfBranchMustBeTerm True y ty tty))

        tz <- fmap Dhall.Core.normalize (loop ctx z)
        ttz <- fmap Dhall.Core.normalize (loop ctx tz)
        case ttz of
            Const Type -> return ()
            _          -> Left (TypeError ctx e (IfBranchMustBeTerm False z tz ttz))

        if Dhall.Core.judgmentallyEqual ty tz
            then return ()
            else Left (TypeError ctx e (IfBranchMismatch y z ty tz))
        return ty
    loop _      Natural           = do
        return (Const Type)
    loop _     (NaturalLit _    ) = do
        return Natural
    loop _      NaturalFold       = do
        return
            (Pi "_" Natural
                (Pi "natural" (Const Type)
                    (Pi "succ" (Pi "_" "natural" "natural")
                        (Pi "zero" "natural" "natural") ) ) )
    loop _      NaturalBuild      = do
        return
            (Pi "_"
                (Pi "natural" (Const Type)
                    (Pi "succ" (Pi "_" "natural" "natural")
                        (Pi "zero" "natural" "natural") ) )
                Natural )
    loop _      NaturalIsZero     = do
        return (Pi "_" Natural Bool)
    loop _      NaturalEven       = do
        return (Pi "_" Natural Bool)
    loop _      NaturalOdd        = do
        return (Pi "_" Natural Bool)
    loop _      NaturalToInteger  = do
        return (Pi "_" Natural Integer)
    loop _      NaturalShow  = do
        return (Pi "_" Natural Text)
    loop _      NaturalSubtract  = do
        return (Pi "_" Natural (Pi "_" Natural Natural))
    loop ctx e@(NaturalPlus  l r) = do
        tl <- fmap Dhall.Core.normalize (loop ctx l)
        case tl of
            Natural -> return ()
            _       -> Left (TypeError ctx e (CantAdd l tl))

        tr <- fmap Dhall.Core.normalize (loop ctx r)
        case tr of
            Natural -> return ()
            _       -> Left (TypeError ctx e (CantAdd r tr))
        return Natural
    loop ctx e@(NaturalTimes l r) = do
        tl <- fmap Dhall.Core.normalize (loop ctx l)
        case tl of
            Natural -> return ()
            _       -> Left (TypeError ctx e (CantMultiply l tl))

        tr <- fmap Dhall.Core.normalize (loop ctx r)
        case tr of
            Natural -> return ()
            _       -> Left (TypeError ctx e (CantMultiply r tr))
        return Natural
    loop _      Integer           = do
        return (Const Type)
    loop _     (IntegerLit _    ) = do
        return Integer
    loop _      IntegerShow  = do
        return (Pi "_" Integer Text)
    loop _      IntegerToDouble = do
        return (Pi "_" Integer Double)
    loop _      Double            = do
        return (Const Type)
    loop _     (DoubleLit _     ) = do
        return Double
    loop _     DoubleShow         = do
        return (Pi "_" Double Text)
    loop _      Text              = do
        return (Const Type)
    loop ctx e@(TextLit (Chunks xys _)) = do
        let process (_, y) = do
                ty <- fmap Dhall.Core.normalize (loop ctx y)
                case ty of
                    Text -> return ()
                    _    -> Left (TypeError ctx e (CantInterpolate y ty))
        mapM_ process xys
        return Text
    loop ctx e@(TextAppend l r  ) = do
        tl <- fmap Dhall.Core.normalize (loop ctx l)
        case tl of
            Text -> return ()
            _    -> Left (TypeError ctx e (CantTextAppend l tl))

        tr <- fmap Dhall.Core.normalize (loop ctx r)
        case tr of
            Text -> return ()
            _    -> Left (TypeError ctx e (CantTextAppend r tr))
        return Text
    loop _      TextShow          = do
        return (Pi "_" Text Text)
    loop _      List              = do
        return (Pi "_" (Const Type) (Const Type))
    loop ctx e@(ListLit  Nothing  xs) = do
        case Data.Sequence.viewl xs of
            x0 :< xs' -> do
                t <- loop ctx x0
                s <- fmap Dhall.Core.normalize (loop ctx t)
                case s of
                    Const Type -> return ()
                    _ -> Left (TypeError ctx e (InvalidListType (App List t)))
                flip traverseWithIndex_ xs' (\i x -> do
                    t' <- loop ctx x
                    if Dhall.Core.judgmentallyEqual t t'
                        then return ()
                        else do
                            let nf_t  = Dhall.Core.normalize t
                            let nf_t' = Dhall.Core.normalize t'
                            let err   = MismatchedListElements i nf_t x nf_t'
                            Left (TypeError ctx x err) )
                return (App List t)
            _ -> Left (TypeError ctx e MissingListType)
    loop ctx e@(ListLit (Just t0) xs) = do
        _ <- loop ctx t0
        let nf_t0 = Dhall.Core.normalize t0
        t1 <- case nf_t0 of
            App List t1 -> do
                s <- fmap Dhall.Core.normalize (loop ctx t1)
                case s of
                    Const Type -> return t1
                    _ -> Left (TypeError ctx e (InvalidListType nf_t0))
            _ -> Left (TypeError ctx e (InvalidListType nf_t0))
        flip traverseWithIndex_ xs (\i x -> do
            t' <- loop ctx x
            if Dhall.Core.judgmentallyEqual t1 t'
                then return ()
                else do
                    let nf_t  = Dhall.Core.normalize t1
                    let nf_t' = Dhall.Core.normalize t'
                    Left (TypeError ctx x (InvalidListElement i nf_t x nf_t')) )
        return (App List t1)
    loop ctx e@(ListAppend l r  ) = do
        tl <- fmap Dhall.Core.normalize (loop ctx l)
        el <- case tl of
            App List el -> return el
            _           -> Left (TypeError ctx e (CantListAppend l tl))

        tr <- fmap Dhall.Core.normalize (loop ctx r)
        er <- case tr of
            App List er -> return er
            _           -> Left (TypeError ctx e (CantListAppend r tr))

        if Dhall.Core.judgmentallyEqual el er
            then return (App List el)
            else Left (TypeError ctx e (ListAppendMismatch el er))
    loop _      ListBuild         = do
        return
            (Pi "a" (Const Type)
                (Pi "_"
                    (Pi "list" (Const Type)
                        (Pi "cons" (Pi "_" "a" (Pi "_" "list" "list"))
                            (Pi "nil" "list" "list") ) )
                    (App List "a") ) )
    loop _      ListFold          = do
        return
            (Pi "a" (Const Type)
                (Pi "_" (App List "a")
                    (Pi "list" (Const Type)
                        (Pi "cons" (Pi "_" "a" (Pi "_" "list" "list"))
                            (Pi "nil" "list" "list")) ) ) )
    loop _      ListLength        = do
        return (Pi "a" (Const Type) (Pi "_" (App List "a") Natural))
    loop _      ListHead          = do
        return (Pi "a" (Const Type) (Pi "_" (App List "a") (App Optional "a")))
    loop _      ListLast          = do
        return (Pi "a" (Const Type) (Pi "_" (App List "a") (App Optional "a")))
    loop _      ListIndexed       = do
        let kts = [("index", Natural), ("value", "a")]
        return
            (Pi "a" (Const Type)
                (Pi "_" (App List "a")
                    (App List (Record (Dhall.Map.fromList kts))) ) )
    loop _      ListReverse       = do
        return (Pi "a" (Const Type) (Pi "_" (App List "a") (App List "a")))
    loop _      Optional          = do
        return (Pi "_" (Const Type) (Const Type))
    loop _      None              = do
        return (Pi "A" (Const Type) (App Optional "A"))
    loop ctx e@(Some a) = do
        _A <- loop ctx a
        s <- fmap Dhall.Core.normalize (loop ctx _A)
        case s of
            Const Type -> return ()
            _          -> Left (TypeError ctx e (InvalidSome a _A s))
        return (App Optional _A)
    loop _      OptionalFold      = do
        return
            (Pi "a" (Const Type)
                (Pi "_" (App Optional "a")
                    (Pi "optional" (Const Type)
                        (Pi "just" (Pi "_" "a" "optional")
                            (Pi "nothing" "optional" "optional") ) ) ) )
    loop _      OptionalBuild     = do
        return
            (Pi "a" (Const Type)
                (Pi "_" f (App Optional "a") ) )
        where f = Pi "optional" (Const Type)
                      (Pi "just" (Pi "_" "a" "optional")
                          (Pi "nothing" "optional" "optional") )
    loop ctx e@(Record    kts   ) = do
        let process k t = do
                s <- lift (fmap Dhall.Core.normalize (loop ctx t))
                case s of
                    Const c -> tell (Max c)
                    _ -> lift (Left (TypeError ctx e (InvalidFieldType k t)))
        Max c <- execWriterT (Dhall.Map.unorderedTraverseWithKey_ process kts)
        return (Const c)
    loop ctx e@(RecordLit kvs   ) = do
        let process k v = do
                t <- loop ctx v
                s <- fmap Dhall.Core.normalize (loop ctx t)
                case s of
                    Const _ -> return t
                    _ -> Left (TypeError ctx e (InvalidFieldType k t))

        Record <$> Dhall.Map.unorderedTraverseWithKey process kvs
    loop ctx e@(Union     kts   ) = do
        let nonEmpty k mt = First (fmap (\t -> (k, t)) mt)

        case getFirst (Dhall.Map.foldMapWithKey nonEmpty kts) of
            Nothing -> do
                return (Const Type)

            Just (k0, t0) -> do
                s0 <- fmap Dhall.Core.normalize (loop ctx t0)

                c0 <- case s0 of
                    Const c0 -> do
                        return c0

                    _ -> do
                        Left (TypeError ctx e (InvalidAlternativeType k0 t0))

                let process _ Nothing = do
                        return ()

                    process k (Just t) = do
                        s <- fmap Dhall.Core.normalize (loop ctx t)

                        c <- case s of
                            Const c -> do
                                return c

                            _ -> do
                                Left (TypeError ctx e (InvalidAlternativeType k t))

                        if c0 == c
                            then return ()
                            else Left (TypeError ctx e (AlternativeAnnotationMismatch k t c k0 t0 c0))

                Dhall.Map.unorderedTraverseWithKey_ process (Dhall.Map.delete k0 kts)

                return (Const c0)
    loop ctx e@(Combine kvsX kvsY) = do
        tKvsX <- fmap Dhall.Core.normalize (loop ctx kvsX)
        ktsX  <- case tKvsX of
            Record kts -> return kts
            _          -> Left (TypeError ctx e (MustCombineARecord '∧' kvsX tKvsX))

        tKvsY <- fmap Dhall.Core.normalize (loop ctx kvsY)
        ktsY  <- case tKvsY of
            Record kts -> return kts
            _          -> Left (TypeError ctx e (MustCombineARecord '∧' kvsY tKvsY))

        let combineTypes ktsL ktsR = do
                let combine _ (Record ktsL') (Record ktsR') = combineTypes ktsL' ktsR'
                    combine k _ _ = Left (TypeError ctx e (FieldCollision k))

                let eKts = Dhall.Map.outerJoin Right Right combine
                                               ktsL ktsR

                fmap Record (Dhall.Map.unorderedTraverseWithKey (\_k v -> v) eKts)

        combineTypes ktsX ktsY
    loop ctx e@(CombineTypes l r) = do
        tL <- loop ctx l
        let l' = Dhall.Core.normalize l
        cL <- case tL of
            Const cL -> return cL
            _        -> Left (TypeError ctx e (CombineTypesRequiresRecordType l l'))
        tR <- loop ctx r
        let r' = Dhall.Core.normalize r
        cR <- case tR of
            Const cR -> return cR
            _        -> Left (TypeError ctx e (CombineTypesRequiresRecordType r r'))
        let c = max cL cR

        ktsL0 <- case l' of
            Record kts -> return kts
            _          -> Left (TypeError ctx e (CombineTypesRequiresRecordType l l'))
        ktsR0 <- case r' of
            Record kts -> return kts
            _          -> Left (TypeError ctx e (CombineTypesRequiresRecordType r r'))

        let combineTypes ktsL ktsR = do
                let mL = Dhall.Map.toMap ktsL
                let mR = Dhall.Map.toMap ktsR

                let combine _ (Record ktsL') (Record ktsR') = combineTypes ktsL' ktsR'
                    combine k _ _ = Left (TypeError ctx e (FieldCollision k))

                Data.Foldable.sequence_ (Data.Map.intersectionWithKey combine mL mR)

        combineTypes ktsL0 ktsR0

        return (Const c)
    loop ctx e@(Prefer kvsX kvsY) = do
        tKvsX <- fmap Dhall.Core.normalize (loop ctx kvsX)
        ktsX  <- case tKvsX of
            Record kts -> return kts
            _          -> Left (TypeError ctx e (MustCombineARecord '⫽' kvsX tKvsX))

        tKvsY <- fmap Dhall.Core.normalize (loop ctx kvsY)
        ktsY  <- case tKvsY of
            Record kts -> return kts
            _          -> Left (TypeError ctx e (MustCombineARecord '⫽' kvsY tKvsY))

        return (Record (Dhall.Map.union ktsY ktsX))
    loop ctx e@(Merge kvsX kvsY mT₁) = do
        tKvsX <- fmap Dhall.Core.normalize (loop ctx kvsX)

        ktsX <- case tKvsX of
            Record kts -> return kts
            _          -> Left (TypeError ctx e (MustMergeARecord kvsX tKvsX))

        tKvsY <- fmap Dhall.Core.normalize (loop ctx kvsY)

        ktsY <- case tKvsY of
            Union kts -> return kts
            _         -> Left (TypeError ctx e (MustMergeUnion kvsY tKvsY))

        let ksX = Dhall.Map.keysSet ktsX
        let ksY = Dhall.Map.keysSet ktsY

        let diffX = Data.Set.difference ksX ksY
        let diffY = Data.Set.difference ksY ksX

        if Data.Set.null diffX
            then return ()
            else Left (TypeError ctx e (UnusedHandler diffX))

        (mKX, _T₁) <- do
            case mT₁ of
                Just _T₁ -> do
                    return (Nothing, _T₁)

                Nothing -> do
                    case Dhall.Map.uncons ktsX of
                        Nothing -> do
                            Left (TypeError ctx e MissingMergeType)

                        Just (kX, tX, _) -> do
                            _T₁ <- do
                                case Dhall.Map.lookup kX ktsY of
                                    Nothing -> do
                                        Left (TypeError ctx e (UnusedHandler diffX))

                                    Just Nothing -> do
                                        return tX

                                    Just (Just _)  ->
                                        case tX of
                                            Pi x _A₀ _T₀ -> do
                                                return (Dhall.Core.shift (-1) (V x 0) _T₀)
                                            _ -> do
                                                Left (TypeError ctx e (HandlerNotAFunction kX tX))

                            return (Just kX, _T₁)

        _ <- loop ctx _T₁

        let process kY mTY = do
                case Dhall.Map.lookup kY ktsX of
                    Nothing -> do
                        Left (TypeError ctx e (MissingHandler diffY))

                    Just tX -> do
                        _T₃ <- do
                            case mTY of
                                Nothing -> do
                                    return tX
                                Just _A₁ -> do
                                    case tX of
                                        Pi x _A₀ _T₂ -> do
                                            if Dhall.Core.judgmentallyEqual _A₀ _A₁
                                                then return ()
                                                else Left (TypeError ctx e (HandlerInputTypeMismatch kY _A₁ _A₀))

                                            return (Dhall.Core.shift (-1) (V x 0) _T₂)
                                        _ -> do
                                            Left (TypeError ctx e (HandlerNotAFunction kY tX))

                        if Dhall.Core.judgmentallyEqual _T₁ _T₃
                            then return ()
                            else
                                case mKX of
                                    Nothing -> do
                                        Left (TypeError ctx e (InvalidHandlerOutputType kY _T₁ _T₃))
                                    Just kX -> do
                                        Left (TypeError ctx e (HandlerOutputTypeMismatch kX _T₁ kY _T₃))

        Dhall.Map.unorderedTraverseWithKey_ process ktsY

        return _T₁

    loop ctx e@(ToMap kvsX mT₁) = do
        tKvsX <- fmap Dhall.Core.normalize (loop ctx kvsX)

        ktsX <- case tKvsX of
            Record kts -> return kts
            _          -> Left (TypeError ctx e (MustMapARecord kvsX tKvsX))

        _TKvsX <- loop ctx tKvsX

        case _TKvsX of
            Const Type -> return ()
            kind       -> Left (TypeError ctx e (InvalidToMapRecordKind tKvsX kind))

        Data.Foldable.traverse_ (loop ctx) mT₁

        let ktX = appEndo (foldMap (Endo . compareFieldTypes) ktsX) Nothing
            mT₂ = fmap Dhall.Core.normalize mT₁
            mapType fieldType = App List (Record $ Dhall.Map.fromList [("mapKey", Text),
                                                                       ("mapValue", fieldType)])
            compareFieldTypes t Nothing = Just (Right t)
            compareFieldTypes t r@(Just (Right t'))
               | Dhall.Core.judgmentallyEqual t t' = r
               | otherwise = Just (Left $ TypeError ctx e (HeterogenousRecordToMap tKvsX t t'))
            compareFieldTypes _ r@(Just Left{}) = r

        case (ktX, mT₂) of
            (Nothing, Nothing) -> Left (TypeError ctx e MissingToMapType)
            (Just err@Left{}, _) -> err
            (Just (Right t), Nothing) -> pure (mapType t)
            (Nothing, Just t@(App List (Record mapItemType)))
               | Just fieldType <- Dhall.Map.lookup "mapValue" mapItemType,
                 Dhall.Core.judgmentallyEqual t (mapType fieldType) -> pure t
            (Nothing, Just t) -> Left (TypeError ctx e $ InvalidToMapType t)
            (Just (Right t₁), Just t₂)
               | Dhall.Core.judgmentallyEqual (mapType t₁) t₂ -> pure t₂
               | otherwise -> Left (TypeError ctx e $ MapTypeMismatch (mapType t₁) t₂)
    loop ctx e@(Field r x       ) = do
        t <- fmap Dhall.Core.normalize (loop ctx r)

        let text = Dhall.Pretty.Internal.docToStrictText (Dhall.Pretty.Internal.prettyLabel x)

        case t of
            Record kts -> do
                _ <- loop ctx t

                case Dhall.Map.lookup x kts of
                    Just t' -> return t'
                    Nothing -> Left (TypeError ctx e (MissingField x t))
            _ -> do
                case Dhall.Core.normalize r of
                  Union kts ->
                    case Dhall.Map.lookup x kts of
                        Just (Just t') -> return (Pi x t' (Union kts))
                        Just Nothing   -> return (Union kts)
                        Nothing -> Left (TypeError ctx e (MissingConstructor x r))
                  r' -> Left (TypeError ctx e (CantAccess text r' t))
    loop ctx e@(Project r (Left xs)) = do
        t <- fmap Dhall.Core.normalize (loop ctx r)

        case t of
            Record kts -> do
                _ <- loop ctx t

                let process k =
                        case Dhall.Map.lookup k kts of
                            Just t' -> return (k, t')
                            Nothing -> Left (TypeError ctx e (MissingField k t))

                let adapt = Record . Dhall.Map.fromList

                fmap adapt (traverse process (Dhall.Set.toList xs))
            _ -> do
                let text =
                        Dhall.Pretty.Internal.docToStrictText (Dhall.Pretty.Internal.prettyLabels xs)

                Left (TypeError ctx e (CantProject text r t))
    loop ctx e@(Project r (Right t)) = do
        _R <- fmap Dhall.Core.normalize (loop ctx r)

        case _R of
            Record ktsR -> do
                _ <- loop ctx t

                case Dhall.Core.normalize t of
                    Record ktsT -> do
                        let actualSubset =
                                Record (Dhall.Map.intersection ktsR ktsT)

                        let expectedSubset = t

                        let process k tT = do
                                case Dhall.Map.lookup k ktsR of
                                    Nothing -> do
                                        Left (TypeError ctx e (MissingField k _R))
                                    Just tR -> do
                                        if Dhall.Core.judgmentallyEqual tT tR
                                            then do
                                                return ()
                                            else do
                                                Left (TypeError ctx e (ProjectionTypeMismatch k tT tR expectedSubset actualSubset))

                        Dhall.Map.unorderedTraverseWithKey_ process ktsT

                        return (Record ktsT)
                    _ -> do
                        Left (TypeError ctx e (CantProjectByExpression t))

            _ -> do
                let text = Dhall.Core.pretty t

                Left (TypeError ctx e (CantProject text r t))
    loop ctx e@(Assert t) = do
        _ <- loop ctx t

        let t' = Dhall.Core.normalize t

        case t' of
            Equivalent x y -> do
                if Dhall.Core.judgmentallyEqual x y
                    then return t'
                    else Left (TypeError ctx e (AssertionFailed x y))

            _ -> Left (TypeError ctx e (NotAnEquivalence t))
    loop ctx e@(Equivalent x y) = do
        _A₀ <- loop ctx x

        c₀ <- loop ctx _A₀
        case c₀ of
            Const Type -> return ()
            _          -> Left (TypeError ctx e (IncomparableExpression x))

        _A₁ <- loop ctx y

        c₁ <- loop ctx _A₁
        case c₁ of
            Const Type -> return ()
            _          -> Left (TypeError ctx e (IncomparableExpression y))

        if Dhall.Core.judgmentallyEqual _A₀ _A₁
            then return ()
            else do
                let nf_A₀ = Dhall.Core.normalize _A₀
                let nf_A₁ = Dhall.Core.normalize _A₁
                Left (TypeError ctx e (EquivalenceTypeMismatch x nf_A₀ y nf_A₁))

        return (Const Type)
    loop ctx   (Note s e'       ) = case loop ctx e' of
        Left (TypeError ctx' (Note s' e'') m) -> Left (TypeError ctx' (Note s' e'') m)
        Left (TypeError ctx'          e''  m) -> Left (TypeError ctx' (Note s  e'') m)
        Right r                               -> Right r
    loop ctx   (ImportAlt l _r  ) =
       fmap Dhall.Core.normalize (loop ctx l)
    loop _     (Embed p         ) = Right $ tpa p

{-| `typeOf` is the same as `typeWith` with an empty context, meaning that the
    expression must be closed (i.e. no free variables), otherwise type-checking
    will fail.
-}
typeOf :: Expr s X -> Either (TypeError s X) (Expr s X)
typeOf = typeWith Dhall.Context.empty

-- | The specific type error
data TypeMessage s a
    = UnboundVariable Text
    | InvalidInputType (Expr s a)
    | InvalidOutputType (Expr s a)
    | NotAFunction (Expr s a) (Expr s a)
    | TypeMismatch (Expr s a) (Expr s a) (Expr s a) (Expr s a)
    | AnnotMismatch (Expr s a) (Expr s a) (Expr s a)
    | Untyped
    | MissingListType
    | MismatchedListElements Int (Expr s a) (Expr s a) (Expr s a)
    | InvalidListElement Int (Expr s a) (Expr s a) (Expr s a)
    | InvalidListType (Expr s a)
    | InvalidSome (Expr s a) (Expr s a) (Expr s a)
    | InvalidPredicate (Expr s a) (Expr s a)
    | IfBranchMismatch (Expr s a) (Expr s a) (Expr s a) (Expr s a)
    | IfBranchMustBeTerm Bool (Expr s a) (Expr s a) (Expr s a)
    | InvalidFieldType Text (Expr s a)
    | InvalidAlternativeType Text (Expr s a)
    | AlternativeAnnotationMismatch Text (Expr s a) Const Text (Expr s a) Const
    | ListAppendMismatch (Expr s a) (Expr s a)
    | MustCombineARecord Char (Expr s a) (Expr s a)
    | CombineTypesRequiresRecordType (Expr s a) (Expr s a)
    | RecordTypeMismatch Const Const (Expr s a) (Expr s a)
    | FieldCollision Text
    | MustMergeARecord (Expr s a) (Expr s a)
    | MustMergeUnion (Expr s a) (Expr s a)
    | MustMapARecord (Expr s a) (Expr s a)
    | InvalidToMapRecordKind (Expr s a) (Expr s a)
    | HeterogenousRecordToMap (Expr s a) (Expr s a) (Expr s a)
    | InvalidToMapType (Expr s a)
    | MapTypeMismatch (Expr s a) (Expr s a)
    | MissingToMapType
    | UnusedHandler (Set Text)
    | MissingHandler (Set Text)
    | HandlerInputTypeMismatch Text (Expr s a) (Expr s a)
    | HandlerOutputTypeMismatch Text (Expr s a) Text (Expr s a)
    | InvalidHandlerOutputType Text (Expr s a) (Expr s a)
    | MissingMergeType
    | HandlerNotAFunction Text (Expr s a)
    | CantAccess Text (Expr s a) (Expr s a)
    | CantProject Text (Expr s a) (Expr s a)
    | CantProjectByExpression (Expr s a)
    | MissingField Text (Expr s a)
    | MissingConstructor Text (Expr s a)
    | ProjectionTypeMismatch Text (Expr s a) (Expr s a) (Expr s a) (Expr s a)
    | AssertionFailed (Expr s a) (Expr s a)
    | NotAnEquivalence (Expr s a)
    | IncomparableExpression (Expr s a)
    | EquivalenceTypeMismatch (Expr s a) (Expr s a) (Expr s a) (Expr s a)
    | CantAnd (Expr s a) (Expr s a)
    | CantOr (Expr s a) (Expr s a)
    | CantEQ (Expr s a) (Expr s a)
    | CantNE (Expr s a) (Expr s a)
    | CantInterpolate (Expr s a) (Expr s a)
    | CantTextAppend (Expr s a) (Expr s a)
    | CantListAppend (Expr s a) (Expr s a)
    | CantAdd (Expr s a) (Expr s a)
    | CantMultiply (Expr s a) (Expr s a)
    deriving (Show)

shortTypeMessage :: (Eq a, Pretty a, ToTerm a) => TypeMessage s a -> Doc Ann
shortTypeMessage msg =
    "\ESC[1;31mError\ESC[0m: " <> short <> "\n"
  where
    ErrorMessages {..} = prettyTypeMessage msg

longTypeMessage :: (Eq a, Pretty a, ToTerm a) => TypeMessage s a -> Doc Ann
longTypeMessage msg =
        "\ESC[1;31mError\ESC[0m: " <> short <> "\n"
    <>  "\n"
    <>  long
  where
    ErrorMessages {..} = prettyTypeMessage msg

data ErrorMessages = ErrorMessages
    { short :: Doc Ann
    -- ^ Default succinct 1-line explanation of what went wrong
    , long  :: Doc Ann
    -- ^ Longer and more detailed explanation of the error
    }

_NOT :: Doc ann
_NOT = "\ESC[1mnot\ESC[0m"

insert :: Pretty a => a -> Doc Ann
insert = Dhall.Util.insert

prettyTypeMessage
    :: (Eq a, Pretty a, ToTerm a) => TypeMessage s a -> ErrorMessages
prettyTypeMessage (UnboundVariable x) = ErrorMessages {..}
  -- We do not need to print variable name here. For the discussion see:
  -- https://github.com/dhall-lang/dhall-haskell/pull/116
  where
    short = "Unbound variable: " <> Pretty.pretty x

    long =
        "Explanation: Expressions can only reference previously introduced (i.e. “bound”)\n\
        \variables that are still “in scope”                                             \n\
        \                                                                                \n\
        \For example, the following valid expressions introduce a “bound” variable named \n\
        \❰x❱:                                                                            \n\
        \                                                                                \n\
        \                                                                                \n\
        \    ┌─────────────────┐                                                         \n\
        \    │ λ(x : Bool) → x │  Anonymous functions introduce “bound” variables        \n\
        \    └─────────────────┘                                                         \n\
        \        ⇧                                                                       \n\
        \        This is the bound variable                                              \n\
        \                                                                                \n\
        \                                                                                \n\
        \    ┌─────────────────┐                                                         \n\
        \    │ let x = 1 in x  │  ❰let❱ expressions introduce “bound” variables          \n\
        \    └─────────────────┘                                                         \n\
        \          ⇧                                                                     \n\
        \          This is the bound variable                                            \n\
        \                                                                                \n\
        \                                                                                \n\
        \However, the following expressions are not valid because they all reference a   \n\
        \variable that has not been introduced yet (i.e. an “unbound” variable):         \n\
        \                                                                                \n\
        \                                                                                \n\
        \    ┌─────────────────┐                                                         \n\
        \    │ λ(x : Bool) → y │  The variable ❰y❱ hasn't been introduced yet            \n\
        \    └─────────────────┘                                                         \n\
        \                    ⇧                                                           \n\
        \                    This is the unbound variable                                \n\
        \                                                                                \n\
        \                                                                                \n\
        \    ┌──────────────────────────┐                                                \n\
        \    │ (let x = True in x) && x │  ❰x❱ is undefined outside the parentheses      \n\
        \    └──────────────────────────┘                                                \n\
        \                             ⇧                                                  \n\
        \                             This is the unbound variable                       \n\
        \                                                                                \n\
        \                                                                                \n\
        \    ┌────────────────┐                                                          \n\
        \    │ let x = x in x │  The definition for ❰x❱ cannot reference itself          \n\
        \    └────────────────┘                                                          \n\
        \              ⇧                                                                 \n\
        \              This is the unbound variable                                      \n\
        \                                                                                \n\
        \                                                                                \n\
        \Some common reasons why you might get this error:                               \n\
        \                                                                                \n\
        \● You misspell a variable name, like this:                                      \n\
        \                                                                                \n\
        \                                                                                \n\
        \    ┌────────────────────────────────────────────────────┐                      \n\
        \    │ λ(empty : Bool) → if emty then \"Empty\" else \"Full\" │                      \n\
        \    └────────────────────────────────────────────────────┘                      \n\
        \                           ⇧                                                    \n\
        \                           Typo                                                 \n\
        \                                                                                \n\
        \                                                                                \n\
        \● You misspell a reserved identifier, like this:                                \n\
        \                                                                                \n\
        \                                                                                \n\
        \    ┌──────────────────────────┐                                                \n\
        \    │ foral (a : Type) → a → a │                                                \n\
        \    └──────────────────────────┘                                                \n\
        \      ⇧                                                                         \n\
        \      Typo                                                                      \n\
        \                                                                                \n\
        \                                                                                \n\
        \● You tried to define a recursive value, like this:                             \n\
        \                                                                                \n\
        \                                                                                \n\
        \    ┌────────────────────┐                                                      \n\
        \    │ let x = x + 1 in x │                                                      \n\
        \    └────────────────────┘                                                      \n\
        \              ⇧                                                                 \n\
        \              Recursive definitions are not allowed                             \n\
        \                                                                                \n\
        \                                                                                \n\
        \● You accidentally forgot a ❰λ❱ or ❰∀❱/❰forall❱                                 \n\
        \                                                                                \n\
        \                                                                                \n\
        \        Unbound variable                                                        \n\
        \        ⇩                                                                       \n\
        \    ┌─────────────────┐                                                         \n\
        \    │  (x : Bool) → x │                                                         \n\
        \    └─────────────────┘                                                         \n\
        \      ⇧                                                                         \n\
        \      A ❰λ❱ here would transform this into a valid anonymous function           \n\
        \                                                                                \n\
        \                                                                                \n\
        \        Unbound variable                                                        \n\
        \        ⇩                                                                       \n\
        \    ┌────────────────────┐                                                      \n\
        \    │  (x : Bool) → Bool │                                                      \n\
        \    └────────────────────┘                                                      \n\
        \      ⇧                                                                         \n\
        \      A ❰∀❱ or ❰forall❱ here would transform this into a valid function type    \n\
        \                                                                                \n\
        \                                                                                \n\
        \● You forgot to prefix a file path with ❰./❱:                                   \n\
        \                                                                                \n\
        \                                                                                \n\
        \    ┌────────────────────┐                                                      \n\
        \    │ path/to/file.dhall │                                                      \n\
        \    └────────────────────┘                                                      \n\
        \      ⇧                                                                         \n\
        \      This should be ❰./path/to/file.dhall❱                                     \n"

prettyTypeMessage (InvalidInputType expr) = ErrorMessages {..}
  where
    short = "Invalid function input"

    long =
        "Explanation: A function can accept an input “term” that has a given “type”, like\n\
        \this:                                                                           \n\
        \                                                                                \n\
        \                                                                                \n\
        \        This is the input term that the function accepts                        \n\
        \        ⇩                                                                       \n\
        \    ┌───────────────────────┐                                                   \n\
        \    │ ∀(x : Natural) → Bool │  This is the type of a function that accepts an   \n\
        \    └───────────────────────┘  input term named ❰x❱ that has type ❰Natural❱     \n\
        \            ⇧                                                                   \n\
        \            This is the type of the input term                                  \n\
        \                                                                                \n\
        \                                                                                \n\
        \    ┌────────────────┐                                                          \n\
        \    │ Bool → Natural │  This is the type of a function that accepts an anonymous\n\
        \    └────────────────┘  input term that has type ❰Bool❱                         \n\
        \      ⇧                                                                         \n\
        \      This is the type of the input term                                        \n\
        \                                                                                \n\
        \                                                                                \n\
        \... or a function can accept an input “type” that has a given “kind”, like this:\n\
        \                                                                                \n\
        \                                                                                \n\
        \        This is the input type that the function accepts                        \n\
        \        ⇩                                                                       \n\
        \    ┌────────────────────┐                                                      \n\
        \    │ ∀(a : Type) → Type │  This is the type of a function that accepts an input\n\
        \    └────────────────────┘  type named ❰a❱ that has kind ❰Type❱                 \n\
        \            ⇧                                                                   \n\
        \            This is the kind of the input type                                  \n\
        \                                                                                \n\
        \                                                                                \n\
        \    ┌──────────────────────┐                                                    \n\
        \    │ (Type → Type) → Type │  This is the type of a function that accepts an    \n\
        \    └──────────────────────┘  anonymous input type that has kind ❰Type → Type❱  \n\
        \       ⇧                                                                        \n\
        \       This is the kind of the input type                                       \n\
        \                                                                                \n\
        \                                                                                \n\
        \Other function inputs are " <> _NOT <> " valid, like this:                      \n\
        \                                                                                \n\
        \                                                                                \n\
        \    ┌──────────────┐                                                            \n\
        \    │ ∀(x : 1) → x │  ❰1❱ is a “term” and not a “type” nor a “kind” so ❰x❱      \n\
        \    └──────────────┘  cannot have “type” ❰1❱ or “kind” ❰1❱                      \n\
        \            ⇧                                                                   \n\
        \            This is not a type or kind                                          \n\
        \                                                                                \n\
        \                                                                                \n\
        \    ┌──────────┐                                                                \n\
        \    │ True → x │  ❰True❱ is a “term” and not a “type” nor a “kind” so the       \n\
        \    └──────────┘  anonymous input cannot have “type” ❰True❱ or “kind” ❰True❱    \n\
        \      ⇧                                                                         \n\
        \      This is not a type or kind                                                \n\
        \                                                                                \n\
        \                                                                                \n\
        \You annotated a function input with the following expression:                   \n\
        \                                                                                \n\
        \" <> txt <> "\n\
        \                                                                                \n\
        \... which is neither a type nor a kind                                          \n"
      where
        txt = insert expr

prettyTypeMessage (InvalidOutputType expr) = ErrorMessages {..}
  where
    short = "Invalid function output"

    long =
        "Explanation: A function can return an output “term” that has a given “type”,    \n\
        \like this:                                                                      \n\
        \                                                                                \n\
        \                                                                                \n\
        \    ┌────────────────────┐                                                      \n\
        \    │ ∀(x : Text) → Bool │  This is the type of a function that returns an      \n\
        \    └────────────────────┘  output term that has type ❰Bool❱                    \n\
        \                    ⇧                                                           \n\
        \                    This is the type of the output term                         \n\
        \                                                                                \n\
        \                                                                                \n\
        \    ┌────────────────┐                                                          \n\
        \    │ Bool → Natural │  This is the type of a function that returns an output   \n\
        \    └────────────────┘  term that has type ❰Natural❱                            \n\
        \             ⇧                                                                  \n\
        \             This is the type of the output term                                \n\
        \                                                                                \n\
        \                                                                                \n\
        \... or a function can return an output “type” that has a given “kind”, like     \n\
        \this:                                                                           \n\
        \                                                                                \n\
        \    ┌────────────────────┐                                                      \n\
        \    │ ∀(a : Type) → Type │  This is the type of a function that returns an      \n\
        \    └────────────────────┘  output type that has kind ❰Type❱                    \n\
        \                    ⇧                                                           \n\
        \                    This is the kind of the output type                         \n\
        \                                                                                \n\
        \                                                                                \n\
        \    ┌──────────────────────┐                                                    \n\
        \    │ (Type → Type) → Type │  This is the type of a function that returns an    \n\
        \    └──────────────────────┘  output type that has kind ❰Type❱                  \n\
        \                      ⇧                                                         \n\
        \                      This is the kind of the output type                       \n\
        \                                                                                \n\
        \                                                                                \n\
        \Other outputs are " <> _NOT <> " valid, like this:                              \n\
        \                                                                                \n\
        \                                                                                \n\
        \    ┌─────────────────┐                                                         \n\
        \    │ ∀(x : Bool) → x │  ❰x❱ is a “term” and not a “type” nor a “kind” so the   \n\
        \    └─────────────────┘  output cannot have “type” ❰x❱ or “kind” ❰x❱            \n\
        \                    ⇧                                                           \n\
        \                    This is not a type or kind                                  \n\
        \                                                                                \n\
        \                                                                                \n\
        \    ┌─────────────┐                                                             \n\
        \    │ Text → True │  ❰True❱ is a “term” and not a “type” nor a “kind” so the    \n\
        \    └─────────────┘  output cannot have “type” ❰True❱ or “kind” ❰True❱          \n\
        \             ⇧                                                                  \n\
        \             This is not a type or kind                                         \n\
        \                                                                                \n\
        \                                                                                \n\
        \Some common reasons why you might get this error:                               \n\
        \                                                                                \n\
        \● You use ❰∀❱ instead of ❰λ❱ by mistake, like this:                             \n\
        \                                                                                \n\
        \                                                                                \n\
        \    ┌────────────────┐                                                          \n\
        \    │ ∀(x: Bool) → x │                                                          \n\
        \    └────────────────┘                                                          \n\
        \      ⇧                                                                         \n\
        \      Using ❰λ❱ here instead of ❰∀❱ would transform this into a valid function  \n\
        \                                                                                \n\
        \                                                                                \n\
        \────────────────────────────────────────────────────────────────────────────────\n\
        \                                                                                \n\
        \You specified that your function outputs a:                                     \n\
        \                                                                                \n\
        \" <> txt <> "\n\
        \                                                                                \n\
        \... which is neither a type nor a kind:                                         \n"
      where
        txt = insert expr

prettyTypeMessage (NotAFunction expr0 expr1) = ErrorMessages {..}
  where
    short = "Not a function"

    long =
        "Explanation: Expressions separated by whitespace denote function application,   \n\
        \like this:                                                                      \n\
        \                                                                                \n\
        \                                                                                \n\
        \    ┌─────┐                                                                     \n\
        \    │ f x │  This denotes the function ❰f❱ applied to an argument named ❰x❱     \n\
        \    └─────┘                                                                     \n\
        \                                                                                \n\
        \                                                                                \n\
        \A function is a term that has type ❰a → b❱ for some ❰a❱ or ❰b❱.  For example,   \n\
        \the following expressions are all functions because they have a function type:  \n\
        \                                                                                \n\
        \                                                                                \n\
        \                        The function's input type is ❰Bool❱                     \n\
        \                        ⇩                                                       \n\
        \    ┌───────────────────────────────┐                                           \n\
        \    │ λ(x : Bool) → x : Bool → Bool │  User-defined anonymous function          \n\
        \    └───────────────────────────────┘                                           \n\
        \                               ⇧                                                \n\
        \                               The function's output type is ❰Bool❱             \n\
        \                                                                                \n\
        \                                                                                \n\
        \                     The function's input type is ❰Natural❱                     \n\
        \                     ⇩                                                          \n\
        \    ┌───────────────────────────────┐                                           \n\
        \    │ Natural/even : Natural → Bool │  Built-in function                        \n\
        \    └───────────────────────────────┘                                           \n\
        \                               ⇧                                                \n\
        \                               The function's output type is ❰Bool❱             \n\
        \                                                                                \n\
        \                                                                                \n\
        \                        The function's input kind is ❰Type❱                     \n\
        \                        ⇩                                                       \n\
        \    ┌───────────────────────────────┐                                           \n\
        \    │ λ(a : Type) → a : Type → Type │  Type-level functions are still functions \n\
        \    └───────────────────────────────┘                                           \n\
        \                               ⇧                                                \n\
        \                               The function's output kind is ❰Type❱             \n\
        \                                                                                \n\
        \                                                                                \n\
        \             The function's input kind is ❰Type❱                                \n\
        \             ⇩                                                                  \n\
        \    ┌────────────────────┐                                                      \n\
        \    │ List : Type → Type │  Built-in type-level function                        \n\
        \    └────────────────────┘                                                      \n\
        \                    ⇧                                                           \n\
        \                    The function's output kind is ❰Type❱                        \n\
        \                                                                                \n\
        \                                                                                \n\
        \                        Function's input has kind ❰Type❱                        \n\
        \                        ⇩                                                       \n\
        \    ┌─────────────────────────────────────────────────┐                         \n\
        \    │ List/head : ∀(a : Type) → (List a → Optional a) │  A function can return  \n\
        \    └─────────────────────────────────────────────────┘  another function       \n\
        \                                ⇧                                               \n\
        \                                Function's output has type ❰List a → Optional a❱\n\
        \                                                                                \n\
        \                                                                                \n\
        \                       The function's input type is ❰List Text❱                 \n\
        \                       ⇩                                                        \n\
        \    ┌────────────────────────────────────────────┐                              \n\
        \    │ List/head Text : List Text → Optional Text │  A function applied to an    \n\
        \    └────────────────────────────────────────────┘  argument can be a function  \n\
        \                                   ⇧                                            \n\
        \                                   The function's output type is ❰Optional Text❱\n\
        \                                                                                \n\
        \                                                                                \n\
        \An expression is not a function if the expression's type is not of the form     \n\
        \❰a → b❱.  For example, these are " <> _NOT <> " functions:                      \n\
        \                                                                                \n\
        \                                                                                \n\
        \    ┌─────────────┐                                                             \n\
        \    │ 1 : Natural │  ❰1❱ is not a function because ❰Natural❱ is not the type of \n\
        \    └─────────────┘  a function                                                 \n\
        \                                                                                \n\
        \                                                                                \n\
        \    ┌───────────────────────┐                                                   \n\
        \    │ Natural/even 2 : Bool │  ❰Natural/even 2❱ is not a function because       \n\
        \    └───────────────────────┘  ❰Bool❱ is not the type of a function             \n\
        \                                                                                \n\
        \                                                                                \n\
        \    ┌──────────────────┐                                                        \n\
        \    │ List Text : Type │  ❰List Text❱ is not a function because ❰Type❱ is not   \n\
        \    └──────────────────┘  the type of a function                                \n\
        \                                                                                \n\
        \                                                                                \n\
        \Some common reasons why you might get this error:                               \n\
        \                                                                                \n\
        \● You tried to add two ❰Natural❱s without a space around the ❰+❱, like this:    \n\
        \                                                                                \n\
        \                                                                                \n\
        \    ┌─────┐                                                                     \n\
        \    │ 2+2 │                                                                     \n\
        \    └─────┘                                                                     \n\
        \                                                                                \n\
        \                                                                                \n\
        \  The above code is parsed as:                                                  \n\
        \                                                                                \n\
        \                                                                                \n\
        \    ┌────────┐                                                                  \n\
        \    │ 2 (+2) │                                                                  \n\
        \    └────────┘                                                                  \n\
        \      ⇧                                                                         \n\
        \      The compiler thinks that this ❰2❱ is a function whose argument is ❰+2❱    \n\
        \                                                                                \n\
        \                                                                                \n\
        \  This is because the ❰+❱ symbol has two meanings: you use ❰+❱ to add two       \n\
        \  numbers, but you also can prefix ❰Natural❱ literals with a ❰+❱ to turn them   \n\
        \  into ❰Integer❱ literals (like ❰+2❱)                                           \n\
        \                                                                                \n\
        \  To fix the code, you need to put spaces around the ❰+❱, like this:            \n\
        \                                                                                \n\
        \                                                                                \n\
        \    ┌───────┐                                                                   \n\
        \    │ 2 + 2 │                                                                   \n\
        \    └───────┘                                                                   \n\
        \                                                                                \n\
        \                                                                                \n\
        \────────────────────────────────────────────────────────────────────────────────\n\
        \                                                                                \n\
        \You tried to use the following expression as a function:                        \n\
        \                                                                                \n\
        \" <> txt0 <> "\n\
        \                                                                                \n\
        \... but this expression's type is:                                              \n\
        \                                                                                \n\
        \" <> txt1 <> "\n\
        \                                                                                \n\
        \... which is not a function type                                                \n"
      where
        txt0 = insert expr0
        txt1 = insert expr1

prettyTypeMessage (TypeMismatch expr0 expr1 expr2 expr3) = ErrorMessages {..}
  where
    short = "Wrong type of function argument\n"
        <>  "\n"
        <>  Dhall.Diff.doc (Dhall.Diff.diffNormalized expr1 expr3)

    long =
        "Explanation: Every function declares what type or kind of argument to accept    \n\
        \                                                                                \n\
        \For example:                                                                    \n\
        \                                                                                \n\
        \                                                                                \n\
        \    ┌───────────────────────────────┐                                           \n\
        \    │ λ(x : Bool) → x : Bool → Bool │  This anonymous function only accepts     \n\
        \    └───────────────────────────────┘  arguments that have type ❰Bool❱          \n\
        \                        ⇧                                                       \n\
        \                        The function's input type                               \n\
        \                                                                                \n\
        \                                                                                \n\
        \    ┌───────────────────────────────┐                                           \n\
        \    │ Natural/even : Natural → Bool │  This built-in function only accepts      \n\
        \    └───────────────────────────────┘  arguments that have type ❰Natural❱       \n\
        \                     ⇧                                                          \n\
        \                     The function's input type                                  \n\
        \                                                                                \n\
        \                                                                                \n\
        \    ┌───────────────────────────────┐                                           \n\
        \    │ λ(a : Type) → a : Type → Type │  This anonymous function only accepts     \n\
        \    └───────────────────────────────┘  arguments that have kind ❰Type❱          \n\
        \                        ⇧                                                       \n\
        \                        The function's input kind                               \n\
        \                                                                                \n\
        \                                                                                \n\
        \    ┌────────────────────┐                                                      \n\
        \    │ List : Type → Type │  This built-in function only accepts arguments that  \n\
        \    └────────────────────┘  have kind ❰Type❱                                    \n\
        \             ⇧                                                                  \n\
        \             The function's input kind                                          \n\
        \                                                                                \n\
        \                                                                                \n\
        \For example, the following expressions are valid:                               \n\
        \                                                                                \n\
        \                                                                                \n\
        \    ┌────────────────────────┐                                                  \n\
        \    │ (λ(x : Bool) → x) True │  ❰True❱ has type ❰Bool❱, which matches the type  \n\
        \    └────────────────────────┘  of argument that the anonymous function accepts \n\
        \                                                                                \n\
        \                                                                                \n\
        \    ┌────────────────┐                                                          \n\
        \    │ Natural/even 2 │  ❰2❱ has type ❰Natural❱, which matches the type of       \n\
        \    └────────────────┘  argument that the ❰Natural/even❱ function accepts,      \n\
        \                                                                                \n\
        \                                                                                \n\
        \    ┌────────────────────────┐                                                  \n\
        \    │ (λ(a : Type) → a) Bool │  ❰Bool❱ has kind ❰Type❱, which matches the kind  \n\
        \    └────────────────────────┘  of argument that the anonymous function accepts \n\
        \                                                                                \n\
        \                                                                                \n\
        \    ┌───────────┐                                                               \n\
        \    │ List Text │  ❰Text❱ has kind ❰Type❱, which matches the kind of argument   \n\
        \    └───────────┘  that that the ❰List❱ function accepts                        \n\
        \                                                                                \n\
        \                                                                                \n\
        \However, you can " <> _NOT <> " apply a function to the wrong type or kind of argument\n\
        \                                                                                \n\
        \For example, the following expressions are not valid:                           \n\
        \                                                                                \n\
        \                                                                                \n\
        \    ┌───────────────────────┐                                                   \n\
        \    │ (λ(x : Bool) → x) \"A\" │  ❰\"A\"❱ has type ❰Text❱, but the anonymous function\n\
        \    └───────────────────────┘  expects an argument that has type ❰Bool❱         \n\
        \                                                                                \n\
        \                                                                                \n\
        \    ┌──────────────────┐                                                        \n\
        \    │ Natural/even \"A\" │  ❰\"A\"❱ has type ❰Text❱, but the ❰Natural/even❱ function\n\
        \    └──────────────────┘  expects an argument that has type ❰Natural❱           \n\
        \                                                                                \n\
        \                                                                                \n\
        \    ┌────────────────────────┐                                                  \n\
        \    │ (λ(a : Type) → a) True │  ❰True❱ has type ❰Bool❱, but the anonymous       \n\
        \    └────────────────────────┘  function expects an argument of kind ❰Type❱     \n\
        \                                                                                \n\
        \                                                                                \n\
        \    ┌────────┐                                                                  \n\
        \    │ List 1 │  ❰1❱ has type ❰Natural❱, but the ❰List❱ function expects an      \n\
        \    └────────┘  argument that has kind ❰Type❱                                   \n\
        \                                                                                \n\
        \                                                                                \n\
        \Some common reasons why you might get this error:                               \n\
        \                                                                                \n\
        \● You omit a function argument by mistake:                                      \n\
        \                                                                                \n\
        \                                                                                \n\
        \    ┌───────────────────────┐                                                   \n\
        \    │ List/head   [1, 2, 3] │                                                   \n\
        \    └───────────────────────┘                                                   \n\
        \                ⇧                                                               \n\
        \                ❰List/head❱ is missing the first argument,                      \n\
        \                which should be: ❰Natural❱                                      \n\
        \                                                                                \n\
        \                                                                                \n\
        \● You supply an ❰Integer❱ literal to a function that expects a ❰Natural❱        \n\
        \                                                                                \n\
        \                                                                                \n\
        \    ┌─────────────────┐                                                         \n\
        \    │ Natural/even +2 │                                                         \n\
        \    └─────────────────┘                                                         \n\
        \                   ⇧                                                            \n\
        \                   This should be ❰2❱                                           \n\
        \                                                                                \n\
        \                                                                                \n\
        \────────────────────────────────────────────────────────────────────────────────\n\
        \                                                                                \n\
        \You tried to invoke the following function:                                     \n\
        \                                                                                \n\
        \" <> txt0 <> "\n\
        \                                                                                \n\
        \... which expects an argument of type or kind:                                  \n\
        \                                                                                \n\
        \" <> txt1 <> "\n\
        \                                                                                \n\
        \... on the following argument:                                                  \n\
        \                                                                                \n\
        \" <> txt2 <> "\n\
        \                                                                                \n\
        \... which has a different type or kind:                                         \n\
        \                                                                                \n\
        \" <> txt3 <> "\n"
      where
        txt0 = insert expr0
        txt1 = insert expr1
        txt2 = insert expr2
        txt3 = insert expr3

prettyTypeMessage (AnnotMismatch expr0 expr1 expr2) = ErrorMessages {..}
  where
    short = "Expression doesn't match annotation\n"
        <>  "\n"
        <>  Dhall.Diff.doc (Dhall.Diff.diffNormalized expr1 expr2)
    long =
        "Explanation: You can annotate an expression with its type or kind using the     \n\
        \❰:❱ symbol, like this:                                                          \n\
        \                                                                                \n\
        \                                                                                \n\
        \    ┌───────┐                                                                   \n\
        \    │ x : t │  ❰x❱ is an expression and ❰t❱ is the annotated type or kind of ❰x❱\n\
        \    └───────┘                                                                   \n\
        \                                                                                \n\
        \The type checker verifies that the expression's type or kind matches the        \n\
        \provided annotation                                                             \n\
        \                                                                                \n\
        \For example, all of the following are valid annotations that the type checker   \n\
        \accepts:                                                                        \n\
        \                                                                                \n\
        \                                                                                \n\
        \    ┌─────────────┐                                                             \n\
        \    │ 1 : Natural │  ❰1❱ is an expression that has type ❰Natural❱, so the type  \n\
        \    └─────────────┘  checker accepts the annotation                             \n\
        \                                                                                \n\
        \                                                                                \n\
        \    ┌───────────────────────┐                                                   \n\
        \    │ Natural/even 2 : Bool │  ❰Natural/even 2❱ has type ❰Bool❱, so the type    \n\
        \    └───────────────────────┘  checker accepts the annotation                   \n\
        \                                                                                \n\
        \                                                                                \n\
        \    ┌────────────────────┐                                                      \n\
        \    │ List : Type → Type │  ❰List❱ is an expression that has kind ❰Type → Type❱,\n\
        \    └────────────────────┘  so the type checker accepts the annotation          \n\
        \                                                                                \n\
        \                                                                                \n\
        \    ┌──────────────────┐                                                        \n\
        \    │ List Text : Type │  ❰List Text❱ is an expression that has kind ❰Type❱, so \n\
        \    └──────────────────┘  the type checker accepts the annotation               \n\
        \                                                                                \n\
        \                                                                                \n\
        \However, the following annotations are " <> _NOT <> " valid and the type checker will\n\
        \reject them:                                                                    \n\
        \                                                                                \n\
        \                                                                                \n\
        \    ┌──────────┐                                                                \n\
        \    │ 1 : Text │  The type checker rejects this because ❰1❱ does not have type  \n\
        \    └──────────┘  ❰Text❱                                                        \n\
        \                                                                                \n\
        \                                                                                \n\
        \    ┌─────────────┐                                                             \n\
        \    │ List : Type │  ❰List❱ does not have kind ❰Type❱                           \n\
        \    └─────────────┘                                                             \n\
        \                                                                                \n\
        \                                                                                \n\
        \Some common reasons why you might get this error:                               \n\
        \                                                                                \n\
        \● The Haskell Dhall interpreter implicitly inserts a top-level annotation       \n\
        \  matching the expected type                                                    \n\
        \                                                                                \n\
        \  For example, if you run the following Haskell code:                           \n\
        \                                                                                \n\
        \                                                                                \n\
        \    ┌───────────────────────────────┐                                           \n\
        \    │ >>> input auto \"1\" :: IO Text │                                         \n\
        \    └───────────────────────────────┘                                           \n\
        \                                                                                \n\
        \                                                                                \n\
        \  ... then the interpreter will actually type check the following annotated     \n\
        \  expression:                                                                   \n\
        \                                                                                \n\
        \                                                                                \n\
        \    ┌──────────┐                                                                \n\
        \    │ 1 : Text │                                                                \n\
        \    └──────────┘                                                                \n\
        \                                                                                \n\
        \                                                                                \n\
        \  ... and then type-checking will fail                                          \n\
        \                                                                                \n\
        \────────────────────────────────────────────────────────────────────────────────\n\
        \                                                                                \n\
        \You or the interpreter annotated this expression:                               \n\
        \                                                                                \n\
        \" <> txt0 <> "\n\
        \                                                                                \n\
        \... with this type or kind:                                                     \n\
        \                                                                                \n\
        \" <> txt1 <> "\n\
        \                                                                                \n\
        \... but the inferred type or kind of the expression is actually:                \n\
        \                                                                                \n\
        \" <> txt2 <> "\n"
      where
        txt0 = insert expr0
        txt1 = insert expr1
        txt2 = insert expr2

prettyTypeMessage Untyped = ErrorMessages {..}
  where
    short = "❰Sort❱ has no type, kind, or sort"

    long =
        "Explanation: There are five levels of expressions that form a hierarchy:        \n\
        \                                                                                \n\
        \● terms                                                                         \n\
        \● types                                                                         \n\
        \● kinds                                                                         \n\
        \● sorts                                                                         \n\
        \● orders                                                                        \n\
        \                                                                                \n\
        \The following example illustrates this hierarchy:                               \n\
        \                                                                                \n\
        \    ┌───────────────────────────────────┐                                       \n\
        \    │ \"ABC\" : Text : Type : Kind : Sort │                                     \n\
        \    └───────────────────────────────────┘                                       \n\
        \       ⇧      ⇧      ⇧      ⇧      ⇧                                            \n\
        \       term   type   kind   sort   order                                        \n\
        \                                                                                \n\
        \There is nothing above ❰Sort❱ in this hierarchy, so if you try to type check any\n\
        \expression containing ❰Sort❱ anywhere in the expression then type checking fails\n\
        \                                                                                \n\
        \Some common reasons why you might get this error:                               \n\
        \                                                                                \n\
        \● You supplied a sort where a kind was expected                                 \n\
        \                                                                                \n\
        \  For example, the following expression will fail to type check:                \n\
        \                                                                                \n\
        \    ┌──────────────────┐                                                        \n\
        \    │ f : Type -> Kind │                                                        \n\
        \    └──────────────────┘                                                        \n\
        \                  ⇧                                                             \n\
        \                  ❰Kind❱ is a sort, not a kind                                  \n"

prettyTypeMessage (InvalidPredicate expr0 expr1) = ErrorMessages {..}
  where
    short = "Invalid predicate for ❰if❱"

    long =
        "Explanation: Every ❰if❱ expression begins with a predicate which must have type \n\
        \❰Bool❱                                                                          \n\
        \                                                                                \n\
        \For example, these are valid ❰if❱ expressions:                                  \n\
        \                                                                                \n\
        \                                                                                \n\
        \    ┌──────────────────────────────┐                                            \n\
        \    │ if True then \"Yes\" else \"No\" │                                        \n\
        \    └──────────────────────────────┘                                            \n\
        \         ⇧                                                                      \n\
        \         Predicate                                                              \n\
        \                                                                                \n\
        \                                                                                \n\
        \    ┌─────────────────────────────────────────┐                                 \n\
        \    │ λ(x : Bool) → if x then False else True │                                 \n\
        \    └─────────────────────────────────────────┘                                 \n\
        \                       ⇧                                                        \n\
        \                       Predicate                                                \n\
        \                                                                                \n\
        \                                                                                \n\
        \... but these are " <> _NOT <> " valid ❰if❱ expressions:                        \n\
        \                                                                                \n\
        \                                                                                \n\
        \    ┌───────────────────────────┐                                               \n\
        \    │ if 0 then \"Yes\" else \"No\" │  ❰0❱ does not have type ❰Bool❱            \n\
        \    └───────────────────────────┘                                               \n\
        \                                                                                \n\
        \                                                                                \n\
        \    ┌────────────────────────────┐                                              \n\
        \    │ if \"\" then False else True │  ❰\"\"❱ does not have type ❰Bool❱          \n\
        \    └────────────────────────────┘                                              \n\
        \                                                                                \n\
        \                                                                                \n\
        \Some common reasons why you might get this error:                               \n\
        \                                                                                \n\
        \● You might be used to other programming languages that accept predicates other \n\
        \  than ❰Bool❱                                                                   \n\
        \                                                                                \n\
        \  For example, some languages permit ❰0❱ or ❰\"\"❱ as valid predicates and treat\n\
        \  them as equivalent to ❰False❱.  However, the Dhall language does not permit   \n\
        \  this                                                                          \n\
        \                                                                                \n\
        \────────────────────────────────────────────────────────────────────────────────\n\
        \                                                                                \n\
        \Your ❰if❱ expression begins with the following predicate:                       \n\
        \                                                                                \n\
        \" <> txt0 <> "\n\
        \                                                                                \n\
        \... that has type:                                                              \n\
        \                                                                                \n\
        \" <> txt1 <> "\n\
        \                                                                                \n\
        \... but the predicate must instead have type ❰Bool❱                             \n"
      where
        txt0 = insert expr0
        txt1 = insert expr1

prettyTypeMessage (IfBranchMustBeTerm b expr0 expr1 expr2) =
    ErrorMessages {..}
  where
    short = "❰if❱ branch is not a term"

    long =
        "Explanation: Every ❰if❱ expression has a ❰then❱ and ❰else❱ branch, each of which\n\
        \is an expression:                                                               \n\
        \                                                                                \n\
        \                                                                                \n\
        \                   Expression for ❰then❱ branch                                 \n\
        \                   ⇩                                                            \n\
        \    ┌────────────────────────────────┐                                          \n\
        \    │ if True then \"Hello, world!\"   │                                        \n\
        \    │         else \"Goodbye, world!\" │                                        \n\
        \    └────────────────────────────────┘                                          \n\
        \                   ⇧                                                            \n\
        \                   Expression for ❰else❱ branch                                 \n\
        \                                                                                \n\
        \                                                                                \n\
        \These expressions must be a “term”, where a “term” is defined as an expression  \n\
        \that has a type thas has kind ❰Type❱                                            \n\
        \                                                                                \n\
        \For example, the following expressions are all valid “terms”:                   \n\
        \                                                                                \n\
        \                                                                                \n\
        \    ┌────────────────────┐                                                      \n\
        \    │ 1 : Natural : Type │  ❰1❱ is a term with a type (❰Natural❱) of kind ❰Type❱\n\
        \    └────────────────────┘                                                      \n\
        \      ⇧                                                                         \n\
        \      term                                                                      \n\
        \                                                                                \n\
        \                                                                                \n\
        \    ┌─────────────────────────────────────┐                                     \n\
        \    │ Natural/odd : Natural → Bool : Type │  ❰Natural/odd❱ is a term with a type\n\
        \    └─────────────────────────────────────┘  (❰Natural → Bool❱) of kind ❰Type❱  \n\
        \      ⇧                                                                         \n\
        \      term                                                                      \n\
        \                                                                                \n\
        \                                                                                \n\
        \However, the following expressions are " <> _NOT <> " valid terms:              \n\
        \                                                                                \n\
        \                                                                                \n\
        \    ┌────────────────────┐                                                      \n\
        \    │ Text : Type : Kind │  ❰Text❱ has kind (❰Type❱) of sort ❰Kind❱ and is      \n\
        \    └────────────────────┘  therefore not a term                                \n\
        \      ⇧                                                                         \n\
        \      type                                                                      \n\
        \                                                                                \n\
        \                                                                                \n\
        \    ┌───────────────────────────┐                                               \n\
        \    │ List : Type → Type : Kind │  ❰List❱ has kind (❰Type → Type❱) of sort      \n\
        \    └───────────────────────────┘  ❰Kind❱ and is therefore not a term           \n\
        \      ⇧                                                                         \n\
        \      type-level function                                                       \n\
        \                                                                                \n\
        \                                                                                \n\
        \This means that you cannot define an ❰if❱ expression that returns a type.  For  \n\
        \example, the following ❰if❱ expression is " <> _NOT <> " valid:                 \n\
        \                                                                                \n\
        \                                                                                \n\
        \    ┌─────────────────────────────┐                                             \n\
        \    │ if True then Text else Bool │  Invalid ❰if❱ expression                    \n\
        \    └─────────────────────────────┘                                             \n\
        \                   ⇧         ⇧                                                  \n\
        \                   type      type                                               \n\
        \                                                                                \n\
        \                                                                                \n\
        \Your ❰" <> txt0 <> "❱ branch of your ❰if❱ expression is:                        \n\
        \                                                                                \n\
        \" <> txt1 <> "\n\
        \                                                                                \n\
        \... which has kind:                                                             \n\
        \                                                                                \n\
        \" <> txt2 <> "\n\
        \                                                                                \n\
        \... of sort:                                                                    \n\
        \                                                                                \n\
        \" <> txt3 <> "\n\
        \                                                                                \n\
        \... and is not a term.  Therefore your ❰if❱ expression is not valid             \n"
      where
        txt0 = if b then "then" else "else"
        txt1 = insert expr0
        txt2 = insert expr1
        txt3 = insert expr2

prettyTypeMessage (IfBranchMismatch expr0 expr1 expr2 expr3) =
    ErrorMessages {..}
  where
    short = "❰if❱ branches must have matching types\n"
        <>  "\n"
        <>  Dhall.Diff.doc (Dhall.Diff.diffNormalized expr1 expr3)

    long =
        "Explanation: Every ❰if❱ expression has a ❰then❱ and ❰else❱ branch, each of which\n\
        \is an expression:                                                               \n\
        \                                                                                \n\
        \                                                                                \n\
        \                   Expression for ❰then❱ branch                                 \n\
        \                   ⇩                                                            \n\
        \    ┌────────────────────────────────┐                                          \n\
        \    │ if True then \"Hello, world!\"   │                                        \n\
        \    │         else \"Goodbye, world!\" │                                        \n\
        \    └────────────────────────────────┘                                          \n\
        \                   ⇧                                                            \n\
        \                   Expression for ❰else❱ branch                                 \n\
        \                                                                                \n\
        \                                                                                \n\
        \These two expressions must have the same type.  For example, the following ❰if❱ \n\
        \expressions are all valid:                                                      \n\
        \                                                                                \n\
        \                                                                                \n\
        \    ┌──────────────────────────────────┐                                        \n\
        \    │ λ(b : Bool) → if b then 0 else 1 │ Both branches have type ❰Natural❱      \n\
        \    └──────────────────────────────────┘                                        \n\
        \                                                                                \n\
        \                                                                                \n\
        \    ┌────────────────────────────┐                                              \n\
        \    │ λ(b : Bool) →              │                                              \n\
        \    │     if b then Natural/even │ Both branches have type ❰Natural → Bool❱     \n\
        \    │          else Natural/odd  │                                              \n\
        \    └────────────────────────────┘                                              \n\
        \                                                                                \n\
        \                                                                                \n\
        \However, the following expression is " <> _NOT <> " valid:                      \n\
        \                                                                                \n\
        \                                                                                \n\
        \                   This branch has type ❰Natural❱                               \n\
        \                   ⇩                                                            \n\
        \    ┌────────────────────────┐                                                  \n\
        \    │ if True then 0         │                                                  \n\
        \    │         else \"ABC\"     │                                                \n\
        \    └────────────────────────┘                                                  \n\
        \                   ⇧                                                            \n\
        \                   This branch has type ❰Text❱                                  \n\
        \                                                                                \n\
        \                                                                                \n\
        \The ❰then❱ and ❰else❱ branches must have matching types, even if the predicate  \n\
        \is always ❰True❱ or ❰False❱                                                     \n\
        \                                                                                \n\
        \Your ❰if❱ expression has the following ❰then❱ branch:                           \n\
        \                                                                                \n\
        \" <> txt0 <> "\n\
        \                                                                                \n\
        \... which has type:                                                             \n\
        \                                                                                \n\
        \" <> txt2 <> "\n\
        \                                                                                \n\
        \... and the following ❰else❱ branch:                                            \n\
        \                                                                                \n\
        \" <> txt1 <> "\n\
        \                                                                                \n\
        \... which has a different type:                                                 \n\
        \                                                                                \n\
        \" <> txt3 <> "\n\
        \                                                                                \n\
        \Fix your ❰then❱ and ❰else❱ branches to have matching types                      \n"
      where
        txt0 = insert expr0
        txt1 = insert expr1
        txt2 = insert expr2
        txt3 = insert expr3

prettyTypeMessage (InvalidListType expr0) = ErrorMessages {..}
  where
    short = "Invalid type for ❰List❱"

    long =
        "Explanation: ❰List❱s can optionally document their type with a type annotation, \n\
        \like this:                                                                      \n\
        \                                                                                \n\
        \                                                                                \n\
        \    ┌──────────────────────────┐                                                \n\
        \    │ [1, 2, 3] : List Natural │  A ❰List❱ of three ❰Natural❱ numbers           \n\
        \    └──────────────────────────┘                                                \n\
        \                       ⇧                                                        \n\
        \                       The type of the ❰List❱'s elements, which are ❰Natural❱   \n\
        \                       numbers                                                  \n\
        \                                                                                \n\
        \                                                                                \n\
        \    ┌───────────────────┐                                                       \n\
        \    │ [] : List Natural │  An empty ❰List❱                                      \n\
        \    └───────────────────┘                                                       \n\
        \           ⇧                                                                    \n\
        \           You must specify the type when the ❰List❱ is empty                   \n\
        \                                                                                \n\
        \                                                                                \n\
        \The type must be of the form ❰List ...❱ and not something else.  For example,   \n\
        \the following type annotation is " <> _NOT <> " valid:                          \n\
        \                                                                                \n\
        \                                                                                \n\
        \    ┌────────────┐                                                              \n\
        \    │ ... : Bool │                                                              \n\
        \    └────────────┘                                                              \n\
        \            ⇧                                                                   \n\
        \            This type does not have the form ❰List ...❱                         \n\
        \                                                                                \n\
        \                                                                                \n\
        \The element type must be a type and not something else.  For example, the       \n\
        \following element types are " <> _NOT <> " valid:                               \n\
        \                                                                                \n\
        \                                                                                \n\
        \    ┌──────────────┐                                                            \n\
        \    │ ... : List 1 │                                                            \n\
        \    └──────────────┘                                                            \n\
        \                 ⇧                                                              \n\
        \                 This is a ❰Natural❱ number and not a ❰Type❱                    \n\
        \                                                                                \n\
        \                                                                                \n\
        \    ┌─────────────────┐                                                         \n\
        \    │ ... : List Type │                                                         \n\
        \    └─────────────────┘                                                         \n\
        \                 ⇧                                                              \n\
        \                 This is a ❰Kind❱ and not a ❰Type❱                              \n\
        \                                                                                \n\
        \                                                                                \n\
        \You declared that the ❰List❱ should have type:                                  \n\
        \                                                                                \n\
        \" <> txt0 <> "\n\
        \                                                                                \n\
        \... which is not a valid list type                                              \n"
      where
        txt0 = insert expr0

prettyTypeMessage MissingListType = do
    ErrorMessages {..}
  where
    short = "An empty list requires a type annotation"

    long =
        "Explanation: Lists do not require a type annotation if they have at least one   \n\
        \element:                                                                        \n\
        \                                                                                \n\
        \                                                                                \n\
        \    ┌───────────┐                                                               \n\
        \    │ [1, 2, 3] │  The compiler can infer that this list has type ❰List Natural❱\n\
        \    └───────────┘                                                               \n\
        \                                                                                \n\
        \                                                                                \n\
        \However, empty lists still require a type annotation:                           \n\
        \                                                                                \n\
        \                                                                                \n\
        \    ┌───────────────────┐                                                       \n\
        \    │ [] : List Natural │  This type annotation is mandatory                    \n\
        \    └───────────────────┘                                                       \n\
        \                                                                                \n\
        \                                                                                \n\
        \You cannot supply an empty list without a type annotation                       \n"

prettyTypeMessage (MismatchedListElements i expr0 _expr1 expr2) =
    ErrorMessages {..}
  where
    short = "List elements should all have the same type\n"
        <>  "\n"
        <>  Dhall.Diff.doc (Dhall.Diff.diffNormalized expr0 expr2)

    long =
        "Explanation: Every element in a list must have the same type                    \n\
        \                                                                                \n\
        \For example, this is a valid ❰List❱:                                            \n\
        \                                                                                \n\
        \                                                                                \n\
        \    ┌───────────┐                                                               \n\
        \    │ [1, 2, 3] │  Every element in this ❰List❱ is a ❰Natural❱ number           \n\
        \    └───────────┘                                                               \n\
        \                                                                                \n\
        \                                                                                \n\
        \.. but this is " <> _NOT <> " a valid ❰List❱:                                   \n\
        \                                                                                \n\
        \                                                                                \n\
        \    ┌───────────────┐                                                           \n\
        \    │ [1, \"ABC\", 3] │  The first and second element have different types      \n\
        \    └───────────────┘                                                           \n\
        \                                                                                \n\
        \                                                                                \n\
        \Your first ❰List❱ element has this type:                                        \n\
        \                                                                                \n\
        \" <> txt0 <> "\n\
        \                                                                                \n\
        \... but the element at index #" <> txt1 <> " has this type instead:             \n\
        \                                                                                \n\
        \" <> txt3 <> "\n"
      where
        txt0 = insert expr0
        txt1 = pretty i
        txt3 = insert expr2

prettyTypeMessage (InvalidListElement i expr0 _expr1 expr2) =
    ErrorMessages {..}
  where
    short = "List element has the wrong type\n"
        <>  "\n"
        <>  Dhall.Diff.doc (Dhall.Diff.diffNormalized expr0 expr2)

    long =
        "Explanation: Every element in the list must have a type matching the type       \n\
        \annotation at the end of the list                                               \n\
        \                                                                                \n\
        \For example, this is a valid ❰List❱:                                            \n\
        \                                                                                \n\
        \                                                                                \n\
        \    ┌──────────────────────────┐                                                \n\
        \    │ [1, 2, 3] : List Natural │  Every element in this ❰List❱ is an ❰Natural❱  \n\
        \    └──────────────────────────┘                                                \n\
        \                                                                                \n\
        \                                                                                \n\
        \.. but this is " <> _NOT <> " a valid ❰List❱:                                   \n\
        \                                                                                \n\
        \                                                                                \n\
        \    ┌──────────────────────────────┐                                            \n\
        \    │ [1, \"ABC\", 3] : List Natural │  The second element is not an ❰Natural❱  \n\
        \    └──────────────────────────────┘                                            \n\
        \                                                                                \n\
        \                                                                                \n\
        \Your ❰List❱ elements should have this type:                                     \n\
        \                                                                                \n\
        \" <> txt0 <> "\n\
        \                                                                                \n\
        \... but the element at index #" <> txt1 <> " has this type instead:             \n\
        \                                                                                \n\
        \" <> txt3 <> "\n"
      where
        txt0 = insert expr0
        txt1 = pretty i
        txt3 = insert expr2

prettyTypeMessage (InvalidSome expr0 expr1 expr2) = ErrorMessages {..}
  where
    short = "❰Some❱ argument has the wrong type"

    long =
        "Explanation: The ❰Some❱ constructor expects an argument that is a term, where   \n\
        \the type of the type of a term must be ❰Type❱                                   \n\
        \                                                                                \n\
        \For example, this is a valid use of ❰Some❱:                                     \n\
        \                                                                                \n\
        \                                                                                \n\
        \    ┌────────┐                                                                  \n\
        \    │ Some 1 │  ❰1❱ is a valid term because ❰1 : Natural : Type❱                \n\
        \    └────────┘                                                                  \n\
        \                                                                                \n\
        \                                                                                \n\
        \... but this is " <> _NOT <> " a valid ❰Optional❱ value:                        \n\
        \                                                                                \n\
        \                                                                                \n\
        \    ┌───────────┐                                                               \n\
        \    │ Some Text │  ❰Text❱ is not a valid term because ❰Text : Type : Kind ❱     \n\
        \    └───────────┘                                                               \n\
        \                                                                                \n\
        \                                                                                \n\
        \The ❰Some❱ argument you provided:                                               \n\
        \                                                                                \n\
        \" <> txt0 <> "\n\
        \                                                                                \n\
        \... has this type:                                                              \n\
        \                                                                                \n\
        \" <> txt1 <> "\n\
        \                                                                                \n\
        \... but the type of that type is:                                               \n\
        \                                                                                \n\
        \" <> txt2 <> "\n\
        \                                                                                \n\
        \... which is not ❰Type❱                                                         \n"
      where
        txt0 = insert expr0
        txt1 = insert expr1
        txt2 = insert expr2

prettyTypeMessage (InvalidFieldType k expr0) = ErrorMessages {..}
  where
    short = "Invalid field type"

    long =
        "Explanation: Every record type annotates each field with a ❰Type❱, a ❰Kind❱, or \n\
        \a ❰Sort❱ like this:                                                             \n\
        \                                                                                \n\
        \                                                                                \n\
        \    ┌──────────────────────────────────────────────┐                            \n\
        \    │ { foo : Natural, bar : Integer, baz : Text } │  Every field is annotated  \n\
        \    └──────────────────────────────────────────────┘  with a ❰Type❱             \n\
        \                                                                                \n\
        \                                                                                \n\
        \    ┌────────────────────────────┐                                              \n\
        \    │ { foo : Type, bar : Type } │  Every field is annotated                    \n\
        \    └────────────────────────────┘  with a ❰Kind❱                               \n\
        \                                                                                \n\
        \                                                                                \n\
        \However, the types of fields may " <> _NOT <> " be term-level values:           \n\
        \                                                                                \n\
        \                                                                                \n\
        \    ┌────────────────────────────┐                                              \n\
        \    │ { foo : Natural, bar : 1 } │  Invalid record type                         \n\
        \    └────────────────────────────┘                                              \n\
        \                             ⇧                                                  \n\
        \                             ❰1❱ is a ❰Natural❱ number and not a ❰Type❱,        \n\
        \                             ❰Kind❱, or ❰Sort❱                                  \n\
        \                                                                                \n\
        \                                                                                \n\
        \You provided a record type with a field named:                                  \n\
        \                                                                                \n\
        \" <> txt0 <> "\n\
        \                                                                                \n\
        \... annotated with the following expression:                                    \n\
        \                                                                                \n\
        \" <> txt1 <> "\n\
        \                                                                                \n\
        \... which is neither a ❰Type❱, a ❰Kind❱, nor a ❰Sort❱                           \n"
      where
        txt0 = insert k
        txt1 = insert expr0

prettyTypeMessage (InvalidAlternativeType k expr0) = ErrorMessages {..}
  where
    short = "Invalid alternative type"

    long =
        "Explanation: Every union type specifies the type of each alternative, like this:\n\
        \                                                                                \n\
        \                                                                                \n\
        \               The type of the first alternative is ❰Bool❱                      \n\
        \               ⇩                                                                \n\
        \    ┌──────────────────────────────────┐                                        \n\
        \    │ < Left : Bool, Right : Natural > │  A union type with two alternatives    \n\
        \    └──────────────────────────────────┘                                        \n\
        \                             ⇧                                                  \n\
        \                             The type of the second alternative is ❰Natural❱    \n\
        \                                                                                \n\
        \                                                                                \n\
        \However, these alternatives can only be annotated with ❰Type❱s, ❰Kind❱s, or     \n\
        \❰Sort❱s.  For example, the following union types are " <> _NOT <> " valid:      \n\
        \                                                                                \n\
        \                                                                                \n\
        \    ┌────────────────────────────┐                                              \n\
        \    │ < Left : Bool, Right : 1 > │  Invalid union type                          \n\
        \    └────────────────────────────┘                                              \n\
        \                             ⇧                                                  \n\
        \                             This is a ❰Natural❱ and not a ❰Type❱, ❰Kind❱, or   \n\
        \                             ❰Sort❱                                             \n\
        \                                                                                \n\
        \                                                                                \n\
        \Some common reasons why you might get this error:                               \n\
        \                                                                                \n\
        \● You accidentally typed ❰:❱ instead of ❰=❱ for a union literal with one        \n\
        \  alternative:                                                                  \n\
        \                                                                                \n\
        \    ┌─────────────────┐                                                         \n\
        \    │ < Example : 1 > │                                                         \n\
        \    └─────────────────┘                                                         \n\
        \                ⇧                                                               \n\
        \                This could be ❰=❱ instead                                       \n\
        \                                                                                \n\
        \                                                                                \n\
        \────────────────────────────────────────────────────────────────────────────────\n\
        \                                                                                \n\
        \You provided a union type with an alternative named:                            \n\
        \                                                                                \n\
        \" <> txt0 <> "\n\
        \                                                                                \n\
        \... annotated with the following expression which is not a ❰Type❱, ❰Kind❱, or   \n\
        \❰Sort❱:                                                                         \n\
        \                                                                                \n\
        \" <> txt1 <> "\n"
      where
        txt0 = insert k
        txt1 = insert expr0

prettyTypeMessage (AlternativeAnnotationMismatch k0 expr0 c0 k1 expr1 c1) = ErrorMessages {..}
  where
    short = "Alternative annotation mismatch"

    long =
        "Explanation: Every union type annotates each alternative with a ❰Type❱ or a     \n\
        \❰Kind❱, like this:                                                              \n\
        \                                                                                \n\
        \                                                                                \n\
        \    ┌───────────────────────────────────┐                                       \n\
        \    │ < Left : Natural | Right : Bool > │  Every alternative is annotated with a\n\
        \    └───────────────────────────────────┘  ❰Type❱                               \n\
        \                                                                                \n\
        \                                                                                \n\
        \    ┌────────────────────────────────────┐                                      \n\
        \    │ < Foo : Type → Type | Bar : Type > │  Every alternative is annotated with \n\
        \    └────────────────────────────────────┘  a ❰Kind❱                            \n\
        \                                                                                \n\
        \                                                                                \n\
        \    ┌────────────────┐                                                          \n\
        \    │ < Baz : Kind > │  Every alternative is annotated with a ❰Sort❱            \n\
        \    └────────────────┘                                                          \n\
        \                                                                                \n\
        \                                                                                \n\
        \However, you cannot have a union type that mixes ❰Type❱s, ❰Kind❱s, or ❰Sort❱s   \n\
        \for the annotations:                                                            \n\
        \                                                                                \n\
        \                                                                                \n\
        \              This is a ❰Type❱ annotation                                       \n\
        \              ⇩                                                                 \n\
        \    ┌───────────────────────────────┐                                           \n\
        \    │ { foo : Natural, bar : Type } │  Invalid union type                       \n\
        \    └───────────────────────────────┘                                           \n\
        \                             ⇧                                                  \n\
        \                             ... but this is a ❰Kind❱ annotation                \n\
        \                                                                                \n\
        \                                                                                \n\
        \You provided a union type with an alternative named:                            \n\
        \                                                                                \n\
        \" <> txt0 <> "\n\
        \                                                                                \n\
        \... annotated with the following expression:                                    \n\
        \                                                                                \n\
        \" <> txt1 <> "\n\
        \                                                                                \n\
        \... which is a " <> level c0 <> " whereas another alternative named:            \n\
        \                                                                                \n\
        \" <> txt2 <> "\n\
        \                                                                                \n\
        \... annotated with the following expression:                                    \n\
        \                                                                                \n\
        \" <> txt3 <> "\n\
        \                                                                                \n\
        \... is a " <> level c1 <> ", which does not match                               \n"
      where
        txt0 = insert k0
        txt1 = insert expr0
        txt2 = insert k1
        txt3 = insert expr1

        level Type = "❰Type❱"
        level Kind = "❰Kind❱"
        level Sort = "❰Sort❱"

prettyTypeMessage (ListAppendMismatch expr0 expr1) = ErrorMessages {..}
  where
    short = "You can only append ❰List❱s with matching element types\n"
        <>  "\n"
        <>  Dhall.Diff.doc (Dhall.Diff.diffNormalized expr0 expr1)

    long =
        "Explanation: You can append two ❰List❱s using the ❰#❱ operator, like this:      \n\
        \                                                                                \n\
        \                                                                                \n\
        \    ┌────────────────────┐                                                      \n\
        \    │ [1, 2, 3] # [4, 5] │                                                      \n\
        \    └────────────────────┘                                                      \n\
        \                                                                                \n\
        \                                                                                \n\
        \... but you cannot append two ❰List❱s if they have different element types.     \n\
        \For example, the following expression is " <> _NOT <> " valid:                  \n\
        \                                                                                \n\
        \                                                                                \n\
        \       These elements have type ❰Natural❱                                       \n\
        \       ⇩                                                                        \n\
        \    ┌───────────────────────────┐                                               \n\
        \    │ [1, 2, 3] # [True, False] │  Invalid: the element types don't match       \n\
        \    └───────────────────────────┘                                               \n\
        \                  ⇧                                                             \n\
        \                  These elements have type ❰Bool❱                               \n\
        \                                                                                \n\
        \                                                                                \n\
        \────────────────────────────────────────────────────────────────────────────────\n\
        \                                                                                \n\
        \You tried to append a ❰List❱ thas has elements of type:                         \n\
        \                                                                                \n\
        \" <> txt0 <> "\n\
        \                                                                                \n\
        \... with another ❰List❱ that has elements of type:                              \n\
        \                                                                                \n\
        \" <> txt1 <> "\n\
        \                                                                                \n\
        \... and those two types do not match                                            \n"
      where
        txt0 = insert expr0
        txt1 = insert expr1

prettyTypeMessage (MustCombineARecord c expr0 expr1) = ErrorMessages {..}
  where
    short = "You can only combine records"

    long =
        "Explanation: You can combine records using the ❰" <> op <> "❱ operator, like this:\n\
        \                                                                                \n\
        \                                                                                \n\
        \    ┌───────────────────────────────────────────┐                               \n\
        \    │ { foo = 1, bar = \"ABC\" } " <> op <> " { baz = True } │                  \n\
        \    └───────────────────────────────────────────┘                               \n\
        \                                                                                \n\
        \                                                                                \n\
        \    ┌─────────────────────────────────────────────┐                             \n\
        \    │ λ(r : { foo : Bool }) → r " <> op <> " { bar = \"ABC\" } │                \n\
        \    └─────────────────────────────────────────────┘                             \n\
        \                                                                                \n\
        \                                                                                \n\
        \... but you cannot combine values that are not records.                         \n\
        \                                                                                \n\
        \For example, the following expressions are " <> _NOT <> " valid:                \n\
        \                                                                                \n\
        \                                                                                \n\
        \    ┌──────────────────────────────┐                                            \n\
        \    │ { foo = 1, bar = \"ABC\" } " <> op <> " 1 │                               \n\
        \    └──────────────────────────────┘                                            \n\
        \                                 ⇧                                              \n\
        \                                 Invalid: Not a record                          \n\
        \                                                                                \n\
        \                                                                                \n\
        \    ┌───────────────────────────────────────────┐                               \n\
        \    │ { foo = 1, bar = \"ABC\" } " <> op <> " { baz : Bool } │                  \n\
        \    └───────────────────────────────────────────┘                               \n\
        \                                 ⇧                                              \n\
        \                                 Invalid: This is a record type and not a record\n\
        \                                                                                \n\
        \                                                                                \n\
        \    ┌───────────────────────────────────────────┐                               \n\
        \    │ { foo = 1, bar = \"ABC\" } " <> op <> " < baz : Bool > │                  \n\
        \    └───────────────────────────────────────────┘                               \n\
        \                                 ⇧                                              \n\
        \                                 Invalid: This is a union type and not a record \n\
        \                                                                                \n\
        \                                                                                \n\
        \You tried to combine the following value:                                       \n\
        \                                                                                \n\
        \" <> txt0 <> "\n\
        \                                                                                \n\
        \... which is not a record, but is actually a:                                   \n\
        \                                                                                \n\
        \" <> txt1 <> "\n"
      where
        op   = pretty c
        txt0 = insert expr0
        txt1 = insert expr1

prettyTypeMessage (CombineTypesRequiresRecordType expr0 expr1) =
    ErrorMessages {..}
  where
    short = "❰⩓❱ requires arguments that are record types"

    long =
        "Explanation: You can only use the ❰⩓❱ operator on arguments that are record type\n\
        \literals, like this:                                                            \n\
        \                                                                                \n\
        \                                                                                \n\
        \    ┌─────────────────────────────────────┐                                     \n\
        \    │ { age : Natural } ⩓ { name : Text } │                                     \n\
        \    └─────────────────────────────────────┘                                     \n\
        \                                                                                \n\
        \                                                                                \n\
        \... but you cannot use the ❰⩓❱ operator on any other type of arguments.  For    \n\
        \example, you cannot use variable arguments:                                     \n\
        \                                                                                \n\
        \                                                                                \n\
        \    ┌───────────────────────────────────┐                                       \n\
        \    │ λ(t : Type) → t ⩓ { name : Text } │  Invalid: ❰t❱ might not be a record   \n\
        \    └───────────────────────────────────┘  type                                 \n\
        \                                                                                \n\
        \                                                                                \n\
        \────────────────────────────────────────────────────────────────────────────────\n\
        \                                                                                \n\
        \You tried to supply the following argument:                                     \n\
        \                                                                                \n\
        \" <> txt0 <> "\n\
        \                                                                                \n\
        \... which normalized to:                                                        \n\
        \                                                                                \n\
        \" <> txt1 <> "\n\
        \                                                                                \n\
        \... which is not a record type literal                                          \n"
      where
        txt0 = insert expr0
        txt1 = insert expr1

prettyTypeMessage (RecordTypeMismatch const0 const1 expr0 expr1) =
    ErrorMessages {..}
  where
    short = "Record type mismatch"

    long =
        "Explanation: You can only use the ❰⩓❱ operator on record types if they are both \n\
        \ ❰Type❱s or ❰Kind❱s:                                                            \n\
        \                                                                                \n\
        \                                                                                \n\
        \    ┌─────────────────────────────────────┐                                     \n\
        \    │ { age : Natural } ⩓ { name : Text } │  Valid: Both arguments are ❰Type❱s  \n\
        \    └─────────────────────────────────────┘                                     \n\
        \                                                                                \n\
        \                                                                                \n\
        \    ┌──────────────────────────────────────┐                                    \n\
        \    │ { Input : Type } ⩓ { Output : Type } │  Valid: Both arguments are ❰Kind❱s \n\
        \    └──────────────────────────────────────┘                                    \n\
        \                                                                                \n\
        \                                                                                \n\
        \... but you cannot combine a ❰Type❱ and a ❰Kind❱:                               \n\
        \                                                                                \n\
        \                                                                                \n\
        \    ┌────────────────────────────────────┐                                      \n\
        \    │ { Input : Type } ⩓ { name : Text } │  Invalid: The arguments do not match \n\
        \    └────────────────────────────────────┘                                      \n\
        \                                                                                \n\
        \                                                                                \n\
        \────────────────────────────────────────────────────────────────────────────────\n\
        \                                                                                \n\
        \You tried to combine the following record type:                                 \n\
        \                                                                                \n\
        \" <> txt0 <> "\n\
        \                                                                                \n\
        \... with this record types:                                                     \n\
        \                                                                                \n\
        \" <> txt1 <> "\n\
        \                                                                                \n\
        \... but the former record type is a:                                            \n\
        \                                                                                \n\
        \" <> txt2 <> "\n\
        \                                                                                \n\
        \... but the latter record type is a:                                            \n\
        \                                                                                \n\
        \" <> txt3 <> "\n"
      where
        txt0 = insert expr0
        txt1 = insert expr1
        txt2 = insert const0
        txt3 = insert const1

prettyTypeMessage (FieldCollision k) = ErrorMessages {..}
  where
    short = "Field collision"

    long =
        "Explanation: You can combine records or record types if they don't share any    \n\
        \fields in common, like this:                                                    \n\
        \                                                                                \n\
        \                                                                                \n\
        \    ┌───────────────────────────────────────────┐                               \n\
        \    │ { foo = 1, bar = \"ABC\" } ∧ { baz = True } │                             \n\
        \    └───────────────────────────────────────────┘                               \n\
        \                                                                                \n\
        \                                                                                \n\
        \    ┌─────────────────────────────────┐                                         \n\
        \    │ { foo : Text } ⩓ { bar : Bool } │                                         \n\
        \    └─────────────────────────────────┘                                         \n\
        \                                                                                \n\
        \                                                                                \n\
        \    ┌────────────────────────────────────────┐                                  \n\
        \    │ λ(r : { baz : Bool}) → { foo = 1 } ∧ r │                                  \n\
        \    └────────────────────────────────────────┘                                  \n\
        \                                                                                \n\
        \                                                                                \n\
        \... but you cannot merge two records that share the same field unless the field \n\
        \is a record on both sides.                                                      \n\
        \                                                                                \n\
        \For example, the following expressions are " <> _NOT <> " valid:                \n\
        \                                                                                \n\
        \                                                                                \n\
        \    ┌───────────────────────────────────────────┐                               \n\
        \    │ { foo = 1, bar = \"ABC\" } ∧ { foo = True } │  Invalid: Colliding ❰foo❱   \n\
        \    └───────────────────────────────────────────┘  fields                       \n\
        \                                                                                \n\
        \                                                                                \n\
        \    ┌─────────────────────────────────┐                                         \n\
        \    │ { foo : Bool } ∧ { foo : Text } │  Invalid: Colliding ❰foo❱ fields        \n\
        \    └─────────────────────────────────┘                                         \n\
        \                                                                                \n\
        \                                                                                \n\
        \... but the following expressions are valid:                                    \n\
        \                                                                                \n\
        \                                                                                \n\
        \    ┌──────────────────────────────────────────────────┐                        \n\
        \    │ { foo = { bar = True } } ∧ { foo = { baz = 1 } } │  Valid: Both ❰foo❱     \n\
        \    └──────────────────────────────────────────────────┘  fields are records    \n\
        \                                                                                \n\
        \                                                                                \n\
        \    ┌─────────────────────────────────────────────────────┐                     \n\
        \    │ { foo : { bar : Bool } } ⩓ { foo : { baz : Text } } │  Valid: Both ❰foo❱  \n\
        \    └─────────────────────────────────────────────────────┘  fields are records \n\
        \                                                                                \n\
        \                                                                                \n\
        \Some common reasons why you might get this error:                               \n\
        \                                                                                \n\
        \● You tried to use ❰∧❱ to update a field's value, like this:                    \n\
        \                                                                                \n\
        \                                                                                \n\
        \    ┌────────────────────────────────────────┐                                  \n\
        \    │ { foo = 1, bar = \"ABC\" } ∧ { foo = 2 } │                                \n\
        \    └────────────────────────────────────────┘                                  \n\
        \                                   ⇧                                            \n\
        \                                  Invalid attempt to update ❰foo❱'s value to ❰2❱\n\
        \                                                                                \n\
        \  Field updates are intentionally not allowed as the Dhall language discourages \n\
        \  patch-oriented programming                                                    \n\
        \                                                                                \n\
        \────────────────────────────────────────────────────────────────────────────────\n\
        \                                                                                \n\
        \You combined two records that share the following field:                        \n\
        \                                                                                \n\
        \" <> txt0 <> "\n\
        \                                                                                \n\
        \... which is not allowed                                                        \n"
      where
        txt0 = insert k

prettyTypeMessage (MustMergeARecord expr0 expr1) = ErrorMessages {..}
  where
    short = "❰merge❱ expects a record of handlers"

    long =
        "Explanation: You can ❰merge❱ the alternatives of a union using a record with one\n\
        \handler per alternative, like this:                                             \n\
        \                                                                                \n\
        \                                                                                \n\
        \    ┌─────────────────────────────────────────────────────────────────────┐     \n\
        \    │     let union    = < Left : Natural | Right : Bool >.Left 2         │     \n\
        \    │ in  let handlers = { Left = Natural/even, Right = λ(x : Bool) → x } │     \n\
        \    │ in  merge handlers union : Bool                                     │     \n\
        \    └─────────────────────────────────────────────────────────────────────┘     \n\
        \                                                                                \n\
        \                                                                                \n\
        \... but the first argument to ❰merge❱ must be a record and not some other type. \n\
        \                                                                                \n\
        \For example, the following expression is " <> _NOT <> " valid:                  \n\
        \                                                                                \n\
        \                                                                                \n\
        \    ┌────────────────────────────────────────────────────┐                      \n\
        \    │ let handler = λ(x : Bool) → x                      │                      \n\
        \    │ in  merge handler (< Foo : Bool >.Foo True) : Bool │                      \n\
        \    └────────────────────────────────────────────────────┘                      \n\
        \                ⇧                                                               \n\
        \                Invalid: ❰handler❱ isn't a record                               \n\
        \                                                                                \n\
        \                                                                                \n\
        \Some common reasons why you might get this error:                               \n\
        \                                                                                \n\
        \● You accidentally provide an empty record type instead of an empty record when \n\
        \  you ❰merge❱ an empty union:                                                   \n\
        \                                                                                \n\
        \                                                                                \n\
        \    ┌──────────────────────────────────────────┐                                \n\
        \    │ λ(x : <>) → λ(a : Type) → merge {} x : a │                                \n\
        \    └──────────────────────────────────────────┘                                \n\
        \                                      ⇧                                         \n\
        \                                      This should be ❰{=}❱ instead              \n\
        \                                                                                \n\
        \                                                                                \n\
        \────────────────────────────────────────────────────────────────────────────────\n\
        \                                                                                \n\
        \You provided the following handler:                                             \n\
        \                                                                                \n\
        \" <> txt0 <> "\n\
        \                                                                                \n\
        \... which is not a record, but is actually a value of type:                     \n\
        \                                                                                \n\
        \" <> txt1 <> "\n"
      where
        txt0 = insert expr0
        txt1 = insert expr1

prettyTypeMessage (MustMergeUnion expr0 expr1) = ErrorMessages {..}
  where
    short = "❰merge❱ expects a union"

    long =
        "Explanation: You can ❰merge❱ the alternatives of a union using a record with one\n\
        \handler per alternative, like this:                                             \n\
        \                                                                                \n\
        \                                                                                \n\
        \    ┌─────────────────────────────────────────────────────────────────┐         \n\
        \    │ let union    = < Left : Natural | Right : Bool >.Left 2         │         \n\
        \    │ let handlers = { Left = Natural/even, Right = λ(x : Bool) → x } │         \n\
        \    │ in  merge handlers union : Bool                                 │         \n\
        \    └─────────────────────────────────────────────────────────────────┘         \n\
        \                                                                                \n\
        \                                                                                \n\
        \... but the second argument to ❰merge❱ must be a union and not some other type. \n\
        \                                                                                \n\
        \For example, the following expression is " <> _NOT <> " valid:                  \n\
        \                                                                                \n\
        \                                                                                \n\
        \    ┌──────────────────────────────────────────┐                                \n\
        \    │ let handlers = { Foo = λ(x : Bool) → x } │                                \n\
        \    │ in  merge handlers True : True           │                                \n\
        \    └──────────────────────────────────────────┘                                \n\
        \                         ⇧                                                      \n\
        \                         Invalid: ❰True❱ isn't a union                          \n\
        \                                                                                \n\
        \                                                                                \n\
        \You tried to ❰merge❱ this expression:                                           \n\
        \                                                                                \n\
        \" <> txt0 <> "\n\
        \                                                                                \n\
        \... which is not a union, but is actually a value of type:                      \n\
        \                                                                                \n\
        \" <> txt1 <> "\n"
      where
        txt0 = insert expr0
        txt1 = insert expr1

prettyTypeMessage (UnusedHandler ks) = ErrorMessages {..}
  where
    short = "Unused handler"

    long =
        "Explanation: You can ❰merge❱ the alternatives of a union using a record with one\n\
        \handler per alternative, like this:                                             \n\
        \                                                                                \n\
        \                                                                                \n\
        \    ┌─────────────────────────────────────────────────────────────────┐         \n\
        \    │ let union    = < Left : Natural | Right : Bool >.Left 2         │         \n\
        \    │ let handlers = { Left = Natural/even, Right = λ(x : Bool) → x } │         \n\
        \    │ in  merge handlers union : Bool                                 │         \n\
        \    └─────────────────────────────────────────────────────────────────┘         \n\
        \                                                                                \n\
        \                                                                                \n\
        \... but you must provide exactly one handler per alternative in the union.  You \n\
        \cannot supply extra handlers                                                    \n\
        \                                                                                \n\
        \For example, the following expression is " <> _NOT <> " valid:                  \n\
        \                                                                                \n\
        \                                                                                \n\
        \    ┌──────────────────────────────────────────┐                                \n\
        \    │ let union    = < Left : Natural >.Left 2 │  The ❰Right❱ alternative is    \n\
        \    │ let handlers =                           │  missing                       \n\
        \    │             { Left  = Natural/even       │                                \n\
        \    │             , Right = λ(x : Bool) → x    │  Invalid: ❰Right❱ handler isn't\n\
        \    │             }                            │           used                 \n\
        \    │ in  merge handlers union : Bool          │                                \n\
        \    └──────────────────────────────────────────┘                                \n\
        \                                                                                \n\
        \                                                                                \n\
        \You provided the following handlers:                                            \n\
        \                                                                                \n\
        \" <> txt0 <> "\n\
        \                                                                                \n\
        \... which had no matching alternatives in the union you tried to ❰merge❱        \n"
      where
        txt0 = insert (Text.intercalate ", " (Data.Set.toList ks))

prettyTypeMessage (MissingHandler ks) = ErrorMessages {..}
  where
    short = "Missing handler"

    long =
        "Explanation: You can ❰merge❱ the alternatives of a union using a record with one\n\
        \handler per alternative, like this:                                             \n\
        \                                                                                \n\
        \                                                                                \n\
        \    ┌─────────────────────────────────────────────────────────────────┐         \n\
        \    │ let union    = < Left : Natural | Right : Bool >.Left 2         │         \n\
        \    │ let handlers = { Left = Natural/even, Right = λ(x : Bool) → x } │         \n\
        \    │ in  merge handlers union : Bool                                 │         \n\
        \    └─────────────────────────────────────────────────────────────────┘         \n\
        \                                                                                \n\
        \                                                                                \n\
        \... but you must provide exactly one handler per alternative in the union.  You \n\
        \cannot omit any handlers                                                        \n\
        \                                                                                \n\
        \For example, the following expression is " <> _NOT <> " valid:                  \n\
        \                                                                                \n\
        \                                                                                \n\
        \                                          Invalid: Missing ❰Right❱ handler      \n\
        \                                          ⇩                                     \n\
        \    ┌──────────────────────────────────────────────────────────────┐            \n\
        \    │ let handlers = { Left = Natural/even }                       │            \n\
        \    │ let union    = < Left : Natural | Right : Bool >.Left 2      │            \n\
        \    │ in  merge handlers union : Bool                              │            \n\
        \    └──────────────────────────────────────────────────────────────┘            \n\
        \                                                                                \n\
        \                                                                                \n\
        \Note that you need to provide handlers for other alternatives even if those     \n\
        \alternatives are never used                                                     \n\
        \                                                                                \n\
        \You need to supply the following handlers:                                      \n\
        \                                                                                \n\
        \" <> txt0 <> "\n"
      where
        txt0 = insert (Text.intercalate ", " (Data.Set.toList ks))

prettyTypeMessage MissingMergeType =
    ErrorMessages {..}
  where
    short = "An empty ❰merge❱ requires a type annotation"

    long =
        "Explanation: A ❰merge❱ does not require a type annotation if the union has at   \n\
        \least one alternative, like this                                                \n\
        \                                                                                \n\
        \                                                                                \n\
        \    ┌─────────────────────────────────────────────────────────────────┐         \n\
        \    │ let union    = < Left : Natural | Right : Bool >.Left 2         │         \n\
        \    │ let handlers = { Left = Natural/even, Right = λ(x : Bool) → x } │         \n\
        \    │ in  merge handlers union : Bool                                 │         \n\
        \    └─────────────────────────────────────────────────────────────────┘         \n\
        \                                                                                \n\
        \                                                                                \n\
        \However, you must provide a type annotation when merging an empty union:        \n\
        \                                                                                \n\
        \                                                                                \n\
        \    ┌────────────────────────────────┐                                          \n\
        \    │ λ(a : <>) → merge {=} a : Bool │                                          \n\
        \    └────────────────────────────────┘                                          \n\
        \                                ⇧                                               \n\
        \                                This can be any type                            \n\
        \                                                                                \n\
        \                                                                                \n\
        \You can provide any type at all as the annotation, since merging an empty       \n\
        \union can produce any type of output                                            \n"

prettyTypeMessage (HandlerInputTypeMismatch expr0 expr1 expr2) =
    ErrorMessages {..}
  where
    short = "Wrong handler input type\n"
        <>  "\n"
        <>  Dhall.Diff.doc (Dhall.Diff.diffNormalized expr1 expr2)

    long =
        "Explanation: You can ❰merge❱ the alternatives of a union using a record with one\n\
        \handler per alternative, like this:                                             \n\
        \                                                                                \n\
        \                                                                                \n\
        \    ┌─────────────────────────────────────────────────────────────────┐         \n\
        \    │ let union    = < Left : Natural | Right : Bool >.Left 2         │         \n\
        \    │ let handlers = { Left = Natural/even, Right = λ(x : Bool) → x } │         \n\
        \    │ in  merge handlers union : Bool                                 │         \n\
        \    └─────────────────────────────────────────────────────────────────┘         \n\
        \                                                                                \n\
        \                                                                                \n\
        \... as long as the input type of each handler function matches the type of the  \n\
        \corresponding alternative:                                                      \n\
        \                                                                                \n\
        \                                                                                \n\
        \    ┌───────────────────────────────────────────────────────────┐               \n\
        \    │ union    : < Left : Natural       | Right : Bool        > │               \n\
        \    └───────────────────────────────────────────────────────────┘               \n\
        \                          ⇧                       ⇧                             \n\
        \                   These must match        These must match                     \n\
        \                          ⇩                       ⇩                             \n\
        \    ┌───────────────────────────────────────────────────────────┐               \n\
        \    │ handlers : { Left : Natural → Bool, Right : Bool → Bool } │               \n\
        \    └───────────────────────────────────────────────────────────┘               \n\
        \                                                                                \n\
        \                                                                                \n\
        \For example, the following expression is " <> _NOT <> " valid:                  \n\
        \                                                                                \n\
        \                                                                                \n\
        \      Invalid: Doesn't match the type of the ❰Right❱ alternative                \n\
        \                                                               ⇩                \n\
        \    ┌──────────────────────────────────────────────────────────────────┐        \n\
        \    │ let handlers = { Left = Natural/even | Right = λ(x : Text) → x } │        \n\
        \    │ let union    = < Left : Natural | Right : Bool >.Left 2          │        \n\
        \    │ in  merge handlers union : Bool                                  │        \n\
        \    └──────────────────────────────────────────────────────────────────┘        \n\
        \                                                                                \n\
        \                                                                                \n\
        \Your handler for the following alternative:                                     \n\
        \                                                                                \n\
        \" <> txt0 <> "\n\
        \                                                                                \n\
        \... needs to accept an input value of type:                                     \n\
        \                                                                                \n\
        \" <> txt1 <> "\n\
        \                                                                                \n\
        \... but actually accepts an input value of a different type:                    \n\
        \                                                                                \n\
        \" <> txt2 <> "\n"
      where
        txt0 = insert expr0
        txt1 = insert expr1
        txt2 = insert expr2

prettyTypeMessage (InvalidHandlerOutputType expr0 expr1 expr2) =
    ErrorMessages {..}
  where
    short = "Wrong handler output type\n"
        <>  "\n"
        <>  Dhall.Diff.doc (Dhall.Diff.diffNormalized expr1 expr2)

    long =
        "Explanation: You can ❰merge❱ the alternatives of a union using a record with one\n\
        \handler per alternative, like this:                                             \n\
        \                                                                                \n\
        \                                                                                \n\
        \    ┌─────────────────────────────────────────────────────────────────┐         \n\
        \    │ let union    = < Left : Natural | Right : Bool >.Left 2         │         \n\
        \    │ let handlers = { Left = Natural/even, Right = λ(x : Bool) → x } │         \n\
        \    │ in  merge handlers union : Bool                                 │         \n\
        \    └─────────────────────────────────────────────────────────────────┘         \n\
        \                                                                                \n\
        \                                                                                \n\
        \... as long as the output type of each handler function matches the declared    \n\
        \type of the result:                                                             \n\
        \                                                                                \n\
        \                                                                                \n\
        \    ┌───────────────────────────────────────────────────────────┐               \n\
        \    │ handlers : { Left : Natural → Bool, Right : Bool → Bool } │               \n\
        \    └───────────────────────────────────────────────────────────┘               \n\
        \                                    ⇧                    ⇧                      \n\
        \                                    These output types ...                      \n\
        \                                                                                \n\
        \                             ... must match the declared type of the ❰merge❱    \n\
        \                             ⇩                                                  \n\
        \    ┌─────────────────────────────┐                                             \n\
        \    │ merge handlers union : Bool │                                             \n\
        \    └─────────────────────────────┘                                             \n\
        \                                                                                \n\
        \                                                                                \n\
        \For example, the following expression is " <> _NOT <> " valid:                  \n\
        \                                                                                \n\
        \                                                                                \n\
        \    ┌──────────────────────────────────────────────────────────────────┐        \n\
        \    │ let union    = < Left : Natural | Right : Bool >.Left 2          │        \n\
        \    │ let handlers = { Left = Natural/even, Right = λ(x : Bool) → x }  │        \n\
        \    │ in  merge handlers union : Text                                  │        \n\
        \    └──────────────────────────────────────────────────────────────────┘        \n\
        \                                 ⇧                                              \n\
        \                                 Invalid: Doesn't match output of either handler\n\
        \                                                                                \n\
        \                                                                                \n\
        \Your handler for the following alternative:                                     \n\
        \                                                                                \n\
        \" <> txt0 <> "\n\
        \                                                                                \n\
        \... needs to return an output value of type:                                    \n\
        \                                                                                \n\
        \" <> txt1 <> "\n\
        \                                                                                \n\
        \... but actually returns an output value of a different type:                   \n\
        \                                                                                \n\
        \" <> txt2 <> "\n"
      where
        txt0 = insert expr0
        txt1 = insert expr1
        txt2 = insert expr2

prettyTypeMessage (HandlerOutputTypeMismatch key0 expr0 key1 expr1) =
    ErrorMessages {..}
  where
    short = "Handlers should have the same output type\n"
        <>  "\n"
        <>  Dhall.Diff.doc (Dhall.Diff.diffNormalized expr0 expr1)

    long =
        "Explanation: You can ❰merge❱ the alternatives of a union using a record with one\n\
        \handler per alternative, like this:                                             \n\
        \                                                                                \n\
        \                                                                                \n\
        \    ┌─────────────────────────────────────────────────────────────────┐         \n\
        \    │ let union    = < Left : Natural | Right : Bool >.Left 2         │         \n\
        \    │ let handlers = { Left = Natural/even, Right = λ(x : Bool) → x } │         \n\
        \    │ in  merge handlers union : Bool                                 │         \n\
        \    └─────────────────────────────────────────────────────────────────┘         \n\
        \                                                                                \n\
        \                                                                                \n\
        \... as long as the output type of each handler function is the same:            \n\
        \                                                                                \n\
        \                                                                                \n\
        \    ┌───────────────────────────────────────────────────────────┐               \n\
        \    │ handlers : { Left : Natural → Bool, Right : Bool → Bool } │               \n\
        \    └───────────────────────────────────────────────────────────┘               \n\
        \                                    ⇧                    ⇧                      \n\
        \                                These output types both match                   \n\
        \                                                                                \n\
        \                                                                                \n\
        \For example, the following expression is " <> _NOT <> " valid:                  \n\
        \                                                                                \n\
        \                                                                                \n\
        \    ┌─────────────────────────────────────────────────┐                         \n\
        \    │ let Union = < Left : Natural | Right : Bool >   │                         \n\
        \    │ let handlers =                                  │                         \n\
        \    │              { Left  = λ(x : Natural) → x       │  This outputs ❰Natural❱ \n\
        \    │              , Right = λ(x : Bool   ) → x       │  This outputs ❰Bool❱    \n\
        \    │              }                                  │                         \n\
        \    │ in  merge handlers (Union.Left 2)               │                         \n\
        \    └─────────────────────────────────────────────────┘                         \n\
        \                ⇧                                                               \n\
        \                Invalid: The handlers in this record don't have matching outputs\n\
        \                                                                                \n\
        \                                                                                \n\
        \The handler for the ❰" <> txt0 <> "❱ alternative has this output type:          \n\
        \                                                                                \n\
        \" <> txt1 <> "\n\
        \                                                                                \n\
        \... but the handler for the ❰" <> txt2 <> "❱ alternative has this output type instead:\n\
        \                                                                                \n\
        \" <> txt3 <> "\n"
      where
        txt0 = pretty key0
        txt1 = insert expr0
        txt2 = pretty key1
        txt3 = insert expr1

prettyTypeMessage (HandlerNotAFunction k expr0) = ErrorMessages {..}
  where
    short = "Handler is not a function"

    long =
        "Explanation: You can ❰merge❱ the alternatives of a union using a record with one\n\
        \handler per alternative, like this:                                             \n\
        \                                                                                \n\
        \                                                                                \n\
        \    ┌─────────────────────────────────────────────────────────────────┐         \n\
        \    │ let union    = < Left : Natural | Right : Bool >.Left 2         │         \n\
        \    │ let handlers = { Left = Natural/even, Right = λ(x : Bool) → x } │         \n\
        \    │ in  merge handlers union : Bool                                 │         \n\
        \    └─────────────────────────────────────────────────────────────────┘         \n\
        \                                                                                \n\
        \                                                                                \n\
        \... as long as each handler is a function -- FIXME                              \n\
        \                                                                                \n\
        \For example, the following expression is " <> _NOT <> " valid:                  \n\
        \                                                                                \n\
        \                                                                                \n\
        \    ┌───────────────────────────────────────────────────────┐                   \n\
        \    │ merge { Foo = True } (< Foo : Natural >.Foo 1) : Bool │                   \n\
        \    └───────────────────────────────────────────────────────┘                   \n\
        \                    ⇧                                                           \n\
        \                    Invalid: Not a function                                     \n\
        \                                                                                \n\
        \                                                                                \n\
        \Your handler for this alternative:                                              \n\
        \                                                                                \n\
        \" <> txt0 <> "\n\
        \                                                                                \n\
        \... has the following type:                                                     \n\
        \                                                                                \n\
        \" <> txt1 <> "\n\
        \                                                                                \n\
        \... which is not the type of a function                                         \n"
      where
        txt0 = insert k
        txt1 = insert expr0

prettyTypeMessage (MustMapARecord _expr0 _expr1) = ErrorMessages {..}
  where
    short = "❰toMap❱ expects a record value"

    long =
        "Explanation: You can apply ❰toMap❱ to any homogenous record, like this:         \n\
        \                                                                                \n\
        \                                                                                \n\
        \    ┌─────────────────────────────────────────────────────────────────────┐     \n\
        \    │ let record = { one = 1, two = 2 }                                   │     \n\
        \    │ in  toMap record : List { mapKey : Text, mapValue : Natural}        │     \n\
        \    └─────────────────────────────────────────────────────────────────────┘     \n\
        \                                                                                \n\
        \                                                                                \n\
        \... but the argument to ❰toMap❱ must be a record and not some other type.       \n"

prettyTypeMessage (InvalidToMapRecordKind type_ kind) = ErrorMessages {..}
  where
    short = "❰toMap❱ expects a record of kind ❰Type❱"

    long =
        "Explanation: You can apply ❰toMap❱ to any homogenous record of kind ❰Type❱, like\n\
        \ this:                                                                          \n\
        \                                                                                \n\
        \                                                                                \n\
        \    ┌─────────────────────────────────────────────────────────────────────┐     \n\
        \    │ let record = { one = 1, two = 2 }                                   │     \n\
        \    │ in  toMap record : List { mapKey : Text, mapValue : Natural}        │     \n\
        \    └─────────────────────────────────────────────────────────────────────┘     \n\
        \                                                                                \n\
        \                                                                                \n\
        \... but records of kind ❰Kind❱ or ❰Sort❱ cannot be turned into ❰List❱s.         \n\
        \────────────────────────────────────────────────────────────────────────────────\n\
        \                                                                                \n\
        \You applied ❰toMap❱ to a record of the following type:                          \n\
        \                                                                                \n\
        \" <> insert type_ <> "\n\
        \                                                                                \n\
        \... which has kind                                                              \n\
        \                                                                                \n\
        \" <> insert kind <> "\n"

prettyTypeMessage (HeterogenousRecordToMap _expr0 _expr1 _expr2) = ErrorMessages {..}
  where
    short = "❰toMap❱ expects a homogenous record"

    long =
        "Explanation: You can apply ❰toMap❱ to any homogenous record, like this:         \n\
        \                                                                                \n\
        \                                                                                \n\
        \    ┌─────────────────────────────────────────────────────────────────────┐     \n\
        \    │ let record = { one = 1, two = 2 }                                   │     \n\
        \    │ in  toMap record : List { mapKey : Text, mapValue : Natural}        │     \n\
        \    └─────────────────────────────────────────────────────────────────────┘     \n\
        \                                                                                \n\
        \                                                                                \n\
        \... but every field of the record must have the same type.                      \n\
        \                                                                                \n\
        \For example, the following expression is " <> _NOT <> " valid:                  \n\
        \                                                                                \n\
        \                                                                                \n\
        \    ┌─────────────────────────────────────────┐                                 \n\
        \    │ toMap { Foo = True, Bar = 0 }           │                                 \n\
        \    └─────────────────────────────────────────┘                                 \n\
        \                    ⇧           ⇧                                               \n\
        \                    Bool        Natural                                         \n"

prettyTypeMessage (MapTypeMismatch expr0 expr1) = ErrorMessages {..}
  where
    short = "❰toMap❱ result type doesn't match annotation"
        <>  "\n"
        <>  Dhall.Diff.doc (Dhall.Diff.diffNormalized expr0 expr1)

    long =
        "Explanation: a ❰toMap❱ application has been annotated with a type that doesn't  \n\
        \match its inferred type.                                                        \n"

prettyTypeMessage (InvalidToMapType expr) =
    ErrorMessages {..}
  where
    short = "An empty ❰toMap❱ was annotated with an invalid type"
        <>  "\n"
        <>  insert expr

    long =
        "Explanation: A ❰toMap❱ applied to an empty record must have a type annotation:  \n\
        \that matches a list of key-value pairs, like this                               \n\
        \                                                                                \n\
        \                                                                                \n\
        \    ┌─────────────────────────────────────────────────────────────────────┐     \n\
        \    │ toMap {=} : List { mapKey : Text, mapValue : Natural}               │     \n\
        \    └─────────────────────────────────────────────────────────────────────┘     \n\
        \                                                                                \n\
        \The type you have provided doesn't match the expected form.                     \n\
        \                                                                                \n"

prettyTypeMessage MissingToMapType =
    ErrorMessages {..}
  where
    short = "An empty ❰toMap❱ requires a type annotation"

    long =
        "Explanation: A ❰toMap❱ does not require a type annotation if the record has at  \n\
        \least one field, like this                                                      \n\
        \                                                                                \n\
        \                                                                                \n\
        \    ┌─────────────────────────────────────────────────────────────────────┐     \n\
        \    │ let record = { one = 1, two = 2 }                                   │     \n\
        \    │ in  toMap record                                                    │     \n\
        \    └─────────────────────────────────────────────────────────────────────┘     \n\
        \                                                                                \n\
        \                                                                                \n\
        \However, you must provide a type annotation with an empty record:               \n\
        \                                                                                \n\
        \                                                                                \n\
        \    ┌─────────────────────────────────────────────────────────────────────┐     \n\
        \    │ toMap {=} : List { mapKey : Text, mapValue : Natural}               │     \n\
        \    └─────────────────────────────────────────────────────────────────────┘     \n\
        \                                                                                \n"

prettyTypeMessage (CantAccess lazyText0 expr0 expr1) = ErrorMessages {..}
  where
    short = "Not a record or a union"

    long =
        "Explanation: You can only access fields on records or unions, like this:        \n\
        \                                                                                \n\
        \                                                                                \n\
        \    ┌───────────────────────────────────┐                                       \n\
        \    │ { foo = True, bar = \"ABC\" }.foo │  This is valid ...                    \n\
        \    └───────────────────────────────────┘                                       \n\
        \                                                                                \n\
        \                                                                                \n\
        \    ┌───────────────────────────────────────────┐                               \n\
        \    │ λ(r : { foo : Bool, bar : Text }) → r.foo │  ... and so is this           \n\
        \    └───────────────────────────────────────────┘                               \n\
        \                                                                                \n\
        \                                                                                \n\
        \    ┌─────────────────────────────────┐                                         \n\
        \    │ < foo : Bool | bar : Text >.foo │  ... and so is this                     \n\
        \    └─────────────────────────────────┘                                         \n\
        \                                                                                \n\
        \                                                                                \n\
        \    ┌────────────────────────────────────────────┐                              \n\
        \    │ λ(r : < foo : Bool | bar : Text >) → r.foo │  ... and so is this          \n\
        \    └────────────────────────────────────────────┘                              \n\
        \                                                                                \n\
        \                                                                                \n\
        \... but you cannot access fields on non-record expressions                      \n\
        \                                                                                \n\
        \For example, the following expression is " <> _NOT <> " valid:                  \n\
        \                                                                                \n\
        \                                                                                \n\
        \    ┌───────┐                                                                   \n\
        \    │ 1.foo │                                                                   \n\
        \    └───────┘                                                                   \n\
        \      ⇧                                                                         \n\
        \      Invalid: Not a record                                                     \n\
        \                                                                                \n\
        \                                                                                \n\
        \────────────────────────────────────────────────────────────────────────────────\n\
        \                                                                                \n\
        \You tried to access the field:                                                  \n\
        \                                                                                \n\
        \" <> txt0 <> "\n\
        \                                                                                \n\
        \... on the following expression which is not a record nor a union type:         \n\
        \                                                                                \n\
        \" <> txt1 <> "\n\
        \                                                                                \n\
        \... but is actually an expression of type:                                      \n\
        \                                                                                \n\
        \" <> txt2 <> "\n"
      where
        txt0 = insert lazyText0
        txt1 = insert expr0
        txt2 = insert expr1

prettyTypeMessage (CantProject lazyText0 expr0 expr1) = ErrorMessages {..}
  where
    short = "Not a record"

    long =
        "Explanation: You can only project fields on records, like this:                 \n\
        \                                                                                \n\
        \                                                                                \n\
        \    ┌─────────────────────────────────────────────────────┐                     \n\
        \    │ { foo = True, bar = \"ABC\", baz = 1 }.{ foo, bar } │  This is valid ...  \n\
        \    └─────────────────────────────────────────────────────┘                     \n\
        \                                                                                \n\
        \                                                                                \n\
        \    ┌────────────────────────────────────────────────────────────────────┐      \n\
        \    │ λ(r : { foo : Bool, bar : Text , baz : Natural }) → r.{ foo, bar } │  ... and so is this           \n\
        \    └────────────────────────────────────────────────────────────────────┘      \n\
        \                                                                                \n\
        \                                                                                \n\
        \... but you cannot project fields on non-record expressions                     \n\
        \                                                                                \n\
        \For example, the following expression is " <> _NOT <> " valid:                  \n\
        \                                                                                \n\
        \                                                                                \n\
        \    ┌────────────────┐                                                          \n\
        \    │ 1.{ foo, bar } │                                                          \n\
        \    └────────────────┘                                                          \n\
        \      ⇧                                                                         \n\
        \      Invalid: Not a record                                                     \n\
        \                                                                                \n\
        \                                                                                \n\
        \Some common reasons why you might get this error:                               \n\
        \                                                                                \n\
        \● You accidentally try to project fields of a union instead of a record, like   \n\
        \  this:                                                                         \n\
        \                                                                                \n\
        \                                                                                \n\
        \    ┌────────────────────────────────────┐                                      \n\
        \    │ < foo : a | bar : b >.{ foo, bar } │                                      \n\
        \    └────────────────────────────────────┘                                      \n\
        \      ⇧                                                                         \n\
        \      This is a union, not a record                                             \n\
        \                                                                                \n\
        \                                                                                \n\
        \────────────────────────────────────────────────────────────────────────────────\n\
        \                                                                                \n\
        \You tried to access the fields:                                                 \n\
        \                                                                                \n\
        \" <> txt0 <> "\n\
        \                                                                                \n\
        \... on the following expression which is not a record:                          \n\
        \                                                                                \n\
        \" <> txt1 <> "\n\
        \                                                                                \n\
        \... but is actually an expression of type:                                      \n\
        \                                                                                \n\
        \" <> txt2 <> "\n"
      where
        txt0 = insert lazyText0
        txt1 = insert expr0
        txt2 = insert expr1

prettyTypeMessage (CantProjectByExpression expr) = ErrorMessages {..}
  where
    short = "Selector is not a record type"

    long =
        "Explanation: You can project by an expression if that expression is a record    \n\
        \type:                                                                           \n\
        \                                                                                \n\
        \    ┌─────────────────────────────────┐                                         \n\
        \    │ { foo = True }.({ foo : Bool }) │  This is valid ...                      \n\
        \    └─────────────────────────────────┘                                         \n\
        \                                                                                \n\
        \                                                                                \n\
        \    ┌──────────────────────────────────────────┐                                \n\
        \    │ λ(r : { foo : Bool }) → r.{ foo : Bool } │  ... and so is this            \n\
        \    └──────────────────────────────────────────┘                                \n\
        \                                                                                \n\
        \                                                                                \n\
        \... but you cannot project by any other type of expression:                     \n\
        \                                                                                \n\
        \For example, the following expression is " <> _NOT <> " valid:                  \n\
        \                                                                                \n\
        \                                                                                \n\
        \    ┌───────────────────────┐                                                   \n\
        \    │ { foo = True }.(True) │                                                   \n\
        \    └───────────────────────┘                                                   \n\
        \                      ⇧                                                         \n\
        \                      Invalid: Not a record type                                \n\
        \                                                                                \n\
        \                                                                                \n\
        \Some common reasons why you might get this error:                               \n\
        \                                                                                \n\
        \● You accidentally try to project by a record value instead of a record type,   \n\
        \  like this:                                                                    \n\
        \                                                                                \n\
        \                                                                                \n\
        \    ┌─────────────────────────────────┐                                         \n\
        \    │ let T = { foo : Bool }          │                                         \n\
        \    │                                 │                                         \n\
        \    │ let x = { foo = True , bar = 1} │                                         \n\
        \    │                                 │                                         \n\
        \    │ let y = { foo = False, bar = 2} │                                         \n\
        \    │                                 │                                         \n\
        \    │ in  x.(y)                       │                                         \n\
        \    └─────────────────────────────────┘                                         \n\
        \             ⇧                                                                  \n\
        \             The user might have meant ❰T❱ here                                 \n\
        \                                                                                \n\
        \                                                                                \n\
        \────────────────────────────────────────────────────────────────────────────────\n\
        \                                                                                \n\
        \You tried to project out the following type:                                    \n\
        \                                                                                \n\
        \" <> txt <> "\n\
        \                                                                                \n\
        \... which is not a record type                                                  \n"
      where
        txt = insert expr

prettyTypeMessage (MissingField k expr0) = ErrorMessages {..}
  where
    short = "Missing record field"

    long =
        "Explanation: You can only access fields on records, like this:                  \n\
        \                                                                                \n\
        \                                                                                \n\
        \    ┌─────────────────────────────────┐                                         \n\
        \    │ { foo = True, bar = \"ABC\" }.foo │  This is valid ...                    \n\
        \    └─────────────────────────────────┘                                         \n\
        \                                                                                \n\
        \                                                                                \n\
        \    ┌───────────────────────────────────────────┐                               \n\
        \    │ λ(r : { foo : Bool, bar : Text }) → r.foo │  ... and so is this           \n\
        \    └───────────────────────────────────────────┘                               \n\
        \                                                                                \n\
        \                                                                                \n\
        \... but you can only access fields if they are present                          \n\
        \                                                                                \n\
        \For example, the following expression is " <> _NOT <> " valid:                  \n\
        \                                                                                \n\
        \                                                                                \n\
        \    ┌─────────────────────────────────┐                                         \n\
        \    │ { foo = True, bar = \"ABC\" }.qux │                                       \n\
        \    └─────────────────────────────────┘                                         \n\
        \                                  ⇧                                             \n\
        \                                  Invalid: the record has no ❰qux❱ field        \n\
        \                                                                                \n\
        \                                                                                \n\
        \You tried to access a field named:                                              \n\
        \                                                                                \n\
        \" <> txt0 <> "\n\
        \                                                                                \n\
        \... but the field is missing because the record only defines the following      \n\
        \fields:                                                                         \n\
        \                                                                                \n\
        \" <> txt1 <> "\n"
      where
        txt0 = insert k
        txt1 = insert expr0

prettyTypeMessage (MissingConstructor k expr0) = ErrorMessages {..}
  where
    short = "Missing constructor"

    long =
        "Explanation: You can access constructors from unions, like this:                \n\
        \                                                                                \n\
        \                                                                                \n\
        \    ┌───────────────────┐                                                       \n\
        \    │ < Foo | Bar >.Foo │  This is valid ...                                    \n\
        \    └───────────────────┘                                                       \n\
        \                                                                                \n\
        \                                                                                \n\
        \... but you can only access constructors if they match an union alternative of  \n\
        \the same name.                                                                  \n\
        \                                                                                \n\
        \For example, the following expression is " <> _NOT <> " valid:                  \n\
        \                                                                                \n\
        \                                                                                \n\
        \    ┌───────────────────┐                                                       \n\
        \    │ < Foo | Bar >.Baz │                                                       \n\
        \    └───────────────────┘                                                       \n\
        \                    ⇧                                                           \n\
        \                    Invalid: the union has no ❰Baz❱ alternative                 \n\
        \                                                                                \n\
        \                                                                                \n\
        \You tried to access a constructor named:                                        \n\
        \                                                                                \n\
        \" <> txt0 <> "\n\
        \                                                                                \n\
        \... but the constructor is missing because the union only defines the following \n\
        \alternatives:                                                                   \n\
        \                                                                                \n\
        \" <> txt1 <> "\n"
      where
        txt0 = insert k
        txt1 = insert expr0

prettyTypeMessage (ProjectionTypeMismatch k expr0 expr1 expr2 expr3) = ErrorMessages {..}
  where
    short = "Projection type mismatch\n"
        <>  "\n"
        <>  Dhall.Diff.doc (Dhall.Diff.diffNormalized expr2 expr3)

    long =
        "Explanation: You can project a subset of fields from a record by specifying the \n\
        \desired type of the final record, like this:                                    \n\
        \                                                                                \n\
        \                                                                                \n\
        \    ┌─────────────────────────────────────────────┐                             \n\
        \    │ { foo = 1, bar = True }.({ foo : Natural }) │  This is valid              \n\
        \    └─────────────────────────────────────────────┘                             \n\
        \                                                                                \n\
        \                                                                                \n\
        \... but the expected type for each desired field must match the actual type of  \n\
        \the corresponding field in the original record.                                 \n\
        \                                                                                \n\
        \For example, the following expression is " <> _NOT <> " valid:                  \n\
        \                                                                                \n\
        \              Invalid: The ❰foo❱ field contains ❰1❱, which has type ❰Natural❱...\n\
        \              ⇩                                                                 \n\
        \    ┌──────────────────────────────────────────┐                                \n\
        \    │ { foo = 1, bar = True }.({ foo : Text }) │                                \n\
        \    └──────────────────────────────────────────┘                                \n\
        \                                       ⇧                                        \n\
        \                                       ... but we requested that the ❰foo❱ field\n\
        \                                       must contain a value of type ❰Text❱      \n\
        \                                                                                \n\
        \                                                                                \n\
        \You tried to project out a field named:                                         \n\
        \                                                                                \n\
        \" <> txt0 <> "\n\
        \                                                                                \n\
        \... that should have type:                                                      \n\
        \                                                                                \n\
        \" <> txt1 <> "\n\
        \                                                                                \n\
        \... but that field instead had a value of type:                                 \n\
        \                                                                                \n\
        \" <> txt2 <> "\n"
      where
        txt0 = insert k
        txt1 = insert expr0
        txt2 = insert expr1

prettyTypeMessage (AssertionFailed expr0 expr1) = ErrorMessages {..}
  where
    short = "Assertion failed\n"
        <>  "\n"
        <>  Dhall.Diff.doc (Dhall.Diff.diffNormalized expr0 expr1)

    long =
        "Explanation: You can assert at type-checking time that two terms are equal if   \n\
        \they have the same normal form, like this:                                      \n\
        \                                                                                \n\
        \                                                                                \n\
        \    ┌────────────────────┐                                                      \n\
        \    │ assert : 2 + 2 ≡ 4 │  This is valid                                       \n\
        \    └────────────────────┘                                                      \n\
        \                                                                                \n\
        \                                                                                \n\
        \... and an assertion still succeeds if the normal forms only differ by renaming \n\
        \bound variables, like this:                                                     \n\
        \                                                                                \n\
        \                                                                                \n\
        \    ┌──────────────────────────────────────────────────────┐                    \n\
        \    │ assert : λ(n : Natural) → n + 0 ≡ λ(m : Natural) → m │  This is also valid\n\
        \    └──────────────────────────────────────────────────────┘                    \n\
        \                                                                                \n\
        \                                                                                \n\
        \However, an assertion fails if the normal forms differ in any other way.  For   \n\
        \example, the following assertion is " <> _NOT <> " valid:                       \n\
        \                                                                                \n\
        \                                                                                \n\
        \    ┌────────────────┐                                                          \n\
        \    │ assert : 0 ≡ 1 │  Invalid: ❰0❱ does not equal ❰1❱                         \n\
        \    └────────────────┘                                                          \n\
        \                                                                                \n\
        \                                                                                \n\
        \Some common reasons why you might get this error:                               \n\
        \                                                                                \n\
        \● You might have tried to ❰assert❱ a precondition on a function's input, like   \n\
        \  this:                                                                         \n\
        \                                                                                \n\
        \                                                                                \n\
        \    ┌──────────────────────────────────────────────────────────────────┐        \n\
        \    │ λ(n : Natural) → let _ = assert : Natural/isZero n ≡ False in n  │        \n\
        \    └──────────────────────────────────────────────────────────────────┘        \n\
        \                                        ⇧                                       \n\
        \                                        Invalid: This assertion will always fail\n\
        \                                                                                \n\
        \                                                                                \n\
        \  This will not work.  Such an assertion is checking all possible inputs to the \n\
        \  function, before you've even used the function at all.                        \n\
        \                                                                                \n\
        \────────────────────────────────────────────────────────────────────────────────\n\
        \                                                                                \n\
        \You tried to assert that this expression:                                       \n\
        \                                                                                \n\
        \" <> txt0 <> "\n\
        \                                                                                \n\
        \... is the same as this other expression:                                       \n\
        \                                                                                \n\
        \" <> txt1 <> "\n\
        \                                                                                \n\
        \... but they differ\n"
      where
        txt0 = insert expr0
        txt1 = insert expr1

prettyTypeMessage (NotAnEquivalence expr) = ErrorMessages {..}
  where
    short = "Not an equivalence\n"

    long =
        "Explanation: The type annotation for an ❰assert❱ must evaluate to an equivalence\n\
        \of the form ❰x ≡ y❱, like this:                                                 \n\
        \                                                                                \n\
        \                                                                                \n\
        \    ┌────────────────────┐                                                      \n\
        \    │ assert : 2 + 2 ≡ 4 │  This is valid                                       \n\
        \    └────────────────────┘                                                      \n\
        \                                                                                \n\
        \                                                                                \n\
        \... but any other type is not a valid annotation.  For example, the following   \n\
        \assertion is " <> _NOT <> " valid:                                              \n\
        \                                                                                \n\
        \                                                                                \n\
        \    ┌───────────────┐                                                           \n\
        \    │ assert : True │  Invalid: ❰True❱ is not an equivalence                    \n\
        \    └───────────────┘                                                           \n\
        \                                                                                \n\
        \                                                                                \n\
        \Some common reasons why you might get this error:                               \n\
        \                                                                                \n\
        \● You tried to supply an expression of type ❰Bool❱ to the assertion, rather than\n\
        \  two separate expressions to compare, like this:                               \n\
        \                                                                                \n\
        \                                                                                \n\
        \    ┌───────────────────────────┐                                               \n\
        \    │ assert : Natural/isZero 0 │  Invalid: A boolean expression is not the     \n\
        \    └───────────────────────────┘  same thing as a type-level equivalence       \n\
        \                                                                                \n\
        \                                                                                \n\
        \  You have to explicitly compare two expressions, even if that just means       \n\
        \  comparing the expression to ❰True❱, like this:                                \n\
        \                                                                                \n\
        \                                                                                \n\
        \    ┌──────────────────────────────────┐                                        \n\
        \    │ assert : Natural/isZero 0 ≡ True │  Valid: You can assert that two boolean\n\
        \    └──────────────────────────────────┘  expressions are equivalent            \n\
        \                                                                                \n\
        \                                                                                \n\
        \────────────────────────────────────────────────────────────────────────────────\n\
        \                                                                                \n\
        \You provided the following type annotation for an ❰assert❱:                     \n\
        \                                                                                \n\
        \" <> txt0 <> "\n\
        \                                                                                \n\
        \... which is not an equivalence\n"
      where
        txt0 = insert expr

prettyTypeMessage (IncomparableExpression expr) = ErrorMessages {..}
  where
    short = "Incomparable expression\n"

    long =
        "Explanation: You can use an ❰assert❱ to compare two terms for equivalence, like \n\
        \this:                                                                           \n\
        \                                                                                \n\
        \                                                                                \n\
        \    ┌────────────────────┐                                                      \n\
        \    │ assert : 2 + 2 ≡ 4 │  This is valid because ❰2 + 2❱ and ❰4❱ are both terms\n\
        \    └────────────────────┘                                                      \n\
        \                                                                                \n\
        \                                                                                \n\
        \... but you cannot compare expressions, that are not terms, such as types.  For \n\
        \example, the following equivalence is " <> _NOT <> " valid:                     \n\
        \                                                                                \n\
        \                                                                                \n\
        \    ┌────────────────────────────┐                                              \n\
        \    │ assert : Natural ≡ Natural │  Invalid: ❰Natural❱ is a type, not a term    \n\
        \    └────────────────────────────┘                                              \n\
        \                                                                                \n\
        \                                                                                \n\
        \You tried to compare the following expression:                                  \n\
        \                                                                                \n\
        \" <> txt0 <> "\n\
        \                                                                                \n\
        \... which is not a term\n"
      where
        txt0 = insert expr

prettyTypeMessage (EquivalenceTypeMismatch l _L r _R) = ErrorMessages {..}
  where
    short = "The two sides of the equivalence have different types"

    long =
        "Explanation: You can use ❰≡❱ to compare two terms of the same type for          \n\
        \equivalence, like this:                                                         \n\
        \                                                                                \n\
        \                                                                                \n\
        \    ┌───────────┐                                                               \n\
        \    │ 2 + 2 ≡ 4 │  This is valid because ❰2 + 2❱ and ❰4❱ have the same type     \n\
        \    └───────────┘                                                               \n\
        \                                                                                \n\
        \                                                                                \n\
        \... but you cannot compare expressions, that have different types.  For example,\n\
        \the following assertion is " <> _NOT <> " valid:                                \n\
        \                                                                                \n\
        \                                                                                \n\
        \    ┌──────────┐                                                                \n\
        \    │ 1 ≡ True │  Invalid: ❰1❱ has type ❰Natural❱, ❰True❱ has type ❰Bool❱       \n\
        \    └──────────┘                                                                \n\
        \                                                                                \n\
        \                                                                                \n\
        \You tried to compare the following expressions:                                 \n\
        \                                                                                \n\
        \" <> insert l <> "\n\
        \                                                                                \n\
        \... which has type\n\
        \                                                                                \n\
        \" <> insert _L <> "\n\
        \                                                                                \n\
        \... and\n\
        \                                                                                \n\
        \" <> insert r <> "\n\
        \                                                                                \n\
        \... which has type\n\
        \                                                                                \n\
        \" <> insert _R <> "\n"

prettyTypeMessage (CantAnd expr0 expr1) =
        buildBooleanOperator "&&" expr0 expr1

prettyTypeMessage (CantOr expr0 expr1) =
        buildBooleanOperator "||" expr0 expr1

prettyTypeMessage (CantEQ expr0 expr1) =
        buildBooleanOperator "==" expr0 expr1

prettyTypeMessage (CantNE expr0 expr1) =
        buildBooleanOperator "!=" expr0 expr1

prettyTypeMessage (CantInterpolate expr0 expr1) = ErrorMessages {..}
  where
    short = "You can only interpolate ❰Text❱"

    long =
        "Explanation: Text interpolation only works on expressions of type ❰Text❱        \n\
        \                                                                                \n\
        \For example, these are all valid uses of string interpolation:                  \n\
        \                                                                                \n\
        \                                                                                \n\
        \    ┌──────────────────┐                                                        \n\
        \    │ \"ABC${\"DEF\"}GHI\" │                                                        \n\
        \    └──────────────────┘                                                        \n\
        \                                                                                \n\
        \                                                                                \n\
        \    ┌────────────────────────────┐                                              \n\
        \    │ λ(x : Text) → \"ABC${x}GHI\" │                                              \n\
        \    └────────────────────────────┘                                              \n\
        \                                                                                \n\
        \                                                                                \n\
        \    ┌───────────────────────────────────────────────┐                           \n\
        \    │ λ(age : Natural) → \"Age: ${Natural/show age}\" │                           \n\
        \    └───────────────────────────────────────────────┘                           \n\
        \                                                                                \n\
        \                                                                                \n\
        \Some common reasons why you might get this error:                               \n\
        \                                                                                \n\
        \● You might have thought that string interpolation automatically converts the   \n\
        \  interpolated value to a ❰Text❱ representation of that value:                  \n\
        \                                                                                \n\
        \                                                                                \n\
        \    ┌──────────────────────────────────┐                                        \n\
        \    │ λ(age : Natural) → \"Age: ${age}\" │                                        \n\
        \    └──────────────────────────────────┘                                        \n\
        \                                  ⇧                                             \n\
        \                                  Invalid: ❰age❱ has type ❰Natural❱             \n\
        \                                                                                \n\
        \                                                                                \n\
        \● You might have forgotten to escape a string interpolation that you wanted     \n\
        \  Dhall to ignore and pass through:                                             \n\
        \                                                                                \n\
        \                                                                                \n\
        \    ┌────────────────┐                                                          \n\
        \    │ \"echo ${HOME}\" │                                                          \n\
        \    └────────────────┘                                                          \n\
        \             ⇧                                                                  \n\
        \             ❰HOME❱ is not in scope and this might have meant to use ❰\\${HOME}❱\n\
        \                                                                                \n\
        \                                                                                \n\
        \────────────────────────────────────────────────────────────────────────────────\n\
        \                                                                                \n\
        \You interpolated this expression:                                               \n\
        \                                                                                \n\
        \" <> txt0 <> "\n\
        \                                                                                \n\
        \... which does not have type ❰Text❱ but instead has type:                       \n\
        \                                                                                \n\
        \" <> txt1 <> "\n"
      where
        txt0 = insert expr0
        txt1 = insert expr1

prettyTypeMessage (CantTextAppend expr0 expr1) = ErrorMessages {..}
  where
    short = "❰++❱ only works on ❰Text❱"

    long =
        "Explanation: The ❰++❱ operator expects two arguments that have type ❰Text❱      \n\
        \                                                                                \n\
        \For example, this is a valid use of ❰++❱:                                       \n\
        \                                                                                \n\
        \                                                                                \n\
        \    ┌────────────────┐                                                          \n\
        \    │ \"ABC\" ++ \"DEF\" │                                                          \n\
        \    └────────────────┘                                                          \n\
        \                                                                                \n\
        \                                                                                \n\
        \Some common reasons why you might get this error:                               \n\
        \                                                                                \n\
        \● You might have thought that ❰++❱ was the operator to combine two lists:       \n\
        \                                                                                \n\
        \                                                                                \n\
        \    ┌────────────────────────┐                                                  \n\
        \    │ [1, 2, 3] ++ [4, 5, 6] │  Not valid                                       \n\
        \    └────────────────────────┘                                                  \n\
        \                                                                                \n\
        \                                                                                \n\
        \  ... but the list concatenation operator is actually ❰#❱:                      \n\
        \                                                                                \n\
        \                                                                                \n\
        \    ┌───────────────────────┐                                                   \n\
        \    │ [1, 2, 3] # [4, 5, 6] │  Valid                                            \n\
        \    └───────────────────────┘                                                   \n\
        \                                                                                \n\
        \                                                                                \n\
        \────────────────────────────────────────────────────────────────────────────────\n\
        \                                                                                \n\
        \You provided this argument:                                                     \n\
        \                                                                                \n\
        \" <> txt0 <> "\n\
        \                                                                                \n\
        \... which does not have type ❰Text❱ but instead has type:                       \n\
        \                                                                                \n\
        \" <> txt1 <> "\n"
      where
        txt0 = insert expr0
        txt1 = insert expr1

prettyTypeMessage (CantListAppend expr0 expr1) = ErrorMessages {..}
  where
    short = "❰#❱ only works on ❰List❱s"

    long =
        "Explanation: The ❰#❱ operator expects two arguments that are both ❰List❱s       \n\
        \                                                                                \n\
        \For example, this is a valid use of ❰#❱:                                        \n\
        \                                                                                \n\
        \                                                                                \n\
        \    ┌───────────────────────┐                                                   \n\
        \    │ [1, 2, 3] # [4, 5, 6] │                                                   \n\
        \    └───────────────────────┘                                                   \n\
        \                                                                                \n\
        \                                                                                \n\
        \────────────────────────────────────────────────────────────────────────────────\n\
        \                                                                                \n\
        \You provided this argument:                                                     \n\
        \                                                                                \n\
        \" <> txt0 <> "\n\
        \                                                                                \n\
        \... which is not a ❰List❱ but instead has type:                                 \n\
        \                                                                                \n\
        \" <> txt1 <> "\n"
      where
        txt0 = insert expr0
        txt1 = insert expr1

prettyTypeMessage (CantAdd expr0 expr1) =
        buildNaturalOperator "+" expr0 expr1

prettyTypeMessage (CantMultiply expr0 expr1) =
        buildNaturalOperator "*" expr0 expr1

buildBooleanOperator :: Pretty a => Text -> Expr s a -> Expr s a -> ErrorMessages
buildBooleanOperator operator expr0 expr1 = ErrorMessages {..}
  where
    short = "❰" <> txt2 <> "❱ only works on ❰Bool❱s"

    long =
        "Explanation: The ❰" <> txt2 <> "❱ operator expects two arguments that have type ❰Bool❱\n\
        \                                                                                \n\
        \For example, this is a valid use of ❰" <> txt2 <> "❱:                           \n\
        \                                                                                \n\
        \                                                                                \n\
        \    ┌───────────────┐                                                           \n\
        \    │ True " <> txt2 <> " False │                                               \n\
        \    └───────────────┘                                                           \n\
        \                                                                                \n\
        \                                                                                \n\
        \You provided this argument:                                                     \n\
        \                                                                                \n\
        \" <> txt0 <> "\n\
        \                                                                                \n\
        \... which does not have type ❰Bool❱ but instead has type:                       \n\
        \                                                                                \n\
        \" <> txt1 <> "\n"
      where
        txt0 = insert expr0
        txt1 = insert expr1

    txt2 = pretty operator

buildNaturalOperator :: Pretty a => Text -> Expr s a -> Expr s a -> ErrorMessages
buildNaturalOperator operator expr0 expr1 = ErrorMessages {..}
  where
    short = "❰" <> txt2 <> "❱ only works on ❰Natural❱s"

    long =
        "Explanation: The ❰" <> txt2 <> "❱ operator expects two arguments that have type ❰Natural❱\n\
        \                                                                                \n\
        \For example, this is a valid use of ❰" <> txt2 <> "❱:                           \n\
        \                                                                                \n\
        \                                                                                \n\
        \    ┌───────┐                                                                   \n\
        \    │ 3 " <> txt2 <> " 5 │                                                      \n\
        \    └───────┘                                                                   \n\
        \                                                                                \n\
        \                                                                                \n\
        \Some common reasons why you might get this error:                               \n\
        \                                                                                \n\
        \● You might have tried to use an ❰Integer❱, which is " <> _NOT <> " allowed:    \n\
        \                                                                                \n\
        \                                                                                \n\
        \    ┌─────────────────────────────────────────┐                                 \n\
        \    │ λ(x : Integer) → λ(y : Integer) → x " <> txt2 <> " y │  Not valid         \n\
        \    └─────────────────────────────────────────┘                                 \n\
        \                                                                                \n\
        \                                                                                \n\
        \  You can only use ❰Natural❱ numbers                                            \n\
        \                                                                                \n\
        \                                                                                \n\
        \● You might have mistakenly used an ❰Integer❱ literal, which is " <> _NOT <> " allowed:\n\
        \                                                                                \n\
        \                                                                                \n\
        \    ┌─────────┐                                                                 \n\
        \    │ +2 " <> txt2 <> " +2 │  Not valid                                         \n\
        \    └─────────┘                                                                 \n\
        \                                                                                \n\
        \                                                                                \n\
        \  You need to remove the leading ❰+❱ to transform them into ❰Natural❱ literals, \n\
        \  like this:                                                                    \n\
        \                                                                                \n\
        \                                                                                \n\
        \    ┌───────┐                                                                   \n\
        \    │ 2 " <> txt2 <> " 2 │  Valid                                               \n\
        \    └───────┘                                                                   \n\
        \                                                                                \n\
        \                                                                                \n\
        \────────────────────────────────────────────────────────────────────────────────\n\
        \                                                                                \n\
        \You provided this argument:                                                     \n\
        \                                                                                \n\
        \" <> txt0 <> "\n\
        \                                                                                \n\
        \... which does not have type ❰Natural❱ but instead has type:                    \n\
        \                                                                                \n\
        \" <> txt1 <> "\n"
      where
        txt0 = insert expr0
        txt1 = insert expr1

    txt2 = pretty operator

-- | A structured type error that includes context
data TypeError s a = TypeError
    { context     :: Context (Expr s a)
    , current     :: Expr s a
    , typeMessage :: TypeMessage s a
    }

instance (Eq a, Pretty s, Pretty a, ToTerm a) => Show (TypeError s a) where
    show = Pretty.renderString . Pretty.layoutPretty layoutOpts . Pretty.pretty

instance (Eq a, Pretty s, Pretty a, ToTerm a, Typeable s, Typeable a) => Exception (TypeError s a)

instance (Eq a, Pretty s, Pretty a, ToTerm a) => Pretty (TypeError s a) where
    pretty (TypeError ctx expr msg)
        = Pretty.unAnnotate
            (   "\n"
            <>  (   if null (Dhall.Context.toList ctx)
                    then ""
                    else prettyContext ctx <> "\n\n"
                )
            <>  shortTypeMessage msg <> "\n"
            <>  source
            )
      where
        prettyKV (key, val) =
            pretty key <> " : " <> Dhall.Util.snipDoc (pretty val)

        prettyContext =
                Pretty.vsep
            .   map prettyKV
            .   reverse
            .   Dhall.Context.toList

        source = case expr of
            Note s _ -> pretty s
            _        -> mempty

{-| Newtype used to wrap error messages so that they render with a more
    detailed explanation of what went wrong
-}
newtype DetailedTypeError s a = DetailedTypeError (TypeError s a)
    deriving (Typeable)

instance (Eq a, Pretty s, Pretty a, ToTerm a) => Show (DetailedTypeError s a) where
    show = Pretty.renderString . Pretty.layoutPretty layoutOpts . Pretty.pretty

instance (Eq a, Pretty s, Pretty a, ToTerm a, Typeable s, Typeable a) => Exception (DetailedTypeError s a)

instance (Eq a, Pretty s, Pretty a, ToTerm a) => Pretty (DetailedTypeError s a) where
    pretty (DetailedTypeError (TypeError ctx expr msg))
        = Pretty.unAnnotate
            (   "\n"
            <>  (   if null (Dhall.Context.toList ctx)
                    then ""
                    else prettyContext ctx <> "\n\n"
                )
            <>  longTypeMessage msg <> "\n"
            <>  "────────────────────────────────────────────────────────────────────────────────\n"
            <>  "\n"
            <>  source
            )
      where
        prettyKV (key, val) =
            pretty key <> " : " <> Dhall.Util.snipDoc (pretty val)

        prettyContext =
                Pretty.vsep
            .   map prettyKV
            .   reverse
            .   Dhall.Context.toList

        source = case expr of
            Note s _ -> pretty s
            _        -> mempty

{-| This function verifies that a custom context is well-formed so that
    type-checking will not loop

    Note that `typeWith` already calls `checkContext` for you on the `Context`
    that you supply
-}
checkContext :: Context (Expr s X) -> Either (TypeError s X) ()
checkContext context =
    case Dhall.Context.match context of
        Nothing -> do
            return ()
        Just (x, v, context') -> do
            let shiftedV       =       Dhall.Core.shift (-1) (V x 0)  v
            let shiftedContext = fmap (Dhall.Core.shift (-1) (V x 0)) context'
            _ <- typeWith shiftedContext shiftedV
            return ()