{-# OPTIONS_GHC -Wunused-imports #-}

module Mikan.TypeChecking.Pretty.Call where

import Prelude hiding ( null )

import Mikan.Syntax.Abstract as A
import Mikan.Syntax.Abstract.Views
import Mikan.Syntax.Common
import Mikan.Syntax.Common.Pretty qualified as P
import Mikan.Syntax.Concrete.Definitions qualified as D
import Mikan.Syntax.Info qualified as A
import Mikan.Syntax.Fixity
import Mikan.Syntax.Internal
import Mikan.Syntax.Position
import Mikan.Syntax.Scope.Monad
import Mikan.Syntax.Translation.AbstractToConcrete

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

import Mikan.Utils.Null

import Mikan.Utils.Impossible

import Mikan.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
_ Origin
_ 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__

    CheckIndexSort QName
d Type
i Sort
s -> [m Doc] -> m Doc
forall (m :: * -> *) (t :: * -> *).
(Applicative m, Foldable t) =>
t (m Doc) -> m Doc
sep ([m Doc] -> m Doc) -> [m Doc] -> m Doc
forall a b. (a -> b) -> a -> b
$
      [ m Doc
"when checking that the index"
      , 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
i m Doc -> m Doc -> m Doc
forall (m :: * -> *). Applicative m => m Doc -> m Doc -> m Doc
<+> m Doc
":" m Doc -> m Doc -> m Doc
forall (m :: * -> *). Applicative m => m Doc -> m Doc -> m Doc
<+> Sort -> m Doc
forall a (m :: * -> *). (PrettyTCM a, MonadPretty m) => a -> m Doc
forall (m :: * -> *). MonadPretty m => Sort -> m Doc
prettyTCM (Type -> Sort
forall a. LensSort a => a -> Sort
getSort Type
i)
      , m Doc
"fits in the sort"
      , 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
$ Sort -> m Doc
forall a (m :: * -> *). (PrettyTCM a, MonadPretty m) => a -> m Doc
forall (m :: * -> *). MonadPretty m => Sort -> m Doc
prettyTCM Sort
s
      , m Doc
"of the datatype" m Doc -> m Doc -> m Doc
forall (m :: * -> *). Applicative m => m Doc -> m Doc -> m Doc
<+> QName -> m Doc
forall a (m :: * -> *). (PrettyTCM a, MonadPretty m) => a -> m Doc
forall (m :: * -> *). MonadPretty m => QName -> m Doc
prettyTCM QName
d
      ]

    CheckConArgFitsIn QName
c Bool
f 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
$
      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
t] [m Doc] -> [m Doc] -> [m Doc]
forall a. [a] -> [a] -> [a]
++
      String -> [m Doc]
forall (m :: * -> *). Applicative m => String -> [m Doc]
pwords String
"of an argument to 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
"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
forall (m :: * -> *). MonadPretty m => Sort -> m Doc
prettyTCM Sort
s] [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 datatype."

    CheckFunDefCall Range
_ QName
f 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
url (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"]

    CheckWithFunctionLet Name
x (LetBinding IsAxiom
_ Origin
_ Term
v Dom Type
t) -> [m Doc] -> m Doc
forall (m :: * -> *) (t :: * -> *).
(Applicative m, Foldable t) =>
t (m Doc) -> m Doc
vcat
      [ m Doc
"when checking that the let-binding"
      , 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
$ [m Doc] -> m Doc
forall (m :: * -> *) (t :: * -> *).
(Applicative m, Foldable t) =>
t (m Doc) -> m Doc
fsep [Name -> m Doc
forall a (m :: * -> *). (PrettyTCM a, MonadPretty m) => a -> m Doc
forall (m :: * -> *). MonadPretty m => Name -> m Doc
prettyTCM Name
x, m Doc
"=", 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
":", Dom Type -> m Doc
forall a (m :: * -> *). (PrettyTCM a, MonadPretty m) => a -> m Doc
forall (m :: * -> *). MonadPretty m => Dom Type -> m Doc
prettyTCM Dom 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
"inherited by 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
url (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]

    CheckNonLocalWhere 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 non-local 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"

    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
_ ModuleName
m1 ModuleApplication
modapp -> do
      [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
-> ModuleName
-> ModuleApplication
-> ScopeCopyInfo
-> ImportDirective
-> Declaration
A.Apply ModuleInfo
info ModuleName
m1 ModuleApplication
modapp ScopeCopyInfo
copy ImportDirective
forall a. Null a => a
empty]
      where
      info :: ModuleInfo
info = Range
-> Range
-> Maybe Name
-> 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 OpenShortHand
forall a. Null a => a
empty Maybe ImportDirective
forall a. Maybe a
Nothing
      copy :: ScopeCopyInfo
copy = ScopeCopyInfo { renNames :: Ren QName
renNames = Ren QName
forall a. Monoid a => a
mempty, renModules :: Ren ModuleName
renModules = Ren ModuleName
forall a. Monoid a => a
mempty, renPublic :: Bool
renPublic = Bool
True, renTrimming :: ScopeCopyRef
renTrimming = ScopeCopyRef
forall a. HasCallStack => a
__IMPOSSIBLE__ }

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