    {-# LANGUAGE CPP #-}
    module Agda.TypeChecking.Errors
        ( prettyError
        , PrettyTCM(..)
        , tcErrString
        ) where

    import Control.Applicative ( (<$>) )
    import Control.Monad.State
    import Control.Monad.Error
    import qualified Data.Map as Map (empty)
    import System.FilePath

    import Agda.Syntax.Common
    import Agda.Syntax.Fixity
    import Agda.Syntax.Position
    import qualified Agda.Syntax.Info as A
    import qualified Agda.Syntax.Concrete as C
    import qualified Agda.Syntax.Concrete.Definitions as D
    import Agda.Syntax.Abstract as A
    import Agda.Syntax.Internal as I
    import qualified Agda.Syntax.Abstract.Pretty as P
    import qualified Agda.Syntax.Concrete.Pretty as P
    import Agda.Syntax.Translation.InternalToAbstract
    import Agda.Syntax.Translation.AbstractToConcrete

    import Agda.TypeChecking.Monad
    import Agda.TypeChecking.Pretty

    import Agda.Utils.FileName
    import Agda.Utils.Monad
    import Agda.Utils.Trace
    import Agda.Utils.Size

    #include "../undefined.h"
    import Agda.Utils.Impossible

    ---------------------------------------------------------------------------
    -- * Top level function
    ---------------------------------------------------------------------------

    prettyError :: MonadTCM tcm => TCErr -> tcm String
    prettyError err = liftTCM $ liftM show $
        prettyTCM err
        `catchError` \err' -> text "panic: error when printing error!" $$ prettyTCM err'
        `catchError` \err'' -> text "much panic: error when printing error from printing error!" $$ prettyTCM err''
        `catchError` \err''' -> fsep (
    	pwords "total panic: error when printing error from printing error from printing error." ++
    	pwords "I give up! Approximations of errors:" )
    	$$ vcat (map (text . tcErrString) [err,err',err'',err'''])

    ---------------------------------------------------------------------------
    -- * Helpers
    ---------------------------------------------------------------------------

    sayWhere :: (MonadTCM tcm, HasRange a) => a -> tcm Doc -> tcm Doc
    sayWhere x d = text (show $ getRange x) $$ d

    sayWhen :: MonadTCM tcm => CallTrace -> tcm Doc -> tcm Doc
    sayWhen tr m = case matchCall interestingCall tr of
      Nothing -> sayWhere tr m
      Just c  -> sayWhere tr (m $$ prettyTCM c)

    panic :: MonadTCM tcm => String -> tcm Doc
    panic s = fwords $ "Panic: " ++ s

    nameWithBinding :: MonadTCM tcm => QName -> tcm Doc
    nameWithBinding q =
      sep [ prettyTCM q, text "bound at", text (show r) ]
      where
        r = nameBindingSite $ qnameName q

    tcErrString :: TCErr -> String
    tcErrString err = show (getRange err) ++ " " ++ case errError err of
        TypeError _ cl  -> errorString $ clValue cl
        Exception r s   -> show r ++ " " ++ s
        IOException r e -> show r ++ " " ++ show e
        PatternErr _    -> "PatternErr"
        AbortAssign _   -> "AbortAssign"

    errorString :: TypeError -> String
    errorString err = case err of
        AmbiguousModule _ _			       -> "AmbiguousModule"
        AmbiguousName _ _			       -> "AmbiguousName"
        AmbiguousParseForApplication _ _	       -> "AmbiguousParseForApplication"
        AmbiguousParseForLHS _ _		       -> "AmbiguousParseForLHS"
        AmbiguousTopLevelModuleName {}	       -> "AmbiguousTopLevelModuleName"
        BothWithAndRHS                             -> "BothWithAndRHS"
        BuiltinInParameterisedModule _	       -> "BuiltinInParameterisedModule"
        BuiltinMustBeConstructor _ _               -> "BuiltinMustBeConstructor"
        ClashingDefinition _ _		       -> "ClashingDefinition"
        ClashingFileNamesFor _ _		       -> "ClashingFileNamesFor"
        ClashingImport _ _			       -> "ClashingImport"
        ClashingModule _ _			       -> "ClashingModule"
        ClashingModuleImport _ _		       -> "ClashingModuleImport"
        CompilationError _                         -> "CompilationError"
        ConstructorPatternInWrongDatatype _ _      -> "ConstructorPatternInWrongDatatype"
        CoverageFailure _ _                        -> "CoverageFailure"
        CoverageCantSplitOn _                      -> "CoverageCantSplitOn"
        CoverageCantSplitType _                    -> "CoverageCantSplitType"
        CyclicModuleDependency _		       -> "CyclicModuleDependency"
        DataMustEndInSort _			       -> "DataMustEndInSort"
        DependentPatternMatchingOnCodata           -> "DependentPatternMatchingOnCodata"
        DifferentArities			       -> "DifferentArities"
        DoesNotConstructAnElementOf{}              -> "DoesNotConstructAnElementOf"
        DuplicateBuiltinBinding _ _ _	       -> "DuplicateBuiltinBinding"
        DuplicateFields _			       -> "DuplicateFields"
        DuplicateConstructors _		       -> "DuplicateConstructors"
        FieldOutsideRecord                         -> "FieldOutsideRecord"
        FileNotFound _ _			       -> "FileNotFound"
        GenericError _			       -> "GenericError"
        IlltypedPattern _ _                        -> "IlltypedPattern"
        IncompletePatternMatching _ _	       -> "IncompletePatternMatching"
        InternalError _			       -> "InternalError"
        InvalidPattern _                           -> "InvalidPattern"
        LocalVsImportedModuleClash _	       -> "LocalVsImportedModuleClash"
        MetaCannotDependOn _ _ _		       -> "MetaCannotDependOn"
        MetaOccursInItself _		       -> "MetaOccursInItself"
        ModuleArityMismatch _ _ _                  -> "ModuleArityMismatch"
        ModuleDefinedInOtherFile {}                -> "ModuleDefinedInOtherFile"
        ModuleDoesntExport _ _		       -> "ModuleDoesntExport"
        ModuleNameDoesntMatchFileName {}	       -> "ModuleNameDoesntMatchFileName"
        NoBindingForBuiltin _		       -> "NoBindingForBuiltin"
        NoParseForApplication _		       -> "NoParseForApplication"
        NoParseForLHS _			       -> "NoParseForLHS"
        NoRHSRequiresAbsurdPattern _	       -> "NoRHSRequiresAbsurdPattern"
        NotInductive {}                            -> "NotInductive"
        AbsurdPatternRequiresNoRHS _	       -> "AbsurdPatternRequiresNoRHS"
        NoSuchBuiltinName _			       -> "NoSuchBuiltinName"
        NoSuchModule _			       -> "NoSuchModule"
        NoSuchPrimitiveFunction _		       -> "NoSuchPrimitiveFunction"
        NotAModuleExpr _			       -> "NotAModuleExpr"
        NotAProperTerm			       -> "NotAProperTerm"
        NotAValidLetBinding _		       -> "NotAValidLetBinding"
        NotAnExpression _			       -> "NotAnExpression"
        NotImplemented _			       -> "NotImplemented"
        NotSupported _			       -> "NotSupported"
        NotInScope _			       -> "NotInScope"
        NotLeqSort _ _			       -> "NotLeqSort"
        NotStrictlyPositive _ _		       -> "NotStrictlyPositive"
        NothingAppliedToHiddenArg _		       -> "NothingAppliedToHiddenArg"
        OverlappingProjects {}                     -> "OverlappingProjects"
        PatternShadowsConstructor {}               -> "PatternShadowsConstructor"
        PropMustBeSingleton			       -> "PropMustBeSingleton"
        RepeatedVariablesInPattern _	       -> "RepeatedVariablesInPattern"
        ShadowedModule _                           -> "ShadowedModule"
        ShouldBeASort _			       -> "ShouldBeASort"
        ShouldBeApplicationOf _ _		       -> "ShouldBeApplicationOf"
        ShouldBeAppliedToTheDatatypeParameters _ _ -> "ShouldBeAppliedToTheDatatypeParameters"
        ShouldBeEmpty _ _			       -> "ShouldBeEmpty"
        ShouldBePi _			       -> "ShouldBePi"
        ShouldBeRecordType _		       -> "ShouldBeRecordType"
        ShouldEndInApplicationOfTheDatatype _      -> "ShouldEndInApplicationOfTheDatatype"
        TerminationCheckFailed _		       -> "TerminationCheckFailed"
        TooFewFields _ _			       -> "TooFewFields"
        TooManyArgumentsInLHS _ _                  -> "TooManyArgumentsInLHS"
        TooManyFields _ _			       -> "TooManyFields"
        UnequalHiding _ _			       -> "UnequalHiding"
        UnequalSorts{}			       -> "UnequalSorts"
        UnequalTerms{}			       -> "UnequalTerms"
        UnequalTypes{}			       -> "UnequalTypes"
        UnequalTelescopes{}			       -> "UnequalTelescopes"
        UnexpectedWithPatterns _                   -> "UnexpectedWithPatterns"
        UninstantiatedDotPattern _                 -> "UninstantiatedDotPattern"
        UninstantiatedModule _		       -> "UninstantiatedModule"
        UnreachableClauses{}                       -> "UnreachableClauses"
        UnsolvedConstraints _		       -> "UnsolvedConstraints"
        UnsolvedMetas _			       -> "UnsolvedMetas"
        WithClausePatternMismatch _ _              -> "WithClausePatternMismatch"
        WrongHidingInApplication _		       -> "WrongHidingInApplication"
        WrongHidingInLHS _			       -> "WrongHidingInLHS"
        WrongHidingInLambda _		       -> "WrongHidingInLambda"
        WrongNumberOfConstructorArguments _ _ _    -> "WrongNumberOfConstructorArguments"

    instance PrettyTCM TCErr where
        prettyTCM err = case errError err of
    	TypeError s e -> do
    	    s0 <- get
    	    put s
    	    d <- sayWhen (clTrace e) $ prettyTCM e
    	    put s0
    	    return d
    	Exception r s   -> sayWhere r $ fwords s
    	IOException r e -> sayWhere r $ fwords $ show e
    	PatternErr _    -> sayWhere err $ panic "uncaught pattern violation"
    	AbortAssign _   -> sayWhere err $ panic "uncaught aborted assignment"

    instance PrettyTCM TypeError where
        prettyTCM err = do
    	trace <- getTrace
    	case err of
    	    InternalError s  -> panic s
    	    NotImplemented s -> fwords $ "Not implemented: " ++ s
    	    NotSupported s -> fwords $ "Not supported: " ++ s
    	    CompilationError s -> sep [fwords "Compilation error:", text s]
    	    GenericError s   -> fwords s
    	    TerminationCheckFailed because -> fsep $
    	      pwords "Termination checking failed for the following functions:" ++
                  [ fsep (punctuate comma (map (text . show . qnameName)
                                               (concatMap fst because))) <> text "." ]
    	    PropMustBeSingleton -> fwords
    		"Datatypes in Prop must have at most one constructor when proof irrelevance is enabled"
    	    DataMustEndInSort t -> fsep $
    		pwords "The type of a datatype must end in a sort."
    		++ [prettyTCM t] ++ pwords "isn't a sort."
    	    ShouldEndInApplicationOfTheDatatype t -> fsep $
    		pwords "The target of a constructor must be the datatype applied to its parameters,"
    		++ [prettyTCM t] ++ pwords "isn't"
    	    ShouldBeAppliedToTheDatatypeParameters s t -> fsep $
    		pwords "The target of the constructor should be" ++ [prettyTCM s] ++
    		pwords "instead of" ++ [prettyTCM t]
    	    ShouldBeApplicationOf t q -> fsep $
    		pwords "The pattern constructs an element of" ++ [prettyTCM q] ++
    		pwords "which is not the right datatype"
    	    ShouldBeRecordType t -> fsep $
    		pwords "Expected record type, found " ++ [prettyTCM t]
    	    DifferentArities ->
    		fwords "The number of arguments in the defining equations differ"
    	    WrongHidingInLHS t -> do
    		fwords "Found an implicit argument where an explicit argument was expected"
    	    WrongHidingInLambda t -> do
    		fwords "Found an implicit lambda where an explicit lambda was expected"
    	    WrongHidingInApplication t -> do
    		fwords "Found an implicit application where an explicit application was expected"
                DependentPatternMatchingOnCodata ->
                  fwords "Dependent pattern matching on codata is not allowed"
                NotInductive t -> fsep $
                  [prettyTCM t] ++ pwords "is not an inductive data type"
                UninstantiatedDotPattern e -> fsep $
                  pwords "Failed to infer the value of dotted pattern"
                IlltypedPattern p a -> fsep $
                  pwords "Type mismatch"
                TooManyArgumentsInLHS n a -> fsep $
                  pwords "Left hand side gives too many arguments to a function of type" ++ [prettyTCM a]
                WrongNumberOfConstructorArguments c expect given -> fsep $
                  pwords "The constructor" ++ [prettyTCM c] ++ pwords "expects" ++
                  [text (show expect)] ++ pwords "arguments, but has been given" ++ [text (show given)]
                DoesNotConstructAnElementOf c t -> fsep $
                  pwords "the constructor" ++ [prettyTCM c] ++
                  pwords "does not construct an element of" ++ [prettyTCM t]
                ConstructorPatternInWrongDatatype c d -> fsep $
                  [prettyTCM c] ++ pwords "is not a constructor of the datatype" ++ [prettyTCM d]
                ShadowedModule [] -> __IMPOSSIBLE__
                ShadowedModule ms@(m : _) -> fsep $
                  pwords "Duplicate definition of module" ++ [prettyTCM m <> text "."] ++
                  pwords "Previous definition at" ++ [text $ show r]
                  where
                    r = case [ r | r <- map (defSiteOfLast . mnameToList) ms
                                 , r /= noRange ] of
                          []    -> noRange
                          r : _ -> r

                    defSiteOfLast [] = noRange
                    defSiteOfLast ns = nameBindingSite (last ns)
                ModuleArityMismatch m EmptyTel args -> fsep $
                  pwords "The module" ++ [prettyTCM m] ++
                  pwords "is not parameterized, but is being applied to arguments"
                ModuleArityMismatch m tel@(ExtendTel _ _) args -> fsep $
                  pwords "The arguments to " ++ [prettyTCM m] ++ pwords "does not fit the telescope" ++
    	      [prettyTCM tel]
                ShouldBeEmpty t [] -> fsep $
    		[prettyTCM t] ++ pwords "should be empty, but it isn't obvious that it is."
    	    ShouldBeEmpty t ps -> fsep (
    		[prettyTCM t] ++
                    pwords "should be empty, but the following constructor patterns are valid:"
                  ) $$ nest 2 (vcat $ map (showPat 0) ps)

    	    ShouldBeASort t -> fsep $
    		[prettyTCM t] ++ pwords "should be a sort, but it isn't"
    	    ShouldBePi t -> fsep $
    		[prettyTCM t] ++ pwords "should be a function type, but it isn't"
    	    NotAProperTerm ->
    		fwords "Found a malformed term"
    	    UnequalTerms cmp s t a -> fsep $
    		[prettyTCM s, f cmp, prettyTCM t] ++ pwords "of type" ++ [prettyTCM a]
                    where
                      f CmpEq  = text "!="
                      f CmpLeq = text "!=<"
    	    UnequalTelescopes cmp a b -> fsep $
    		[prettyTCM a, f cmp, prettyTCM b]
                    where
                      f CmpEq  = text "!="
                      f CmpLeq = text "!=<"
    	    UnequalTypes cmp a b -> fsep $
    		[prettyTCM a, f cmp, prettyTCM b]
                    where
                      f CmpEq  = text "!="
                      f CmpLeq = text "!=<"
    	    UnequalHiding a b -> fsep $
    		[prettyTCM a] ++ pwords "!=" ++ [prettyTCM b] ++
    		pwords "because one is an implicit function type and the other is an explicit function type"
    	    UnequalSorts s1 s2 -> fsep $
    		[prettyTCM s1] ++ pwords "!=" ++ [prettyTCM s2]
    	    NotLeqSort s1 s2 -> fsep $
    		pwords "The type of the constructor does not fit in the sort of the datatype, since"
    		++ [prettyTCM s1] ++ pwords "is not less or equal than" ++ [prettyTCM s2]
    	    TooFewFields r xs -> fsep $
    		pwords "Missing fields" ++ punctuate comma (map pretty xs) ++
    		pwords "in an element of the record" ++ [prettyTCM r]
    	    TooManyFields r xs -> fsep $
    		pwords "The record type" ++ [prettyTCM r] ++
    		pwords "does not have the fields" ++ punctuate comma (map pretty xs)
    	    DuplicateConstructors xs -> fsep $
    		pwords "Duplicate constructors" ++ punctuate comma (map pretty xs) ++
    		pwords "in datatype"
    	    DuplicateFields xs -> fsep $
    		pwords "Duplicate fields" ++ punctuate comma (map pretty xs) ++
    		pwords "in record"
                UnexpectedWithPatterns ps -> fsep $
                  pwords "Unexpected with patterns" ++ (punctuate (text " |") $ map prettyA ps)
                WithClausePatternMismatch p q -> fsep $
                  pwords "With clause pattern" ++ [prettyA p] ++
                  pwords "is not an instance of its parent pattern" -- TODO: pretty for internal patterns
    	    MetaCannotDependOn m ps i -> fsep $
    		    pwords "The metavariable" ++ [prettyTCM $ MetaV m []] ++ pwords "cannot depend on" ++ [pvar i] ++
    		    pwords "because it" ++ deps
    		where
    		    pvar i = prettyTCM $ I.Var i []
    		    deps = case map pvar ps of
    			[]  -> pwords "does not depend on any variables"
    			[x] -> pwords "only depends on the variable" ++ [x]
    			xs  -> pwords "only depends on the variables" ++ punctuate comma xs

    	    MetaOccursInItself m -> fsep $
    		pwords "Cannot construct infinite solution of metavariable" ++ [prettyTCM $ MetaV m []]
                BuiltinMustBeConstructor s e -> fsep $
                    [prettyA e] ++ pwords "must be a constructor in the binding to builtin" ++ [text s]
    	    NoSuchBuiltinName s -> fsep $
    		pwords "There is no built-in thing called" ++ [text s]
    	    DuplicateBuiltinBinding b x y -> fsep $
    		pwords "Duplicate binding for built-in thing" ++ [text b <> comma] ++
    		pwords "previous binding to" ++ [prettyTCM x]
    	    NoBindingForBuiltin x -> fsep $
    		pwords "No binding for builtin thing" ++ [text x <> comma] ++
    		pwords ("use {-# BUILTIN " ++ x ++ " name #-} to bind it to 'name'")
    	    NoSuchPrimitiveFunction x -> fsep $
    		pwords "There is no primitive function called" ++ [text x]
    	    BuiltinInParameterisedModule x -> fwords $
    		"The BUILTIN pragma cannot appear inside a bound context " ++
    		"(for instance, in a parameterised module or as a local declaration)"
    	    NoRHSRequiresAbsurdPattern ps -> fwords $
    		"The right-hand side can only be omitted if there " ++
    		"is an absurd pattern, () or {}, in the left-hand side."
    	    AbsurdPatternRequiresNoRHS ps -> fwords $
    		"The right-hand side must be omitted if there " ++
    		"is an absurd pattern, () or {}, in the left-hand side."
    	    LocalVsImportedModuleClash m -> fsep $
    		pwords "The module" ++ [text $ show m] ++
    		pwords "can refer to either a local module or an imported module"
    	    UnsolvedMetas rs ->
    		fsep ( pwords "Unsolved metas at the following locations:" )
    		$$ nest 2 (vcat $ map (text . show) rs)
    	    UnsolvedConstraints cs ->
    		fsep ( pwords "Failed to solve the following constraints:" )
    		$$ nest 2 (vcat $ map prettyTCM cs)
    	    CyclicModuleDependency ms ->
    		fsep (pwords "cyclic module dependency:")
    		$$ nest 2 (vcat $ map pretty ms)
    	    FileNotFound x files ->
    		fsep ( pwords "Failed to find source of module" ++ [pretty x] ++
    		       pwords "in any of the following locations:"
    		     ) $$ nest 2 (vcat $ map (text . filePath) files)
                OverlappingProjects f m1 m2 ->
    	        fsep ( pwords "The file" ++ [text (filePath f)] ++
                           pwords "can be accessed via several project roots. Both" ++
                           [pretty m1] ++ pwords "and" ++ [pretty m2] ++
                           pwords "point to this file."
                         )
    	    AmbiguousTopLevelModuleName x files ->
    		fsep ( pwords "Ambiguous module name. The module name" ++
                           [pretty x] ++
    		       pwords "could refer to any of the following files:"
    		     ) $$ nest 2 (vcat $ map (text . filePath) files)
    	    ClashingFileNamesFor x files ->
    		fsep ( pwords "Multiple possible sources for module" ++ [text $ show x] ++
    		       pwords "found:"
    		     ) $$ nest 2 (vcat $ map (text . filePath) files)
                ModuleDefinedInOtherFile mod file file' -> fsep $
                  pwords "You tried to load" ++ [text (filePath file)] ++
                  pwords "which defines the module" ++ [pretty mod <> text "."] ++
                  pwords "However, according to the include path this module should" ++
                  pwords "be defined in" ++ [text (filePath file') <> text "."]
    	    ModuleNameDoesntMatchFileName given files ->
                  fsep (pwords "The name of the top level module does not match the file name. The module" ++
                       [ pretty given ] ++ pwords "should be defined in one of the following files:")
    	      $$ nest 2 (vcat $ map (text . filePath) files)
                BothWithAndRHS -> fsep $
                  pwords "Unexpected right hand side"
    	    NotInScope xs ->
    		fsep (pwords "Not in scope:") $$ nest 2 (vcat $ map name xs)
    		where
                      name x = fsep [ pretty x, text "at" <+> text (show $ getRange x), suggestion (show x) ]
                      suggestion s
                        | elem ':' s    = parens $ text "did you forget space around the ':'?"
                        | elem "->" two = parens $ text "did you forget space around the '->'?"
                        | otherwise     = empty
                        where
                          two = zipWith (\a b -> [a,b]) s (tail s)
    	    NoSuchModule x -> fsep $
    		pwords "No such module" ++ [pretty x]
    	    AmbiguousName x ys -> vcat
    	      [ fsep $ pwords "Ambiguous name" ++ [pretty x <> text "."] ++
    		       pwords "It could refer to any one of"
    	      , nest 2 $ vcat $ map nameWithBinding ys
    	      ]
    	    AmbiguousModule x ys -> vcat
    	      [ fsep $ pwords "Ambiguous module name" ++ [pretty x <> text "."] ++
    		       pwords "It could refer to any one of"
    	      , nest 2 $ vcat $ map prettyTCM ys
    	      ]
    	    UninstantiatedModule x -> fsep (
    		    pwords "Cannot access the contents of the parameterised module" ++ [pretty x <> text "."] ++
    		    pwords "To do this the module first has to be instantiated. For instance:"
    		) $$ nest 2 (hsep [ text "module", pretty x <> text "'", text "=", pretty x, text "e1 .. en" ])
    	    ClashingDefinition x y -> fsep $
    		pwords "Multiple definitions of" ++ [pretty x <> text "."] ++
    		pwords "Previous definition at" ++ [text $ show $ nameBindingSite $ qnameName y]
    	    ClashingModule m1 m2 -> fsep $
    		pwords "The modules" ++ [prettyTCM m1, text "and", prettyTCM m2] ++ pwords "clash."
    	    ClashingImport x y -> fsep $
    		pwords "Import clash between" ++ [pretty x, text "and", prettyTCM y]
    	    ClashingModuleImport x y -> fsep $
    		pwords "Module import clash between" ++ [pretty x, text "and", prettyTCM y]
    	    PatternShadowsConstructor x c -> fsep $
                    pwords "The pattern variable" ++ [prettyTCM x] ++
                    pwords "has the same name as the constructor" ++ [prettyTCM c]
    	    ModuleDoesntExport m xs -> fsep $
    		pwords "The module" ++ [pretty m] ++ pwords "doesn't export the following:" ++
    		punctuate comma (map pretty xs)
    	    NotAModuleExpr e -> fsep $
    		pwords "The right-hand side of a module definition must have the form 'M e1 .. en'" ++
    		pwords "where M is a module name. The expression" ++ [pretty e, text "doesn't."]
                FieldOutsideRecord -> fsep $
                  pwords "Field appearing outside record declaration."
                InvalidPattern p -> fsep $
                  pretty p : pwords "is not a valid pattern"
    	    RepeatedVariablesInPattern xs -> fsep $
    	      pwords "Repeated variables in left hand side:" ++ map pretty xs
    	    NotAnExpression e -> fsep $
    		[pretty e] ++ pwords "is not a valid expression."
    	    NotAValidLetBinding nd -> fwords $
    		"Not a valid let-declaration"
    	    NothingAppliedToHiddenArg e	-> fsep $
    		[pretty e] ++ pwords "cannot appear by itself. It needs to be the argument to" ++
    		pwords "a function expecting an implicit argument."
    	    NoParseForApplication es -> fsep $
    		pwords "Could not parse the application" ++ [pretty $ C.RawApp noRange es]
    	    AmbiguousParseForApplication es es' -> fsep (
    		    pwords "Don't know how to parse" ++ [pretty (C.RawApp noRange es) <> text "."] ++
    		    pwords "Could mean any one of:"
    		) $$ nest 2 (vcat $ map pretty es')
    	    NoParseForLHS p -> fsep $
    		pwords "Could not parse the left-hand side" ++ [pretty p]
    	    AmbiguousParseForLHS p ps -> fsep (
    		    pwords "Don't know how to parse" ++ [pretty p <> text "."] ++
    		    pwords "Could mean any one of:"
    		) $$ nest 2 (vcat $ map pretty ps)
    	    IncompletePatternMatching v args -> fsep $
    		pwords "Incomplete pattern matching for" ++ [prettyTCM v <> text "."] ++
    		pwords "No match for" ++ map prettyTCM args
                UnreachableClauses f pss -> fsep $
                    pwords "Unreachable" ++ pwords (plural (length pss) "clause")
                    where
                      plural 1 thing = thing
                      plural n thing = thing ++ "s"
                CoverageFailure f pss -> fsep (
                    pwords "Incomplete pattern matching for" ++ [prettyTCM f <> text "."] ++
                    pwords "Missing cases:") $$ nest 2 (vcat $ map display pss)
                    where
                      display ps = do
                        ps <- nicify f ps
                        prettyTCM f <+> fsep (map showArg ps)

                      nicify f ps = do
                        showImp <- showImplicitArguments
                        if showImp
                          then return ps
                          else return ps  -- TODO: remove implicit arguments which aren't constructors

                CoverageCantSplitOn c -> fsep $
                  pwords "Cannot split on the constructor" ++ [prettyTCM c]

                CoverageCantSplitType a -> fsep $
                  pwords "Cannot split on argument of non-datatype" ++ [prettyTCM a]

    	    NotStrictlyPositive d ocs -> fsep $
    		pwords "The datatype" ++ [prettyTCM d] ++ pwords "is not strictly positive, because"
    		++ prettyOcc "it" ocs
    		where
    		    prettyOcc _ [] = []
    		    prettyOcc it (OccCon d c r : ocs) = concat
    			[ pwords it, pwords "occurs", prettyR r
    			, pwords "in the constructor", [prettyTCM c], pwords "of"
    			, [prettyTCM d <> com ocs], prettyOcc "which" ocs
    			]
    		    prettyOcc it (OccClause f n r : ocs) = concat
    			[ pwords it, pwords "occurs", prettyR r
    			, pwords "in the", [th n], pwords "clause of"
    			, [prettyTCM f <> com ocs], prettyOcc "which" ocs
    			]
    		    prettyR NonPositively = pwords "negatively"
    		    prettyR (ArgumentTo i q) =
    			pwords "as the" ++ [th i] ++
    			pwords "argument to" ++ [prettyTCM q]
    		    th 0 = text "first"
    		    th 1 = text "second"
    		    th 2 = text "third"
    		    th n = text (show $ n - 1) <> text "th"

    		    com []    = empty
    		    com (_:_) = comma

              where
                mpar n args
                  | n > 0 && not (null args) = parens
                  | otherwise                = id

                showArg (Arg Hidden x)    = braces $ showPat 0 x
                showArg (Arg NotHidden x) = showPat 1 x

                showPat _ (I.VarP _)      = text "_"
                showPat _ (I.DotP _)      = text "._"
                showPat n (I.ConP c args) = mpar n args $ prettyTCM c <+> fsep (map showArg args)
                showPat _ (I.LitP l)      = text (show l)

    instance PrettyTCM Call where
        prettyTCM c = case c of
    	CheckClause t cl _  -> fsep $
    	    pwords "when checking that the clause"
    	    ++ [P.prettyA cl] ++ pwords "has type" ++ [prettyTCM t]
    	CheckPattern p tel t _ -> addCtxTel tel $ fsep $
    	    pwords "when checking that the pattern"
    	    ++ [prettyA p] ++ pwords "has type" ++ [prettyTCM t]
    	CheckLetBinding b _ -> fsep $
    	    pwords "when checking the let binding" ++ [P.prettyA b]
    	InferExpr e _ -> fsep $
    	    pwords "when inferring the type of" ++ [prettyA e]
    	CheckExpr e t _ -> fsep $
    	    pwords "when checking that the expression"
    	    ++ [prettyA e] ++ pwords "has type" ++ [prettyTCM t]
    	IsTypeCall e s _ -> fsep $
    	    pwords "when checking that the expression"
    	    ++ [prettyA e] ++ pwords "is a type of sort" ++ [prettyTCM s]
    	IsType_ e _ -> fsep $
    	    pwords "when checking that the expression"
    	    ++ [prettyA e] ++ pwords "is a type"
    	CheckArguments r es t0 t1 _ -> fsep $
    	    pwords "when checking that" ++
    	    map hPretty es ++ pwords "are valid arguments to a function of type" ++ [prettyTCM t0]
    	CheckRecDef _ x ps cs _ ->
    	    fsep $ pwords "when checking the definition of" ++ [prettyTCM x]
    	CheckDataDef _ x ps cs _ ->
    	    fsep $ pwords "when checking the definition of" ++ [prettyTCM x]
    	CheckConstructor d _ _ (A.Axiom _ c _) _ -> fsep $
    	    pwords "when checking the constructor" ++ [prettyTCM c] ++
    	    pwords "in the declaration of" ++ [prettyTCM d]
    	CheckConstructor _ _ _ _ _ -> __IMPOSSIBLE__
    	CheckFunDef _ f _ _ ->
    	    fsep $ pwords "when checking the definition of" ++ [prettyTCM f]
    	CheckPragma _ p _ ->
    	    fsep $ pwords "when checking the pragma" ++ [prettyA $ RangeAndPragma noRange p]
    	CheckPrimitive _ x e _ -> fsep $
    	    pwords "when checking that the type of the primitive function" ++
    	    [prettyTCM x] ++ pwords "is" ++ [prettyA e]
            CheckDotPattern e v _ -> fsep $
                pwords "when checking that the given dot pattern" ++ [prettyA e] ++
                pwords "matches the inferred value" ++ [prettyTCM v]
            CheckPatternShadowing c _ -> fsep $
                pwords "when checking the clause" ++ [P.prettyA c]
    	InferVar x _ ->
    	    fsep $ pwords "when inferring the type of" ++ [prettyTCM x]
    	InferDef _ x _ ->
    	    fsep $ pwords "when inferring the type of" ++ [prettyTCM x]
    	ScopeCheckExpr e _ ->
    	    fsep $ pwords "when scope checking" ++ [pretty e]
    	ScopeCheckDeclaration d _ ->
    	    fwords "when scope checking the declaration" $$
    	    nest 2 (pretty $ simpleDecl d)
    	ScopeCheckDefinition d _ ->
    	    fwords "when scope checking the definition" $$
    	    nest 2 (vcat $ map pretty $ simpleDef d)
    	ScopeCheckLHS x p _ ->
    	    fsep $ pwords "when scope checking the left-hand side" ++ [pretty p] ++
    		   pwords "in the definition of" ++ [pretty x]
    	TermFunDef _ f _ _ ->
    	    fsep $ pwords "when termination checking the definition of" ++ [prettyTCM f]
    	SetRange r _ ->
    	    fsep $ pwords "when doing something at" ++ [text $ show r]
            CheckSectionApplication _ m1 ptel m2 args _ -> fsep $
              pwords "when checking the module application" ++
              [prettyA $ A.Apply info m1 ptel m2 args Map.empty Map.empty]
              where
                info = A.ModuleInfo noRange noRange Nothing

    	where
    	    hPretty a@(Arg h _) = pretty =<< abstractToConcreteCtx (hiddenArgumentCtx h) a

    	    simpleDef d = case d of
    	      D.FunDef _ ds _ _ _ _ _	 -> ds
    	      D.DataDef r ind fx p a d bs cs ->
    		[ C.Data r ind d (map bind bs) (C.Underscore noRange Nothing)
    		    $ map simpleDecl cs
    		]
    	      D.RecDef r fx p a d c bs cs ->
    		[ C.Record r d (name <$> c) (map bind bs) (C.Underscore noRange Nothing)
    		    $ map simpleDecl cs
    		]
    	      where
    		bind :: C.LamBinding -> C.TypedBindings
    		bind (C.DomainFull b) = b
    		bind (C.DomainFree h x) = C.TypedBindings r h [C.TBind r [x] (C.Underscore r Nothing)]
    		  where r = getRange x

                    name (D.Axiom _ _ _ _ n _) = n
                    name _                     = __IMPOSSIBLE__

    	    simpleDecl d = case d of
    		D.Axiom _ _ _ _ x e		       -> C.TypeSig x e
    		D.NiceField _ _ _ _ h x e	       -> C.Field h x e
    		D.PrimitiveFunction r _ _ _ x e	       -> C.Primitive r [C.TypeSig x e]
    		D.NiceDef r ds _ _		       -> C.Mutual r ds
    		D.NiceModule r _ _ x tel _	       -> C.Module r x tel []
    		D.NiceModuleMacro r _ _ x tel e op dir -> C.ModuleMacro r x tel e op dir
    		D.NiceOpen r x dir		       -> C.Open r x dir
    		D.NiceImport r x as op dir	       -> C.Import r x as op dir
    		D.NicePragma _ p		       -> C.Pragma p

    interestingCall :: Closure Call -> Maybe (Closure Call)
    interestingCall cl = case clValue cl of
        InferVar _ _	      -> Nothing
        InferDef _ _ _	      -> Nothing
        CheckArguments _ [] _ _ _ -> Nothing
        SetRange _ _	      -> Nothing
        _			      -> Just cl