    {-# OPTIONS_GHC -Wunused-imports #-}

    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 qualified Agda.Syntax.Common.Pretty as P
    import qualified Agda.Syntax.Concrete.Definitions as D
    import qualified Agda.Syntax.Info as A
    import Agda.Syntax.Fixity
    import Agda.Syntax.Internal
    import Agda.Syntax.Position
    import Agda.Syntax.Scope.Monad
    import Agda.Syntax.Translation.AbstractToConcrete

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

    import Agda.Utils.Null

    import Agda.Utils.Impossible

    import Agda.Version (docsUrl)

    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 = Range -> m Doc
    forall a (m :: * -> *). (PrettyTCM a, MonadPretty m) => a -> m Doc
    forall (m :: * -> *). MonadPretty m => Range -> m Doc
    prettyTCM (a -> Range
    forall a. HasRange a => a -> Range
    getRange a
    x) m Doc -> m Doc -> m Doc
    forall (m :: * -> *). Applicative m => m Doc -> m Doc -> m Doc
    $$ m Doc
    d

    instance PrettyTCM CallInfo where
      prettyTCM :: forall (m :: * -> *). MonadPretty m => CallInfo -> m Doc
    prettyTCM (CallInfo QName
    callInfoTarget Closure Term
    callInfoCall) = do
        let call :: m Doc
    call = Closure Term -> m Doc
    forall a (m :: * -> *). (PrettyTCM a, MonadPretty m) => a -> m Doc
    forall (m :: * -> *). MonadPretty m => Closure Term -> m Doc
    prettyTCM Closure Term
    callInfoCall
            r :: Range
    r    = QName -> Range
    forall a. HasRange a => a -> Range
    getRange QName
    callInfoTarget
        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
    forall (m :: * -> *). MonadPretty m => Range -> m Doc
    prettyTCM Range
    r) m Doc -> m Doc -> m Doc
    forall a. Semigroup a => a -> a -> a
    <> m Doc
    ")"
      {-# SPECIALIZE prettyTCM :: CallInfo -> TCM 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

          String -> Int -> m () -> m ()
    forall (m :: * -> *). MonadDebug m => String -> Int -> m () -> m ()
    verboseS  String
    "error.checkclause" Int
    40 (m () -> m ()) -> m () -> m ()
    forall a b. (a -> b) -> a -> b
    $ do
            String -> Int -> String -> m ()
    forall (m :: * -> *).
    MonadDebug m =>
    String -> Int -> String -> m ()
    reportSLn String
    "error.checkclause" Int
    60 (String -> m ()) -> String -> m ()
    forall a b. (a -> b) -> a -> b
    $ String
    "prettyTCM CheckClause: cl = " String -> String -> String
    forall a. [a] -> [a] -> [a]
    ++ SpineClause -> String
    forall a. Show a => a -> String
    show (SpineClause -> SpineClause
    forall a. ExprLike a => a -> a
    deepUnscope SpineClause
    cl)
            clc <- SpineClause -> m (ConOfAbs SpineClause)
    forall a (m :: * -> *).
    (ToConcrete a, MonadAbsToCon m) =>
    a -> m (ConOfAbs a)
    abstractToConcrete_ SpineClause
    cl
            reportSLn "error.checkclause" 40 $ "cl (Concrete) = " ++ show 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
    $
            String -> [m Doc]
    forall (m :: * -> *). Applicative m => String -> [m Doc]
    pwords String
    "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]
    ++ String -> [m Doc]
    forall (m :: * -> *). Applicative m => String -> [m Doc]
    pwords String
    "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
    forall (m :: * -> *). MonadPretty m => Type -> 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
    $ String -> [m Doc]
    forall (m :: * -> *). Applicative m => String -> [m Doc]
    pwords String
    "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 { A.spLhsInfo = (A.spLhsInfo lhs) { A.lhsEllipsis = 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
    forall (m :: * -> *) a.
    MonadAddContext m =>
    Telescope -> 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
    $
          String -> [m Doc]
    forall (m :: * -> *). Applicative m => String -> [m Doc]
    pwords String
    "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]
    ++ String -> [m Doc]
    forall (m :: * -> *). Applicative m => String -> [m Doc]
    pwords String
    "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
    forall (m :: * -> *). MonadPretty m => Type -> 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
    $
          String -> [m Doc]
    forall (m :: * -> *). Applicative m => String -> [m Doc]
    pwords String
    "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]
    ++ String -> [m Doc]
    forall (m :: * -> *). Applicative m => String -> [m Doc]
    pwords String
    "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
    $
          String -> [m Doc]
    forall (m :: * -> *). Applicative m => String -> [m Doc]
    pwords String
    "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]
    ++ String -> [m Doc]
    forall (m :: * -> *). Applicative m => String -> [m Doc]
    pwords String
    "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
    $
          String -> [m Doc]
    forall (m :: * -> *). Applicative m => String -> [m Doc]
    pwords String
    "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
    $ String -> [m Doc]
    forall (m :: * -> *). Applicative m => String -> [m Doc]
    pwords String
    "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
    $
          String -> [m Doc]
    forall (m :: * -> *). Applicative m => String -> [m Doc]
    pwords String
    "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]
    ++ String -> [m Doc]
    forall (m :: * -> *). Applicative m => String -> [m Doc]
    pwords String
    "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
    forall (m :: * -> *). MonadPretty m => Type -> 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
    $
          String -> [m Doc]
    forall (m :: * -> *). Applicative m => String -> [m Doc]
    pwords String
    "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]
    ++ String -> [m Doc]
    forall (m :: * -> *). Applicative m => String -> [m Doc]
    pwords String
    "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
    forall (m :: * -> *). MonadPretty m => Sort -> 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
    $
          String -> [m Doc]
    forall (m :: * -> *). Applicative m => String -> [m Doc]
    pwords String
    "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]
    ++ String -> [m Doc]
    forall (m :: * -> *). Applicative m => String -> [m Doc]
    pwords String
    "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
    $
          String -> [m Doc]
    forall (m :: * -> *). Applicative m => String -> [m Doc]
    pwords String
    "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
    forall (m :: * -> *). MonadPretty m => QName -> 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
    forall (m :: * -> *). MonadPretty m => Type -> m Doc
    prettyTCM Type
    t ] ]

        CheckArguments Expr
    r [NamedArg Expr]
    es Type
    t0 Maybe Type
    t1 -> do
          TelV tel cod <- Type -> m (TelV Type)
    forall (m :: * -> *).
    (MonadReduce m, MonadAddContext m) =>
    Type -> m (TelV Type)
    telView Type
    t0
          let
            prefix =
              String -> [m Doc]
    forall (m :: * -> *). Applicative m => String -> [m Doc]
    pwords String
    "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]
    ++
              String -> [m Doc]
    forall (m :: * -> *). Applicative m => String -> [m Doc]
    pwords ([NamedArg Expr] -> String -> String -> String
    forall a c. Sized a => a -> c -> c -> c
    P.singPlural [NamedArg Expr]
    es String
    "is a valid argument" String
    "are valid arguments")
          case unEl cod of
            Dummy{} -> [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
    $
              [m Doc]
    prefix [m Doc] -> [m Doc] -> [m Doc]
    forall a. [a] -> [a] -> [a]
    ++
              String -> [m Doc]
    forall (m :: * -> *). Applicative m => String -> [m Doc]
    pwords String
    "to a function accepting arguments of type" [m Doc] -> [m Doc] -> [m Doc]
    forall a. [a] -> [a] -> [a]
    ++
              [Telescope -> m Doc
    forall a (m :: * -> *). (PrettyTCM a, MonadPretty m) => a -> m Doc
    forall (m :: * -> *). MonadPretty m => Telescope -> m Doc
    prettyTCM Telescope
    tel]
            Term
    _ -> [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
    $
              [m Doc]
    prefix [m Doc] -> [m Doc] -> [m Doc]
    forall a. [a] -> [a] -> [a]
    ++
              String -> [m Doc]
    forall (m :: * -> *). Applicative m => String -> [m Doc]
    pwords String
    "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
    forall (m :: * -> *). MonadPretty m => Type -> 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
    $
          String -> [m Doc]
    forall (m :: * -> *). Applicative m => String -> [m Doc]
    pwords String
    "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
    forall (m :: * -> *). MonadPretty m => Term -> m Doc
    prettyTCM Term
    v] [m Doc] -> [m Doc] -> [m Doc]
    forall a. [a] -> [a] -> [a]
    ++
          String -> [m Doc]
    forall (m :: * -> *). Applicative m => String -> [m Doc]
    pwords String
    "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
    forall (m :: * -> *). MonadPretty m => MetaId -> m Doc
    prettyTCM MetaId
    m] [m Doc] -> [m Doc] -> [m Doc]
    forall a. [a] -> [a] -> [a]
    ++
          String -> [m Doc]
    forall (m :: * -> *). Applicative m => String -> [m Doc]
    pwords String
    "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
    forall (m :: * -> *). MonadPretty m => Type -> 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
    forall (m :: * -> *). MonadPretty m => Type -> 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
    forall (m :: * -> *). MonadPretty m => Type -> 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
    $ String -> [m Doc]
    forall (m :: * -> *). Applicative m => String -> [m Doc]
    pwords String
    "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
    forall (m :: * -> *). MonadPretty m => QName -> 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
    $ String -> [m Doc]
    forall (m :: * -> *). Applicative m => String -> [m Doc]
    pwords String
    "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
    forall (m :: * -> *). MonadPretty m => QName -> m Doc
    prettyTCM QName
    x]

        CheckConstructor QName
    d Telescope
    _ Sort
    _ (A.Axiom KindOfName
    _ DefInfo
    _ ArgInfo
    _ Maybe PragmaPolarities
    _ 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
    $
          String -> [m Doc]
    forall (m :: * -> *). Applicative m => String -> [m Doc]
    pwords String
    "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
    forall (m :: * -> *). MonadPretty m => QName -> m Doc
    prettyTCM QName
    c] [m Doc] -> [m Doc] -> [m Doc]
    forall a. [a] -> [a] -> [a]
    ++
          String -> [m Doc]
    forall (m :: * -> *). Applicative m => String -> [m Doc]
    pwords String
    "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
    forall (m :: * -> *). MonadPretty m => QName -> m Doc
    prettyTCM QName
    d]

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

        CheckConArgFitsIn QName
    c Bool
    f Type
    t Sort
    s -> do
          woK <- m Bool
    forall (m :: * -> *). HasOptions m => m Bool
    withoutKOption
          let
            hint = [m Doc] -> m Doc
    forall (m :: * -> *) (t :: * -> *).
    (Applicative m, Foldable t) =>
    t (m Doc) -> m Doc
    fsep (String -> [m Doc]
    forall (m :: * -> *). Applicative m => String -> [m Doc]
    pwords String
    "Note: this argument is forced by the indices 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
    forall (m :: * -> *). MonadPretty m => QName -> m Doc
    prettyTCM QName
    c m Doc -> m Doc -> m Doc
    forall a. Semigroup a => a -> a -> a
    <> m Doc
    forall (m :: * -> *). Applicative m => m Doc
    comma] [m Doc] -> [m Doc] -> [m Doc]
    forall a. [a] -> [a] -> [a]
    ++ String -> [m Doc]
    forall (m :: * -> *). Applicative m => String -> [m Doc]
    pwords String
    "so this definition would be allowed under --large-indices.")
            -- Only add hint about large-indices when --with-K
            addh m Doc
    d
              | Bool
    f Bool -> Bool -> Bool
    && Bool -> Bool
    not Bool
    woK = m Doc
    d m Doc -> m Doc -> m Doc
    forall (m :: * -> *). Applicative m => m Doc -> m Doc -> m Doc
    $$ m Doc
    forall a. Null a => a
    empty m Doc -> m Doc -> m Doc
    forall (m :: * -> *). Applicative m => m Doc -> m Doc -> m Doc
    $$ m Doc
    hint
              | Bool
    otherwise    = m Doc
    d

          addh $ fsep $
            pwords "when checking that the type" ++ [prettyTCM t] ++
            pwords "of an argument to the constructor" ++ [prettyTCM c] ++
            pwords "fits in the sort" ++ [prettyTCM s] ++
            pwords "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
    $ String -> [m Doc]
    forall (m :: * -> *). Applicative m => String -> [m Doc]
    pwords String
    "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
    forall (m :: * -> *). MonadPretty m => QName -> 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
    $ String -> [m Doc]
    forall (m :: * -> *). Applicative m => String -> [m Doc]
    pwords String
    "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
    $
          String -> [m Doc]
    forall (m :: * -> *). Applicative m => String -> [m Doc]
    pwords String
    "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
    forall (m :: * -> *). MonadPretty m => QName -> m Doc
    prettyTCM QName
    x] [m Doc] -> [m Doc] -> [m Doc]
    forall a. [a] -> [a] -> [a]
    ++ String -> [m Doc]
    forall (m :: * -> *). Applicative m => String -> [m Doc]
    pwords String
    "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]

        CheckModuleParameters ModuleName
    m Telescope
    _tel -> [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
    $
          String -> [m Doc]
    forall (m :: * -> *). Applicative m => String -> [m Doc]
    pwords String
    "when checking the parameters of module" [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]

        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
    $
          String -> [m Doc]
    forall (m :: * -> *). Applicative m => String -> [m Doc]
    pwords String
    "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
    forall (m :: * -> *). MonadPretty m => Type -> m Doc
    prettyTCM Type
    a] [m Doc] -> [m Doc] -> [m Doc]
    forall a. [a] -> [a] -> [a]
    ++ String -> [m Doc]
    forall (m :: * -> *). Applicative m => String -> [m Doc]
    pwords String
    "of the generated with function is well-formed" [m Doc] -> [m Doc] -> [m Doc]
    forall a. [a] -> [a] -> [a]
    ++
          [m Doc -> m Doc
    forall (m :: * -> *). Functor m => m Doc -> m Doc
    parens (m Doc -> m Doc) -> m Doc -> m Doc
    forall a b. (a -> b) -> a -> b
    $ String -> m Doc
    forall (m :: * -> *). Applicative m => String -> m Doc
    text (String -> m Doc) -> String -> m Doc
    forall a b. (a -> b) -> a -> b
    $ String -> String
    docsUrl String
    "language/with-abstraction.html#ill-typed-with-abstractions"]

        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
    $
          String -> [m Doc]
    forall (m :: * -> *). Applicative m => String -> [m Doc]
    pwords String
    "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]
    ++
          String -> [m Doc]
    forall (m :: * -> *). Applicative m => String -> [m Doc]
    pwords String
    "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
    forall (m :: * -> *). MonadPretty m => Term -> 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
    $
          String -> [m Doc]
    forall (m :: * -> *). Applicative m => String -> [m Doc]
    pwords String
    "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
    $ String -> [m Doc]
    forall (m :: * -> *). Applicative m => String -> [m Doc]
    pwords String
    "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
    forall (m :: * -> *). MonadPretty m => Name -> 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
    $ String -> [m Doc]
    forall (m :: * -> *). Applicative m => String -> [m Doc]
    pwords String
    "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
    forall (m :: * -> *). MonadPretty m => QName -> 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
    $ String -> [m Doc]
    forall (m :: * -> *). Applicative m => String -> [m Doc]
    pwords String
    "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
    forall (m :: * -> *). MonadPretty m => Type -> m Doc
    prettyTCM Type
    t] [m Doc] -> [m Doc] -> [m Doc]
    forall a. [a] -> [a] -> [a]
    ++
                 String -> [m Doc]
    forall (m :: * -> *). Applicative m => String -> [m Doc]
    pwords String
    "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
    $ String -> [m Doc]
    forall (m :: * -> *). Applicative m => String -> [m Doc]
    pwords String
    "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
    forall (m :: * -> *). MonadPretty m => QName -> m Doc
    prettyTCM QName
    r1] [m Doc] -> [m Doc] -> [m Doc]
    forall a. [a] -> [a] -> [a]
    ++ String -> [m Doc]
    forall (m :: * -> *). Applicative m => String -> [m Doc]
    pwords String
    "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 String -> [m Doc]
    forall (m :: * -> *). Applicative m => String -> [m Doc]
    pwords String
    "itself" else [QName -> m Doc
    forall a (m :: * -> *). (PrettyTCM a, MonadPretty m) => a -> m Doc
    forall (m :: * -> *). MonadPretty m => QName -> 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
    $ String -> [m Doc]
    forall (m :: * -> *). Applicative m => String -> [m Doc]
    pwords String
    "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 ->
          [m Doc] -> m Doc
    forall (m :: * -> *) (t :: * -> *).
    (Applicative m, Foldable t) =>
    t (m Doc) -> m Doc
    fsep (String -> [m Doc]
    forall (m :: * -> *). Applicative m => String -> [m Doc]
    pwords String
    "when scope checking the" [m Doc] -> [m Doc] -> [m Doc]
    forall a. [a] -> [a] -> [a]
    ++ [ List1 Declaration -> m Doc -> m Doc
    forall (m :: * -> *) a. (Functor m, Sized a) => a -> m Doc -> m Doc
    pluralS List1 Declaration
    ds m Doc
    "declaration" ]) 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 (NonEmpty (m Doc) -> m Doc
    forall (m :: * -> *) (t :: * -> *).
    (Applicative m, Foldable t) =>
    t (m Doc) -> m Doc
    vcat (NonEmpty (m Doc) -> m Doc) -> NonEmpty (m Doc) -> m Doc
    forall a b. (a -> b) -> a -> b
    $ (Declaration -> m Doc) -> List1 Declaration -> NonEmpty (m Doc)
    forall a b. (a -> b) -> NonEmpty a -> NonEmpty b
    forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
    fmap Declaration -> m Doc
    forall (m :: * -> *) a. (Applicative m, Pretty a) => a -> m Doc
    pretty List1 Declaration
    ds)
          where
          ds :: List1 Declaration
    ds     = NiceDeclaration -> List1 Declaration
    D.notSoNiceDeclarations NiceDeclaration
    d

        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
    $ String -> [m Doc]
    forall (m :: * -> *). Applicative m => String -> [m Doc]
    pwords String
    "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]
    ++
                 String -> [m Doc]
    forall (m :: * -> *). Applicative m => String -> [m Doc]
    pwords String
    "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 (String -> [m Doc]
    forall (m :: * -> *). Applicative m => String -> [m Doc]
    pwords String
    "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
    forall (m :: * -> *). MonadPretty m => Range -> m Doc
    prettyTCM Range
    r

        CheckSectionApplication Range
    _ Erased
    erased 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
    $
          String -> [m Doc]
    forall (m :: * -> *). Applicative m => String -> [m Doc]
    pwords String
    "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
    -> Erased
    -> ModuleName
    -> ModuleApplication
    -> ScopeCopyInfo
    -> ImportDirective
    -> Declaration
    A.Apply ModuleInfo
    info Erased
    erased 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
    $ String -> [m Doc]
    forall (m :: * -> *). Applicative m => String -> [m Doc]
    pwords String
    "when retrieving the contents of a module"

        CheckIApplyConfluence Range
    _ QName
    qn Term
    fn Term
    l Term
    r Type
    t -> do
          [m Doc] -> m Doc
    forall (m :: * -> *) (t :: * -> *).
    (Applicative m, Foldable t) =>
    t (m Doc) -> m Doc
    vcat
            [ [m Doc] -> m Doc
    forall (m :: * -> *) (t :: * -> *).
    (Applicative m, Foldable t) =>
    t (m Doc) -> m Doc
    fsep (String -> [m Doc]
    forall (m :: * -> *). Applicative m => String -> [m Doc]
    pwords String
    "when checking that a clause 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
    forall (m :: * -> *). MonadPretty m => QName -> m Doc
    prettyTCM QName
    qn] [m Doc] -> [m Doc] -> [m Doc]
    forall a. [a] -> [a] -> [a]
    ++ String -> [m Doc]
    forall (m :: * -> *). Applicative m => String -> [m Doc]
    pwords String
    "has the correct boundary.")
            , m Doc
    ""
            , m Doc
    "Specifically, the terms"
            , Int -> m Doc -> m Doc
    forall (m :: * -> *). Functor m => Int -> m Doc -> m Doc
    nest Int
    2 (Term -> m Doc
    forall a (m :: * -> *). (PrettyTCM a, MonadPretty m) => a -> m Doc
    forall (m :: * -> *). MonadPretty m => Term -> m Doc
    prettyTCM Term
    l)
            , m Doc
    "and"
            , Int -> m Doc -> m Doc
    forall (m :: * -> *). Functor m => Int -> m Doc -> m Doc
    nest Int
    2 (Term -> m Doc
    forall a (m :: * -> *). (PrettyTCM a, MonadPretty m) => a -> m Doc
    forall (m :: * -> *). MonadPretty m => Term -> m Doc
    prettyTCM Term
    r)
            , [m Doc] -> m Doc
    forall (m :: * -> *) (t :: * -> *).
    (Applicative m, Foldable t) =>
    t (m Doc) -> m Doc
    fsep (String -> [m Doc]
    forall (m :: * -> *). Applicative m => String -> [m Doc]
    pwords String
    "must be equal, since" [m Doc] -> [m Doc] -> [m Doc]
    forall a. [a] -> [a] -> [a]
    ++ [Term -> m Doc
    forall a (m :: * -> *). (PrettyTCM a, MonadPretty m) => a -> m Doc
    forall (m :: * -> *). MonadPretty m => Term -> m Doc
    prettyTCM Term
    fn] [m Doc] -> [m Doc] -> [m Doc]
    forall a. [a] -> [a] -> [a]
    ++ String -> [m Doc]
    forall (m :: * -> *). Applicative m => String -> [m Doc]
    pwords String
    "could reduce to either.")
            ]

        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 String)) Expr) -> m Doc
    forall (m :: * -> *) a. (Applicative m, Pretty a) => a -> m Doc
    pretty (Arg (Named (WithOrigin (Ranged String)) Expr) -> m Doc)
    -> m (Arg (Named (WithOrigin (Ranged String)) 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
      {-# SPECIALIZE prettyTCM :: Call -> TCM Doc #-}