{-# 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 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.Internal
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.Function
import Agda.Utils.Null
import qualified Agda.Syntax.Common.Pretty as P

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 = forall b a. IsBool b => b -> (a -> a) -> a -> a
applyUnless (forall a. Null a => a -> Bool
null Range
r) (forall a (m :: * -> *). (PrettyTCM a, MonadPretty m) => a -> m Doc
prettyTCM Range
r forall (m :: * -> *). Applicative m => m Doc -> m Doc -> m Doc
$$) m Doc
d
  where r :: Range
r = 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 = 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 = forall (m :: * -> *) a.
(MonadPretty m, HasRange a) =>
a -> m Doc -> m Doc
sayWhere Range
r (m Doc
m forall (m :: * -> *). Applicative m => m Doc -> m Doc -> 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 QName
callInfoTarget Closure Term
callInfoCall) = do
    let call :: m Doc
call = forall a (m :: * -> *). (PrettyTCM a, MonadPretty m) => a -> m Doc
prettyTCM Closure Term
callInfoCall
        r :: Range
r    = forall a. HasRange a => a -> Range
getRange QName
callInfoTarget
    if forall a. Null a => a -> Bool
null forall a b. (a -> b) -> a -> b
$ forall a. Pretty a => a -> Doc
P.pretty Range
r
      then m Doc
call
      else m Doc
call forall (m :: * -> *). Applicative m => m Doc -> m Doc -> m Doc
$$ forall (m :: * -> *). Functor m => Int -> m Doc -> m Doc
nest Int
2 (m Doc
"(at" forall (m :: * -> *). Applicative m => m Doc -> m Doc -> m Doc
<+> forall a (m :: * -> *). (PrettyTCM a, MonadPretty m) => a -> m Doc
prettyTCM Range
r) forall a. Semigroup a => a -> a -> a
<> m Doc
")"

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

    CheckClause Type
t SpineClause
cl -> do

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

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

    CheckLHS SpineLHS
lhs -> forall (m :: * -> *) (t :: * -> *).
(Applicative m, Foldable t) =>
t (m Doc) -> m Doc
vcat forall a b. (a -> b) -> a -> b
$
      [ forall (m :: * -> *) (t :: * -> *).
(Applicative m, Foldable t) =>
t (m Doc) -> m Doc
fsep forall a b. (a -> b) -> a -> b
$ forall (m :: * -> *). Applicative m => [Char] -> [m Doc]
pwords [Char]
"when checking the clause left hand side"
      , forall a (m :: * -> *).
(ToConcrete a, Pretty (ConOfAbs a), MonadAbsToCon m) =>
a -> m Doc
prettyA 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 -> forall b (m :: * -> *) a.
(AddContext b, MonadAddContext m) =>
b -> m a -> m a
addContext Telescope
tel forall a b. (a -> b) -> a -> b
$ forall (m :: * -> *) (t :: * -> *).
(Applicative m, Foldable t) =>
t (m Doc) -> m Doc
fsep forall a b. (a -> b) -> a -> b
$
      forall (m :: * -> *). Applicative m => [Char] -> [m Doc]
pwords [Char]
"when checking that the pattern"
      forall a. [a] -> [a] -> [a]
++ [forall a (m :: * -> *).
(ToConcrete a, Pretty (ConOfAbs a), MonadAbsToCon m) =>
a -> m Doc
prettyA Pattern
p] forall a. [a] -> [a] -> [a]
++ forall (m :: * -> *). Applicative m => [Char] -> [m Doc]
pwords [Char]
"has type" forall a. [a] -> [a] -> [a]
++ [forall a (m :: * -> *). (PrettyTCM a, MonadPretty m) => a -> m Doc
prettyTCM Type
t]

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

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

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

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

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

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

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

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

    CheckArguments Range
r [NamedArg Expr]
es Type
t0 Maybe Type
t1 -> do
      TelV Telescope
tel Type
cod <- forall (m :: * -> *).
(MonadReduce m, MonadAddContext m) =>
Type -> m (TelV Type)
telView Type
t0
      let
        prefix :: [m Doc]
prefix =
          forall (m :: * -> *). Applicative m => [Char] -> [m Doc]
pwords [Char]
"when checking that" forall a. [a] -> [a] -> [a]
++
          forall a b. (a -> b) -> [a] -> [b]
map forall (m :: * -> *). MonadPretty m => NamedArg Expr -> m Doc
hPretty [NamedArg Expr]
es forall a. [a] -> [a] -> [a]
++
          forall (m :: * -> *). Applicative m => [Char] -> [m Doc]
pwords (forall a c. Sized a => a -> c -> c -> c
P.singPlural [NamedArg Expr]
es [Char]
"is a valid argument" [Char]
"are valid arguments")
      case forall t a. Type'' t a -> a
unEl Type
cod of
        Dummy{} -> forall (m :: * -> *) (t :: * -> *).
(Applicative m, Foldable t) =>
t (m Doc) -> m Doc
fsep forall a b. (a -> b) -> a -> b
$
          [m Doc]
prefix forall a. [a] -> [a] -> [a]
++
          forall (m :: * -> *). Applicative m => [Char] -> [m Doc]
pwords [Char]
"to a function accepting arguments of type" forall a. [a] -> [a] -> [a]
++
          [forall a (m :: * -> *). (PrettyTCM a, MonadPretty m) => a -> m Doc
prettyTCM Telescope
tel]
        Term
_ -> forall (m :: * -> *) (t :: * -> *).
(Applicative m, Foldable t) =>
t (m Doc) -> m Doc
fsep forall a b. (a -> b) -> a -> b
$
          [m Doc]
prefix forall a. [a] -> [a] -> [a]
++
          forall (m :: * -> *). Applicative m => [Char] -> [m Doc]
pwords [Char]
"to a function of type" forall a. [a] -> [a] -> [a]
++
          [forall a (m :: * -> *). (PrettyTCM a, MonadPretty m) => a -> m Doc
prettyTCM Type
t0]

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

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

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

    CheckDataDef Range
_ QName
x [LamBinding]
ps [Declaration]
cs ->
      forall (m :: * -> *) (t :: * -> *).
(Applicative m, Foldable t) =>
t (m Doc) -> m Doc
fsep forall a b. (a -> b) -> a -> b
$ forall (m :: * -> *). Applicative m => [Char] -> [m Doc]
pwords [Char]
"when checking the definition of" forall a. [a] -> [a] -> [a]
++ [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
_) -> forall (m :: * -> *) (t :: * -> *).
(Applicative m, Foldable t) =>
t (m Doc) -> m Doc
fsep forall a b. (a -> b) -> a -> b
$
      forall (m :: * -> *). Applicative m => [Char] -> [m Doc]
pwords [Char]
"when checking the constructor" forall a. [a] -> [a] -> [a]
++ [forall a (m :: * -> *). (PrettyTCM a, MonadPretty m) => a -> m Doc
prettyTCM QName
c] forall a. [a] -> [a] -> [a]
++
      forall (m :: * -> *). Applicative m => [Char] -> [m Doc]
pwords [Char]
"in the declaration of" forall a. [a] -> [a] -> [a]
++ [forall a (m :: * -> *). (PrettyTCM a, MonadPretty m) => a -> m Doc
prettyTCM QName
d]

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

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

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

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

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

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

    CheckModuleParameters ModuleName
m Telescope
_tel -> forall (m :: * -> *) (t :: * -> *).
(Applicative m, Foldable t) =>
t (m Doc) -> m Doc
fsep forall a b. (a -> b) -> a -> b
$
      forall (m :: * -> *). Applicative m => [Char] -> [m Doc]
pwords [Char]
"when checking the parameters of module" forall a. [a] -> [a] -> [a]
++ [forall a (m :: * -> *).
(ToConcrete a, Pretty (ConOfAbs a), MonadAbsToCon m) =>
a -> m Doc
prettyA ModuleName
m]

    CheckWithFunctionType Type
a -> forall (m :: * -> *) (t :: * -> *).
(Applicative m, Foldable t) =>
t (m Doc) -> m Doc
fsep forall a b. (a -> b) -> a -> b
$
      forall (m :: * -> *). Applicative m => [Char] -> [m Doc]
pwords [Char]
"when checking that the type" forall a. [a] -> [a] -> [a]
++
      [forall a (m :: * -> *). (PrettyTCM a, MonadPretty m) => a -> m Doc
prettyTCM Type
a] forall a. [a] -> [a] -> [a]
++ forall (m :: * -> *). Applicative m => [Char] -> [m Doc]
pwords [Char]
"of the generated with function is well-formed" forall a. [a] -> [a] -> [a]
++
      [forall (m :: * -> *). Functor m => m Doc -> m Doc
parens forall a b. (a -> b) -> a -> b
$ forall (m :: * -> *). Applicative m => [Char] -> m Doc
text forall a b. (a -> b) -> a -> b
$ [Char] -> [Char]
docsUrl [Char]
"language/with-abstraction.html#ill-typed-with-abstractions"]

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

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

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

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

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

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

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

    ScopeCheckDeclaration NiceDeclaration
d ->
      forall (m :: * -> *). Applicative m => [Char] -> m Doc
fwords ([Char]
"when scope checking the declaration" forall a. [a] -> [a] -> [a]
++ [Char]
suffix) forall (m :: * -> *). Applicative m => m Doc -> m Doc -> m Doc
$$
      forall (m :: * -> *). Functor m => Int -> m Doc -> m Doc
nest Int
2 (forall (m :: * -> *) (t :: * -> *).
(Applicative m, Foldable t) =>
t (m Doc) -> m Doc
vcat forall a b. (a -> b) -> a -> b
$ forall a b. (a -> b) -> [a] -> [b]
map 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 ->
      forall (m :: * -> *) (t :: * -> *).
(Applicative m, Foldable t) =>
t (m Doc) -> m Doc
fsep forall a b. (a -> b) -> a -> b
$ forall (m :: * -> *). Applicative m => [Char] -> [m Doc]
pwords [Char]
"when scope checking the left-hand side" forall a. [a] -> [a] -> [a]
++ [forall (m :: * -> *) a. (Applicative m, Pretty a) => a -> m Doc
pretty Pattern
p] forall a. [a] -> [a] -> [a]
++
             forall (m :: * -> *). Applicative m => [Char] -> [m Doc]
pwords [Char]
"in the definition of" forall a. [a] -> [a] -> [a]
++ [forall (m :: * -> *) a. (Applicative m, Pretty a) => a -> m Doc
pretty QName
x]

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

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

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

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

    CheckIApplyConfluence Range
_ QName
qn Term
fn Term
l Term
r Type
t -> do
      forall (m :: * -> *) (t :: * -> *).
(Applicative m, Foldable t) =>
t (m Doc) -> m Doc
vcat
        [ forall (m :: * -> *) (t :: * -> *).
(Applicative m, Foldable t) =>
t (m Doc) -> m Doc
fsep (forall (m :: * -> *). Applicative m => [Char] -> [m Doc]
pwords [Char]
"when checking that a clause of" forall a. [a] -> [a] -> [a]
++ [forall a (m :: * -> *). (PrettyTCM a, MonadPretty m) => a -> m Doc
prettyTCM QName
qn] forall a. [a] -> [a] -> [a]
++ forall (m :: * -> *). Applicative m => [Char] -> [m Doc]
pwords [Char]
"has the correct boundary.")
        , m Doc
""
        , m Doc
"Specifically, the terms"
        , forall (m :: * -> *). Functor m => Int -> m Doc -> m Doc
nest Int
2 (forall a (m :: * -> *). (PrettyTCM a, MonadPretty m) => a -> m Doc
prettyTCM Term
l)
        , m Doc
"and"
        , forall (m :: * -> *). Functor m => Int -> m Doc -> m Doc
nest Int
2 (forall a (m :: * -> *). (PrettyTCM a, MonadPretty m) => a -> m Doc
prettyTCM Term
r)
        , forall (m :: * -> *) (t :: * -> *).
(Applicative m, Foldable t) =>
t (m Doc) -> m Doc
fsep (forall (m :: * -> *). Applicative m => [Char] -> [m Doc]
pwords [Char]
"must be equal, since" forall a. [a] -> [a] -> [a]
++ [forall a (m :: * -> *). (PrettyTCM a, MonadPretty m) => a -> m Doc
prettyTCM Term
fn] forall a. [a] -> [a] -> [a]
++ forall (m :: * -> *). Applicative m => [Char] -> [m Doc]
pwords [Char]
"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
      forall (m :: * -> *) a. ReadTCState m => Precedence -> m a -> m a
withContextPrecedence (ParenPreference -> Precedence
ArgumentCtx ParenPreference
PreferParen) forall a b. (a -> b) -> a -> b
$
        forall (m :: * -> *) a. (Applicative m, Pretty a) => a -> m Doc
pretty forall (m :: * -> *) a b. Monad m => (a -> m b) -> m a -> m b
=<< forall i a (m :: * -> *).
(LensHiding i, ToConcrete a, MonadAbsToCon m) =>
i -> a -> m (ConOfAbs a)
abstractToConcreteHiding NamedArg Expr
a NamedArg Expr
a