    module Agda.TypeChecking.Pretty.Call where

    import Prelude hiding ( null )

    import Agda.Syntax.Abstract as A
    import Agda.Syntax.Abstract.Views
    import Agda.Syntax.Common
    import Agda.Syntax.Fixity
    import qualified Agda.Syntax.Concrete.Definitions as D
    import qualified Agda.Syntax.Info as A
    import Agda.Syntax.Position
    import Agda.Syntax.Scope.Monad
    import Agda.Syntax.Translation.AbstractToConcrete

    import Agda.TypeChecking.Monad.Base
    import Agda.TypeChecking.Monad.Context
    import Agda.TypeChecking.Monad.Debug
    import Agda.TypeChecking.Pretty

    import Agda.Utils.Function
    import Agda.Utils.Null
    import qualified Agda.Utils.Pretty as P

    import Agda.Utils.Impossible

    sayWhere :: MonadPretty m => HasRange a => a -> m Doc -> m Doc
    sayWhere :: forall (m :: * -> *) a.
    (MonadPretty m, HasRange a) =>
    a -> m Doc -> m Doc
    sayWhere a
    x m Doc
    d = Bool -> (m Doc -> m Doc) -> m Doc -> m Doc
    forall a. Bool -> (a -> a) -> a -> a
    applyUnless (Range -> Bool
    forall a. Null a => a -> Bool
    null Range
    r) (Range -> m Doc
    forall a (m :: * -> *). (PrettyTCM a, MonadPretty m) => a -> m Doc
    prettyTCM Range
    r m Doc -> m Doc -> m Doc
    forall (m :: * -> *). Applicative m => m Doc -> m Doc -> m Doc
    $$) m Doc
    d
      where r :: Range
    r = a -> Range
    forall a. HasRange a => a -> Range
    getRange a
    x

    sayWhen :: MonadPretty m => Range -> Maybe (Closure Call) -> m Doc -> m Doc
    sayWhen :: forall (m :: * -> *).
    MonadPretty m =>
    Range -> Maybe (Closure Call) -> m Doc -> m Doc
    sayWhen Range
    r Maybe (Closure Call)
    Nothing   m Doc
    m = Range -> m Doc -> m Doc
    forall (m :: * -> *) a.
    (MonadPretty m, HasRange a) =>
    a -> m Doc -> m Doc
    sayWhere Range
    r m Doc
    m
    sayWhen Range
    r (Just Closure Call
    cl) m Doc
    m = Range -> m Doc -> m Doc
    forall (m :: * -> *) a.
    (MonadPretty m, HasRange a) =>
    a -> m Doc -> m Doc
    sayWhere Range
    r (m Doc
    m m Doc -> m Doc -> m Doc
    forall (m :: * -> *). Applicative m => m Doc -> m Doc -> m Doc
    $$ Closure Call -> m Doc
    forall a (m :: * -> *). (PrettyTCM a, MonadPretty m) => a -> m Doc
    prettyTCM Closure Call
    cl)

    instance PrettyTCM CallInfo where
      prettyTCM :: forall (m :: * -> *). MonadPretty m => CallInfo -> m Doc
    prettyTCM CallInfo
    c = do
        let call :: m Doc
    call = Closure Term -> m Doc
    forall a (m :: * -> *). (PrettyTCM a, MonadPretty m) => a -> m Doc
    prettyTCM (Closure Term -> m Doc) -> Closure Term -> m Doc
    forall a b. (a -> b) -> a -> b
    $ CallInfo -> Closure Term
    callInfoCall CallInfo
    c
            r :: Range
    r    = CallInfo -> Range
    callInfoRange CallInfo
    c
        if Doc -> Bool
    forall a. Null a => a -> Bool
    null (Doc -> Bool) -> Doc -> Bool
    forall a b. (a -> b) -> a -> b
    $ Range -> Doc
    forall a. Pretty a => a -> Doc
    P.pretty Range
    r
          then m Doc
    call
          else m Doc
    call m Doc -> m Doc -> m Doc
    forall (m :: * -> *). Applicative m => m Doc -> m Doc -> m Doc
    $$ Int -> m Doc -> m Doc
    forall (m :: * -> *). Functor m => Int -> m Doc -> m Doc
    nest Int
    2 (m Doc
    "(at" m Doc -> m Doc -> m Doc
    forall (m :: * -> *). Applicative m => m Doc -> m Doc -> m Doc
    <+> Range -> m Doc
    forall a (m :: * -> *). (PrettyTCM a, MonadPretty m) => a -> m Doc
    prettyTCM Range
    r) m Doc -> m Doc -> m Doc
    forall a. Semigroup a => a -> a -> a
    <> m Doc
    ")"

    instance PrettyTCM Call where
      prettyTCM :: forall (m :: * -> *). MonadPretty m => Call -> m Doc
    prettyTCM = Precedence -> m Doc -> m Doc
    forall (m :: * -> *) a. ReadTCState m => Precedence -> m a -> m a
    withContextPrecedence Precedence
    TopCtx (m Doc -> m Doc) -> (Call -> m Doc) -> Call -> m Doc
    forall b c a. (b -> c) -> (a -> b) -> a -> c
    . \case

        CheckClause Type
    t SpineClause
    cl -> do

          [Char] -> Int -> m () -> m ()
    forall (m :: * -> *). MonadDebug m => [Char] -> Int -> m () -> m ()
    verboseS  [Char]
    "error.checkclause" Int
    40 (m () -> m ()) -> m () -> m ()
    forall a b. (a -> b) -> a -> b
    $ do
            [Char] -> Int -> [Char] -> m ()
    forall (m :: * -> *).
    MonadDebug m =>
    [Char] -> Int -> [Char] -> m ()
    reportSLn [Char]
    "error.checkclause" Int
    60 ([Char] -> m ()) -> [Char] -> m ()
    forall a b. (a -> b) -> a -> b
    $ [Char]
    "prettyTCM CheckClause: cl = " [Char] -> [Char] -> [Char]
    forall a. [a] -> [a] -> [a]
    ++ SpineClause -> [Char]
    forall a. Show a => a -> [Char]
    show (SpineClause -> SpineClause
    forall a. ExprLike a => a -> a
    deepUnscope SpineClause
    cl)
            [Declaration]
    clc <- SpineClause -> m (ConOfAbs SpineClause)
    forall a (m :: * -> *).
    (ToConcrete a, MonadAbsToCon m) =>
    a -> m (ConOfAbs a)
    abstractToConcrete_ SpineClause
    cl
            [Char] -> Int -> [Char] -> m ()
    forall (m :: * -> *).
    MonadDebug m =>
    [Char] -> Int -> [Char] -> m ()
    reportSLn [Char]
    "error.checkclause" Int
    40 ([Char] -> m ()) -> [Char] -> m ()
    forall a b. (a -> b) -> a -> b
    $ [Char]
    "cl (Concrete) = " [Char] -> [Char] -> [Char]
    forall a. [a] -> [a] -> [a]
    ++ [Declaration] -> [Char]
    forall a. Show a => a -> [Char]
    show [Declaration]
    clc

          [m Doc] -> m Doc
    forall (m :: * -> *) (t :: * -> *).
    (Applicative m, Foldable t) =>
    t (m Doc) -> m Doc
    fsep ([m Doc] -> m Doc) -> [m Doc] -> m Doc
    forall a b. (a -> b) -> a -> b
    $
            [Char] -> [m Doc]
    forall (m :: * -> *). Applicative m => [Char] -> [m Doc]
    pwords [Char]
    "when checking that the clause"
            [m Doc] -> [m Doc] -> [m Doc]
    forall a. [a] -> [a] -> [a]
    ++ [SpineClause -> m Doc
    forall a (m :: * -> *).
    (ToConcrete a, Pretty (ConOfAbs a), MonadAbsToCon m) =>
    a -> m Doc
    prettyA SpineClause
    cl] [m Doc] -> [m Doc] -> [m Doc]
    forall a. [a] -> [a] -> [a]
    ++ [Char] -> [m Doc]
    forall (m :: * -> *). Applicative m => [Char] -> [m Doc]
    pwords [Char]
    "has type" [m Doc] -> [m Doc] -> [m Doc]
    forall a. [a] -> [a] -> [a]
    ++ [Type -> m Doc
    forall a (m :: * -> *). (PrettyTCM a, MonadPretty m) => a -> m Doc
    prettyTCM Type
    t]

        CheckLHS SpineLHS
    lhs -> [m Doc] -> m Doc
    forall (m :: * -> *) (t :: * -> *).
    (Applicative m, Foldable t) =>
    t (m Doc) -> m Doc
    vcat ([m Doc] -> m Doc) -> [m Doc] -> m Doc
    forall a b. (a -> b) -> a -> b
    $
          [ [m Doc] -> m Doc
    forall (m :: * -> *) (t :: * -> *).
    (Applicative m, Foldable t) =>
    t (m Doc) -> m Doc
    fsep ([m Doc] -> m Doc) -> [m Doc] -> m Doc
    forall a b. (a -> b) -> a -> b
    $ [Char] -> [m Doc]
    forall (m :: * -> *). Applicative m => [Char] -> [m Doc]
    pwords [Char]
    "when checking the clause left hand side"
          , SpineLHS -> m Doc
    forall a (m :: * -> *).
    (ToConcrete a, Pretty (ConOfAbs a), MonadAbsToCon m) =>
    a -> m Doc
    prettyA (SpineLHS -> m Doc) -> SpineLHS -> m Doc
    forall a b. (a -> b) -> a -> b
    $ SpineLHS
    lhs { spLhsInfo :: LHSInfo
    A.spLhsInfo = (SpineLHS -> LHSInfo
    A.spLhsInfo SpineLHS
    lhs) { lhsEllipsis :: ExpandedEllipsis
    A.lhsEllipsis = ExpandedEllipsis
    NoEllipsis } }
          ]

        CheckPattern Pattern
    p Telescope
    tel Type
    t -> Telescope -> m Doc -> m Doc
    forall b (m :: * -> *) a.
    (AddContext b, MonadAddContext m) =>
    b -> m a -> m a
    addContext Telescope
    tel (m Doc -> m Doc) -> m Doc -> m Doc
    forall a b. (a -> b) -> a -> b
    $ [m Doc] -> m Doc
    forall (m :: * -> *) (t :: * -> *).
    (Applicative m, Foldable t) =>
    t (m Doc) -> m Doc
    fsep ([m Doc] -> m Doc) -> [m Doc] -> m Doc
    forall a b. (a -> b) -> a -> b
    $
          [Char] -> [m Doc]
    forall (m :: * -> *). Applicative m => [Char] -> [m Doc]
    pwords [Char]
    "when checking that the pattern"
          [m Doc] -> [m Doc] -> [m Doc]
    forall a. [a] -> [a] -> [a]
    ++ [Pattern -> m Doc
    forall a (m :: * -> *).
    (ToConcrete a, Pretty (ConOfAbs a), MonadAbsToCon m) =>
    a -> m Doc
    prettyA Pattern
    p] [m Doc] -> [m Doc] -> [m Doc]
    forall a. [a] -> [a] -> [a]
    ++ [Char] -> [m Doc]
    forall (m :: * -> *). Applicative m => [Char] -> [m Doc]
    pwords [Char]
    "has type" [m Doc] -> [m Doc] -> [m Doc]
    forall a. [a] -> [a] -> [a]
    ++ [Type -> m Doc
    forall a (m :: * -> *). (PrettyTCM a, MonadPretty m) => a -> m Doc
    prettyTCM Type
    t]

        CheckPatternLinearityType Name
    x -> [m Doc] -> m Doc
    forall (m :: * -> *) (t :: * -> *).
    (Applicative m, Foldable t) =>
    t (m Doc) -> m Doc
    fsep ([m Doc] -> m Doc) -> [m Doc] -> m Doc
    forall a b. (a -> b) -> a -> b
    $
          [Char] -> [m Doc]
    forall (m :: * -> *). Applicative m => [Char] -> [m Doc]
    pwords [Char]
    "when checking that all occurrences of pattern variable"
          [m Doc] -> [m Doc] -> [m Doc]
    forall a. [a] -> [a] -> [a]
    ++ [Name -> m Doc
    forall (m :: * -> *) a. (Applicative m, Pretty a) => a -> m Doc
    pretty Name
    x] [m Doc] -> [m Doc] -> [m Doc]
    forall a. [a] -> [a] -> [a]
    ++ [Char] -> [m Doc]
    forall (m :: * -> *). Applicative m => [Char] -> [m Doc]
    pwords [Char]
    "have the same type"

        CheckPatternLinearityValue Name
    x -> [m Doc] -> m Doc
    forall (m :: * -> *) (t :: * -> *).
    (Applicative m, Foldable t) =>
    t (m Doc) -> m Doc
    fsep ([m Doc] -> m Doc) -> [m Doc] -> m Doc
    forall a b. (a -> b) -> a -> b
    $
          [Char] -> [m Doc]
    forall (m :: * -> *). Applicative m => [Char] -> [m Doc]
    pwords [Char]
    "when checking that all occurrences of pattern variable"
          [m Doc] -> [m Doc] -> [m Doc]
    forall a. [a] -> [a] -> [a]
    ++ [Name -> m Doc
    forall (m :: * -> *) a. (Applicative m, Pretty a) => a -> m Doc
    pretty Name
    x] [m Doc] -> [m Doc] -> [m Doc]
    forall a. [a] -> [a] -> [a]
    ++ [Char] -> [m Doc]
    forall (m :: * -> *). Applicative m => [Char] -> [m Doc]
    pwords [Char]
    "have the same value"

        CheckLetBinding LetBinding
    b -> [m Doc] -> m Doc
    forall (m :: * -> *) (t :: * -> *).
    (Applicative m, Foldable t) =>
    t (m Doc) -> m Doc
    fsep ([m Doc] -> m Doc) -> [m Doc] -> m Doc
    forall a b. (a -> b) -> a -> b
    $
          [Char] -> [m Doc]
    forall (m :: * -> *). Applicative m => [Char] -> [m Doc]
    pwords [Char]
    "when checking the let binding" [m Doc] -> [m Doc] -> [m Doc]
    forall a. [a] -> [a] -> [a]
    ++ [LetBinding -> m Doc
    forall a (m :: * -> *).
    (ToConcrete a, Pretty (ConOfAbs a), MonadAbsToCon m) =>
    a -> m Doc
    prettyA LetBinding
    b]

        InferExpr Expr
    e -> [m Doc] -> m Doc
    forall (m :: * -> *) (t :: * -> *).
    (Applicative m, Foldable t) =>
    t (m Doc) -> m Doc
    fsep ([m Doc] -> m Doc) -> [m Doc] -> m Doc
    forall a b. (a -> b) -> a -> b
    $ [Char] -> [m Doc]
    forall (m :: * -> *). Applicative m => [Char] -> [m Doc]
    pwords [Char]
    "when inferring the type of" [m Doc] -> [m Doc] -> [m Doc]
    forall a. [a] -> [a] -> [a]
    ++ [Expr -> m Doc
    forall a (m :: * -> *).
    (ToConcrete a, Pretty (ConOfAbs a), MonadAbsToCon m) =>
    a -> m Doc
    prettyA Expr
    e]

        CheckExprCall Comparison
    cmp Expr
    e Type
    t -> [m Doc] -> m Doc
    forall (m :: * -> *) (t :: * -> *).
    (Applicative m, Foldable t) =>
    t (m Doc) -> m Doc
    fsep ([m Doc] -> m Doc) -> [m Doc] -> m Doc
    forall a b. (a -> b) -> a -> b
    $
          [Char] -> [m Doc]
    forall (m :: * -> *). Applicative m => [Char] -> [m Doc]
    pwords [Char]
    "when checking that the expression"
          [m Doc] -> [m Doc] -> [m Doc]
    forall a. [a] -> [a] -> [a]
    ++ [Expr -> m Doc
    forall a (m :: * -> *).
    (ToConcrete a, Pretty (ConOfAbs a), MonadAbsToCon m) =>
    a -> m Doc
    prettyA Expr
    e] [m Doc] -> [m Doc] -> [m Doc]
    forall a. [a] -> [a] -> [a]
    ++ [Char] -> [m Doc]
    forall (m :: * -> *). Applicative m => [Char] -> [m Doc]
    pwords [Char]
    "has type" [m Doc] -> [m Doc] -> [m Doc]
    forall a. [a] -> [a] -> [a]
    ++ [Type -> m Doc
    forall a (m :: * -> *). (PrettyTCM a, MonadPretty m) => a -> m Doc
    prettyTCM Type
    t]

        IsTypeCall Comparison
    cmp Expr
    e Sort
    s -> [m Doc] -> m Doc
    forall (m :: * -> *) (t :: * -> *).
    (Applicative m, Foldable t) =>
    t (m Doc) -> m Doc
    fsep ([m Doc] -> m Doc) -> [m Doc] -> m Doc
    forall a b. (a -> b) -> a -> b
    $
          [Char] -> [m Doc]
    forall (m :: * -> *). Applicative m => [Char] -> [m Doc]
    pwords [Char]
    "when checking that the expression"
          [m Doc] -> [m Doc] -> [m Doc]
    forall a. [a] -> [a] -> [a]
    ++ [Expr -> m Doc
    forall a (m :: * -> *).
    (ToConcrete a, Pretty (ConOfAbs a), MonadAbsToCon m) =>
    a -> m Doc
    prettyA Expr
    e] [m Doc] -> [m Doc] -> [m Doc]
    forall a. [a] -> [a] -> [a]
    ++ [Char] -> [m Doc]
    forall (m :: * -> *). Applicative m => [Char] -> [m Doc]
    pwords [Char]
    "is a type of sort" [m Doc] -> [m Doc] -> [m Doc]
    forall a. [a] -> [a] -> [a]
    ++ [Sort -> m Doc
    forall a (m :: * -> *). (PrettyTCM a, MonadPretty m) => a -> m Doc
    prettyTCM Sort
    s]

        IsType_ Expr
    e -> [m Doc] -> m Doc
    forall (m :: * -> *) (t :: * -> *).
    (Applicative m, Foldable t) =>
    t (m Doc) -> m Doc
    fsep ([m Doc] -> m Doc) -> [m Doc] -> m Doc
    forall a b. (a -> b) -> a -> b
    $
          [Char] -> [m Doc]
    forall (m :: * -> *). Applicative m => [Char] -> [m Doc]
    pwords [Char]
    "when checking that the expression"
          [m Doc] -> [m Doc] -> [m Doc]
    forall a. [a] -> [a] -> [a]
    ++ [Expr -> m Doc
    forall a (m :: * -> *).
    (ToConcrete a, Pretty (ConOfAbs a), MonadAbsToCon m) =>
    a -> m Doc
    prettyA Expr
    e] [m Doc] -> [m Doc] -> [m Doc]
    forall a. [a] -> [a] -> [a]
    ++ [Char] -> [m Doc]
    forall (m :: * -> *). Applicative m => [Char] -> [m Doc]
    pwords [Char]
    "is a type"

        CheckProjection Range
    _ QName
    x Type
    t -> [m Doc] -> m Doc
    forall (m :: * -> *) (t :: * -> *).
    (Applicative m, Foldable t) =>
    t (m Doc) -> m Doc
    fsep ([m Doc] -> m Doc) -> [m Doc] -> m Doc
    forall a b. (a -> b) -> a -> b
    $
          [Char] -> [m Doc]
    forall (m :: * -> *). Applicative m => [Char] -> [m Doc]
    pwords [Char]
    "when checking the projection" [m Doc] -> [m Doc] -> [m Doc]
    forall a. [a] -> [a] -> [a]
    ++
          [ [m Doc] -> m Doc
    forall (m :: * -> *) (t :: * -> *).
    (Applicative m, Foldable t) =>
    t (m Doc) -> m Doc
    sep [ QName -> m Doc
    forall a (m :: * -> *). (PrettyTCM a, MonadPretty m) => a -> m Doc
    prettyTCM QName
    x m Doc -> m Doc -> m Doc
    forall (m :: * -> *). Applicative m => m Doc -> m Doc -> m Doc
    <+> m Doc
    ":"
                , Int -> m Doc -> m Doc
    forall (m :: * -> *). Functor m => Int -> m Doc -> m Doc
    nest Int
    2 (m Doc -> m Doc) -> m Doc -> m Doc
    forall a b. (a -> b) -> a -> b
    $ Type -> m Doc
    forall a (m :: * -> *). (PrettyTCM a, MonadPretty m) => a -> m Doc
    prettyTCM Type
    t ] ]

        CheckArguments Range
    r [NamedArg Expr]
    es Type
    t0 Maybe Type
    t1 -> [m Doc] -> m Doc
    forall (m :: * -> *) (t :: * -> *).
    (Applicative m, Foldable t) =>
    t (m Doc) -> m Doc
    fsep ([m Doc] -> m Doc) -> [m Doc] -> m Doc
    forall a b. (a -> b) -> a -> b
    $
          [Char] -> [m Doc]
    forall (m :: * -> *). Applicative m => [Char] -> [m Doc]
    pwords [Char]
    "when checking that" [m Doc] -> [m Doc] -> [m Doc]
    forall a. [a] -> [a] -> [a]
    ++
          (NamedArg Expr -> m Doc) -> [NamedArg Expr] -> [m Doc]
    forall a b. (a -> b) -> [a] -> [b]
    map NamedArg Expr -> m Doc
    forall (m :: * -> *). MonadPretty m => NamedArg Expr -> m Doc
    hPretty [NamedArg Expr]
    es [m Doc] -> [m Doc] -> [m Doc]
    forall a. [a] -> [a] -> [a]
    ++
          [Char] -> [m Doc]
    forall (m :: * -> *). Applicative m => [Char] -> [m Doc]
    pwords ([NamedArg Expr] -> [Char] -> [Char] -> [Char]
    forall a c. Sized a => a -> c -> c -> c
    P.singPlural [NamedArg Expr]
    es [Char]
    "is a valid argument" [Char]
    "are valid arguments") [m Doc] -> [m Doc] -> [m Doc]
    forall a. [a] -> [a] -> [a]
    ++
          [Char] -> [m Doc]
    forall (m :: * -> *). Applicative m => [Char] -> [m Doc]
    pwords [Char]
    "to a function of type" [m Doc] -> [m Doc] -> [m Doc]
    forall a. [a] -> [a] -> [a]
    ++
          [Type -> m Doc
    forall a (m :: * -> *). (PrettyTCM a, MonadPretty m) => a -> m Doc
    prettyTCM Type
    t0]

        CheckMetaSolution Range
    r MetaId
    m Type
    a Term
    v -> [m Doc] -> m Doc
    forall (m :: * -> *) (t :: * -> *).
    (Applicative m, Foldable t) =>
    t (m Doc) -> m Doc
    fsep ([m Doc] -> m Doc) -> [m Doc] -> m Doc
    forall a b. (a -> b) -> a -> b
    $
          [Char] -> [m Doc]
    forall (m :: * -> *). Applicative m => [Char] -> [m Doc]
    pwords [Char]
    "when checking that the solution" [m Doc] -> [m Doc] -> [m Doc]
    forall a. [a] -> [a] -> [a]
    ++ [Term -> m Doc
    forall a (m :: * -> *). (PrettyTCM a, MonadPretty m) => a -> m Doc
    prettyTCM Term
    v] [m Doc] -> [m Doc] -> [m Doc]
    forall a. [a] -> [a] -> [a]
    ++
          [Char] -> [m Doc]
    forall (m :: * -> *). Applicative m => [Char] -> [m Doc]
    pwords [Char]
    "of metavariable" [m Doc] -> [m Doc] -> [m Doc]
    forall a. [a] -> [a] -> [a]
    ++ [MetaId -> m Doc
    forall a (m :: * -> *). (PrettyTCM a, MonadPretty m) => a -> m Doc
    prettyTCM MetaId
    m] [m Doc] -> [m Doc] -> [m Doc]
    forall a. [a] -> [a] -> [a]
    ++
          [Char] -> [m Doc]
    forall (m :: * -> *). Applicative m => [Char] -> [m Doc]
    pwords [Char]
    "has the expected type" [m Doc] -> [m Doc] -> [m Doc]
    forall a. [a] -> [a] -> [a]
    ++ [Type -> m Doc
    forall a (m :: * -> *). (PrettyTCM a, MonadPretty m) => a -> m Doc
    prettyTCM Type
    a]

        CheckTargetType Range
    r Type
    infTy Type
    expTy -> [m Doc] -> m Doc
    forall (m :: * -> *) (t :: * -> *).
    (Applicative m, Foldable t) =>
    t (m Doc) -> m Doc
    sep
          [ m Doc
    "when checking that the inferred type of an application"
          , Int -> m Doc -> m Doc
    forall (m :: * -> *). Functor m => Int -> m Doc -> m Doc
    nest Int
    2 (m Doc -> m Doc) -> m Doc -> m Doc
    forall a b. (a -> b) -> a -> b
    $ Type -> m Doc
    forall a (m :: * -> *). (PrettyTCM a, MonadPretty m) => a -> m Doc
    prettyTCM Type
    infTy
          , m Doc
    "matches the expected type"
          , Int -> m Doc -> m Doc
    forall (m :: * -> *). Functor m => Int -> m Doc -> m Doc
    nest Int
    2 (m Doc -> m Doc) -> m Doc -> m Doc
    forall a b. (a -> b) -> a -> b
    $ Type -> m Doc
    forall a (m :: * -> *). (PrettyTCM a, MonadPretty m) => a -> m Doc
    prettyTCM Type
    expTy ]

        CheckRecDef Range
    _ QName
    x [LamBinding]
    ps [Declaration]
    cs ->
          [m Doc] -> m Doc
    forall (m :: * -> *) (t :: * -> *).
    (Applicative m, Foldable t) =>
    t (m Doc) -> m Doc
    fsep ([m Doc] -> m Doc) -> [m Doc] -> m Doc
    forall a b. (a -> b) -> a -> b
    $ [Char] -> [m Doc]
    forall (m :: * -> *). Applicative m => [Char] -> [m Doc]
    pwords [Char]
    "when checking the definition of" [m Doc] -> [m Doc] -> [m Doc]
    forall a. [a] -> [a] -> [a]
    ++ [QName -> m Doc
    forall a (m :: * -> *). (PrettyTCM a, MonadPretty m) => a -> m Doc
    prettyTCM QName
    x]

        CheckDataDef Range
    _ QName
    x [LamBinding]
    ps [Declaration]
    cs ->
          [m Doc] -> m Doc
    forall (m :: * -> *) (t :: * -> *).
    (Applicative m, Foldable t) =>
    t (m Doc) -> m Doc
    fsep ([m Doc] -> m Doc) -> [m Doc] -> m Doc
    forall a b. (a -> b) -> a -> b
    $ [Char] -> [m Doc]
    forall (m :: * -> *). Applicative m => [Char] -> [m Doc]
    pwords [Char]
    "when checking the definition of" [m Doc] -> [m Doc] -> [m Doc]
    forall a. [a] -> [a] -> [a]
    ++ [QName -> m Doc
    forall a (m :: * -> *). (PrettyTCM a, MonadPretty m) => a -> m Doc
    prettyTCM QName
    x]

        CheckConstructor QName
    d Telescope
    _ Sort
    _ (A.Axiom KindOfName
    _ DefInfo
    _ ArgInfo
    _ Maybe [Occurrence]
    _ QName
    c Expr
    _) -> [m Doc] -> m Doc
    forall (m :: * -> *) (t :: * -> *).
    (Applicative m, Foldable t) =>
    t (m Doc) -> m Doc
    fsep ([m Doc] -> m Doc) -> [m Doc] -> m Doc
    forall a b. (a -> b) -> a -> b
    $
          [Char] -> [m Doc]
    forall (m :: * -> *). Applicative m => [Char] -> [m Doc]
    pwords [Char]
    "when checking the constructor" [m Doc] -> [m Doc] -> [m Doc]
    forall a. [a] -> [a] -> [a]
    ++ [QName -> m Doc
    forall a (m :: * -> *). (PrettyTCM a, MonadPretty m) => a -> m Doc
    prettyTCM QName
    c] [m Doc] -> [m Doc] -> [m Doc]
    forall a. [a] -> [a] -> [a]
    ++
          [Char] -> [m Doc]
    forall (m :: * -> *). Applicative m => [Char] -> [m Doc]
    pwords [Char]
    "in the declaration of" [m Doc] -> [m Doc] -> [m Doc]
    forall a. [a] -> [a] -> [a]
    ++ [QName -> m Doc
    forall a (m :: * -> *). (PrettyTCM a, MonadPretty m) => a -> m Doc
    prettyTCM QName
    d]

        CheckConstructor{} -> m Doc
    forall a. HasCallStack => a
    __IMPOSSIBLE__

        CheckConstructorFitsIn QName
    c Type
    t Sort
    s -> [m Doc] -> m Doc
    forall (m :: * -> *) (t :: * -> *).
    (Applicative m, Foldable t) =>
    t (m Doc) -> m Doc
    fsep ([m Doc] -> m Doc) -> [m Doc] -> m Doc
    forall a b. (a -> b) -> a -> b
    $
          [Char] -> [m Doc]
    forall (m :: * -> *). Applicative m => [Char] -> [m Doc]
    pwords [Char]
    "when checking that the type" [m Doc] -> [m Doc] -> [m Doc]
    forall a. [a] -> [a] -> [a]
    ++ [Type -> m Doc
    forall a (m :: * -> *). (PrettyTCM a, MonadPretty m) => a -> m Doc
    prettyTCM Type
    t] [m Doc] -> [m Doc] -> [m Doc]
    forall a. [a] -> [a] -> [a]
    ++
          [Char] -> [m Doc]
    forall (m :: * -> *). Applicative m => [Char] -> [m Doc]
    pwords [Char]
    "of the constructor" [m Doc] -> [m Doc] -> [m Doc]
    forall a. [a] -> [a] -> [a]
    ++ [QName -> m Doc
    forall a (m :: * -> *). (PrettyTCM a, MonadPretty m) => a -> m Doc
    prettyTCM QName
    c] [m Doc] -> [m Doc] -> [m Doc]
    forall a. [a] -> [a] -> [a]
    ++
          [Char] -> [m Doc]
    forall (m :: * -> *). Applicative m => [Char] -> [m Doc]
    pwords [Char]
    "fits in the sort" [m Doc] -> [m Doc] -> [m Doc]
    forall a. [a] -> [a] -> [a]
    ++ [Sort -> m Doc
    forall a (m :: * -> *). (PrettyTCM a, MonadPretty m) => a -> m Doc
    prettyTCM Sort
    s] [m Doc] -> [m Doc] -> [m Doc]
    forall a. [a] -> [a] -> [a]
    ++
          [Char] -> [m Doc]
    forall (m :: * -> *). Applicative m => [Char] -> [m Doc]
    pwords [Char]
    "of the datatype."

        CheckFunDefCall Range
    _ QName
    f [Clause]
    _ Bool
    _ ->
          [m Doc] -> m Doc
    forall (m :: * -> *) (t :: * -> *).
    (Applicative m, Foldable t) =>
    t (m Doc) -> m Doc
    fsep ([m Doc] -> m Doc) -> [m Doc] -> m Doc
    forall a b. (a -> b) -> a -> b
    $ [Char] -> [m Doc]
    forall (m :: * -> *). Applicative m => [Char] -> [m Doc]
    pwords [Char]
    "when checking the definition of" [m Doc] -> [m Doc] -> [m Doc]
    forall a. [a] -> [a] -> [a]
    ++ [QName -> m Doc
    forall a (m :: * -> *). (PrettyTCM a, MonadPretty m) => a -> m Doc
    prettyTCM QName
    f]

        CheckPragma Range
    _ Pragma
    p ->
          [m Doc] -> m Doc
    forall (m :: * -> *) (t :: * -> *).
    (Applicative m, Foldable t) =>
    t (m Doc) -> m Doc
    fsep ([m Doc] -> m Doc) -> [m Doc] -> m Doc
    forall a b. (a -> b) -> a -> b
    $ [Char] -> [m Doc]
    forall (m :: * -> *). Applicative m => [Char] -> [m Doc]
    pwords [Char]
    "when checking the pragma"
                 [m Doc] -> [m Doc] -> [m Doc]
    forall a. [a] -> [a] -> [a]
    ++ [RangeAndPragma -> m Doc
    forall a (m :: * -> *).
    (ToConcrete a, Pretty (ConOfAbs a), MonadAbsToCon m) =>
    a -> m Doc
    prettyA (RangeAndPragma -> m Doc) -> RangeAndPragma -> m Doc
    forall a b. (a -> b) -> a -> b
    $ Range -> Pragma -> RangeAndPragma
    RangeAndPragma Range
    forall a. Range' a
    noRange Pragma
    p]

        CheckPrimitive Range
    _ QName
    x Expr
    e -> [m Doc] -> m Doc
    forall (m :: * -> *) (t :: * -> *).
    (Applicative m, Foldable t) =>
    t (m Doc) -> m Doc
    fsep ([m Doc] -> m Doc) -> [m Doc] -> m Doc
    forall a b. (a -> b) -> a -> b
    $
          [Char] -> [m Doc]
    forall (m :: * -> *). Applicative m => [Char] -> [m Doc]
    pwords [Char]
    "when checking that the type of the primitive function" [m Doc] -> [m Doc] -> [m Doc]
    forall a. [a] -> [a] -> [a]
    ++
          [QName -> m Doc
    forall a (m :: * -> *). (PrettyTCM a, MonadPretty m) => a -> m Doc
    prettyTCM QName
    x] [m Doc] -> [m Doc] -> [m Doc]
    forall a. [a] -> [a] -> [a]
    ++ [Char] -> [m Doc]
    forall (m :: * -> *). Applicative m => [Char] -> [m Doc]
    pwords [Char]
    "is" [m Doc] -> [m Doc] -> [m Doc]
    forall a. [a] -> [a] -> [a]
    ++ [Expr -> m Doc
    forall a (m :: * -> *).
    (ToConcrete a, Pretty (ConOfAbs a), MonadAbsToCon m) =>
    a -> m Doc
    prettyA Expr
    e]

        CheckWithFunctionType Type
    a -> [m Doc] -> m Doc
    forall (m :: * -> *) (t :: * -> *).
    (Applicative m, Foldable t) =>
    t (m Doc) -> m Doc
    fsep ([m Doc] -> m Doc) -> [m Doc] -> m Doc
    forall a b. (a -> b) -> a -> b
    $
          [Char] -> [m Doc]
    forall (m :: * -> *). Applicative m => [Char] -> [m Doc]
    pwords [Char]
    "when checking that the type" [m Doc] -> [m Doc] -> [m Doc]
    forall a. [a] -> [a] -> [a]
    ++
          [Type -> m Doc
    forall a (m :: * -> *). (PrettyTCM a, MonadPretty m) => a -> m Doc
    prettyTCM Type
    a] [m Doc] -> [m Doc] -> [m Doc]
    forall a. [a] -> [a] -> [a]
    ++ [Char] -> [m Doc]
    forall (m :: * -> *). Applicative m => [Char] -> [m Doc]
    pwords [Char]
    "of the generated with function is well-formed"

        CheckDotPattern Expr
    e Term
    v -> [m Doc] -> m Doc
    forall (m :: * -> *) (t :: * -> *).
    (Applicative m, Foldable t) =>
    t (m Doc) -> m Doc
    fsep ([m Doc] -> m Doc) -> [m Doc] -> m Doc
    forall a b. (a -> b) -> a -> b
    $
          [Char] -> [m Doc]
    forall (m :: * -> *). Applicative m => [Char] -> [m Doc]
    pwords [Char]
    "when checking that the given dot pattern" [m Doc] -> [m Doc] -> [m Doc]
    forall a. [a] -> [a] -> [a]
    ++ [Expr -> m Doc
    forall a (m :: * -> *).
    (ToConcrete a, Pretty (ConOfAbs a), MonadAbsToCon m) =>
    a -> m Doc
    prettyA Expr
    e] [m Doc] -> [m Doc] -> [m Doc]
    forall a. [a] -> [a] -> [a]
    ++
          [Char] -> [m Doc]
    forall (m :: * -> *). Applicative m => [Char] -> [m Doc]
    pwords [Char]
    "matches the inferred value" [m Doc] -> [m Doc] -> [m Doc]
    forall a. [a] -> [a] -> [a]
    ++ [Term -> m Doc
    forall a (m :: * -> *). (PrettyTCM a, MonadPretty m) => a -> m Doc
    prettyTCM Term
    v]

        CheckNamedWhere ModuleName
    m -> [m Doc] -> m Doc
    forall (m :: * -> *) (t :: * -> *).
    (Applicative m, Foldable t) =>
    t (m Doc) -> m Doc
    fsep ([m Doc] -> m Doc) -> [m Doc] -> m Doc
    forall a b. (a -> b) -> a -> b
    $
          [Char] -> [m Doc]
    forall (m :: * -> *). Applicative m => [Char] -> [m Doc]
    pwords [Char]
    "when checking the named where block" [m Doc] -> [m Doc] -> [m Doc]
    forall a. [a] -> [a] -> [a]
    ++ [ModuleName -> m Doc
    forall a (m :: * -> *).
    (ToConcrete a, Pretty (ConOfAbs a), MonadAbsToCon m) =>
    a -> m Doc
    prettyA ModuleName
    m]

        InferVar Name
    x ->
          [m Doc] -> m Doc
    forall (m :: * -> *) (t :: * -> *).
    (Applicative m, Foldable t) =>
    t (m Doc) -> m Doc
    fsep ([m Doc] -> m Doc) -> [m Doc] -> m Doc
    forall a b. (a -> b) -> a -> b
    $ [Char] -> [m Doc]
    forall (m :: * -> *). Applicative m => [Char] -> [m Doc]
    pwords [Char]
    "when inferring the type of" [m Doc] -> [m Doc] -> [m Doc]
    forall a. [a] -> [a] -> [a]
    ++ [Name -> m Doc
    forall a (m :: * -> *). (PrettyTCM a, MonadPretty m) => a -> m Doc
    prettyTCM Name
    x]

        InferDef QName
    x ->
          [m Doc] -> m Doc
    forall (m :: * -> *) (t :: * -> *).
    (Applicative m, Foldable t) =>
    t (m Doc) -> m Doc
    fsep ([m Doc] -> m Doc) -> [m Doc] -> m Doc
    forall a b. (a -> b) -> a -> b
    $ [Char] -> [m Doc]
    forall (m :: * -> *). Applicative m => [Char] -> [m Doc]
    pwords [Char]
    "when inferring the type of" [m Doc] -> [m Doc] -> [m Doc]
    forall a. [a] -> [a] -> [a]
    ++ [QName -> m Doc
    forall a (m :: * -> *). (PrettyTCM a, MonadPretty m) => a -> m Doc
    prettyTCM QName
    x]

        CheckIsEmpty Range
    r Type
    t ->
          [m Doc] -> m Doc
    forall (m :: * -> *) (t :: * -> *).
    (Applicative m, Foldable t) =>
    t (m Doc) -> m Doc
    fsep ([m Doc] -> m Doc) -> [m Doc] -> m Doc
    forall a b. (a -> b) -> a -> b
    $ [Char] -> [m Doc]
    forall (m :: * -> *). Applicative m => [Char] -> [m Doc]
    pwords [Char]
    "when checking that" [m Doc] -> [m Doc] -> [m Doc]
    forall a. [a] -> [a] -> [a]
    ++ [Type -> m Doc
    forall a (m :: * -> *). (PrettyTCM a, MonadPretty m) => a -> m Doc
    prettyTCM Type
    t] [m Doc] -> [m Doc] -> [m Doc]
    forall a. [a] -> [a] -> [a]
    ++
                 [Char] -> [m Doc]
    forall (m :: * -> *). Applicative m => [Char] -> [m Doc]
    pwords [Char]
    "has no constructors"

        CheckConfluence QName
    r1 QName
    r2 ->
          [m Doc] -> m Doc
    forall (m :: * -> *) (t :: * -> *).
    (Applicative m, Foldable t) =>
    t (m Doc) -> m Doc
    fsep ([m Doc] -> m Doc) -> [m Doc] -> m Doc
    forall a b. (a -> b) -> a -> b
    $ [Char] -> [m Doc]
    forall (m :: * -> *). Applicative m => [Char] -> [m Doc]
    pwords [Char]
    "when checking confluence of the rewrite rule" [m Doc] -> [m Doc] -> [m Doc]
    forall a. [a] -> [a] -> [a]
    ++
                 [QName -> m Doc
    forall a (m :: * -> *). (PrettyTCM a, MonadPretty m) => a -> m Doc
    prettyTCM QName
    r1] [m Doc] -> [m Doc] -> [m Doc]
    forall a. [a] -> [a] -> [a]
    ++ [Char] -> [m Doc]
    forall (m :: * -> *). Applicative m => [Char] -> [m Doc]
    pwords [Char]
    "with" [m Doc] -> [m Doc] -> [m Doc]
    forall a. [a] -> [a] -> [a]
    ++
                 if QName
    r1 QName -> QName -> Bool
    forall a. Eq a => a -> a -> Bool
    == QName
    r2 then [Char] -> [m Doc]
    forall (m :: * -> *). Applicative m => [Char] -> [m Doc]
    pwords [Char]
    "itself" else [QName -> m Doc
    forall a (m :: * -> *). (PrettyTCM a, MonadPretty m) => a -> m Doc
    prettyTCM QName
    r2]

        ScopeCheckExpr Expr
    e -> [m Doc] -> m Doc
    forall (m :: * -> *) (t :: * -> *).
    (Applicative m, Foldable t) =>
    t (m Doc) -> m Doc
    fsep ([m Doc] -> m Doc) -> [m Doc] -> m Doc
    forall a b. (a -> b) -> a -> b
    $ [Char] -> [m Doc]
    forall (m :: * -> *). Applicative m => [Char] -> [m Doc]
    pwords [Char]
    "when scope checking" [m Doc] -> [m Doc] -> [m Doc]
    forall a. [a] -> [a] -> [a]
    ++ [Expr -> m Doc
    forall (m :: * -> *) a. (Applicative m, Pretty a) => a -> m Doc
    pretty Expr
    e]

        ScopeCheckDeclaration NiceDeclaration
    d ->
          [Char] -> m Doc
    forall (m :: * -> *). Applicative m => [Char] -> m Doc
    fwords ([Char]
    "when scope checking the declaration" [Char] -> [Char] -> [Char]
    forall a. [a] -> [a] -> [a]
    ++ [Char]
    suffix) m Doc -> m Doc -> m Doc
    forall (m :: * -> *). Applicative m => m Doc -> m Doc -> m Doc
    $$
          Int -> m Doc -> m Doc
    forall (m :: * -> *). Functor m => Int -> m Doc -> m Doc
    nest Int
    2 ([m Doc] -> m Doc
    forall (m :: * -> *) (t :: * -> *).
    (Applicative m, Foldable t) =>
    t (m Doc) -> m Doc
    vcat ([m Doc] -> m Doc) -> [m Doc] -> m Doc
    forall a b. (a -> b) -> a -> b
    $ (Declaration -> m Doc) -> [Declaration] -> [m Doc]
    forall a b. (a -> b) -> [a] -> [b]
    map Declaration -> m Doc
    forall (m :: * -> *) a. (Applicative m, Pretty a) => a -> m Doc
    pretty [Declaration]
    ds)
          where
          ds :: [Declaration]
    ds     = NiceDeclaration -> [Declaration]
    D.notSoNiceDeclarations NiceDeclaration
    d
          suffix :: [Char]
    suffix = case [Declaration]
    ds of
            [Declaration
    _] -> [Char]
    ""
            [Declaration]
    _   -> [Char]
    "s"

        ScopeCheckLHS QName
    x Pattern
    p ->
          [m Doc] -> m Doc
    forall (m :: * -> *) (t :: * -> *).
    (Applicative m, Foldable t) =>
    t (m Doc) -> m Doc
    fsep ([m Doc] -> m Doc) -> [m Doc] -> m Doc
    forall a b. (a -> b) -> a -> b
    $ [Char] -> [m Doc]
    forall (m :: * -> *). Applicative m => [Char] -> [m Doc]
    pwords [Char]
    "when scope checking the left-hand side" [m Doc] -> [m Doc] -> [m Doc]
    forall a. [a] -> [a] -> [a]
    ++ [Pattern -> m Doc
    forall (m :: * -> *) a. (Applicative m, Pretty a) => a -> m Doc
    pretty Pattern
    p] [m Doc] -> [m Doc] -> [m Doc]
    forall a. [a] -> [a] -> [a]
    ++
                 [Char] -> [m Doc]
    forall (m :: * -> *). Applicative m => [Char] -> [m Doc]
    pwords [Char]
    "in the definition of" [m Doc] -> [m Doc] -> [m Doc]
    forall a. [a] -> [a] -> [a]
    ++ [QName -> m Doc
    forall (m :: * -> *) a. (Applicative m, Pretty a) => a -> m Doc
    pretty QName
    x]

        Call
    NoHighlighting -> m Doc
    forall a. Null a => a
    empty

        SetRange Range
    r -> [m Doc] -> m Doc
    forall (m :: * -> *) (t :: * -> *).
    (Applicative m, Foldable t) =>
    t (m Doc) -> m Doc
    fsep ([Char] -> [m Doc]
    forall (m :: * -> *). Applicative m => [Char] -> [m Doc]
    pwords [Char]
    "when doing something at") m Doc -> m Doc -> m Doc
    forall (m :: * -> *). Applicative m => m Doc -> m Doc -> m Doc
    <+> Range -> m Doc
    forall a (m :: * -> *). (PrettyTCM a, MonadPretty m) => a -> m Doc
    prettyTCM Range
    r

        CheckSectionApplication Range
    _ ModuleName
    m1 ModuleApplication
    modapp -> [m Doc] -> m Doc
    forall (m :: * -> *) (t :: * -> *).
    (Applicative m, Foldable t) =>
    t (m Doc) -> m Doc
    fsep ([m Doc] -> m Doc) -> [m Doc] -> m Doc
    forall a b. (a -> b) -> a -> b
    $
          [Char] -> [m Doc]
    forall (m :: * -> *). Applicative m => [Char] -> [m Doc]
    pwords [Char]
    "when checking the module application" [m Doc] -> [m Doc] -> [m Doc]
    forall a. [a] -> [a] -> [a]
    ++
          [Declaration -> m Doc
    forall a (m :: * -> *).
    (ToConcrete a, Pretty (ConOfAbs a), MonadAbsToCon m) =>
    a -> m Doc
    prettyA (Declaration -> m Doc) -> Declaration -> m Doc
    forall a b. (a -> b) -> a -> b
    $ ModuleInfo
    -> ModuleName
    -> ModuleApplication
    -> ScopeCopyInfo
    -> ImportDirective
    -> Declaration
    A.Apply ModuleInfo
    info ModuleName
    m1 ModuleApplication
    modapp ScopeCopyInfo
    initCopyInfo ImportDirective
    forall a. Null a => a
    empty]
          where
          info :: ModuleInfo
    info = Range
    -> Range
    -> Maybe Name
    -> Maybe OpenShortHand
    -> Maybe ImportDirective
    -> ModuleInfo
    A.ModuleInfo Range
    forall a. Range' a
    noRange Range
    forall a. Range' a
    noRange Maybe Name
    forall a. Maybe a
    Nothing Maybe OpenShortHand
    forall a. Maybe a
    Nothing Maybe ImportDirective
    forall a. Maybe a
    Nothing

        Call
    ModuleContents -> [m Doc] -> m Doc
    forall (m :: * -> *) (t :: * -> *).
    (Applicative m, Foldable t) =>
    t (m Doc) -> m Doc
    fsep ([m Doc] -> m Doc) -> [m Doc] -> m Doc
    forall a b. (a -> b) -> a -> b
    $ [Char] -> [m Doc]
    forall (m :: * -> *). Applicative m => [Char] -> [m Doc]
    pwords [Char]
    "when retrieving the contents of a module"

        where
        hPretty :: MonadPretty m => Arg (Named_ Expr) -> m Doc
        hPretty :: forall (m :: * -> *). MonadPretty m => NamedArg Expr -> m Doc
    hPretty NamedArg Expr
    a = do
          Precedence -> m Doc -> m Doc
    forall (m :: * -> *) a. ReadTCState m => Precedence -> m a -> m a
    withContextPrecedence (ParenPreference -> Precedence
    ArgumentCtx ParenPreference
    PreferParen) (m Doc -> m Doc) -> m Doc -> m Doc
    forall a b. (a -> b) -> a -> b
    $
            Arg (Named (WithOrigin (Ranged [Char])) Expr) -> m Doc
    forall (m :: * -> *) a. (Applicative m, Pretty a) => a -> m Doc
    pretty (Arg (Named (WithOrigin (Ranged [Char])) Expr) -> m Doc)
    -> m (Arg (Named (WithOrigin (Ranged [Char])) Expr)) -> m Doc
    forall (m :: * -> *) a b. Monad m => (a -> m b) -> m a -> m b
    =<< NamedArg Expr -> NamedArg Expr -> m (ConOfAbs (NamedArg Expr))
    forall i a (m :: * -> *).
    (LensHiding i, ToConcrete a, MonadAbsToCon m) =>
    i -> a -> m (ConOfAbs a)
    abstractToConcreteHiding NamedArg Expr
    a NamedArg Expr
    a