{-# LANGUAGE NondecreasingIndentation #-}

{-# OPTIONS_GHC -fno-warn-orphans #-}

module Agda.TypeChecking.Errors
  ( prettyError
  , tcErrString
  , prettyTCWarnings'
  , prettyTCWarnings
  , tcWarningsToError
  , applyFlagsToTCWarningsPreserving
  , applyFlagsToTCWarnings
  , getAllUnsolvedWarnings
  , getAllWarningsPreserving
  , getAllWarnings
  , getAllWarningsOfTCErr
  , dropTopLevelModule
  , topLevelModuleDropper
  , stringTCErr
  , explainWhyInScope
  , Verbalize(verbalize)
  ) where

import Prelude hiding ( null, foldl )

import qualified Control.Exception as E
import Control.Monad.Except

import qualified Data.CaseInsensitive as CaseInsens
import Data.Foldable (foldl)
import Data.Function
import Data.List (sortBy, dropWhileEnd, intercalate)
import Data.Maybe
import qualified Data.Set as Set
import qualified Text.PrettyPrint.Boxes as Boxes

import Agda.Syntax.Common
import Agda.Syntax.Concrete.Definitions (notSoNiceDeclarations)
import Agda.Syntax.Concrete.Pretty (prettyHiding, prettyRelevance)
import Agda.Syntax.Notation
import Agda.Syntax.Position
import qualified Agda.Syntax.Concrete as C
import Agda.Syntax.Abstract as A
import Agda.Syntax.Internal as I
import Agda.Syntax.Translation.InternalToAbstract
import Agda.Syntax.Scope.Monad (isDatatypeModule)
import Agda.Syntax.Scope.Base

import Agda.TypeChecking.Monad.Base
import Agda.TypeChecking.Monad.Closure
import Agda.TypeChecking.Monad.Context
import Agda.TypeChecking.Monad.Debug
import Agda.TypeChecking.Monad.Env
import Agda.TypeChecking.Monad.Builtin
import Agda.TypeChecking.Monad.SizedTypes ( sizeType )
import Agda.TypeChecking.Monad.State
import Agda.TypeChecking.Pretty
import Agda.TypeChecking.Pretty.Call
import Agda.TypeChecking.Pretty.Warning
import Agda.TypeChecking.Substitute
import Agda.TypeChecking.Telescope ( ifPiType )
import Agda.TypeChecking.Reduce (instantiate)

import Agda.Utils.FileName
import Agda.Utils.Float  ( toStringWithoutDotZero )
import Agda.Utils.Function
import Agda.Utils.List   ( initLast )
import Agda.Utils.List1 (List1, pattern (:|))
import qualified Agda.Utils.List1 as List1
import Agda.Utils.Maybe
import Agda.Utils.Null
import Agda.Utils.Pretty ( prettyShow, render )
import qualified Agda.Utils.Pretty as P
import Agda.Utils.Size

import Agda.Utils.Impossible

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

{-# SPECIALIZE prettyError :: TCErr -> TCM String #-}
prettyError :: MonadTCM tcm => TCErr -> tcm String
prettyError :: forall (tcm :: * -> *). MonadTCM tcm => TCErr -> tcm [Char]
prettyError TCErr
err = forall (tcm :: * -> *) a. MonadTCM tcm => TCM a -> tcm a
liftTCM forall a b. (a -> b) -> a -> b
$ forall a. Show a => a -> [Char]
show forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> TCErr -> [TCErr] -> TCMT IO Doc
prettyError' TCErr
err []
  where
  prettyError' :: TCErr -> [TCErr] -> TCM Doc
  prettyError' :: TCErr -> [TCErr] -> TCMT IO Doc
prettyError' TCErr
err [TCErr]
errs
    | forall (t :: * -> *) a. Foldable t => t a -> Int
length [TCErr]
errs forall a. Ord a => a -> a -> Bool
> Int
3 = forall (m :: * -> *) (t :: * -> *).
(Applicative m, Foldable t) =>
t (m Doc) -> m Doc
fsep (
        forall (m :: * -> *). Applicative m => [Char] -> [m Doc]
pwords [Char]
"total panic: error when printing error from printing error from printing error." forall a. [a] -> [a] -> [a]
++
        forall (m :: * -> *). Applicative m => [Char] -> [m Doc]
pwords [Char]
"I give up! Approximations of errors (original error last):" )
        forall (m :: * -> *). Applicative m => m Doc -> m Doc -> m Doc
$$ forall (m :: * -> *) (t :: * -> *).
(Applicative m, Foldable t) =>
t (m Doc) -> m Doc
vcat (forall a b. (a -> b) -> [a] -> [b]
map (forall (m :: * -> *). Applicative m => [Char] -> m Doc
text forall b c a. (b -> c) -> (a -> b) -> a -> c
. TCErr -> [Char]
tcErrString) [TCErr]
errs)
    | Bool
otherwise = forall a. Bool -> (a -> a) -> a -> a
applyUnless (forall a. Null a => a -> Bool
null [TCErr]
errs) (TCMT IO Doc
"panic: error when printing error!" forall (m :: * -> *). Applicative m => m Doc -> m Doc -> m Doc
$$) forall a b. (a -> b) -> a -> b
$ do
        (forall a (m :: * -> *). (PrettyTCM a, MonadPretty m) => a -> m Doc
prettyTCM TCErr
err forall (m :: * -> *). Applicative m => m Doc -> m Doc -> m Doc
$$ forall (m :: * -> *) (t :: * -> *).
(Applicative m, Foldable t) =>
t (m Doc) -> m Doc
vcat (forall a b. (a -> b) -> [a] -> [b]
map (forall (m :: * -> *). Applicative m => [Char] -> m Doc
text forall b c a. (b -> c) -> (a -> b) -> a -> c
. ([Char]
"when printing error " forall a. [a] -> [a] -> [a]
++) forall b c a. (b -> c) -> (a -> b) -> a -> c
. TCErr -> [Char]
tcErrString) [TCErr]
errs))
        forall e (m :: * -> *) a.
MonadError e m =>
m a -> (e -> m a) -> m a
`catchError` \ TCErr
err' -> TCErr -> [TCErr] -> TCMT IO Doc
prettyError' TCErr
err' (TCErr
errforall a. a -> [a] -> [a]
:[TCErr]
errs)

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

panic :: Monad m => String -> m Doc
panic :: forall (m :: * -> *). Monad m => [Char] -> m Doc
panic [Char]
s = forall (m :: * -> *). Applicative m => [Char] -> m Doc
fwords forall a b. (a -> b) -> a -> b
$ [Char]
"Panic: " forall a. [a] -> [a] -> [a]
++ [Char]
s

nameWithBinding :: MonadPretty m => QName -> m Doc
nameWithBinding :: forall (m :: * -> *). MonadPretty m => QName -> m Doc
nameWithBinding QName
q =
  (forall a (m :: * -> *). (PrettyTCM a, MonadPretty m) => a -> m Doc
prettyTCM QName
q forall (m :: * -> *). Applicative m => m Doc -> m Doc -> m Doc
<+> m Doc
"bound at") forall (m :: * -> *). Applicative m => m Doc -> m Doc -> m Doc
<?> forall a (m :: * -> *). (PrettyTCM a, MonadPretty m) => a -> m Doc
prettyTCM Range
r
  where
    r :: Range
r = Name -> Range
nameBindingSite forall a b. (a -> b) -> a -> b
$ QName -> Name
qnameName QName
q

tcErrString :: TCErr -> String
tcErrString :: TCErr -> [Char]
tcErrString TCErr
err = forall a. Pretty a => a -> [Char]
prettyShow (forall a. HasRange a => a -> Range
getRange TCErr
err) forall a. [a] -> [a] -> [a]
++ [Char]
" " forall a. [a] -> [a] -> [a]
++ case TCErr
err of
  TypeError CallStack
_ TCState
_ Closure TypeError
cl  -> TypeError -> [Char]
errorString forall a b. (a -> b) -> a -> b
$ forall a. Closure a -> a
clValue Closure TypeError
cl
  Exception Range
r Doc
s     -> forall a. Pretty a => a -> [Char]
prettyShow Range
r forall a. [a] -> [a] -> [a]
++ [Char]
" " forall a. [a] -> [a] -> [a]
++ forall a. Show a => a -> [Char]
show Doc
s
  IOException TCState
_ Range
r IOException
e -> forall a. Pretty a => a -> [Char]
prettyShow Range
r forall a. [a] -> [a] -> [a]
++ [Char]
" " forall a. [a] -> [a] -> [a]
++ forall e. Exception e => e -> [Char]
E.displayException IOException
e
  PatternErr{}      -> [Char]
"PatternErr"

stringTCErr :: String -> TCErr
stringTCErr :: [Char] -> TCErr
stringTCErr = Range -> Doc -> TCErr
Exception forall a. Range' a
noRange forall b c a. (b -> c) -> (a -> b) -> a -> c
. [Char] -> Doc
P.text

errorString :: TypeError -> String
errorString :: TypeError -> [Char]
errorString TypeError
err = case TypeError
err of
  AmbiguousModule{}                        -> [Char]
"AmbiguousModule"
  AmbiguousName{}                          -> [Char]
"AmbiguousName"
  AmbiguousParseForApplication{}           -> [Char]
"AmbiguousParseForApplication"
  AmbiguousParseForLHS{}                   -> [Char]
"AmbiguousParseForLHS"
--  AmbiguousParseForPatternSynonym{}        -> "AmbiguousParseForPatternSynonym"
  AmbiguousTopLevelModuleName {}           -> [Char]
"AmbiguousTopLevelModuleName"
  BadArgumentsToPatternSynonym{}           -> [Char]
"BadArgumentsToPatternSynonym"
  TooFewArgumentsToPatternSynonym{}        -> [Char]
"TooFewArgumentsToPatternSynonym"
  CannotResolveAmbiguousPatternSynonym{}   -> [Char]
"CannotResolveAmbiguousPatternSynonym"
  TypeError
BothWithAndRHS                           -> [Char]
"BothWithAndRHS"
  BuiltinInParameterisedModule{}           -> [Char]
"BuiltinInParameterisedModule"
  BuiltinMustBeConstructor{}               -> [Char]
"BuiltinMustBeConstructor"
  ClashingDefinition{}                     -> [Char]
"ClashingDefinition"
  ClashingFileNamesFor{}                   -> [Char]
"ClashingFileNamesFor"
  ClashingImport{}                         -> [Char]
"ClashingImport"
  ClashingModule{}                         -> [Char]
"ClashingModule"
  ClashingModuleImport{}                   -> [Char]
"ClashingModuleImport"
  CompilationError{}                       -> [Char]
"CompilationError"
  ConstructorPatternInWrongDatatype{}      -> [Char]
"ConstructorPatternInWrongDatatype"
  CyclicModuleDependency{}                 -> [Char]
"CyclicModuleDependency"
  DataMustEndInSort{}                      -> [Char]
"DataMustEndInSort"
-- UNUSED:    DataTooManyParameters{}                  -> "DataTooManyParameters"
  CantResolveOverloadedConstructorsTargetingSameDatatype{} -> [Char]
"CantResolveOverloadedConstructorsTargetingSameDatatype"
  DoesNotConstructAnElementOf{}            -> [Char]
"DoesNotConstructAnElementOf"
  DuplicateBuiltinBinding{}                -> [Char]
"DuplicateBuiltinBinding"
  DuplicateConstructors{}                  -> [Char]
"DuplicateConstructors"
  DuplicateFields{}                        -> [Char]
"DuplicateFields"
  DuplicateImports{}                       -> [Char]
"DuplicateImports"
  TypeError
FieldOutsideRecord                       -> [Char]
"FieldOutsideRecord"
  FileNotFound{}                           -> [Char]
"FileNotFound"
  GenericError{}                           -> [Char]
"GenericError"
  GenericDocError{}                        -> [Char]
"GenericDocError"
  InstanceNoCandidate{}                    -> [Char]
"InstanceNoCandidate"
  IllformedProjectionPattern{}             -> [Char]
"IllformedProjectionPattern"
  CannotEliminateWithPattern{}             -> [Char]
"CannotEliminateWithPattern"
  IllegalLetInTelescope{}                  -> [Char]
"IllegalLetInTelescope"
  IllegalPatternInTelescope{}              -> [Char]
"IllegalPatternInTelescope"
-- UNUSED:  IncompletePatternMatching{}              -> "IncompletePatternMatching"
  InternalError{}                          -> [Char]
"InternalError"
  InvalidPattern{}                         -> [Char]
"InvalidPattern"
  LocalVsImportedModuleClash{}             -> [Char]
"LocalVsImportedModuleClash"
  MetaCannotDependOn{}                     -> [Char]
"MetaCannotDependOn"
  MetaOccursInItself{}                     -> [Char]
"MetaOccursInItself"
  MetaIrrelevantSolution{}                 -> [Char]
"MetaIrrelevantSolution"
  MetaErasedSolution{}                     -> [Char]
"MetaErasedSolution"
  ModuleArityMismatch{}                    -> [Char]
"ModuleArityMismatch"
  ModuleDefinedInOtherFile {}              -> [Char]
"ModuleDefinedInOtherFile"
  ModuleNameUnexpected{}                   -> [Char]
"ModuleNameUnexpected"
  ModuleNameDoesntMatchFileName {}         -> [Char]
"ModuleNameDoesntMatchFileName"
  NeedOptionCopatterns{}                   -> [Char]
"NeedOptionCopatterns"
  NeedOptionRewriting{}                    -> [Char]
"NeedOptionRewriting"
  NeedOptionProp{}                         -> [Char]
"NeedOptionProp"
  NeedOptionTwoLevel{}                     -> [Char]
"NeedOptionTwoLevel"
  GeneralizeNotSupportedHere{}             -> [Char]
"GeneralizeNotSupportedHere"
  GeneralizeCyclicDependency{}             -> [Char]
"GeneralizeCyclicDependency"
  GeneralizeUnsolvedMeta{}                 -> [Char]
"GeneralizeUnsolvedMeta"
  MultipleFixityDecls{}                    -> [Char]
"MultipleFixityDecls"
  MultiplePolarityPragmas{}                -> [Char]
"MultiplePolarityPragmas"
  NoBindingForBuiltin{}                    -> [Char]
"NoBindingForBuiltin"
  NoParseForApplication{}                  -> [Char]
"NoParseForApplication"
  NoParseForLHS{}                          -> [Char]
"NoParseForLHS"
--  NoParseForPatternSynonym{}               -> "NoParseForPatternSynonym"
  NoRHSRequiresAbsurdPattern{}             -> [Char]
"NoRHSRequiresAbsurdPattern"
  NoSuchBuiltinName{}                      -> [Char]
"NoSuchBuiltinName"
  NoSuchModule{}                           -> [Char]
"NoSuchModule"
  DuplicatePrimitiveBinding{}              -> [Char]
"DuplicatePrimitiveBinding"
  NoSuchPrimitiveFunction{}                -> [Char]
"NoSuchPrimitiveFunction"
  WrongModalityForPrimitive{}              -> [Char]
"WrongModalityForPrimitive"
  NotAModuleExpr{}                         -> [Char]
"NotAModuleExpr"
  TypeError
NotAProperTerm                           -> [Char]
"NotAProperTerm"
  InvalidType{}                            -> [Char]
"InvalidType"
  InvalidTypeSort{}                        -> [Char]
"InvalidTypeSort"
  FunctionTypeInSizeUniv{}                 -> [Char]
"FunctionTypeInSizeUniv"
  NotAValidLetBinding{}                    -> [Char]
"NotAValidLetBinding"
  NotValidBeforeField{}                    -> [Char]
"NotValidBeforeField"
  NotAnExpression{}                        -> [Char]
"NotAnExpression"
  NotImplemented{}                         -> [Char]
"NotImplemented"
  NotSupported{}                           -> [Char]
"NotSupported"
  AbstractConstructorNotInScope{}          -> [Char]
"AbstractConstructorNotInScope"
  NotInScope{}                             -> [Char]
"NotInScope"
  NotLeqSort{}                             -> [Char]
"NotLeqSort"
  NothingAppliedToHiddenArg{}              -> [Char]
"NothingAppliedToHiddenArg"
  NothingAppliedToInstanceArg{}            -> [Char]
"NothingAppliedToInstanceArg"
  OverlappingProjects {}                   -> [Char]
"OverlappingProjects"
  OperatorInformation {}                   -> [Char]
"OperatorInformation"
  PatternShadowsConstructor {}             -> [Char]
"PatternShadowsConstructor"
  TypeError
PropMustBeSingleton                      -> [Char]
"PropMustBeSingleton"
  RepeatedVariablesInPattern{}             -> [Char]
"RepeatedVariablesInPattern"
  ShadowedModule{}                         -> [Char]
"ShadowedModule"
  ShouldBeASort{}                          -> [Char]
"ShouldBeASort"
  ShouldBeApplicationOf{}                  -> [Char]
"ShouldBeApplicationOf"
  ShouldBeAppliedToTheDatatypeParameters{} -> [Char]
"ShouldBeAppliedToTheDatatypeParameters"
  ShouldBeEmpty{}                          -> [Char]
"ShouldBeEmpty"
  ShouldBePi{}                             -> [Char]
"ShouldBePi"
  ShouldBePath{}                           -> [Char]
"ShouldBePath"
  ShouldBeRecordType{}                     -> [Char]
"ShouldBeRecordType"
  ShouldBeRecordPattern{}                  -> [Char]
"ShouldBeRecordPattern"
  NotAProjectionPattern{}                  -> [Char]
"NotAProjectionPattern"
  ShouldEndInApplicationOfTheDatatype{}    -> [Char]
"ShouldEndInApplicationOfTheDatatype"
  SplitError{}                             -> [Char]
"SplitError"
  ImpossibleConstructor{}                  -> [Char]
"ImpossibleConstructor"
  TooManyFields{}                          -> [Char]
"TooManyFields"
  TooManyPolarities{}                      -> [Char]
"TooManyPolarities"
  SplitOnIrrelevant{}                      -> [Char]
"SplitOnIrrelevant"
  SplitOnUnusableCohesion{}                -> [Char]
"SplitOnUnusableCohesion"
  -- UNUSED: -- SplitOnErased{}                          -> "SplitOnErased"
  SplitOnNonVariable{}                     -> [Char]
"SplitOnNonVariable"
  SplitOnNonEtaRecord{}                    -> [Char]
"SplitOnNonEtaRecord"
  DefinitionIsIrrelevant{}                 -> [Char]
"DefinitionIsIrrelevant"
  DefinitionIsErased{}                     -> [Char]
"DefinitionIsErased"
  VariableIsIrrelevant{}                   -> [Char]
"VariableIsIrrelevant"
  VariableIsErased{}                       -> [Char]
"VariableIsErased"
  VariableIsOfUnusableCohesion{}           -> [Char]
"VariableIsOfUnusableCohesion"
  UnequalBecauseOfUniverseConflict{}       -> [Char]
"UnequalBecauseOfUniverseConflict"
  UnequalRelevance{}                       -> [Char]
"UnequalRelevance"
  UnequalQuantity{}                        -> [Char]
"UnequalQuantity"
  UnequalCohesion{}                        -> [Char]
"UnequalCohesion"
  UnequalFiniteness{}                      -> [Char]
"UnequalFiniteness"
  UnequalHiding{}                          -> [Char]
"UnequalHiding"
  UnequalLevel{}                           -> [Char]
"UnequalLevel"
  UnequalSorts{}                           -> [Char]
"UnequalSorts"
  UnequalTerms{}                           -> [Char]
"UnequalTerms"
  UnequalTypes{}                           -> [Char]
"UnequalTypes"
--  UnequalTelescopes{}                      -> "UnequalTelescopes" -- UNUSED
  WithOnFreeVariable{}                     -> [Char]
"WithOnFreeVariable"
  UnexpectedWithPatterns{}                 -> [Char]
"UnexpectedWithPatterns"
  UninstantiatedDotPattern{}               -> [Char]
"UninstantiatedDotPattern"
  ForcedConstructorNotInstantiated{}       -> [Char]
"ForcedConstructorNotInstantiated"
  SolvedButOpenHoles{}                     -> [Char]
"SolvedButOpenHoles"
  TypeError
UnusedVariableInPatternSynonym           -> [Char]
"UnusedVariableInPatternSynonym"
  UnquoteFailed{}                          -> [Char]
"UnquoteFailed"
  DeBruijnIndexOutOfScope{}                -> [Char]
"DeBruijnIndexOutOfScope"
  WithClausePatternMismatch{}              -> [Char]
"WithClausePatternMismatch"
  WrongHidingInApplication{}               -> [Char]
"WrongHidingInApplication"
  WrongHidingInLHS{}                       -> [Char]
"WrongHidingInLHS"
  WrongHidingInLambda{}                    -> [Char]
"WrongHidingInLambda"
  WrongIrrelevanceInLambda{}               -> [Char]
"WrongIrrelevanceInLambda"
  WrongQuantityInLambda{}                  -> [Char]
"WrongQuantityInLambda"
  WrongCohesionInLambda{}                  -> [Char]
"WrongCohesionInLambda"
  WrongNamedArgument{}                     -> [Char]
"WrongNamedArgument"
  WrongNumberOfConstructorArguments{}      -> [Char]
"WrongNumberOfConstructorArguments"
  QuantityMismatch{}                       -> [Char]
"QuantityMismatch"
  HidingMismatch{}                         -> [Char]
"HidingMismatch"
  RelevanceMismatch{}                      -> [Char]
"RelevanceMismatch"
  NonFatalErrors{}                         -> [Char]
"NonFatalErrors"
  InstanceSearchDepthExhausted{}           -> [Char]
"InstanceSearchDepthExhausted"
  TriedToCopyConstrainedPrim{}             -> [Char]
"TriedToCopyConstrainedPrim"
  SortOfSplitVarError{}                    -> [Char]
"SortOfSplitVarError"

instance PrettyTCM TCErr where
  prettyTCM :: forall (m :: * -> *). MonadPretty m => TCErr -> m Doc
prettyTCM TCErr
err = case TCErr
err of
    -- Gallais, 2016-05-14
    -- Given where `NonFatalErrors` are created, we know for a
    -- fact that ̀ws` is non-empty.
    TypeError CallStack
loc TCState
_ Closure{ clValue :: forall a. Closure a -> a
clValue = NonFatalErrors [TCWarning]
ws } -> do
      forall (m :: * -> *).
MonadDebug m =>
[Char] -> Int -> [Char] -> m ()
reportSLn [Char]
"error" Int
2 forall a b. (a -> b) -> a -> b
$ [Char]
"Error raised at " forall a. [a] -> [a] -> [a]
++ forall a. Pretty a => a -> [Char]
prettyShow CallStack
loc
      forall (t :: * -> *) a. Foldable t => (a -> a -> a) -> t a -> a
foldr1 forall (m :: * -> *). Applicative m => m Doc -> m Doc -> m Doc
($$) forall a b. (a -> b) -> a -> b
$ forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap forall a (m :: * -> *). (PrettyTCM a, MonadPretty m) => a -> m Doc
prettyTCM [TCWarning]
ws
    -- Andreas, 2014-03-23
    -- This use of withTCState seems ok since we do not collect
    -- Benchmark info during printing errors.
    TypeError CallStack
loc TCState
s Closure TypeError
e -> forall (m :: * -> *) a.
ReadTCState m =>
(TCState -> TCState) -> m a -> m a
withTCState (forall a b. a -> b -> a
const TCState
s) forall a b. (a -> b) -> a -> b
$ do
      forall (m :: * -> *).
MonadDebug m =>
[Char] -> Int -> [Char] -> m ()
reportSLn [Char]
"error" Int
2 forall a b. (a -> b) -> a -> b
$ [Char]
"Error raised at " forall a. [a] -> [a] -> [a]
++ forall a. Pretty a => a -> [Char]
prettyShow CallStack
loc
      forall (m :: * -> *).
MonadPretty m =>
Range -> Maybe (Closure Call) -> m Doc -> m Doc
sayWhen (TCEnv -> Range
envRange forall a b. (a -> b) -> a -> b
$ forall a. Closure a -> TCEnv
clEnv Closure TypeError
e) (TCEnv -> Maybe (Closure Call)
envCall forall a b. (a -> b) -> a -> b
$ forall a. Closure a -> TCEnv
clEnv Closure TypeError
e) forall a b. (a -> b) -> a -> b
$ forall a (m :: * -> *). (PrettyTCM a, MonadPretty m) => a -> m Doc
prettyTCM Closure TypeError
e
    Exception Range
r Doc
s     -> forall (m :: * -> *) a.
(MonadPretty m, HasRange a) =>
a -> m Doc -> m Doc
sayWhere Range
r forall a b. (a -> b) -> a -> b
$ forall (m :: * -> *) a. Monad m => a -> m a
return Doc
s
    IOException TCState
_ Range
r IOException
e -> forall (m :: * -> *) a.
(MonadPretty m, HasRange a) =>
a -> m Doc -> m Doc
sayWhere Range
r forall a b. (a -> b) -> a -> b
$ forall (m :: * -> *). Applicative m => [Char] -> m Doc
fwords forall a b. (a -> b) -> a -> b
$ forall a. Show a => a -> [Char]
show IOException
e
    PatternErr{}      -> forall (m :: * -> *) a.
(MonadPretty m, HasRange a) =>
a -> m Doc -> m Doc
sayWhere TCErr
err forall a b. (a -> b) -> a -> b
$ forall (m :: * -> *). Monad m => [Char] -> m Doc
panic [Char]
"uncaught pattern violation"

-- | Drops given amount of leading components of the qualified name.
dropTopLevelModule' :: Int -> QName -> QName
dropTopLevelModule' :: Int -> QName -> QName
dropTopLevelModule' Int
k (QName (MName [Name]
ns) Name
n) = ModuleName -> Name -> QName
QName ([Name] -> ModuleName
MName (forall a. Int -> [a] -> [a]
drop Int
k [Name]
ns)) Name
n

-- | Drops the filename component of the qualified name.
dropTopLevelModule :: QName -> TCM QName
dropTopLevelModule :: QName -> TCM QName
dropTopLevelModule QName
q = (forall a b. (a -> b) -> a -> b
$ QName
q) forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> forall (m :: * -> *).
(MonadDebug m, MonadTCEnv m, ReadTCState m) =>
m (QName -> QName)
topLevelModuleDropper

-- | Produces a function which drops the filename component of the qualified name.
topLevelModuleDropper :: (MonadDebug m, MonadTCEnv m, ReadTCState m) => m (QName -> QName)
topLevelModuleDropper :: forall (m :: * -> *).
(MonadDebug m, MonadTCEnv m, ReadTCState m) =>
m (QName -> QName)
topLevelModuleDropper =
  forall (m :: * -> *) a b.
Monad m =>
m (Maybe a) -> m b -> (a -> m b) -> m b
caseMaybeM forall (m :: * -> *).
(MonadTCEnv m, ReadTCState m) =>
m (Maybe TopLevelModuleName)
currentTopLevelModule
    (forall (m :: * -> *) a. Monad m => a -> m a
return forall a. a -> a
id)
    (forall (m :: * -> *) a. Monad m => a -> m a
return forall b c a. (b -> c) -> (a -> b) -> a -> c
. Int -> QName -> QName
dropTopLevelModule' forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall a. Sized a => a -> Int
size)

instance PrettyTCM TypeError where
  prettyTCM :: forall (m :: * -> *). MonadPretty m => TypeError -> m Doc
prettyTCM TypeError
err = case TypeError
err of
    InternalError [Char]
s -> forall (m :: * -> *). Monad m => [Char] -> m Doc
panic [Char]
s

    NotImplemented [Char]
s -> forall (m :: * -> *). Applicative m => [Char] -> m Doc
fwords forall a b. (a -> b) -> a -> b
$ [Char]
"Not implemented: " forall a. [a] -> [a] -> [a]
++ [Char]
s

    NotSupported [Char]
s -> forall (m :: * -> *). Applicative m => [Char] -> m Doc
fwords forall a b. (a -> b) -> a -> b
$ [Char]
"Not supported: " forall a. [a] -> [a] -> [a]
++ [Char]
s

    CompilationError [Char]
s -> forall (m :: * -> *) (t :: * -> *).
(Applicative m, Foldable t) =>
t (m Doc) -> m Doc
sep [forall (m :: * -> *). Applicative m => [Char] -> m Doc
fwords [Char]
"Compilation error:", forall (m :: * -> *). Applicative m => [Char] -> m Doc
text [Char]
s]

    GenericError [Char]
s -> forall (m :: * -> *). Applicative m => [Char] -> m Doc
fwords [Char]
s

    GenericDocError Doc
d -> forall (m :: * -> *) a. Monad m => a -> m a
return Doc
d

    TypeError
PropMustBeSingleton -> forall (m :: * -> *). Applicative m => [Char] -> m Doc
fwords
      [Char]
"Datatypes in Prop must have at most one constructor when proof irrelevance is enabled"

    DataMustEndInSort Term
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]
"The type of a datatype must end in a sort."
      forall a. [a] -> [a] -> [a]
++ [forall a (m :: * -> *). (PrettyTCM a, MonadPretty m) => a -> m Doc
prettyTCM Term
t] forall a. [a] -> [a] -> [a]
++ forall (m :: * -> *). Applicative m => [Char] -> [m Doc]
pwords [Char]
"isn't a sort."

{- UNUSED:
    DataTooManyParameters -> fsep $ pwords "Too many parameters given to data type."
-}

    ShouldEndInApplicationOfTheDatatype 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]
"The target of a constructor must be the datatype applied to its parameters,"
      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]
"isn't"

    ShouldBeAppliedToTheDatatypeParameters Term
s Term
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]
"The target of the constructor should be" forall a. [a] -> [a] -> [a]
++ [forall a (m :: * -> *). (PrettyTCM a, MonadPretty m) => a -> m Doc
prettyTCM Term
s] forall a. [a] -> [a] -> [a]
++
      forall (m :: * -> *). Applicative m => [Char] -> [m Doc]
pwords [Char]
"instead of" forall a. [a] -> [a] -> [a]
++ [forall a (m :: * -> *). (PrettyTCM a, MonadPretty m) => a -> m Doc
prettyTCM Term
t]

    ShouldBeApplicationOf Type
t QName
q -> 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]
"The pattern constructs an element of" forall a. [a] -> [a] -> [a]
++ [forall a (m :: * -> *). (PrettyTCM a, MonadPretty m) => a -> m Doc
prettyTCM QName
q] forall a. [a] -> [a] -> [a]
++
      forall (m :: * -> *). Applicative m => [Char] -> [m Doc]
pwords [Char]
"which is not the right datatype"

    ShouldBeRecordType 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]
"Expected non-abstract record type, found " forall a. [a] -> [a] -> [a]
++ [forall a (m :: * -> *). (PrettyTCM a, MonadPretty m) => a -> m Doc
prettyTCM Type
t]

    ShouldBeRecordPattern DeBruijnPattern
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]
"Expected record pattern" -- ", found " ++ [prettyTCM p]

    NotAProjectionPattern NamedArg 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]
"Not a valid projection for a copattern: " forall a. [a] -> [a] -> [a]
++ [ forall a (m :: * -> *).
(ToConcrete a, Pretty (ConOfAbs a), MonadAbsToCon m) =>
a -> m Doc
prettyA NamedArg Pattern
p ]

    TypeError
WrongHidingInLHS -> forall (m :: * -> *). Applicative m => [Char] -> m Doc
fwords [Char]
"Unexpected implicit argument"

    WrongHidingInLambda Type
t ->
      forall (m :: * -> *). Applicative m => [Char] -> m Doc
fwords [Char]
"Found an implicit lambda where an explicit lambda was expected"

    TypeError
WrongIrrelevanceInLambda ->
      forall (m :: * -> *). Applicative m => [Char] -> m Doc
fwords [Char]
"Found a non-strict lambda where a irrelevant lambda was expected"

    TypeError
WrongQuantityInLambda ->
      forall (m :: * -> *). Applicative m => [Char] -> m Doc
fwords [Char]
"Incorrect quantity annotation in lambda"

    TypeError
WrongCohesionInLambda ->
      forall (m :: * -> *). Applicative m => [Char] -> m Doc
fwords [Char]
"Incorrect cohesion annotation in lambda"

    WrongNamedArgument NamedArg Expr
a [NamedName]
xs0 -> 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]
"Function does not accept argument "
      forall a. [a] -> [a] -> [a]
++ [forall a (m :: * -> *). (PrettyTCM a, MonadPretty m) => a -> m Doc
prettyTCM NamedArg Expr
a] -- ++ pwords " (wrong argument name)"
      forall a. [a] -> [a] -> [a]
++ [forall (m :: * -> *). Functor m => m Doc -> m Doc
parens 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
text [Char]
"possible arguments:" forall a. a -> [a] -> [a]
: forall a b. (a -> b) -> [a] -> [b]
map forall (m :: * -> *) a. (Applicative m, Pretty a) => a -> m Doc
pretty [NamedName]
xs | Bool -> Bool
not (forall a. Null a => a -> Bool
null [NamedName]
xs)]
      where
      xs :: [NamedName]
xs = forall a. (a -> Bool) -> [a] -> [a]
filter (Bool -> Bool
not forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall a. IsNoName a => a -> Bool
isNoName) [NamedName]
xs0

    WrongHidingInApplication Type
t ->
      forall (m :: * -> *). Applicative m => [Char] -> m Doc
fwords [Char]
"Found an implicit application where an explicit application was expected"

    HidingMismatch Hiding
h Hiding
h' -> forall (m :: * -> *). Applicative m => [Char] -> m Doc
fwords forall a b. (a -> b) -> a -> b
$
      [Char]
"Expected " forall a. [a] -> [a] -> [a]
++ forall a. Verbalize a => a -> [Char]
verbalize (forall a. a -> Indefinite a
Indefinite Hiding
h') forall a. [a] -> [a] -> [a]
++ [Char]
" argument, but found " forall a. [a] -> [a] -> [a]
++
      forall a. Verbalize a => a -> [Char]
verbalize (forall a. a -> Indefinite a
Indefinite Hiding
h) forall a. [a] -> [a] -> [a]
++ [Char]
" argument"

    RelevanceMismatch Relevance
r Relevance
r' -> forall (m :: * -> *). Applicative m => [Char] -> m Doc
fwords forall a b. (a -> b) -> a -> b
$
      [Char]
"Expected " forall a. [a] -> [a] -> [a]
++ forall a. Verbalize a => a -> [Char]
verbalize (forall a. a -> Indefinite a
Indefinite Relevance
r') forall a. [a] -> [a] -> [a]
++ [Char]
" argument, but found " forall a. [a] -> [a] -> [a]
++
      forall a. Verbalize a => a -> [Char]
verbalize (forall a. a -> Indefinite a
Indefinite Relevance
r) forall a. [a] -> [a] -> [a]
++ [Char]
" argument"

    QuantityMismatch Quantity
q Quantity
q' -> forall (m :: * -> *). Applicative m => [Char] -> m Doc
fwords forall a b. (a -> b) -> a -> b
$
      [Char]
"Expected " forall a. [a] -> [a] -> [a]
++ forall a. Verbalize a => a -> [Char]
verbalize (forall a. a -> Indefinite a
Indefinite Quantity
q') forall a. [a] -> [a] -> [a]
++ [Char]
" argument, but found " forall a. [a] -> [a] -> [a]
++
      forall a. Verbalize a => a -> [Char]
verbalize (forall a. a -> Indefinite a
Indefinite Quantity
q) forall a. [a] -> [a] -> [a]
++ [Char]
" argument"

    UninstantiatedDotPattern 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]
"Failed to infer the value of dotted pattern"

    ForcedConstructorNotInstantiated 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]
"Failed to infer that constructor 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]
" is forced"

    IllformedProjectionPattern 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]
"Ill-formed projection pattern " forall a. [a] -> [a] -> [a]
++ [forall a (m :: * -> *).
(ToConcrete a, Pretty (ConOfAbs a), MonadAbsToCon m) =>
a -> m Doc
prettyA Pattern
p]

    CannotEliminateWithPattern Maybe Blocker
b NamedArg Pattern
p Type
a -> do
      let isProj :: Bool
isProj = forall a. Maybe a -> Bool
isJust (forall a. IsProjP a => a -> Maybe (ProjOrigin, AmbiguousQName)
isProjP NamedArg 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]
"Cannot eliminate type" forall a. [a] -> [a] -> [a]
++ forall a (m :: * -> *). (PrettyTCM a, MonadPretty m) => a -> m Doc
prettyTCM Type
a forall a. a -> [a] -> [a]
: if
         | Bool
isProj -> forall (m :: * -> *). Applicative m => [Char] -> [m Doc]
pwords [Char]
"with projection pattern" forall a. [a] -> [a] -> [a]
++ [forall a (m :: * -> *).
(ToConcrete a, Pretty (ConOfAbs a), MonadAbsToCon m) =>
a -> m Doc
prettyA NamedArg Pattern
p]
         | A.ProjP PatInfo
_ ProjOrigin
_ AmbiguousQName
f <- forall a. NamedArg a -> a
namedArg NamedArg Pattern
p -> forall (m :: * -> *). Applicative m => [Char] -> [m Doc]
pwords [Char]
"with pattern" forall a. [a] -> [a] -> [a]
++ [forall a (m :: * -> *).
(ToConcrete a, Pretty (ConOfAbs a), MonadAbsToCon m) =>
a -> m Doc
prettyA NamedArg Pattern
p] forall a. [a] -> [a] -> [a]
++
             forall (m :: * -> *). Applicative m => [Char] -> [m Doc]
pwords [Char]
"(suggestion: write" forall a. [a] -> [a] -> [a]
++ [m Doc
".(" forall a. Semigroup a => a -> a -> a
<> forall a (m :: * -> *).
(ToConcrete a, Pretty (ConOfAbs a), MonadAbsToCon m) =>
a -> m Doc
prettyA (ProjOrigin -> AmbiguousQName -> Expr
A.Proj ProjOrigin
ProjPrefix AmbiguousQName
f) forall a. Semigroup a => a -> a -> a
<> m Doc
")"] forall a. [a] -> [a] -> [a]
++ forall (m :: * -> *). Applicative m => [Char] -> [m Doc]
pwords [Char]
"for a dot pattern," forall a. [a] -> [a] -> [a]
++
             forall (m :: * -> *). Applicative m => [Char] -> [m Doc]
pwords [Char]
"or remove the braces for a postfix projection)"
         | Bool
otherwise ->
             m Doc
"with" forall a. a -> [a] -> [a]
: forall (m :: * -> *). Applicative m => [Char] -> m Doc
text (forall {e}. Pattern' e -> [Char]
kindOfPattern (forall a. NamedArg a -> a
namedArg NamedArg Pattern
p)) forall a. a -> [a] -> [a]
: m Doc
"pattern" forall a. a -> [a] -> [a]
: forall a (m :: * -> *).
(ToConcrete a, Pretty (ConOfAbs a), MonadAbsToCon m) =>
a -> m Doc
prettyA NamedArg Pattern
p forall a. a -> [a] -> [a]
:
             forall (m :: * -> *). Applicative m => [Char] -> [m Doc]
pwords [Char]
"(did you supply too many arguments?)"
      where
      kindOfPattern :: Pattern' e -> [Char]
kindOfPattern = \case
        A.VarP{}    -> [Char]
"variable"
        A.ConP{}    -> [Char]
"constructor"
        A.ProjP{}   -> forall a. HasCallStack => a
__IMPOSSIBLE__
        A.DefP{}    -> forall a. HasCallStack => a
__IMPOSSIBLE__
        A.WildP{}   -> [Char]
"wildcard"
        A.DotP{}    -> [Char]
"dot"
        A.AbsurdP{} -> [Char]
"absurd"
        A.LitP{}    -> [Char]
"literal"
        A.RecP{}    -> [Char]
"record"
        A.WithP{}   -> [Char]
"with"
        A.EqualP{}  -> [Char]
"equality"
        A.AsP PatInfo
_ BindName
_ Pattern' e
p -> Pattern' e -> [Char]
kindOfPattern Pattern' e
p
        A.PatternSynP{} -> forall a. HasCallStack => a
__IMPOSSIBLE__
        A.AnnP PatInfo
_ e
_ Pattern' e
p -> Pattern' e -> [Char]
kindOfPattern Pattern' e
p

    WrongNumberOfConstructorArguments QName
c Int
expect Int
given -> 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]
"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]
"expects" forall a. [a] -> [a] -> [a]
++ [forall a (m :: * -> *). (PrettyTCM a, MonadPretty m) => a -> m Doc
prettyTCM Int
expect] forall a. [a] -> [a] -> [a]
++
      forall (m :: * -> *). Applicative m => [Char] -> [m Doc]
pwords [Char]
"arguments (including hidden ones), but has been given"
      forall a. [a] -> [a] -> [a]
++ [forall a (m :: * -> *). (PrettyTCM a, MonadPretty m) => a -> m Doc
prettyTCM Int
given] forall a. [a] -> [a] -> [a]
++ forall (m :: * -> *). Applicative m => [Char] -> [m Doc]
pwords [Char]
"(including hidden ones)"

    CantResolveOverloadedConstructorsTargetingSameDatatype QName
d List1 QName
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]
"Can't resolve overloaded constructors targeting the same datatype"
      forall a. [a] -> [a] -> [a]
++ [forall (m :: * -> *). Functor m => m Doc -> m Doc
parens (forall a (m :: * -> *). (PrettyTCM a, MonadPretty m) => a -> m Doc
prettyTCM (QName -> QName
qnameToConcrete QName
d)) forall a. Semigroup a => a -> a -> a
<> forall (m :: * -> *). Applicative m => m Doc
colon]
      forall a. [a] -> [a] -> [a]
++ forall a b. (a -> b) -> [a] -> [b]
map forall (m :: * -> *) a. (Applicative m, Pretty a) => a -> m Doc
pretty (forall l. IsList l => l -> [Item l]
List1.toList List1 QName
cs)

    DoesNotConstructAnElementOf QName
c 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]
"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]
"does not construct an element of" forall a. [a] -> [a] -> [a]
++ [forall a (m :: * -> *). (PrettyTCM a, MonadPretty m) => a -> m Doc
prettyTCM Type
t]

    ConstructorPatternInWrongDatatype QName
c QName
d -> forall (m :: * -> *) (t :: * -> *).
(Applicative m, Foldable t) =>
t (m Doc) -> m Doc
fsep forall a b. (a -> b) -> a -> b
$
      [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]
"is not a constructor of the datatype"
      forall a. [a] -> [a] -> [a]
++ [forall a (m :: * -> *). (PrettyTCM a, MonadPretty m) => a -> m Doc
prettyTCM QName
d]

    ShadowedModule Name
x [] -> forall a. HasCallStack => a
__IMPOSSIBLE__

    ShadowedModule Name
x ms :: [ModuleName]
ms@(ModuleName
m0 : [ModuleName]
_) -> do
      -- Clash! Concrete module name x already points to the abstract names ms.
      (Range
r, ModuleName
m) <- do
        -- Andreas, 2017-07-28, issue #719.
        -- First, we try to find whether one of the abstract names @ms@ points back to @x@
        ScopeInfo
scope <- forall (m :: * -> *). ReadTCState m => m ScopeInfo
getScope
        -- Get all pairs (y,m) such that y points to some m ∈ ms.
        let xms0 :: [(QName, ModuleName)]
xms0 = [ModuleName]
ms forall (m :: * -> *) a b. Monad m => m a -> (a -> m b) -> m b
>>= \ ModuleName
m -> forall a b. (a -> b) -> [a] -> [b]
map (,ModuleName
m) forall a b. (a -> b) -> a -> b
$ ModuleName -> ScopeInfo -> [QName]
inverseScopeLookupModule ModuleName
m ScopeInfo
scope
        forall (m :: * -> *).
MonadDebug m =>
[Char] -> Int -> [Char] -> m ()
reportSLn [Char]
"scope.clash.error" Int
30 forall a b. (a -> b) -> a -> b
$ [Char]
"candidates = " forall a. [a] -> [a] -> [a]
++ forall a. Pretty a => a -> [Char]
prettyShow [(QName, ModuleName)]
xms0

        -- Try to find x (which will have a different Range, if it has one (#2649)).
        let xms :: [(QName, ModuleName)]
xms = forall a. (a -> Bool) -> [a] -> [a]
filter ((\ QName
y -> Bool -> Bool
not (forall a. Null a => a -> Bool
null forall a b. (a -> b) -> a -> b
$ forall a. HasRange a => a -> Range
getRange QName
y) Bool -> Bool -> Bool
&& QName
y forall a. Eq a => a -> a -> Bool
== Name -> QName
C.QName Name
x) forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall a b. (a, b) -> a
fst) [(QName, ModuleName)]
xms0
        forall (m :: * -> *).
MonadDebug m =>
[Char] -> Int -> [Char] -> m ()
reportSLn [Char]
"scope.class.error" Int
30 forall a b. (a -> b) -> a -> b
$ [Char]
"filtered candidates = " forall a. [a] -> [a] -> [a]
++ forall a. Pretty a => a -> [Char]
prettyShow [(QName, ModuleName)]
xms

        -- If we found a copy of x with non-empty range, great!
        forall a b. Maybe a -> (a -> b) -> b -> b
ifJust (forall a. [a] -> Maybe a
listToMaybe [(QName, ModuleName)]
xms) (\ (QName
x', ModuleName
m) -> forall (m :: * -> *) a. Monad m => a -> m a
return (forall a. HasRange a => a -> Range
getRange QName
x', ModuleName
m)) forall a b. (a -> b) -> a -> b
$ {-else-} do

        -- If that failed, we pick the first m from ms which has a nameBindingSite.
        let rms :: [(Range, ModuleName)]
rms = [ModuleName]
ms forall (m :: * -> *) a b. Monad m => m a -> (a -> m b) -> m b
>>= \ ModuleName
m -> forall a b. (a -> b) -> [a] -> [b]
map (,ModuleName
m) forall a b. (a -> b) -> a -> b
$
              forall a. (a -> Bool) -> [a] -> [a]
filter (forall a. Range' a
noRange forall a. Eq a => a -> a -> Bool
/=) forall a b. (a -> b) -> a -> b
$ forall a b. (a -> b) -> [a] -> [b]
map Name -> Range
nameBindingSite forall a b. (a -> b) -> a -> b
$ forall a. [a] -> [a]
reverse forall a b. (a -> b) -> a -> b
$ ModuleName -> [Name]
mnameToList ModuleName
m
              -- Andreas, 2017-07-25, issue #2649
              -- Take the first nameBindingSite we can get hold of.
        forall (m :: * -> *).
MonadDebug m =>
[Char] -> Int -> [Char] -> m ()
reportSLn [Char]
"scope.class.error" Int
30 forall a b. (a -> b) -> a -> b
$ [Char]
"rangeful clashing modules = " forall a. [a] -> [a] -> [a]
++ forall a. Pretty a => a -> [Char]
prettyShow [(Range, ModuleName)]
rms

        -- If even this fails, we pick the first m and give no range.
        forall (m :: * -> *) a. Monad m => a -> m a
return forall a b. (a -> b) -> a -> b
$ forall a. a -> Maybe a -> a
fromMaybe (forall a. Range' a
noRange, ModuleName
m0) forall a b. (a -> b) -> a -> b
$ forall a. [a] -> Maybe a
listToMaybe [(Range, ModuleName)]
rms

      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]
"Duplicate definition of module" forall a. [a] -> [a] -> [a]
++ [forall a (m :: * -> *). (PrettyTCM a, MonadPretty m) => a -> m Doc
prettyTCM Name
x forall a. Semigroup a => a -> a -> a
<> m Doc
"."] forall a. [a] -> [a] -> [a]
++
        forall (m :: * -> *). Applicative m => [Char] -> [m Doc]
pwords [Char]
"Previous definition of" forall a. [a] -> [a] -> [a]
++ [forall (m :: * -> *). MonadPretty m => ModuleName -> m Doc
help ModuleName
m] forall a. [a] -> [a] -> [a]
++ forall (m :: * -> *). Applicative m => [Char] -> [m Doc]
pwords [Char]
"module" forall a. [a] -> [a] -> [a]
++ [forall a (m :: * -> *). (PrettyTCM a, MonadPretty m) => a -> m Doc
prettyTCM Name
x] forall a. [a] -> [a] -> [a]
++
        forall (m :: * -> *). Applicative m => [Char] -> [m Doc]
pwords [Char]
"at" forall a. [a] -> [a] -> [a]
++ [forall a (m :: * -> *). (PrettyTCM a, MonadPretty m) => a -> m Doc
prettyTCM Range
r]
      where
        help :: MonadPretty m => ModuleName -> m Doc
        help :: forall (m :: * -> *). MonadPretty m => ModuleName -> m Doc
help ModuleName
m = forall (m :: * -> *) a b.
Monad m =>
m (Maybe a) -> m b -> (a -> m b) -> m b
caseMaybeM (forall (m :: * -> *).
ReadTCState m =>
ModuleName -> m (Maybe DataOrRecordModule)
isDatatypeModule ModuleName
m) forall a. Null a => a
empty forall a b. (a -> b) -> a -> b
$ \case
          DataOrRecordModule
IsDataModule   -> m Doc
"(datatype)"
          DataOrRecordModule
IsRecordModule -> m Doc
"(record)"

    ModuleArityMismatch ModuleName
m Telescope
EmptyTel [NamedArg Expr]
args -> 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]
"The module" forall a. [a] -> [a] -> [a]
++ [forall a (m :: * -> *). (PrettyTCM a, MonadPretty m) => a -> m Doc
prettyTCM ModuleName
m] forall a. [a] -> [a] -> [a]
++
      forall (m :: * -> *). Applicative m => [Char] -> [m Doc]
pwords [Char]
"is not parameterized, but is being applied to arguments"

    ModuleArityMismatch ModuleName
m tel :: Telescope
tel@(ExtendTel Dom Type
_ Abs Telescope
_) [NamedArg Expr]
args -> 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]
"The arguments to " forall a. [a] -> [a] -> [a]
++ [forall a (m :: * -> *). (PrettyTCM a, MonadPretty m) => a -> m Doc
prettyTCM ModuleName
m] forall a. [a] -> [a] -> [a]
++ forall (m :: * -> *). Applicative m => [Char] -> [m Doc]
pwords [Char]
"do not fit the telescope" forall a. [a] -> [a] -> [a]
++
      [forall a (m :: * -> *). (PrettyTCM a, MonadPretty m) => a -> m Doc
prettyTCM Telescope
tel]

    ShouldBeEmpty Type
t [] -> forall (m :: * -> *) (t :: * -> *).
(Applicative m, Foldable t) =>
t (m Doc) -> m Doc
fsep forall a b. (a -> b) -> a -> b
$
       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]
"should be empty, but that's not obvious to me"

    ShouldBeEmpty Type
t [DeBruijnPattern]
ps -> forall (m :: * -> *) (t :: * -> *).
(Applicative m, Foldable t) =>
t (m Doc) -> m Doc
fsep (
      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]
"should be empty, but the following constructor patterns are valid:"
      ) 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.
MonadPretty m =>
Integer -> Pattern' a -> m Doc
prettyPat Integer
0) [DeBruijnPattern]
ps)

    ShouldBeASort Type
t -> forall (m :: * -> *) (t :: * -> *).
(Applicative m, Foldable t) =>
t (m Doc) -> m Doc
fsep forall a b. (a -> b) -> a -> b
$
      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]
"should be a sort, but it isn't"

    ShouldBePi Type
t -> forall (m :: * -> *) (t :: * -> *).
(Applicative m, Foldable t) =>
t (m Doc) -> m Doc
fsep forall a b. (a -> b) -> a -> b
$
      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]
"should be a function type, but it isn't"

    ShouldBePath Type
t -> forall (m :: * -> *) (t :: * -> *).
(Applicative m, Foldable t) =>
t (m Doc) -> m Doc
fsep forall a b. (a -> b) -> a -> b
$
      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]
"should be a Path or PathP type, but it isn't"

    TypeError
NotAProperTerm -> forall (m :: * -> *). Applicative m => [Char] -> m Doc
fwords [Char]
"Found a malformed term"

    InvalidTypeSort Sort
s -> forall (m :: * -> *) (t :: * -> *).
(Applicative m, Foldable t) =>
t (m Doc) -> m Doc
fsep forall a b. (a -> b) -> a -> b
$ 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]
"is not a valid type"
    InvalidType Term
v -> forall (m :: * -> *) (t :: * -> *).
(Applicative m, Foldable t) =>
t (m Doc) -> m Doc
fsep forall a b. (a -> b) -> a -> b
$ 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]
"is not a valid type"

    FunctionTypeInSizeUniv 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]
"Functions may not return sizes, thus, function type " 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]
" is illegal"

    SplitOnIrrelevant Dom 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]
"Cannot pattern match against" forall a. [a] -> [a] -> [a]
++ [forall (m :: * -> *). Applicative m => [Char] -> m Doc
text forall a b. (a -> b) -> a -> b
$ forall a. Verbalize a => a -> [Char]
verbalize forall a b. (a -> b) -> a -> b
$ forall a. LensRelevance a => a -> Relevance
getRelevance Dom Type
t] forall a. [a] -> [a] -> [a]
++
      forall (m :: * -> *). Applicative m => [Char] -> [m Doc]
pwords [Char]
"argument of type" forall a. [a] -> [a] -> [a]
++ [forall a (m :: * -> *). (PrettyTCM a, MonadPretty m) => a -> m Doc
prettyTCM forall a b. (a -> b) -> a -> b
$ forall t e. Dom' t e -> e
unDom Dom Type
t]

    SplitOnUnusableCohesion Dom 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]
"Cannot pattern match against" forall a. [a] -> [a] -> [a]
++ [forall (m :: * -> *). Applicative m => [Char] -> m Doc
text forall a b. (a -> b) -> a -> b
$ forall a. Verbalize a => a -> [Char]
verbalize forall a b. (a -> b) -> a -> b
$ forall a. LensCohesion a => a -> Cohesion
getCohesion Dom Type
t] forall a. [a] -> [a] -> [a]
++
      forall (m :: * -> *). Applicative m => [Char] -> [m Doc]
pwords [Char]
"argument of type" forall a. [a] -> [a] -> [a]
++ [forall a (m :: * -> *). (PrettyTCM a, MonadPretty m) => a -> m Doc
prettyTCM forall a b. (a -> b) -> a -> b
$ forall t e. Dom' t e -> e
unDom Dom Type
t]

    -- UNUSED:
    -- SplitOnErased t -> fsep $
    --   pwords "Cannot pattern match against" ++ [text $ verbalize $ getQuantity t] ++
    --   pwords "argument of type" ++ [prettyTCM $ unDom t]

    SplitOnNonVariable Term
v 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]
"Cannot pattern match because the (refined) argument " 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]
" is not a variable."

    SplitOnNonEtaRecord QName
q -> forall (m :: * -> *) (t :: * -> *).
(Applicative m, Foldable t) =>
t (m Doc) -> m Doc
fsep forall a b. (a -> b) -> a -> b
$ forall (t :: * -> *) a. Foldable t => t [a] -> [a]
concat
      [ forall (m :: * -> *). Applicative m => [Char] -> [m Doc]
pwords [Char]
"Pattern matching on no-eta record type"
      , [ forall a (m :: * -> *). (PrettyTCM a, MonadPretty m) => a -> m Doc
prettyTCM QName
q, forall (m :: * -> *). Functor m => m Doc -> m Doc
parens (m Doc
"defined 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 (m :: * -> *). Applicative m => [Char] -> [m Doc]
pwords [Char]
"is not allowed"
      , [ forall (m :: * -> *). Functor m => m Doc -> m Doc
parens m Doc
"to activate, add declaration `pattern` to record definition" ]
      ]
      where r :: Range
r = Name -> Range
nameBindingSite forall a b. (a -> b) -> a -> b
$ QName -> Name
qnameName QName
q

    DefinitionIsIrrelevant QName
x -> forall (m :: * -> *) (t :: * -> *).
(Applicative m, Foldable t) =>
t (m Doc) -> m Doc
fsep forall a b. (a -> b) -> a -> b
$
      m Doc
"Identifier" 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 declared irrelevant, so it cannot be used here"

    DefinitionIsErased QName
x -> forall (m :: * -> *) (t :: * -> *).
(Applicative m, Foldable t) =>
t (m Doc) -> m Doc
fsep forall a b. (a -> b) -> a -> b
$
      m Doc
"Identifier" 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 declared erased, so it cannot be used here"

    VariableIsIrrelevant Name
x -> forall (m :: * -> *) (t :: * -> *).
(Applicative m, Foldable t) =>
t (m Doc) -> m Doc
fsep forall a b. (a -> b) -> a -> b
$
      m Doc
"Variable" forall a. a -> [a] -> [a]
: forall a (m :: * -> *). (PrettyTCM a, MonadPretty m) => a -> m Doc
prettyTCM (Name -> Name
nameConcrete Name
x) forall a. a -> [a] -> [a]
: forall (m :: * -> *). Applicative m => [Char] -> [m Doc]
pwords [Char]
"is declared irrelevant, so it cannot be used here"

    VariableIsErased Name
x -> forall (m :: * -> *) (t :: * -> *).
(Applicative m, Foldable t) =>
t (m Doc) -> m Doc
fsep forall a b. (a -> b) -> a -> b
$
      m Doc
"Variable" forall a. a -> [a] -> [a]
: forall a (m :: * -> *). (PrettyTCM a, MonadPretty m) => a -> m Doc
prettyTCM (Name -> Name
nameConcrete Name
x) forall a. a -> [a] -> [a]
: forall (m :: * -> *). Applicative m => [Char] -> [m Doc]
pwords [Char]
"is declared erased, so it cannot be used here"

    VariableIsOfUnusableCohesion Name
x Cohesion
c -> forall (m :: * -> *) (t :: * -> *).
(Applicative m, Foldable t) =>
t (m Doc) -> m Doc
fsep
      [m Doc
"Variable", forall a (m :: * -> *). (PrettyTCM a, MonadPretty m) => a -> m Doc
prettyTCM (Name -> Name
nameConcrete Name
x), m Doc
"is declared", forall (m :: * -> *). Applicative m => [Char] -> m Doc
text (forall a. Show a => a -> [Char]
show Cohesion
c), m Doc
"so it cannot be used here"]

    UnequalBecauseOfUniverseConflict Comparison
cmp Term
s Term
t -> forall (m :: * -> *) (t :: * -> *).
(Applicative m, Foldable t) =>
t (m Doc) -> m Doc
fsep forall a b. (a -> b) -> a -> b
$
      [forall a (m :: * -> *). (PrettyTCM a, MonadPretty m) => a -> m Doc
prettyTCM Term
s, forall (m :: * -> *). MonadPretty m => Comparison -> m Doc
notCmp Comparison
cmp, forall a (m :: * -> *). (PrettyTCM a, MonadPretty m) => a -> m Doc
prettyTCM Term
t, m Doc
"because this would result in an invalid use of Setω" ]

    UnequalTerms Comparison
cmp Term
s Term
t CompareAs
a -> case (Term
s,Term
t) of
      (Sort Sort
s1      , Sort Sort
s2      )
        | Comparison
CmpEq  <- Comparison
cmp              -> forall a (m :: * -> *). (PrettyTCM a, MonadPretty m) => a -> m Doc
prettyTCM forall a b. (a -> b) -> a -> b
$ Sort -> Sort -> TypeError
UnequalSorts Sort
s1 Sort
s2
        | Comparison
CmpLeq <- Comparison
cmp              -> forall a (m :: * -> *). (PrettyTCM a, MonadPretty m) => a -> m Doc
prettyTCM forall a b. (a -> b) -> a -> b
$ Sort -> Sort -> TypeError
NotLeqSort Sort
s1 Sort
s2
      (Sort MetaS{} , Term
t            ) -> forall a (m :: * -> *). (PrettyTCM a, MonadPretty m) => a -> m Doc
prettyTCM forall a b. (a -> b) -> a -> b
$ Type -> TypeError
ShouldBeASort forall a b. (a -> b) -> a -> b
$ forall t a. Sort' t -> a -> Type'' t a
El forall a. HasCallStack => a
__IMPOSSIBLE__ Term
t
      (Term
s            , Sort MetaS{} ) -> forall a (m :: * -> *). (PrettyTCM a, MonadPretty m) => a -> m Doc
prettyTCM forall a b. (a -> b) -> a -> b
$ Type -> TypeError
ShouldBeASort forall a b. (a -> b) -> a -> b
$ forall t a. Sort' t -> a -> Type'' t a
El forall a. HasCallStack => a
__IMPOSSIBLE__ Term
s
      (Sort DefS{}  , Term
t            ) -> forall a (m :: * -> *). (PrettyTCM a, MonadPretty m) => a -> m Doc
prettyTCM forall a b. (a -> b) -> a -> b
$ Type -> TypeError
ShouldBeASort forall a b. (a -> b) -> a -> b
$ forall t a. Sort' t -> a -> Type'' t a
El forall a. HasCallStack => a
__IMPOSSIBLE__ Term
t
      (Term
s            , Sort DefS{}  ) -> forall a (m :: * -> *). (PrettyTCM a, MonadPretty m) => a -> m Doc
prettyTCM forall a b. (a -> b) -> a -> b
$ Type -> TypeError
ShouldBeASort forall a b. (a -> b) -> a -> b
$ forall t a. Sort' t -> a -> Type'' t a
El forall a. HasCallStack => a
__IMPOSSIBLE__ Term
s
      (Term
_            , Term
_            ) -> do
        (Doc
d1, Doc
d2, Doc
d) <- forall (m :: * -> *).
MonadPretty m =>
Term -> Term -> m (Doc, Doc, Doc)
prettyInEqual Term
s Term
t
        forall (m :: * -> *) (t :: * -> *).
(Applicative m, Foldable t) =>
t (m Doc) -> m Doc
fsep forall a b. (a -> b) -> a -> b
$ forall (t :: * -> *) a. Foldable t => t [a] -> [a]
concat forall a b. (a -> b) -> a -> b
$
          [ [forall (m :: * -> *) a. Monad m => a -> m a
return Doc
d1, forall (m :: * -> *). MonadPretty m => Comparison -> m Doc
notCmp Comparison
cmp, forall (m :: * -> *) a. Monad m => a -> m a
return Doc
d2]
          , case CompareAs
a of
                AsTermsOf Type
t -> forall (m :: * -> *). Applicative m => [Char] -> [m Doc]
pwords [Char]
"of type" forall a. [a] -> [a] -> [a]
++ [forall a (m :: * -> *). (PrettyTCM a, MonadPretty m) => a -> m Doc
prettyTCM Type
t]
                CompareAs
AsSizes     -> forall (m :: * -> *). Applicative m => [Char] -> [m Doc]
pwords [Char]
"of type" forall a. [a] -> [a] -> [a]
++ [forall a (m :: * -> *). (PrettyTCM a, MonadPretty m) => a -> m Doc
prettyTCM forall (m :: * -> *) a b. Monad m => (a -> m b) -> m a -> m b
=<< forall (m :: * -> *).
(HasBuiltins m, MonadTCEnv m, ReadTCState m) =>
m Type
sizeType]
                CompareAs
AsTypes     -> []
          , [forall (m :: * -> *) a. Monad m => a -> m a
return Doc
d]
          ]

    UnequalLevel Comparison
cmp Level
s Level
t -> forall (m :: * -> *) (t :: * -> *).
(Applicative m, Foldable t) =>
t (m Doc) -> m Doc
fsep forall a b. (a -> b) -> a -> b
$
      [forall a (m :: * -> *). (PrettyTCM a, MonadPretty m) => a -> m Doc
prettyTCM Level
s, forall (m :: * -> *). MonadPretty m => Comparison -> m Doc
notCmp Comparison
cmp, forall a (m :: * -> *). (PrettyTCM a, MonadPretty m) => a -> m Doc
prettyTCM Level
t]

-- UnequalTelescopes is UNUSED
--   UnequalTelescopes cmp a b -> fsep $
--     [prettyTCM a, notCmp cmp, prettyTCM b]

    UnequalTypes Comparison
cmp Type
a Type
b -> forall a (m :: * -> *).
(PrettyUnequal a, MonadPretty m) =>
a -> m Doc -> a -> m Doc
prettyUnequal Type
a (forall (m :: * -> *). MonadPretty m => Comparison -> m Doc
notCmp Comparison
cmp) Type
b
--              fsep $ [prettyTCM a, notCmp cmp, prettyTCM b]

    UnequalRelevance Comparison
cmp Term
a Term
b -> forall (m :: * -> *) (t :: * -> *).
(Applicative m, Foldable t) =>
t (m Doc) -> m Doc
fsep forall a b. (a -> b) -> a -> b
$
      [forall a (m :: * -> *). (PrettyTCM a, MonadPretty m) => a -> m Doc
prettyTCM Term
a, forall (m :: * -> *). MonadPretty m => Comparison -> m Doc
notCmp Comparison
cmp, forall a (m :: * -> *). (PrettyTCM a, MonadPretty m) => a -> m Doc
prettyTCM Term
b] forall a. [a] -> [a] -> [a]
++
      forall (m :: * -> *). Applicative m => [Char] -> [m Doc]
pwords [Char]
"because one is a relevant function type and the other is an irrelevant function type"

    UnequalQuantity Comparison
cmp Term
a Term
b -> forall (m :: * -> *) (t :: * -> *).
(Applicative m, Foldable t) =>
t (m Doc) -> m Doc
fsep forall a b. (a -> b) -> a -> b
$
      [forall a (m :: * -> *). (PrettyTCM a, MonadPretty m) => a -> m Doc
prettyTCM Term
a, forall (m :: * -> *). MonadPretty m => Comparison -> m Doc
notCmp Comparison
cmp, forall a (m :: * -> *). (PrettyTCM a, MonadPretty m) => a -> m Doc
prettyTCM Term
b] forall a. [a] -> [a] -> [a]
++
      forall (m :: * -> *). Applicative m => [Char] -> [m Doc]
pwords [Char]
"because one is a non-erased function type and the other is an erased function type"

    UnequalCohesion Comparison
cmp Term
a Term
b -> forall (m :: * -> *) (t :: * -> *).
(Applicative m, Foldable t) =>
t (m Doc) -> m Doc
fsep forall a b. (a -> b) -> a -> b
$
      [forall a (m :: * -> *). (PrettyTCM a, MonadPretty m) => a -> m Doc
prettyTCM Term
a, forall (m :: * -> *). MonadPretty m => Comparison -> m Doc
notCmp Comparison
cmp, forall a (m :: * -> *). (PrettyTCM a, MonadPretty m) => a -> m Doc
prettyTCM Term
b] forall a. [a] -> [a] -> [a]
++
      forall (m :: * -> *). Applicative m => [Char] -> [m Doc]
pwords [Char]
"because one is a non-flat function type and the other is a flat function type"
      -- FUTURE Cohesion: update message if/when introducing sharp.

    UnequalFiniteness Comparison
cmp Term
a Term
b -> forall (m :: * -> *) (t :: * -> *).
(Applicative m, Foldable t) =>
t (m Doc) -> m Doc
fsep forall a b. (a -> b) -> a -> b
$
      [forall a (m :: * -> *). (PrettyTCM a, MonadPretty m) => a -> m Doc
prettyTCM Term
a, forall (m :: * -> *). MonadPretty m => Comparison -> m Doc
notCmp Comparison
cmp, forall a (m :: * -> *). (PrettyTCM a, MonadPretty m) => a -> m Doc
prettyTCM Term
b] forall a. [a] -> [a] -> [a]
++
      forall (m :: * -> *). Applicative m => [Char] -> [m Doc]
pwords [Char]
"because one is a type of partial elements and the other is a function type"
      -- FUTURE Cohesion: update message if/when introducing sharp.

    UnequalHiding Term
a Term
b -> forall (m :: * -> *) (t :: * -> *).
(Applicative m, Foldable t) =>
t (m Doc) -> m Doc
fsep forall a b. (a -> b) -> a -> b
$
      [forall a (m :: * -> *). (PrettyTCM a, MonadPretty m) => a -> m Doc
prettyTCM Term
a, m Doc
"!=", forall a (m :: * -> *). (PrettyTCM a, MonadPretty m) => a -> m Doc
prettyTCM Term
b] forall a. [a] -> [a] -> [a]
++
      forall (m :: * -> *). Applicative m => [Char] -> [m Doc]
pwords [Char]
"because one is an implicit function type and the other is an explicit function type"

    UnequalSorts Sort
s1 Sort
s2 -> forall (m :: * -> *) (t :: * -> *).
(Applicative m, Foldable t) =>
t (m Doc) -> m Doc
fsep forall a b. (a -> b) -> a -> b
$
      [forall a (m :: * -> *). (PrettyTCM a, MonadPretty m) => a -> m Doc
prettyTCM Sort
s1, m Doc
"!=", forall a (m :: * -> *). (PrettyTCM a, MonadPretty m) => a -> m Doc
prettyTCM Sort
s2]

    NotLeqSort Sort
s1 Sort
s2 -> forall (m :: * -> *) (t :: * -> *).
(Applicative m, Foldable t) =>
t (m Doc) -> m Doc
fsep forall a b. (a -> b) -> a -> b
$
      [forall a (m :: * -> *). (PrettyTCM a, MonadPretty m) => a -> m Doc
prettyTCM Sort
s1] forall a. [a] -> [a] -> [a]
++ forall (m :: * -> *). Applicative m => [Char] -> [m Doc]
pwords [Char]
"is not less or equal than" forall a. [a] -> [a] -> [a]
++ [forall a (m :: * -> *). (PrettyTCM a, MonadPretty m) => a -> m Doc
prettyTCM Sort
s2]

    TooManyFields QName
r [Name]
missing [Name]
xs -> forall (m :: * -> *).
MonadPretty m =>
QName -> [Name] -> [Name] -> m Doc
prettyTooManyFields QName
r [Name]
missing [Name]
xs

    DuplicateConstructors [Name]
xs -> 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]
"Duplicate" forall a. [a] -> [a] -> [a]
++ forall {a} {m :: * -> *}. (Sized a, Applicative m) => a -> [m Doc]
constructors [Name]
xs forall a. [a] -> [a] -> [a]
++ forall (m :: * -> *) (t :: * -> *).
(Applicative m, Semigroup (m Doc), Foldable t) =>
m Doc -> t (m Doc) -> [m Doc]
punctuate forall (m :: * -> *). Applicative m => m Doc
comma (forall a b. (a -> b) -> [a] -> [b]
map forall (m :: * -> *) a. (Applicative m, Pretty a) => a -> m Doc
pretty [Name]
xs) forall a. [a] -> [a] -> [a]
++
      forall (m :: * -> *). Applicative m => [Char] -> [m Doc]
pwords [Char]
"in datatype"
      where
      constructors :: a -> [m Doc]
constructors a
ys = forall a c. Sized a => a -> c -> c -> c
P.singPlural a
ys [forall (m :: * -> *). Applicative m => [Char] -> m Doc
text [Char]
"constructor"] [forall (m :: * -> *). Applicative m => [Char] -> m Doc
text [Char]
"constructors"]

    DuplicateFields [Name]
xs -> forall (m :: * -> *). MonadPretty m => [Name] -> m Doc
prettyDuplicateFields [Name]
xs

    WithOnFreeVariable Expr
e Term
v -> do
      Doc
de <- forall a (m :: * -> *).
(ToConcrete a, Pretty (ConOfAbs a), MonadAbsToCon m) =>
a -> m Doc
prettyA Expr
e
      Doc
dv <- forall a (m :: * -> *). (PrettyTCM a, MonadPretty m) => a -> m Doc
prettyTCM Term
v
      if forall a. Show a => a -> [Char]
show Doc
de forall a. Eq a => a -> a -> Bool
== forall a. Show a => a -> [Char]
show Doc
dv
        then 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]
"Cannot `with` on variable" forall a. [a] -> [a] -> [a]
++ [forall (m :: * -> *) a. Monad m => a -> m a
return Doc
dv] forall a. [a] -> [a] -> [a]
++
          forall (m :: * -> *). Applicative m => [Char] -> [m Doc]
pwords [Char]
" bound in a module telescope (or patterns of a parent clause)"
        else 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]
"Cannot `with` on expression" forall a. [a] -> [a] -> [a]
++ [forall (m :: * -> *) a. Monad m => a -> m a
return Doc
de] forall a. [a] -> [a] -> [a]
++ forall (m :: * -> *). Applicative m => [Char] -> [m Doc]
pwords [Char]
"which reduces to variable" forall a. [a] -> [a] -> [a]
++ [forall (m :: * -> *) a. Monad m => a -> m a
return Doc
dv] forall a. [a] -> [a] -> [a]
++
          forall (m :: * -> *). Applicative m => [Char] -> [m Doc]
pwords [Char]
" bound in a module telescope (or patterns of a parent clause)"

    UnexpectedWithPatterns [Pattern]
ps -> 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]
"Unexpected with patterns" forall a. [a] -> [a] -> [a]
++ forall (m :: * -> *) (t :: * -> *).
(Applicative m, Semigroup (m Doc), Foldable t) =>
m Doc -> t (m Doc) -> [m Doc]
punctuate m Doc
" |" (forall a b. (a -> b) -> [a] -> [b]
map forall a (m :: * -> *).
(ToConcrete a, Pretty (ConOfAbs a), MonadAbsToCon m) =>
a -> m Doc
prettyA [Pattern]
ps)

    WithClausePatternMismatch Pattern
p NamedArg DeBruijnPattern
q -> 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]
"With clause 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]
" is not an instance of its parent pattern " forall a. [a] -> [a] -> [a]
++ [forall (t :: * -> *). Foldable t => t Doc -> Doc
P.fsep forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> forall (m :: * -> *).
MonadPretty m =>
[NamedArg DeBruijnPattern] -> m [Doc]
prettyTCMPatterns [NamedArg DeBruijnPattern
q]]

    -- The following error is caught and reraised as GenericDocError in Occurs.hs
    MetaCannotDependOn MetaId
m {- ps -} Int
i -> 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]
"The metavariable" forall a. [a] -> [a] -> [a]
++ [forall a (m :: * -> *). (PrettyTCM a, MonadPretty m) => a -> m Doc
prettyTCM forall a b. (a -> b) -> a -> b
$ MetaId -> Elims -> Term
MetaV MetaId
m []] forall a. [a] -> [a] -> [a]
++
      forall (m :: * -> *). Applicative m => [Char] -> [m Doc]
pwords [Char]
"cannot depend on" forall a. [a] -> [a] -> [a]
++ [Int -> m Doc
pvar Int
i] forall a. [a] -> [a] -> [a]
++
      [] -- pwords "because it" ++ deps
        where
          pvar :: Int -> m Doc
pvar = forall a (m :: * -> *). (PrettyTCM a, MonadPretty m) => a -> m Doc
prettyTCM forall b c a. (b -> c) -> (a -> b) -> a -> c
. Int -> Term
I.var
          -- deps = case map pvar ps of
          --   []  -> pwords "does not depend on any variables"
          --   [x] -> pwords "only depends on the variable" ++ [x]
          --   xs  -> pwords "only depends on the variables" ++ punctuate comma xs

    -- The following error is caught and reraised as GenericDocError in Occurs.hs
    MetaOccursInItself MetaId
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]
"Cannot construct infinite solution of metavariable" forall a. [a] -> [a] -> [a]
++ [forall a (m :: * -> *). (PrettyTCM a, MonadPretty m) => a -> m Doc
prettyTCM forall a b. (a -> b) -> a -> b
$ MetaId -> Elims -> Term
MetaV MetaId
m []]

    -- The following error is caught and reraised as GenericDocError in Occurs.hs
    MetaIrrelevantSolution MetaId
m Term
_ -> 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]
"Cannot instantiate the metavariable because (part of) the" forall a. [a] -> [a] -> [a]
++
      forall (m :: * -> *). Applicative m => [Char] -> [m Doc]
pwords [Char]
"solution was created in an irrelevant context."

    -- The following error is caught and reraised as GenericDocError in Occurs.hs
    MetaErasedSolution MetaId
m Term
_ -> 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]
"Cannot instantiate the metavariable because (part of) the" forall a. [a] -> [a] -> [a]
++
      forall (m :: * -> *). Applicative m => [Char] -> [m Doc]
pwords [Char]
"solution was created in an erased context."

    BuiltinMustBeConstructor [Char]
s Expr
e -> forall (m :: * -> *) (t :: * -> *).
(Applicative m, Foldable t) =>
t (m Doc) -> m Doc
fsep forall a b. (a -> b) -> a -> b
$
      [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]
"must be a constructor in the binding to builtin" forall a. [a] -> [a] -> [a]
++ [forall (m :: * -> *). Applicative m => [Char] -> m Doc
text [Char]
s]

    NoSuchBuiltinName [Char]
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]
"There is no built-in thing called" forall a. [a] -> [a] -> [a]
++ [forall (m :: * -> *). Applicative m => [Char] -> m Doc
text [Char]
s]

    DuplicateBuiltinBinding [Char]
b Term
x Term
y -> 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]
"Duplicate binding for built-in thing" forall a. [a] -> [a] -> [a]
++ [forall (m :: * -> *). Applicative m => [Char] -> m Doc
text [Char]
b 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]
"previous binding to" forall a. [a] -> [a] -> [a]
++ [forall a (m :: * -> *). (PrettyTCM a, MonadPretty m) => a -> m Doc
prettyTCM Term
x]

    NoBindingForBuiltin [Char]
x
      | [Char]
x forall (t :: * -> *) a. (Foldable t, Eq a) => a -> t a -> Bool
`elem` [[Char]
builtinZero, [Char]
builtinSuc] -> 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]
"No binding for builtin " forall a. [a] -> [a] -> [a]
++ [forall (m :: * -> *). Applicative m => [Char] -> m Doc
text [Char]
x 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]
"use {-# BUILTIN " forall a. [a] -> [a] -> [a]
++ [Char]
builtinNat forall a. [a] -> [a] -> [a]
++ [Char]
" name #-} to bind builtin natural " forall a. [a] -> [a] -> [a]
++
                [Char]
"numbers to the type 'name'")
      | Bool
otherwise -> 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]
"No binding for builtin thing" forall a. [a] -> [a] -> [a]
++ [forall (m :: * -> *). Applicative m => [Char] -> m Doc
text [Char]
x 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]
"use {-# BUILTIN " forall a. [a] -> [a] -> [a]
++ [Char]
x forall a. [a] -> [a] -> [a]
++ [Char]
" name #-} to bind it to 'name'")

    DuplicatePrimitiveBinding [Char]
b QName
x QName
y -> 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]
"Duplicate binding for primitive thing" forall a. [a] -> [a] -> [a]
++ [forall (m :: * -> *). Applicative m => [Char] -> m Doc
text [Char]
b 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]
"previous binding to" forall a. [a] -> [a] -> [a]
++ [forall a (m :: * -> *). (PrettyTCM a, MonadPretty m) => a -> m Doc
prettyTCM QName
x]

    NoSuchPrimitiveFunction [Char]
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]
"There is no primitive function called" forall a. [a] -> [a] -> [a]
++ [forall (m :: * -> *). Applicative m => [Char] -> m Doc
text [Char]
x]

    WrongModalityForPrimitive [Char]
x ArgInfo
got ArgInfo
expect ->
      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 a b. (a -> b) -> a -> b
$ forall (m :: * -> *). Applicative m => [Char] -> [m Doc]
pwords [Char]
"Wrong modality for primitive" forall a. [a] -> [a] -> [a]
++ [forall (m :: * -> *). Applicative m => [Char] -> m Doc
text [Char]
x]
           , forall (m :: * -> *). Functor m => Int -> m Doc -> m Doc
nest Int
2 forall a b. (a -> b) -> a -> b
$ forall (m :: * -> *). Applicative m => [Char] -> m Doc
text forall a b. (a -> b) -> a -> b
$ [Char]
"Got:      " forall a. [a] -> [a] -> [a]
++ forall a. [a] -> [[a]] -> [a]
intercalate [Char]
", " [[Char]]
gs
           , forall (m :: * -> *). Functor m => Int -> m Doc -> m Doc
nest Int
2 forall a b. (a -> b) -> a -> b
$ forall (m :: * -> *). Applicative m => [Char] -> m Doc
text forall a b. (a -> b) -> a -> b
$ [Char]
"Expected: " forall a. [a] -> [a] -> [a]
++ forall a. [a] -> [[a]] -> [a]
intercalate [Char]
", " [[Char]]
es ]
      where
        ([[Char]]
gs, [[Char]]
es) = forall a b. [(a, b)] -> ([a], [b])
unzip [ ([Char], [Char])
p | p :: ([Char], [Char])
p@([Char]
g, [Char]
e) <- forall a b. [a] -> [b] -> [(a, b)]
zip (forall {a}.
(LensHiding a, LensRelevance a, LensQuantity a, LensCohesion a) =>
a -> [[Char]]
things ArgInfo
got) (forall {a}.
(LensHiding a, LensRelevance a, LensQuantity a, LensCohesion a) =>
a -> [[Char]]
things ArgInfo
expect), [Char]
g forall a. Eq a => a -> a -> Bool
/= [Char]
e ]
        things :: a -> [[Char]]
things a
i = [forall a. Verbalize a => a -> [Char]
verbalize forall a b. (a -> b) -> a -> b
$ forall a. LensHiding a => a -> Hiding
getHiding a
i,
                    forall a. Verbalize a => a -> [Char]
verbalize forall a b. (a -> b) -> a -> b
$ forall a. LensRelevance a => a -> Relevance
getRelevance a
i,
                    forall a. Verbalize a => a -> [Char]
verbalize forall a b. (a -> b) -> a -> b
$ forall a. LensQuantity a => a -> Quantity
getQuantity a
i,
                    forall a. Verbalize a => a -> [Char]
verbalize forall a b. (a -> b) -> a -> b
$ forall a. LensCohesion a => a -> Cohesion
getCohesion a
i]

    BuiltinInParameterisedModule [Char]
x -> forall (m :: * -> *). Applicative m => [Char] -> m Doc
fwords forall a b. (a -> b) -> a -> b
$
      [Char]
"The BUILTIN pragma cannot appear inside a bound context " forall a. [a] -> [a] -> [a]
++
      [Char]
"(for instance, in a parameterised module or as a local declaration)"

    IllegalLetInTelescope TypedBinding
tb -> forall (m :: * -> *) (t :: * -> *).
(Applicative m, Foldable t) =>
t (m Doc) -> m Doc
fsep forall a b. (a -> b) -> a -> b
$
      -- pwords "The binding" ++
      forall (m :: * -> *) a. (Applicative m, Pretty a) => a -> m Doc
pretty TypedBinding
tb forall a. a -> [a] -> [a]
:
      forall (m :: * -> *). Applicative m => [Char] -> [m Doc]
pwords [Char]
" is not allowed in a telescope here."

    IllegalPatternInTelescope Binder
bd -> forall (m :: * -> *) (t :: * -> *).
(Applicative m, Foldable t) =>
t (m Doc) -> m Doc
fsep forall a b. (a -> b) -> a -> b
$
      forall (m :: * -> *) a. (Applicative m, Pretty a) => a -> m Doc
pretty Binder
bd forall a. a -> [a] -> [a]
:
      forall (m :: * -> *). Applicative m => [Char] -> [m Doc]
pwords [Char]
" is not allowed in a telescope here."

    NoRHSRequiresAbsurdPattern [NamedArg Pattern]
ps -> forall (m :: * -> *). Applicative m => [Char] -> m Doc
fwords forall a b. (a -> b) -> a -> b
$
      [Char]
"The right-hand side can only be omitted if there " forall a. [a] -> [a] -> [a]
++
      [Char]
"is an absurd pattern, () or {}, in the left-hand side."

    LocalVsImportedModuleClash 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]
"The module" forall a. [a] -> [a] -> [a]
++ [forall a (m :: * -> *). (PrettyTCM a, MonadPretty m) => a -> m Doc
prettyTCM ModuleName
m] forall a. [a] -> [a] -> [a]
++
      forall (m :: * -> *). Applicative m => [Char] -> [m Doc]
pwords [Char]
"can refer to either a local module or an imported module"

    TypeError
SolvedButOpenHoles -> 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]
"Module cannot be imported since it has open interaction points" forall a. [a] -> [a] -> [a]
++
      forall (m :: * -> *). Applicative m => [Char] -> [m Doc]
pwords [Char]
"(consider adding {-# OPTIONS --allow-unsolved-metas #-} to this module)"

    CyclicModuleDependency [TopLevelModuleName]
ms ->
      forall (m :: * -> *) (t :: * -> *).
(Applicative m, Foldable t) =>
t (m Doc) -> m Doc
fsep (forall (m :: * -> *). Applicative m => [Char] -> [m Doc]
pwords [Char]
"cyclic module dependency:")
      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 [TopLevelModuleName]
ms)

    FileNotFound TopLevelModuleName
x [AbsolutePath]
files ->
      forall (m :: * -> *) (t :: * -> *).
(Applicative m, Foldable t) =>
t (m Doc) -> m Doc
fsep ( forall (m :: * -> *). Applicative m => [Char] -> [m Doc]
pwords [Char]
"Failed to find source of module" forall a. [a] -> [a] -> [a]
++ [forall (m :: * -> *) a. (Applicative m, Pretty a) => a -> m Doc
pretty TopLevelModuleName
x] forall a. [a] -> [a] -> [a]
++
             forall (m :: * -> *). Applicative m => [Char] -> [m Doc]
pwords [Char]
"in any of the following locations:"
           ) 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 :: * -> *). Applicative m => [Char] -> m Doc
text forall b c a. (b -> c) -> (a -> b) -> a -> c
. AbsolutePath -> [Char]
filePath) [AbsolutePath]
files)

    OverlappingProjects AbsolutePath
f TopLevelModuleName
m1 TopLevelModuleName
m2
      | Doc -> CI [Char]
canon Doc
d1 forall a. Eq a => a -> a -> Bool
== Doc -> CI [Char]
canon Doc
d2 -> forall (m :: * -> *) (t :: * -> *).
(Applicative m, Foldable t) =>
t (m Doc) -> m Doc
fsep forall a b. (a -> b) -> a -> b
$ forall (t :: * -> *) a. Foldable t => t [a] -> [a]
concat
          [ forall (m :: * -> *). Applicative m => [Char] -> [m Doc]
pwords [Char]
"Case mismatch when accessing file"
          , [ forall (m :: * -> *). Applicative m => [Char] -> m Doc
text forall a b. (a -> b) -> a -> b
$ AbsolutePath -> [Char]
filePath AbsolutePath
f ]
          , forall (m :: * -> *). Applicative m => [Char] -> [m Doc]
pwords [Char]
"through module name"
          , [ forall (f :: * -> *) a. Applicative f => a -> f a
pure Doc
d2 ]
          ]
      | Bool
otherwise -> forall (m :: * -> *) (t :: * -> *).
(Applicative m, Foldable t) =>
t (m Doc) -> m Doc
fsep
           ( forall (m :: * -> *). Applicative m => [Char] -> [m Doc]
pwords [Char]
"The file" forall a. [a] -> [a] -> [a]
++ [forall (m :: * -> *). Applicative m => [Char] -> m Doc
text (AbsolutePath -> [Char]
filePath AbsolutePath
f)] forall a. [a] -> [a] -> [a]
++
             forall (m :: * -> *). Applicative m => [Char] -> [m Doc]
pwords [Char]
"can be accessed via several project roots. Both" forall a. [a] -> [a] -> [a]
++
             [ forall (f :: * -> *) a. Applicative f => a -> f a
pure Doc
d1 ] forall a. [a] -> [a] -> [a]
++ forall (m :: * -> *). Applicative m => [Char] -> [m Doc]
pwords [Char]
"and" forall a. [a] -> [a] -> [a]
++ [ forall (f :: * -> *) a. Applicative f => a -> f a
pure Doc
d2 ] forall a. [a] -> [a] -> [a]
++
             forall (m :: * -> *). Applicative m => [Char] -> [m Doc]
pwords [Char]
"point to this file."
           )
      where
      canon :: Doc -> CI [Char]
canon = forall s. FoldCase s => s -> CI s
CaseInsens.mk forall b c a. (b -> c) -> (a -> b) -> a -> c
. Doc -> [Char]
P.render
      d1 :: Doc
d1 = forall a. Pretty a => a -> Doc
P.pretty TopLevelModuleName
m1
      d2 :: Doc
d2 = forall a. Pretty a => a -> Doc
P.pretty TopLevelModuleName
m2

    AmbiguousTopLevelModuleName TopLevelModuleName
x [AbsolutePath]
files ->
      forall (m :: * -> *) (t :: * -> *).
(Applicative m, Foldable t) =>
t (m Doc) -> m Doc
fsep ( forall (m :: * -> *). Applicative m => [Char] -> [m Doc]
pwords [Char]
"Ambiguous module name. The module name" forall a. [a] -> [a] -> [a]
++
             [forall (m :: * -> *) a. (Applicative m, Pretty a) => a -> m Doc
pretty TopLevelModuleName
x] forall a. [a] -> [a] -> [a]
++
             forall (m :: * -> *). Applicative m => [Char] -> [m Doc]
pwords [Char]
"could refer to any of the following files:"
           ) 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 :: * -> *). Applicative m => [Char] -> m Doc
text forall b c a. (b -> c) -> (a -> b) -> a -> c
. AbsolutePath -> [Char]
filePath) [AbsolutePath]
files)

    ClashingFileNamesFor ModuleName
x [AbsolutePath]
files ->
      forall (m :: * -> *) (t :: * -> *).
(Applicative m, Foldable t) =>
t (m Doc) -> m Doc
fsep ( forall (m :: * -> *). Applicative m => [Char] -> [m Doc]
pwords [Char]
"Multiple possible sources for module"
             forall a. [a] -> [a] -> [a]
++ [forall a (m :: * -> *). (PrettyTCM a, MonadPretty m) => a -> m Doc
prettyTCM ModuleName
x] forall a. [a] -> [a] -> [a]
++ forall (m :: * -> *). Applicative m => [Char] -> [m Doc]
pwords [Char]
"found:"
           ) 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 :: * -> *). Applicative m => [Char] -> m Doc
text forall b c a. (b -> c) -> (a -> b) -> a -> c
. AbsolutePath -> [Char]
filePath) [AbsolutePath]
files)

    ModuleDefinedInOtherFile TopLevelModuleName
mod AbsolutePath
file AbsolutePath
file' -> 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]
"You tried to load" forall a. [a] -> [a] -> [a]
++ [forall (m :: * -> *). Applicative m => [Char] -> m Doc
text (AbsolutePath -> [Char]
filePath AbsolutePath
file)] forall a. [a] -> [a] -> [a]
++
      forall (m :: * -> *). Applicative m => [Char] -> [m Doc]
pwords [Char]
"which defines the module" forall a. [a] -> [a] -> [a]
++ [forall (m :: * -> *) a. (Applicative m, Pretty a) => a -> m Doc
pretty TopLevelModuleName
mod forall a. Semigroup a => a -> a -> a
<> m Doc
"."] forall a. [a] -> [a] -> [a]
++
      forall (m :: * -> *). Applicative m => [Char] -> [m Doc]
pwords [Char]
"However, according to the include path this module should" forall a. [a] -> [a] -> [a]
++
      forall (m :: * -> *). Applicative m => [Char] -> [m Doc]
pwords [Char]
"be defined in" forall a. [a] -> [a] -> [a]
++ [forall (m :: * -> *). Applicative m => [Char] -> m Doc
text (AbsolutePath -> [Char]
filePath AbsolutePath
file') forall a. Semigroup a => a -> a -> a
<> m Doc
"."]

    ModuleNameUnexpected TopLevelModuleName
given TopLevelModuleName
expected
      | Doc -> CI [Char]
canon Doc
dGiven forall a. Eq a => a -> a -> Bool
== Doc -> CI [Char]
canon Doc
dExpected -> forall (m :: * -> *) (t :: * -> *).
(Applicative m, Foldable t) =>
t (m Doc) -> m Doc
fsep forall a b. (a -> b) -> a -> b
$ forall (t :: * -> *) a. Foldable t => t [a] -> [a]
concat
          [ forall (m :: * -> *). Applicative m => [Char] -> [m Doc]
pwords [Char]
"Case mismatch between the actual module name"
          , [ forall (f :: * -> *) a. Applicative f => a -> f a
pure Doc
dGiven ]
          , forall (m :: * -> *). Applicative m => [Char] -> [m Doc]
pwords [Char]
"and the expected module name"
          , [ forall (f :: * -> *) a. Applicative f => a -> f a
pure Doc
dExpected ]
          ]
      | Bool
otherwise -> forall (m :: * -> *) (t :: * -> *).
(Applicative m, Foldable t) =>
t (m Doc) -> m Doc
fsep forall a b. (a -> b) -> a -> b
$ forall (t :: * -> *) a. Foldable t => t [a] -> [a]
concat
          [ forall (m :: * -> *). Applicative m => [Char] -> [m Doc]
pwords [Char]
"The name of the top level module does not match the file name. The module"
          , [ forall (f :: * -> *) a. Applicative f => a -> f a
pure Doc
dGiven ]
          , forall (m :: * -> *). Applicative m => [Char] -> [m Doc]
pwords [Char]
"should probably be named"
          , [ forall (f :: * -> *) a. Applicative f => a -> f a
pure Doc
dExpected ]
          ]
      where
      canon :: Doc -> CI [Char]
canon = forall s. FoldCase s => s -> CI s
CaseInsens.mk forall b c a. (b -> c) -> (a -> b) -> a -> c
. Doc -> [Char]
P.render
      dGiven :: Doc
dGiven    = forall a. Pretty a => a -> Doc
P.pretty TopLevelModuleName
given
      dExpected :: Doc
dExpected = forall a. Pretty a => a -> Doc
P.pretty TopLevelModuleName
expected


    ModuleNameDoesntMatchFileName TopLevelModuleName
given [AbsolutePath]
files ->
      forall (m :: * -> *) (t :: * -> *).
(Applicative m, Foldable t) =>
t (m Doc) -> m Doc
fsep (forall (m :: * -> *). Applicative m => [Char] -> [m Doc]
pwords [Char]
"The name of the top level module does not match the file name. The module" forall a. [a] -> [a] -> [a]
++
           [ forall (m :: * -> *) a. (Applicative m, Pretty a) => a -> m Doc
pretty TopLevelModuleName
given ] forall a. [a] -> [a] -> [a]
++ forall (m :: * -> *). Applicative m => [Char] -> [m Doc]
pwords [Char]
"should be defined in one of the following files:")
      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 :: * -> *). Applicative m => [Char] -> m Doc
text forall b c a. (b -> c) -> (a -> b) -> a -> c
. AbsolutePath -> [Char]
filePath) [AbsolutePath]
files)

    TypeError
BothWithAndRHS -> 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]
"Unexpected right hand side"

    AbstractConstructorNotInScope QName
q -> forall (m :: * -> *) (t :: * -> *).
(Applicative m, Foldable t) =>
t (m Doc) -> m Doc
fsep forall a b. (a -> b) -> a -> b
$
      [ m Doc
"Constructor"
      , forall a (m :: * -> *). (PrettyTCM a, MonadPretty m) => a -> m Doc
prettyTCM QName
q
      ] forall a. [a] -> [a] -> [a]
++ forall (m :: * -> *). Applicative m => [Char] -> [m Doc]
pwords [Char]
"is abstract, thus, not in scope here"

    NotInScope [QName]
xs ->
      -- using the warning version to avoid code duplication
      forall (m :: * -> *). MonadPretty m => Warning -> m Doc
prettyWarning ([QName] -> Warning
NotInScopeW [QName]
xs)

    NoSuchModule 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]
"No module" forall a. [a] -> [a] -> [a]
++ [forall (m :: * -> *) a. (Applicative m, Pretty a) => a -> m Doc
pretty QName
x] forall a. [a] -> [a] -> [a]
++ forall (m :: * -> *). Applicative m => [Char] -> [m Doc]
pwords [Char]
"in scope"

    AmbiguousName QName
x AmbiguousNameReason
reason -> 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 a b. (a -> b) -> a -> b
$ forall (m :: * -> *). Applicative m => [Char] -> [m Doc]
pwords [Char]
"Ambiguous name" forall a. [a] -> [a] -> [a]
++ [forall (m :: * -> *) a. (Applicative m, Pretty a) => a -> m Doc
pretty QName
x forall a. Semigroup a => a -> a -> a
<> m Doc
"."] forall a. [a] -> [a] -> [a]
++
               forall (m :: * -> *). Applicative m => [Char] -> [m Doc]
pwords [Char]
"It could refer to any one of"
      , forall (m :: * -> *). Functor m => Int -> m Doc -> m Doc
nest Int
2 forall a b. (a -> b) -> a -> b
$ forall (m :: * -> *) (t :: * -> *).
(Applicative m, Foldable t) =>
t (m Doc) -> m Doc
vcat forall a b. (a -> b) -> a -> b
$ forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap forall (m :: * -> *). MonadPretty m => QName -> m Doc
nameWithBinding forall a b. (a -> b) -> a -> b
$ AmbiguousNameReason -> List2 QName
ambiguousNamesInReason AmbiguousNameReason
reason
      , forall (m :: * -> *). MonadPretty m => WhyInScopeData -> m Doc
explainWhyInScope forall a b. (a -> b) -> a -> b
$ QName -> AmbiguousNameReason -> WhyInScopeData
whyInScopeDataFromAmbiguousNameReason QName
x AmbiguousNameReason
reason
      ]

    AmbiguousModule QName
x List1 ModuleName
ys -> 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 a b. (a -> b) -> a -> b
$ forall (m :: * -> *). Applicative m => [Char] -> [m Doc]
pwords [Char]
"Ambiguous module name" forall a. [a] -> [a] -> [a]
++ [forall (m :: * -> *) a. (Applicative m, Pretty a) => a -> m Doc
pretty QName
x forall a. Semigroup a => a -> a -> a
<> m Doc
"."] forall a. [a] -> [a] -> [a]
++
               forall (m :: * -> *). Applicative m => [Char] -> [m Doc]
pwords [Char]
"It could refer to any one of"
      , forall (m :: * -> *). Functor m => Int -> m Doc -> m Doc
nest Int
2 forall a b. (a -> b) -> a -> b
$ forall (m :: * -> *) (t :: * -> *).
(Applicative m, Foldable t) =>
t (m Doc) -> m Doc
vcat forall a b. (a -> b) -> a -> b
$ forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap forall (m :: * -> *). MonadPretty m => ModuleName -> m Doc
help List1 ModuleName
ys
      , forall (m :: * -> *). Applicative m => [Char] -> m Doc
fwords [Char]
"(hint: Use C-c C-w (in Emacs) if you want to know why)"
      ]
      where
        help :: MonadPretty m => ModuleName -> m Doc
        help :: forall (m :: * -> *). MonadPretty m => ModuleName -> m Doc
help ModuleName
m = do
          m Doc
anno <- forall (m :: * -> *) a b.
Monad m =>
m (Maybe a) -> m b -> (a -> m b) -> m b
caseMaybeM (forall (m :: * -> *).
ReadTCState m =>
ModuleName -> m (Maybe DataOrRecordModule)
isDatatypeModule ModuleName
m) (forall (m :: * -> *) a. Monad m => a -> m a
return forall a. Null a => a
empty) forall a b. (a -> b) -> a -> b
$ \case
            DataOrRecordModule
IsDataModule   -> forall (m :: * -> *) a. Monad m => a -> m a
return forall a b. (a -> b) -> a -> b
$ m Doc
"(datatype module)"
            DataOrRecordModule
IsRecordModule -> forall (m :: * -> *) a. Monad m => a -> m a
return forall a b. (a -> b) -> a -> b
$ m Doc
"(record module)"
          forall (m :: * -> *) (t :: * -> *).
(Applicative m, Foldable t) =>
t (m Doc) -> m Doc
sep [forall a (m :: * -> *). (PrettyTCM a, MonadPretty m) => a -> m Doc
prettyTCM ModuleName
m, m Doc
anno ]

    ClashingDefinition QName
x QName
y Maybe NiceDeclaration
suggestion -> 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]
"Multiple definitions of" forall a. [a] -> [a] -> [a]
++ [forall (m :: * -> *) a. (Applicative m, Pretty a) => a -> m Doc
pretty QName
x forall a. Semigroup a => a -> a -> a
<> m Doc
"."] forall a. [a] -> [a] -> [a]
++
      forall (m :: * -> *). Applicative m => [Char] -> [m Doc]
pwords [Char]
"Previous definition at"
      forall a. [a] -> [a] -> [a]
++ [forall a (m :: * -> *). (PrettyTCM a, MonadPretty m) => a -> m Doc
prettyTCM forall a b. (a -> b) -> a -> b
$ Name -> Range
nameBindingSite forall a b. (a -> b) -> a -> b
$ QName -> Name
qnameName QName
y] forall a. [a] -> [a] -> [a]
++
      forall a b. Maybe a -> b -> (a -> b) -> b
caseMaybe Maybe NiceDeclaration
suggestion [] (\NiceDeclaration
d ->
        [  m Doc
"Perhaps you meant to write "
        forall (m :: * -> *). Applicative m => m Doc -> m Doc -> m Doc
$$ forall (m :: * -> *). Functor m => Int -> m Doc -> m Doc
nest Int
2 (m Doc
"'" forall a. Semigroup a => a -> a -> a
<> forall (m :: * -> *) a. (Applicative m, Pretty a) => a -> m Doc
pretty (NiceDeclaration -> [Declaration]
notSoNiceDeclarations NiceDeclaration
d) forall a. Semigroup a => a -> a -> a
<> m Doc
"'")
        forall (m :: * -> *). Applicative m => m Doc -> m Doc -> m Doc
$$ (m Doc
"at" forall (m :: * -> *). Applicative m => m Doc -> m Doc -> m Doc
<+> (forall (m :: * -> *) a. (Applicative m, Pretty a) => a -> m Doc
pretty forall b c a. (b -> c) -> (a -> b) -> a -> c
. TCEnv -> Range
envRange forall (m :: * -> *) a b. Monad m => (a -> m b) -> m a -> m b
=<< forall (m :: * -> *). MonadTCEnv m => m TCEnv
askTC)) forall a. Semigroup a => a -> a -> a
<> m Doc
"?"
        forall (m :: * -> *). Applicative m => m Doc -> m Doc -> m Doc
$$ m Doc
"In data definitions separate from data declaration, the ':' and type must be omitted."
        ])

    ClashingModule ModuleName
m1 ModuleName
m2 -> 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]
"The modules" forall a. [a] -> [a] -> [a]
++ [forall a (m :: * -> *). (PrettyTCM a, MonadPretty m) => a -> m Doc
prettyTCM ModuleName
m1, m Doc
"and", forall a (m :: * -> *). (PrettyTCM a, MonadPretty m) => a -> m Doc
prettyTCM ModuleName
m2]
      forall a. [a] -> [a] -> [a]
++ forall (m :: * -> *). Applicative m => [Char] -> [m Doc]
pwords [Char]
"clash."

    ClashingImport Name
x QName
y -> 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]
"Import clash between" forall a. [a] -> [a] -> [a]
++ [forall (m :: * -> *) a. (Applicative m, Pretty a) => a -> m Doc
pretty Name
x, m Doc
"and", forall a (m :: * -> *). (PrettyTCM a, MonadPretty m) => a -> m Doc
prettyTCM QName
y]

    ClashingModuleImport Name
x ModuleName
y -> 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]
"Module import clash between" forall a. [a] -> [a] -> [a]
++ [forall (m :: * -> *) a. (Applicative m, Pretty a) => a -> m Doc
pretty Name
x, m Doc
"and", forall a (m :: * -> *). (PrettyTCM a, MonadPretty m) => a -> m Doc
prettyTCM ModuleName
y]

    PatternShadowsConstructor Name
x QName
c -> 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]
"The pattern variable" forall a. [a] -> [a] -> [a]
++ [forall a (m :: * -> *). (PrettyTCM a, MonadPretty m) => a -> m Doc
prettyTCM Name
x] forall a. [a] -> [a] -> [a]
++
      forall (m :: * -> *). Applicative m => [Char] -> [m Doc]
pwords [Char]
"has the same name as the constructor" forall a. [a] -> [a] -> [a]
++ [forall a (m :: * -> *). (PrettyTCM a, MonadPretty m) => a -> m Doc
prettyTCM QName
c]

    DuplicateImports QName
m [ImportedName]
xs -> 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]
"Ambiguous imports from module" forall a. [a] -> [a] -> [a]
++ [forall (m :: * -> *) a. (Applicative m, Pretty a) => a -> m Doc
pretty QName
m] forall a. [a] -> [a] -> [a]
++ forall (m :: * -> *). Applicative m => [Char] -> [m Doc]
pwords [Char]
"for" forall a. [a] -> [a] -> [a]
++
      forall (m :: * -> *) (t :: * -> *).
(Applicative m, Semigroup (m Doc), Foldable t) =>
m Doc -> t (m Doc) -> [m Doc]
punctuate forall (m :: * -> *). Applicative m => m Doc
comma (forall a b. (a -> b) -> [a] -> [b]
map forall (m :: * -> *) a. (Applicative m, Pretty a) => a -> m Doc
pretty [ImportedName]
xs)

    NotAModuleExpr 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]
"The right-hand side of a module definition must have the form 'M e1 .. en'" forall a. [a] -> [a] -> [a]
++
      forall (m :: * -> *). Applicative m => [Char] -> [m Doc]
pwords [Char]
"where M is a module name. The expression"
      forall a. [a] -> [a] -> [a]
++ [forall (m :: * -> *) a. (Applicative m, Pretty a) => a -> m Doc
pretty Expr
e, m Doc
"doesn't."]

    TypeError
FieldOutsideRecord -> 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]
"Field appearing outside record declaration."

    InvalidPattern Pattern
p -> forall (m :: * -> *) (t :: * -> *).
(Applicative m, Foldable t) =>
t (m Doc) -> m Doc
fsep forall a b. (a -> b) -> a -> b
$
      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]
"is not a valid pattern"

    RepeatedVariablesInPattern [Name]
xs -> 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]
"Repeated variables in pattern:" forall a. [a] -> [a] -> [a]
++ forall a b. (a -> b) -> [a] -> [b]
map forall (m :: * -> *) a. (Applicative m, Pretty a) => a -> m Doc
pretty [Name]
xs

    NotAnExpression Expr
e -> forall (m :: * -> *) (t :: * -> *).
(Applicative m, Foldable t) =>
t (m Doc) -> m Doc
fsep forall a b. (a -> b) -> a -> b
$
      forall (m :: * -> *) a. (Applicative m, Pretty a) => a -> m Doc
pretty Expr
e forall a. a -> [a] -> [a]
: forall (m :: * -> *). Applicative m => [Char] -> [m Doc]
pwords [Char]
"is not a valid expression."

    NotAValidLetBinding NiceDeclaration
nd -> forall (m :: * -> *). Applicative m => [Char] -> m Doc
fwords forall a b. (a -> b) -> a -> b
$
      [Char]
"Not a valid let-declaration"

    NotValidBeforeField NiceDeclaration
nd -> forall (m :: * -> *). Applicative m => [Char] -> m Doc
fwords forall a b. (a -> b) -> a -> b
$
      [Char]
"This declaration is illegal in a record before the last field"

    NothingAppliedToHiddenArg Expr
e -> forall (m :: * -> *) (t :: * -> *).
(Applicative m, Foldable t) =>
t (m Doc) -> m Doc
fsep forall a b. (a -> b) -> a -> b
$
      [forall (m :: * -> *) a. (Applicative m, Pretty a) => a -> m Doc
pretty Expr
e] forall a. [a] -> [a] -> [a]
++ forall (m :: * -> *). Applicative m => [Char] -> [m Doc]
pwords [Char]
"cannot appear by itself. It needs to be the argument to" forall a. [a] -> [a] -> [a]
++
      forall (m :: * -> *). Applicative m => [Char] -> [m Doc]
pwords [Char]
"a function expecting an implicit argument."

    NothingAppliedToInstanceArg Expr
e -> forall (m :: * -> *) (t :: * -> *).
(Applicative m, Foldable t) =>
t (m Doc) -> m Doc
fsep forall a b. (a -> b) -> a -> b
$
      [forall (m :: * -> *) a. (Applicative m, Pretty a) => a -> m Doc
pretty Expr
e] forall a. [a] -> [a] -> [a]
++ forall (m :: * -> *). Applicative m => [Char] -> [m Doc]
pwords [Char]
"cannot appear by itself. It needs to be the argument to" forall a. [a] -> [a] -> [a]
++
      forall (m :: * -> *). Applicative m => [Char] -> [m Doc]
pwords [Char]
"a function expecting an instance argument."

    NoParseForApplication List2 Expr
es -> forall (m :: * -> *) (t :: * -> *).
(Applicative m, Foldable t) =>
t (m Doc) -> m Doc
fsep (
      forall (m :: * -> *). Applicative m => [Char] -> [m Doc]
pwords [Char]
"Could not parse the application" forall a. [a] -> [a] -> [a]
++ [forall (m :: * -> *) a. (Applicative m, Pretty a) => a -> m Doc
pretty forall a b. (a -> b) -> a -> b
$ Range -> List2 Expr -> Expr
C.RawApp forall a. Range' a
noRange List2 Expr
es])

    AmbiguousParseForApplication List2 Expr
es List1 Expr
es' -> forall (m :: * -> *) (t :: * -> *).
(Applicative m, Foldable t) =>
t (m Doc) -> m Doc
fsep (
      forall (m :: * -> *). Applicative m => [Char] -> [m Doc]
pwords [Char]
"Don't know how to parse" forall a. [a] -> [a] -> [a]
++ [forall (m :: * -> *). MonadPretty m => m Doc
pretty_es forall a. Semigroup a => a -> a -> a
<> m Doc
"."] forall a. [a] -> [a] -> [a]
++
      forall (m :: * -> *). Applicative m => [Char] -> [m Doc]
pwords [Char]
"Could mean any one of:"
      ) 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 (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap forall (m :: * -> *). MonadPretty m => Expr -> m Doc
pretty' List1 Expr
es')
      where
        pretty_es :: MonadPretty m => m Doc
        pretty_es :: forall (m :: * -> *). MonadPretty m => m Doc
pretty_es = forall (m :: * -> *) a. (Applicative m, Pretty a) => a -> m Doc
pretty forall a b. (a -> b) -> a -> b
$ Range -> List2 Expr -> Expr
C.RawApp forall a. Range' a
noRange List2 Expr
es

        pretty' :: MonadPretty m => C.Expr -> m Doc
        pretty' :: forall (m :: * -> *). MonadPretty m => Expr -> m Doc
pretty' Expr
e = do
          Doc
p1 <- forall (m :: * -> *). MonadPretty m => m Doc
pretty_es
          Doc
p2 <- forall (m :: * -> *) a. (Applicative m, Pretty a) => a -> m Doc
pretty Expr
e
          if Doc -> [Char]
render Doc
p1 forall a. Eq a => a -> a -> Bool
== Doc -> [Char]
render Doc
p2 then forall (m :: * -> *). MonadPretty m => Expr -> m Doc
unambiguous Expr
e else forall (m :: * -> *) a. Monad m => a -> m a
return Doc
p2

        unambiguous :: MonadPretty m => C.Expr -> m Doc
        unambiguous :: forall (m :: * -> *). MonadPretty m => Expr -> m Doc
unambiguous e :: Expr
e@(C.OpApp Range
r QName
op Set Name
_ OpAppArgs
xs)
          | forall (t :: * -> *) a. Foldable t => (a -> Bool) -> t a -> Bool
all (forall e. MaybePlaceholder (OpApp e) -> Bool
isOrdinary forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall a. NamedArg a -> a
namedArg) OpAppArgs
xs =
            forall (m :: * -> *) a. (Applicative m, Pretty a) => a -> m Doc
pretty forall a b. (a -> b) -> a -> b
$
              forall (t :: * -> *) b a.
Foldable t =>
(b -> a -> b) -> b -> t a -> b
foldl (Range -> Expr -> NamedArg Expr -> Expr
C.App Range
r) (QName -> Expr
C.Ident QName
op) forall a b. (a -> b) -> a -> b
$
                (forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap) forall e. MaybePlaceholder (OpApp e) -> e
fromOrdinary OpAppArgs
xs
          | forall (t :: * -> *) a. Foldable t => (a -> Bool) -> t a -> Bool
any (forall a. MaybePlaceholder a -> Bool
isPlaceholder forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall a. NamedArg a -> a
namedArg) OpAppArgs
xs =
              forall (m :: * -> *) a. (Applicative m, Pretty a) => a -> m Doc
pretty Expr
e forall (m :: * -> *). Applicative m => m Doc -> m Doc -> m Doc
<+> m Doc
"(section)"
        unambiguous Expr
e = forall (m :: * -> *) a. (Applicative m, Pretty a) => a -> m Doc
pretty Expr
e

        isOrdinary :: MaybePlaceholder (C.OpApp e) -> Bool
        isOrdinary :: forall e. MaybePlaceholder (OpApp e) -> Bool
isOrdinary (NoPlaceholder Maybe PositionInName
_ (C.Ordinary e
_)) = Bool
True
        isOrdinary MaybePlaceholder (OpApp e)
_                                = Bool
False

        fromOrdinary :: MaybePlaceholder (C.OpApp e) -> e
        fromOrdinary :: forall e. MaybePlaceholder (OpApp e) -> e
fromOrdinary (NoPlaceholder Maybe PositionInName
_ (C.Ordinary e
e)) = e
e
        fromOrdinary MaybePlaceholder (OpApp e)
_                                = forall a. HasCallStack => a
__IMPOSSIBLE__

        isPlaceholder :: MaybePlaceholder a -> Bool
        isPlaceholder :: forall a. MaybePlaceholder a -> Bool
isPlaceholder Placeholder{}   = Bool
True
        isPlaceholder NoPlaceholder{} = Bool
False

    BadArgumentsToPatternSynonym AmbiguousQName
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]
"Bad arguments to pattern synonym " forall a. [a] -> [a] -> [a]
++ [forall a (m :: * -> *). (PrettyTCM a, MonadPretty m) => a -> m Doc
prettyTCM forall a b. (a -> b) -> a -> b
$ AmbiguousQName -> QName
headAmbQ AmbiguousQName
x]

    TooFewArgumentsToPatternSynonym AmbiguousQName
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]
"Too few arguments to pattern synonym " forall a. [a] -> [a] -> [a]
++ [forall a (m :: * -> *). (PrettyTCM a, MonadPretty m) => a -> m Doc
prettyTCM forall a b. (a -> b) -> a -> b
$ AmbiguousQName -> QName
headAmbQ AmbiguousQName
x]

    CannotResolveAmbiguousPatternSynonym List1 (QName, PatternSynDefn)
defs -> 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 a b. (a -> b) -> a -> b
$ forall (m :: * -> *). Applicative m => [Char] -> [m Doc]
pwords [Char]
"Cannot resolve overloaded pattern synonym" forall a. [a] -> [a] -> [a]
++ [forall a (m :: * -> *). (PrettyTCM a, MonadPretty m) => a -> m Doc
prettyTCM QName
x 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]
"since candidates have different shapes:"
      , forall (m :: * -> *). Functor m => Int -> m Doc -> m Doc
nest Int
2 forall a b. (a -> b) -> a -> b
$ forall (m :: * -> *) (t :: * -> *).
(Applicative m, Foldable t) =>
t (m Doc) -> m Doc
vcat forall a b. (a -> b) -> a -> b
$ forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap forall {m :: * -> *}.
(MonadFresh NameId m, MonadInteractionPoints m,
 MonadStConcreteNames m, PureTCM m, IsString (m Doc), Null (m Doc),
 Semigroup (m Doc)) =>
(QName, PatternSynDefn) -> m Doc
prDef List1 (QName, PatternSynDefn)
defs
      , 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]
"(hint: overloaded pattern synonyms must be equal up to variable and constructor names)"
      ]
      where
        (QName
x, PatternSynDefn
_) = forall a. NonEmpty a -> a
List1.head List1 (QName, PatternSynDefn)
defs
        prDef :: (QName, PatternSynDefn) -> m Doc
prDef (QName
x, ([Arg Name]
xs, Pattern' Void
p)) = forall a (m :: * -> *).
(ToConcrete a, Pretty (ConOfAbs a), MonadAbsToCon m) =>
a -> m Doc
prettyA (QName -> [Arg BindName] -> Pattern' Void -> Declaration
A.PatternSynDef QName
x (forall a b. (a -> b) -> [a] -> [b]
map (forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap Name -> BindName
BindName) [Arg Name]
xs) Pattern' Void
p) forall (m :: * -> *). Applicative m => m Doc -> m Doc -> m Doc
<?> (m Doc
"at" forall (m :: * -> *). Applicative m => m Doc -> m Doc -> m Doc
<+> forall (m :: * -> *) a. (Applicative m, Pretty a) => a -> m Doc
pretty Range
r)
          where r :: Range
r = Name -> Range
nameBindingSite forall a b. (a -> b) -> a -> b
$ QName -> Name
qnameName QName
x

    TypeError
UnusedVariableInPatternSynonym -> 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]
"Unused variable in pattern synonym."

    NoParseForLHS LHSOrPatSyn
lhsOrPatSyn [Pattern]
errs Pattern
p -> 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 a b. (a -> b) -> a -> b
$ forall (m :: * -> *). Applicative m => [Char] -> [m Doc]
pwords [Char]
"Could not parse the" forall a. [a] -> [a] -> [a]
++ [m Doc]
prettyLhsOrPatSyn forall a. [a] -> [a] -> [a]
++ [forall (m :: * -> *) a. (Applicative m, Pretty a) => a -> m Doc
pretty Pattern
p]
      , m Doc
prettyErrs
      ]
      where
      prettyLhsOrPatSyn :: [m Doc]
prettyLhsOrPatSyn = forall (m :: * -> *). Applicative m => [Char] -> [m Doc]
pwords forall a b. (a -> b) -> a -> b
$ case LHSOrPatSyn
lhsOrPatSyn of
        LHSOrPatSyn
IsLHS    -> [Char]
"left-hand side"
        LHSOrPatSyn
IsPatSyn -> [Char]
"pattern synonym"
      prettyErrs :: m Doc
prettyErrs = case [Pattern]
errs of
        []     -> forall a. Null a => a
empty
        Pattern
p0 : [Pattern]
_ -> 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]
"Problematic expression:" forall a. [a] -> [a] -> [a]
++ [forall (m :: * -> *) a. (Applicative m, Pretty a) => a -> m Doc
pretty Pattern
p0]

{- UNUSED
    NoParseForPatternSynonym p -> fsep $
      pwords "Could not parse the pattern synonym" ++ [pretty p]
-}

    AmbiguousParseForLHS LHSOrPatSyn
lhsOrPatSyn Pattern
p [Pattern]
ps -> do
      Doc
d <- forall (m :: * -> *) a. (Applicative m, Pretty a) => a -> m Doc
pretty Pattern
p
      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]
"Don't know how to parse" forall a. [a] -> [a] -> [a]
++ [forall (f :: * -> *) a. Applicative f => a -> f a
pure Doc
d forall a. Semigroup a => a -> a -> a
<> m Doc
"."] forall a. [a] -> [a] -> [a]
++
            forall (m :: * -> *). Applicative m => [Char] -> [m Doc]
pwords [Char]
"Could mean any one of:"
        ]
          forall a. [a] -> [a] -> [a]
++
        forall a b. (a -> b) -> [a] -> [b]
map (forall (m :: * -> *). Functor m => Int -> m Doc -> m Doc
nest Int
2 forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall (m :: * -> *). MonadPretty m => Doc -> Pattern -> m Doc
pretty' Doc
d) [Pattern]
ps
      where
        pretty' :: MonadPretty m => Doc -> C.Pattern -> m Doc
        pretty' :: forall (m :: * -> *). MonadPretty m => Doc -> Pattern -> m Doc
pretty' Doc
d1 Pattern
p' = do
          Doc
d2 <- forall (m :: * -> *) a. (Applicative m, Pretty a) => a -> m Doc
pretty Pattern
p'
          if Doc -> [Char]
render Doc
d1 forall a. Eq a => a -> a -> Bool
== Doc -> [Char]
render Doc
d2 then forall (m :: * -> *) a. (Applicative m, Pretty a) => a -> m Doc
pretty forall a b. (a -> b) -> a -> b
$ Pattern -> Pattern
unambiguousP Pattern
p' else forall (m :: * -> *) a. Monad m => a -> m a
return Doc
d2

        -- the entire pattern is shown, not just the ambiguous part,
        -- so we need to dig in order to find the OpAppP's.
        unambiguousP :: C.Pattern -> C.Pattern
        unambiguousP :: Pattern -> Pattern
unambiguousP (C.AppP Pattern
x Arg (Named NamedName Pattern)
y)         = Pattern -> Arg (Named NamedName Pattern) -> Pattern
C.AppP (Pattern -> Pattern
unambiguousP Pattern
x) forall a b. (a -> b) -> a -> b
$ (forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmapforall b c a. (b -> c) -> (a -> b) -> a -> c
.forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap) Pattern -> Pattern
unambiguousP Arg (Named NamedName Pattern)
y
        unambiguousP (C.HiddenP Range
r Named NamedName Pattern
x)      = Range -> Named NamedName Pattern -> Pattern
C.HiddenP Range
r forall a b. (a -> b) -> a -> b
$ forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap Pattern -> Pattern
unambiguousP Named NamedName Pattern
x
        unambiguousP (C.InstanceP Range
r Named NamedName Pattern
x)    = Range -> Named NamedName Pattern -> Pattern
C.InstanceP Range
r forall a b. (a -> b) -> a -> b
$ forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap Pattern -> Pattern
unambiguousP Named NamedName Pattern
x
        unambiguousP (C.ParenP Range
r Pattern
x)       = Range -> Pattern -> Pattern
C.ParenP Range
r forall a b. (a -> b) -> a -> b
$ Pattern -> Pattern
unambiguousP Pattern
x
        unambiguousP (C.AsP Range
r Name
n Pattern
x)        = Range -> Name -> Pattern -> Pattern
C.AsP Range
r Name
n forall a b. (a -> b) -> a -> b
$ Pattern -> Pattern
unambiguousP Pattern
x
        unambiguousP (C.OpAppP Range
r QName
op Set Name
_ [Arg (Named NamedName Pattern)]
xs) = forall (t :: * -> *) b a.
Foldable t =>
(b -> a -> b) -> b -> t a -> b
foldl Pattern -> Arg (Named NamedName Pattern) -> Pattern
C.AppP (QName -> Pattern
C.IdentP QName
op) [Arg (Named NamedName Pattern)]
xs
        unambiguousP Pattern
e                    = Pattern
e

    OperatorInformation [NotationSection]
sects TypeError
err ->
      forall a (m :: * -> *). (PrettyTCM a, MonadPretty m) => a -> m Doc
prettyTCM TypeError
err
        forall (m :: * -> *). Applicative m => m Doc -> m Doc -> m Doc
$+$
      forall (m :: * -> *) (t :: * -> *).
(Applicative m, Foldable t) =>
t (m Doc) -> m Doc
fsep (forall (m :: * -> *). Applicative m => [Char] -> [m Doc]
pwords [Char]
"Operators used in the grammar:")
        forall (m :: * -> *). Applicative m => m Doc -> m Doc -> m Doc
$$
      forall (m :: * -> *). Functor m => Int -> m Doc -> m Doc
nest Int
2
        (if forall a. Null a => a -> Bool
null [NotationSection]
sects then m Doc
"None" else
         forall (m :: * -> *) (t :: * -> *).
(Applicative m, Foldable t) =>
t (m Doc) -> m Doc
vcat (forall a b. (a -> b) -> [a] -> [b]
map forall (m :: * -> *). Applicative m => [Char] -> m Doc
text forall a b. (a -> b) -> a -> b
$
               [Char] -> [[Char]]
lines forall a b. (a -> b) -> a -> b
$
               Box -> [Char]
Boxes.render forall a b. (a -> b) -> a -> b
$
               (\([Box]
col1, [Box]
col2, [Box]
col3) ->
                   forall (f :: * -> *).
Foldable f =>
Int -> Alignment -> f Box -> Box
Boxes.hsep Int
1 Alignment
Boxes.top forall a b. (a -> b) -> a -> b
$
                   forall a b. (a -> b) -> [a] -> [b]
map (forall (f :: * -> *). Foldable f => Alignment -> f Box -> Box
Boxes.vcat Alignment
Boxes.left) [[Box]
col1, [Box]
col2, [Box]
col3]) forall a b. (a -> b) -> a -> b
$
               forall a b c. [(a, b, c)] -> ([a], [b], [c])
unzip3 forall a b. (a -> b) -> a -> b
$
               forall a b. (a -> b) -> [a] -> [b]
map NotationSection -> (Box, Box, Box)
prettySect forall a b. (a -> b) -> a -> b
$
               forall a. (a -> a -> Ordering) -> [a] -> [a]
sortBy (forall a. Ord a => a -> a -> Ordering
compare forall b c a. (b -> b -> c) -> (a -> b) -> a -> a -> c
`on` forall a. Pretty a => a -> [Char]
prettyShow forall b c a. (b -> c) -> (a -> b) -> a -> c
. NewNotation -> QName
notaName forall b c a. (b -> c) -> (a -> b) -> a -> c
. NotationSection -> NewNotation
sectNotation) forall a b. (a -> b) -> a -> b
$
               forall a. (a -> Bool) -> [a] -> [a]
filter (Bool -> Bool
not forall b c a. (b -> c) -> (a -> b) -> a -> c
. NotationSection -> Bool
closedWithoutHoles) [NotationSection]
sects))
      where
      trimLeft :: [NotationPart] -> [NotationPart]
trimLeft  = forall a. (a -> Bool) -> [a] -> [a]
dropWhile NotationPart -> Bool
isAHole
      trimRight :: [NotationPart] -> [NotationPart]
trimRight = forall a. (a -> Bool) -> [a] -> [a]
dropWhileEnd NotationPart -> Bool
isAHole

      closedWithoutHoles :: NotationSection -> Bool
closedWithoutHoles NotationSection
sect =
        NotationSection -> NotationKind
sectKind NotationSection
sect forall a. Eq a => a -> a -> Bool
== NotationKind
NonfixNotation
          Bool -> Bool -> Bool
&&
        forall a. Null a => a -> Bool
null [ () | HolePart{} <- [NotationPart] -> [NotationPart]
trimLeft forall a b. (a -> b) -> a -> b
$ [NotationPart] -> [NotationPart]
trimRight forall a b. (a -> b) -> a -> b
$
                                    NewNotation -> [NotationPart]
notation (NotationSection -> NewNotation
sectNotation NotationSection
sect) ]

      prettyName :: Name -> Box
prettyName Name
n = [Char] -> Box
Boxes.text forall a b. (a -> b) -> a -> b
$
        Doc -> [Char]
P.render (forall a. Pretty a => a -> Doc
P.pretty Name
n) forall a. [a] -> [a] -> [a]
++
        [Char]
" (" forall a. [a] -> [a] -> [a]
++ Doc -> [Char]
P.render (forall a. Pretty a => a -> Doc
P.pretty (Name -> Range
nameBindingSite Name
n)) forall a. [a] -> [a] -> [a]
++ [Char]
")"

      prettySect :: NotationSection -> (Box, Box, Box)
prettySect NotationSection
sect =
        ( [Char] -> Box
Boxes.text (Doc -> [Char]
P.render (forall a. Pretty a => a -> Doc
P.pretty [NotationPart]
section))
            Box -> Box -> Box
Boxes.//
          Box
strut
        , [Char] -> Box
Boxes.text
            ([Char]
"(" forall a. [a] -> [a] -> [a]
++
             [Char]
kind forall a. [a] -> [a] -> [a]
++ [Char]
" " forall a. [a] -> [a] -> [a]
++
             (if NewNotation -> Bool
notaIsOperator NewNotation
nota
              then [Char]
"operator"
              else [Char]
"notation") forall a. [a] -> [a] -> [a]
++
             (if NotationSection -> Bool
sectIsSection NotationSection
sect
              then [Char]
" section"
              else [Char]
"") forall a. [a] -> [a] -> [a]
++
             (case NotationSection -> Maybe FixityLevel
sectLevel NotationSection
sect of
                Maybe FixityLevel
Nothing          -> [Char]
""
                Just FixityLevel
Unrelated   -> [Char]
", unrelated"
                Just (Related PrecedenceLevel
l) -> [Char]
", level " forall a. [a] -> [a] -> [a]
++ PrecedenceLevel -> [Char]
toStringWithoutDotZero PrecedenceLevel
l) forall a. [a] -> [a] -> [a]
++
             [Char]
")")
            Box -> Box -> Box
Boxes.//
          Box
strut
        , Box
"["
            Box -> Box -> Box
Boxes.<>
          forall (f :: * -> *). Foldable f => Alignment -> f Box -> Box
Boxes.vcat Alignment
Boxes.left
            (forall a b. (a -> b) -> [a] -> [b]
map (\Name
n -> Name -> Box
prettyName Name
n Box -> Box -> Box
Boxes.<> Box
",") [Name]
names forall a. [a] -> [a] -> [a]
++
             [Name -> Box
prettyName Name
name Box -> Box -> Box
Boxes.<> Box
"]"])
        )
        where
        nota :: NewNotation
nota    = NotationSection -> NewNotation
sectNotation NotationSection
sect
        section :: [NotationPart]
section = [Char] -> [NotationPart] -> [NotationPart]
qualifyFirstIdPart
                    (forall (t :: * -> *) a b.
Foldable t =>
(a -> b -> b) -> b -> t a -> b
foldr (\Name
x [Char]
s -> Name -> [Char]
C.nameToRawName Name
x forall a. [a] -> [a] -> [a]
++ [Char]
"." forall a. [a] -> [a] -> [a]
++ [Char]
s)
                           [Char]
""
                           (forall a. NonEmpty a -> [a]
List1.init (QName -> List1 Name
C.qnameParts (NewNotation -> QName
notaName NewNotation
nota))))
                    ([NotationPart] -> [NotationPart]
spacesBetweenAdjacentIds forall a b. (a -> b) -> a -> b
$
                     [NotationPart] -> [NotationPart]
trim (NewNotation -> [NotationPart]
notation NewNotation
nota))

        qualifyFirstIdPart :: [Char] -> [NotationPart] -> [NotationPart]
qualifyFirstIdPart [Char]
_ []              = []
        qualifyFirstIdPart [Char]
q (IdPart Ranged [Char]
x : [NotationPart]
ps) = Ranged [Char] -> NotationPart
IdPart (forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap ([Char]
q forall a. [a] -> [a] -> [a]
++) Ranged [Char]
x) forall a. a -> [a] -> [a]
: [NotationPart]
ps
        qualifyFirstIdPart [Char]
q (NotationPart
p : [NotationPart]
ps)        = NotationPart
p forall a. a -> [a] -> [a]
: [Char] -> [NotationPart] -> [NotationPart]
qualifyFirstIdPart [Char]
q [NotationPart]
ps

        spacesBetweenAdjacentIds :: [NotationPart] -> [NotationPart]
spacesBetweenAdjacentIds (IdPart Ranged [Char]
x : ps :: [NotationPart]
ps@(IdPart Ranged [Char]
_ : [NotationPart]
_)) =
          Ranged [Char] -> NotationPart
IdPart Ranged [Char]
x forall a. a -> [a] -> [a]
: Ranged [Char] -> NotationPart
IdPart (forall a. a -> Ranged a
unranged [Char]
" ") forall a. a -> [a] -> [a]
: [NotationPart] -> [NotationPart]
spacesBetweenAdjacentIds [NotationPart]
ps
        spacesBetweenAdjacentIds (NotationPart
p : [NotationPart]
ps) =
          NotationPart
p forall a. a -> [a] -> [a]
: [NotationPart] -> [NotationPart]
spacesBetweenAdjacentIds [NotationPart]
ps
        spacesBetweenAdjacentIds [] = []

        trim :: [NotationPart] -> [NotationPart]
trim = case NotationSection -> NotationKind
sectKind NotationSection
sect of
          NotationKind
InfixNotation   -> [NotationPart] -> [NotationPart]
trimLeft forall b c a. (b -> c) -> (a -> b) -> a -> c
. [NotationPart] -> [NotationPart]
trimRight
          NotationKind
PrefixNotation  -> [NotationPart] -> [NotationPart]
trimRight
          NotationKind
PostfixNotation -> [NotationPart] -> [NotationPart]
trimLeft
          NotationKind
NonfixNotation  -> forall a. a -> a
id
          NotationKind
NoNotation      -> forall a. HasCallStack => a
__IMPOSSIBLE__

        ([Name]
names, Name
name) = forall a. a -> Maybe a -> a
fromMaybe forall a. HasCallStack => a
__IMPOSSIBLE__ forall a b. (a -> b) -> a -> b
$ forall a. [a] -> Maybe ([a], a)
initLast forall a b. (a -> b) -> a -> b
$ forall a. Set a -> [a]
Set.toList forall a b. (a -> b) -> a -> b
$ NewNotation -> Set Name
notaNames NewNotation
nota

        strut :: Box
strut = Int -> Int -> Box
Boxes.emptyBox (forall (t :: * -> *) a. Foldable t => t a -> Int
length [Name]
names) Int
0

        kind :: [Char]
kind = case NotationSection -> NotationKind
sectKind NotationSection
sect of
          NotationKind
PrefixNotation  -> [Char]
"prefix"
          NotationKind
PostfixNotation -> [Char]
"postfix"
          NotationKind
NonfixNotation  -> [Char]
"closed"
          NotationKind
NoNotation      -> forall a. HasCallStack => a
__IMPOSSIBLE__
          NotationKind
InfixNotation   ->
            case Fixity -> Associativity
fixityAssoc forall a b. (a -> b) -> a -> b
$ NewNotation -> Fixity
notaFixity NewNotation
nota of
              Associativity
NonAssoc   -> [Char]
"infix"
              Associativity
LeftAssoc  -> [Char]
"infixl"
              Associativity
RightAssoc -> [Char]
"infixr"

{- UNUSED
    AmbiguousParseForPatternSynonym p ps -> fsep (
      pwords "Don't know how to parse" ++ [pretty p <> "."] ++
      pwords "Could mean any one of:"
      ) $$ nest 2 (vcat $ map pretty ps)
-}

{- UNUSED
    IncompletePatternMatching v args -> fsep $
      pwords "Incomplete pattern matching for" ++ [prettyTCM v <> "."] ++
      pwords "No match for" ++ map prettyTCM args
-}

    SplitError SplitError
e -> forall a (m :: * -> *). (PrettyTCM a, MonadPretty m) => a -> m Doc
prettyTCM SplitError
e

    ImpossibleConstructor QName
c NegativeUnification
neg -> 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]
"The case for 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]
" is impossible" forall a. [a] -> [a] -> [a]
++ [forall a (m :: * -> *). (PrettyTCM a, MonadPretty m) => a -> m Doc
prettyTCM NegativeUnification
neg] forall a. [a] -> [a] -> [a]
++
      forall (m :: * -> *). Applicative m => [Char] -> [m Doc]
pwords [Char]
"Possible solution: remove the clause, or use an absurd pattern ()."

    TooManyPolarities QName
x Int
n -> 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]
"Too many polarities given in the POLARITY pragma for" 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]
"(at most" forall a. [a] -> [a] -> [a]
++ [forall (m :: * -> *). Applicative m => [Char] -> m Doc
text (forall a. Show a => a -> [Char]
show Int
n)] forall a. [a] -> [a] -> [a]
++ forall (m :: * -> *). Applicative m => [Char] -> [m Doc]
pwords [Char]
"allowed)."

    InstanceNoCandidate Type
t [(Term, TCErr)]
errs -> 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]
"No instance of 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]
"was found in scope."
      , 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} {a}.
(MonadFresh NameId m, MonadInteractionPoints m,
 MonadStConcreteNames m, PureTCM m, IsString (m Doc), Null (m Doc),
 Semigroup (m Doc), PrettyTCM a, PrettyTCM a) =>
(a, a) -> m Doc
prCand [(Term, TCErr)]
errs ]
      where
        prCand :: (a, a) -> m Doc
prCand (a
term, a
err) =
          forall (m :: * -> *). Applicative m => [Char] -> m Doc
text [Char]
"-" forall (m :: * -> *). Applicative m => m Doc -> m Doc -> m Doc
<+>
            forall (m :: * -> *) (t :: * -> *).
(Applicative m, Foldable t) =>
t (m Doc) -> m Doc
vcat [ forall a (m :: * -> *). (PrettyTCM a, MonadPretty m) => a -> m Doc
prettyTCM a
term forall (m :: * -> *). Applicative m => m Doc -> m Doc -> m Doc
<?> forall (m :: * -> *). Applicative m => [Char] -> m Doc
text [Char]
"was ruled out because"
                 , forall a (m :: * -> *). (PrettyTCM a, MonadPretty m) => a -> m Doc
prettyTCM a
err ]

    UnquoteFailed UnquoteError
e -> case UnquoteError
e of
      BadVisibility [Char]
msg Arg Term
arg -> 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 forall a b. (a -> b) -> a -> b
$ [Char]
"Unable to unquote the argument. It should be `" forall a. [a] -> [a] -> [a]
++ [Char]
msg forall a. [a] -> [a] -> [a]
++ [Char]
"'."

      ConInsteadOfDef QName
x [Char]
def [Char]
con -> 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]
"Use " forall a. [a] -> [a] -> [a]
++ [Char]
con forall a. [a] -> [a] -> [a]
++ [Char]
" instead of " forall a. [a] -> [a] -> [a]
++ [Char]
def forall a. [a] -> [a] -> [a]
++ [Char]
" for constructor") forall a. [a] -> [a] -> [a]
++
        [forall a (m :: * -> *). (PrettyTCM a, MonadPretty m) => a -> m Doc
prettyTCM QName
x]

      DefInsteadOfCon QName
x [Char]
def [Char]
con -> 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]
"Use " forall a. [a] -> [a] -> [a]
++ [Char]
def forall a. [a] -> [a] -> [a]
++ [Char]
" instead of " forall a. [a] -> [a] -> [a]
++ [Char]
con forall a. [a] -> [a] -> [a]
++ [Char]
" for non-constructor")
        forall a. [a] -> [a] -> [a]
++ [forall a (m :: * -> *). (PrettyTCM a, MonadPretty m) => a -> m Doc
prettyTCM QName
x]

      NonCanonical [Char]
kind Term
t ->
        forall (m :: * -> *). Applicative m => [Char] -> m Doc
fwords ([Char]
"Cannot unquote non-canonical " forall a. [a] -> [a] -> [a]
++ [Char]
kind)
        forall (m :: * -> *). Applicative m => m Doc -> m Doc -> m Doc
$$ forall (m :: * -> *). Functor m => Int -> m Doc -> m Doc
nest Int
2 (forall a (m :: * -> *). (PrettyTCM a, MonadPretty m) => a -> m Doc
prettyTCM Term
t)

      BlockedOnMeta TCState
_ Blocker
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 forall a b. (a -> b) -> a -> b
$ [Char]
"Unquote failed because of unsolved meta variables."

      UnquotePanic [Char]
err -> forall a. HasCallStack => a
__IMPOSSIBLE__

    DeBruijnIndexOutOfScope Int
i Telescope
EmptyTel [] -> 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 forall a b. (a -> b) -> a -> b
$ [Char]
"de Bruijn index " forall a. [a] -> [a] -> [a]
++ forall a. Show a => a -> [Char]
show Int
i forall a. [a] -> [a] -> [a]
++ [Char]
" is not in scope in the empty context"
    DeBruijnIndexOutOfScope Int
i Telescope
cxt [Name]
names ->
        forall (m :: * -> *) (t :: * -> *).
(Applicative m, Foldable t) =>
t (m Doc) -> m Doc
sep [ forall (m :: * -> *). Applicative m => [Char] -> m Doc
text ([Char]
"de Bruijn index " forall a. [a] -> [a] -> [a]
++ forall a. Show a => a -> [Char]
show Int
i forall a. [a] -> [a] -> [a]
++ [Char]
" is not in scope in the context")
            , forall (tcm :: * -> *) a.
(MonadTCEnv tcm, ReadTCState tcm) =>
tcm a -> tcm a
inTopContext forall a b. (a -> b) -> a -> b
$ forall b (m :: * -> *) a.
(AddContext b, MonadAddContext m) =>
b -> m a -> m a
addContext ([Char]
"_" :: String) forall a b. (a -> b) -> a -> b
$ forall a (m :: * -> *). (PrettyTCM a, MonadPretty m) => a -> m Doc
prettyTCM Telescope
cxt' ]
      where
        cxt' :: Telescope
cxt' = Telescope
cxt forall t. Abstract t => Telescope -> t -> t
`abstract` forall a. Subst a => Int -> a -> a
raise (forall a. Sized a => a -> Int
size Telescope
cxt) ([Name] -> Telescope
nameCxt [Name]
names)
        nameCxt :: [Name] -> I.Telescope
        nameCxt :: [Name] -> Telescope
nameCxt [] = forall a. Tele a
EmptyTel
        nameCxt (Name
x : [Name]
xs) = forall a. a -> Abs (Tele a) -> Tele a
ExtendTel (forall a. a -> Dom a
defaultDom (forall t a. Sort' t -> a -> Type'' t a
El HasCallStack => Sort
__DUMMY_SORT__ forall a b. (a -> b) -> a -> b
$ Int -> Term
I.var Int
0)) forall a b. (a -> b) -> a -> b
$
          forall a. [Char] -> a -> Abs a
NoAbs (forall a. Pretty a => a -> [Char]
P.prettyShow Name
x) forall a b. (a -> b) -> a -> b
$ [Name] -> Telescope
nameCxt [Name]
xs

    TypeError
NeedOptionCopatterns -> 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]
"Option --copatterns needed to enable destructor patterns"

    TypeError
NeedOptionRewriting  -> 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]
"Option --rewriting needed to add and use rewrite rules"

    TypeError
NeedOptionProp       -> 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]
"Universe Prop is disabled (use options --prop and --no-prop to enable/disable Prop)"

    TypeError
NeedOptionTwoLevel   -> 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]
"Universe SSet is disabled (use option --two-level to enable SSet)"

    GeneralizeNotSupportedHere 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 forall a b. (a -> b) -> a -> b
$ [Char]
"Generalizable variable " forall a. [a] -> [a] -> [a]
++ forall a. Pretty a => a -> [Char]
prettyShow QName
x forall a. [a] -> [a] -> [a]
++ [Char]
" is not supported here"

    TypeError
GeneralizeCyclicDependency -> 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]
"Cyclic dependency between generalized variables"

    TypeError
GeneralizeUnsolvedMeta -> 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]
"Unsolved meta not generalized"

    MultipleFixityDecls [(Name, [Fixity'])]
xs ->
      forall (m :: * -> *) (t :: * -> *).
(Applicative m, Foldable t) =>
t (m Doc) -> m Doc
sep [ 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]
"Multiple fixity or syntax declarations for"
          , 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} {a}.
(Applicative m, Semigroup (m Doc), IsString (m Doc), Pretty a,
 Pretty a) =>
(a, [a]) -> m Doc
f [(Name, [Fixity'])]
xs
          ]
      where
        f :: (a, [a]) -> m Doc
f (a
x, [a]
fs) = (forall (m :: * -> *) a. (Applicative m, Pretty a) => a -> m Doc
pretty a
x forall a. Semigroup a => a -> a -> a
<> m Doc
": ") forall (m :: * -> *). Applicative m => m Doc -> m Doc -> m Doc
<+> forall (m :: * -> *) (t :: * -> *).
(Applicative m, Foldable t) =>
t (m Doc) -> m Doc
fsep (forall a b. (a -> b) -> [a] -> [b]
map forall (m :: * -> *) a. (Applicative m, Pretty a) => a -> m Doc
pretty [a]
fs)

    MultiplePolarityPragmas [Name]
xs -> 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]
"Multiple polarity pragmas for" forall a. [a] -> [a] -> [a]
++ forall a b. (a -> b) -> [a] -> [b]
map forall (m :: * -> *) a. (Applicative m, Pretty a) => a -> m Doc
pretty [Name]
xs

    NonFatalErrors [TCWarning]
ws -> forall (t :: * -> *) a. Foldable t => (a -> a -> a) -> t a -> a
foldr1 forall (m :: * -> *). Applicative m => m Doc -> m Doc -> m Doc
($$) forall a b. (a -> b) -> a -> b
$ forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap forall a (m :: * -> *). (PrettyTCM a, MonadPretty m) => a -> m Doc
prettyTCM [TCWarning]
ws

    InstanceSearchDepthExhausted Term
c Type
a Int
d -> 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]
"Instance search depth exhausted (max depth: " forall a. [a] -> [a] -> [a]
++ forall a. Show a => a -> [Char]
show Int
d forall a. [a] -> [a] -> [a]
++ [Char]
") for candidate") forall a. [a] -> [a] -> [a]
++
      [forall (m :: * -> *).
Applicative m =>
m Doc -> Int -> m Doc -> m Doc
hang (forall a (m :: * -> *). (PrettyTCM a, MonadPretty m) => a -> m Doc
prettyTCM Term
c forall (m :: * -> *). Applicative m => m Doc -> m Doc -> m Doc
<+> m Doc
":") Int
2 (forall a (m :: * -> *). (PrettyTCM a, MonadPretty m) => a -> m Doc
prettyTCM Type
a)]

    TriedToCopyConstrainedPrim QName
q -> 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]
"Cannot create a module containing a copy of" forall a. [a] -> [a] -> [a]
++ [forall a (m :: * -> *). (PrettyTCM a, MonadPretty m) => a -> m Doc
prettyTCM QName
q]
    SortOfSplitVarError Maybe Blocker
_ Doc
doc -> forall (m :: * -> *) a. Monad m => a -> m a
return Doc
doc

    where
    mpar :: a -> a -> m Doc -> m Doc
mpar a
n a
args
      | a
n forall a. Ord a => a -> a -> Bool
> a
0 Bool -> Bool -> Bool
&& Bool -> Bool
not (forall a. Null a => a -> Bool
null a
args) = forall (m :: * -> *). Functor m => m Doc -> m Doc
parens
      | Bool
otherwise                = forall a. a -> a
id

    prettyArg :: MonadPretty m => Arg (I.Pattern' a) -> m Doc
    prettyArg :: forall (m :: * -> *) a. MonadPretty m => Arg (Pattern' a) -> m Doc
prettyArg (Arg ArgInfo
info Pattern' a
x) = case forall a. LensHiding a => a -> Hiding
getHiding ArgInfo
info of
      Hiding
Hidden     -> forall (m :: * -> *). Functor m => m Doc -> m Doc
braces forall a b. (a -> b) -> a -> b
$ forall (m :: * -> *) a.
MonadPretty m =>
Integer -> Pattern' a -> m Doc
prettyPat Integer
0 Pattern' a
x
      Instance{} -> forall (m :: * -> *). Functor m => m Doc -> m Doc
dbraces forall a b. (a -> b) -> a -> b
$ forall (m :: * -> *) a.
MonadPretty m =>
Integer -> Pattern' a -> m Doc
prettyPat Integer
0 Pattern' a
x
      Hiding
NotHidden  -> forall (m :: * -> *) a.
MonadPretty m =>
Integer -> Pattern' a -> m Doc
prettyPat Integer
1 Pattern' a
x

    prettyPat :: MonadPretty m => Integer -> (I.Pattern' a) -> m Doc
    prettyPat :: forall (m :: * -> *) a.
MonadPretty m =>
Integer -> Pattern' a -> m Doc
prettyPat Integer
_ (I.VarP PatternInfo
_ a
_) = m Doc
"_"
    prettyPat Integer
_ (I.DotP PatternInfo
_ Term
_) = m Doc
"._"
    prettyPat Integer
n (I.ConP ConHead
c ConPatternInfo
_ [NamedArg (Pattern' a)]
args) =
      forall {a} {a} {m :: * -> *}.
(Ord a, Num a, Null a, Functor m) =>
a -> a -> m Doc -> m Doc
mpar Integer
n [NamedArg (Pattern' a)]
args forall a b. (a -> b) -> a -> b
$
        forall a (m :: * -> *). (PrettyTCM a, MonadPretty m) => a -> m Doc
prettyTCM ConHead
c forall (m :: * -> *). Applicative m => m Doc -> m Doc -> m Doc
<+> forall (m :: * -> *) (t :: * -> *).
(Applicative m, Foldable t) =>
t (m Doc) -> m Doc
fsep (forall a b. (a -> b) -> [a] -> [b]
map (forall (m :: * -> *) a. MonadPretty m => Arg (Pattern' a) -> m Doc
prettyArg forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap forall name a. Named name a -> a
namedThing) [NamedArg (Pattern' a)]
args)
    prettyPat Integer
n (I.DefP PatternInfo
o QName
q [NamedArg (Pattern' a)]
args) =
      forall {a} {a} {m :: * -> *}.
(Ord a, Num a, Null a, Functor m) =>
a -> a -> m Doc -> m Doc
mpar Integer
n [NamedArg (Pattern' a)]
args forall a b. (a -> b) -> a -> b
$
        forall a (m :: * -> *). (PrettyTCM a, MonadPretty m) => a -> m Doc
prettyTCM QName
q forall (m :: * -> *). Applicative m => m Doc -> m Doc -> m Doc
<+> forall (m :: * -> *) (t :: * -> *).
(Applicative m, Foldable t) =>
t (m Doc) -> m Doc
fsep (forall a b. (a -> b) -> [a] -> [b]
map (forall (m :: * -> *) a. MonadPretty m => Arg (Pattern' a) -> m Doc
prettyArg forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap forall name a. Named name a -> a
namedThing) [NamedArg (Pattern' a)]
args)
    prettyPat Integer
_ (I.LitP PatternInfo
_ Literal
l) = forall a (m :: * -> *). (PrettyTCM a, MonadPretty m) => a -> m Doc
prettyTCM Literal
l
    prettyPat Integer
_ (I.ProjP ProjOrigin
_ QName
p) = m Doc
"." forall a. Semigroup a => a -> a -> a
<> forall a (m :: * -> *). (PrettyTCM a, MonadPretty m) => a -> m Doc
prettyTCM QName
p
    prettyPat Integer
_ (I.IApplyP PatternInfo
_ Term
_ Term
_ a
_) = m Doc
"_"

notCmp :: MonadPretty m => Comparison -> m Doc
notCmp :: forall (m :: * -> *). MonadPretty m => Comparison -> m Doc
notCmp Comparison
cmp = m Doc
"!" forall a. Semigroup a => a -> a -> a
<> forall a (m :: * -> *). (PrettyTCM a, MonadPretty m) => a -> m Doc
prettyTCM Comparison
cmp

-- | Print two terms that are supposedly unequal.
--   If they print to the same identifier, add some explanation
--   why they are different nevertheless.
prettyInEqual :: MonadPretty m => Term -> Term -> m (Doc, Doc, Doc)
prettyInEqual :: forall (m :: * -> *).
MonadPretty m =>
Term -> Term -> m (Doc, Doc, Doc)
prettyInEqual Term
t1 Term
t2 = do
  Doc
d1 <- forall a (m :: * -> *). (PrettyTCM a, MonadPretty m) => a -> m Doc
prettyTCM Term
t1
  Doc
d2 <- forall a (m :: * -> *). (PrettyTCM a, MonadPretty m) => a -> m Doc
prettyTCM Term
t2
  (Doc
d1, Doc
d2,) forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> do
     -- if printed differently, no extra explanation needed
    if Doc -> [Char]
P.render Doc
d1 forall a. Eq a => a -> a -> Bool
/= Doc -> [Char]
P.render Doc
d2 then forall a. Null a => a
empty else do
      (Term
v1, Term
v2) <- forall a (m :: * -> *). (Instantiate a, MonadReduce m) => a -> m a
instantiate (Term
t1, Term
t2)
      case (Term
v1, Term
v2) of
        (I.Var Int
i1 Elims
_, I.Var Int
i2 Elims
_)
          | Int
i1 forall a. Eq a => a -> a -> Bool
== Int
i2  -> forall (m :: * -> *). MonadPretty m => m Doc
generic -- possible, see issue 1826
          | Bool
otherwise -> forall (m :: * -> *). MonadPretty m => Int -> Int -> m Doc
varVar Int
i1 Int
i2
        (I.Def{}, I.Con{}) -> forall a. HasCallStack => a
__IMPOSSIBLE__  -- ambiguous identifiers
        (I.Con{}, I.Def{}) -> forall a. HasCallStack => a
__IMPOSSIBLE__
        (I.Var{}, I.Def{}) -> forall (m :: * -> *). MonadPretty m => m Doc
varDef
        (I.Def{}, I.Var{}) -> forall (m :: * -> *). MonadPretty m => m Doc
varDef
        (I.Var{}, I.Con{}) -> forall (m :: * -> *). MonadPretty m => m Doc
varCon
        (I.Con{}, I.Var{}) -> forall (m :: * -> *). MonadPretty m => m Doc
varCon
        (Term, Term)
_                  -> forall a. Null a => a
empty
  where
    varDef, varCon, generic :: MonadPretty m => m Doc
    varDef :: forall (m :: * -> *). MonadPretty m => m Doc
varDef = forall (m :: * -> *). Functor m => m Doc -> m Doc
parens forall a b. (a -> b) -> a -> b
$ forall (m :: * -> *). Applicative m => [Char] -> m Doc
fwords [Char]
"because one is a variable and one a defined identifier"
    varCon :: forall (m :: * -> *). MonadPretty m => m Doc
varCon = forall (m :: * -> *). Functor m => m Doc -> m Doc
parens forall a b. (a -> b) -> a -> b
$ forall (m :: * -> *). Applicative m => [Char] -> m Doc
fwords [Char]
"because one is a variable and one a constructor"
    generic :: forall (m :: * -> *). MonadPretty m => m Doc
generic = forall (m :: * -> *). Functor m => m Doc -> m Doc
parens forall a b. (a -> b) -> a -> b
$ forall (m :: * -> *). Applicative m => [Char] -> m Doc
fwords forall a b. (a -> b) -> a -> b
$ [Char]
"although these terms are looking the same, " forall a. [a] -> [a] -> [a]
++
      [Char]
"they contain different but identically rendered identifiers somewhere"
    varVar :: MonadPretty m => Int -> Int -> m Doc
    varVar :: forall (m :: * -> *). MonadPretty m => Int -> Int -> m Doc
varVar Int
i Int
j = forall (m :: * -> *). Functor m => m Doc -> m Doc
parens forall a b. (a -> b) -> a -> b
$ forall (m :: * -> *). Applicative m => [Char] -> m Doc
fwords forall a b. (a -> b) -> a -> b
$
                   [Char]
"because one has de Bruijn index " forall a. [a] -> [a] -> [a]
++ forall a. Show a => a -> [Char]
show Int
i
                   forall a. [a] -> [a] -> [a]
++ [Char]
" and the other " forall a. [a] -> [a] -> [a]
++ forall a. Show a => a -> [Char]
show Int
j

class PrettyUnequal a where
  prettyUnequal :: MonadPretty m => a -> m Doc -> a -> m Doc

instance PrettyUnequal Term where
  prettyUnequal :: forall (m :: * -> *).
MonadPretty m =>
Term -> m Doc -> Term -> m Doc
prettyUnequal Term
t1 m Doc
ncmp Term
t2 = do
    (Doc
d1, Doc
d2, Doc
d) <- forall (m :: * -> *).
MonadPretty m =>
Term -> Term -> m (Doc, Doc, Doc)
prettyInEqual Term
t1 Term
t2
    forall (m :: * -> *) (t :: * -> *).
(Applicative m, Foldable t) =>
t (m Doc) -> m Doc
fsep forall a b. (a -> b) -> a -> b
$ forall (m :: * -> *) a. Monad m => a -> m a
return Doc
d1 forall a. a -> [a] -> [a]
: m Doc
ncmp forall a. a -> [a] -> [a]
: forall (m :: * -> *) a. Monad m => a -> m a
return Doc
d2 forall a. a -> [a] -> [a]
: forall (m :: * -> *) a. Monad m => a -> m a
return Doc
d forall a. a -> [a] -> [a]
: []

instance PrettyUnequal I.Type where
  prettyUnequal :: forall (m :: * -> *).
MonadPretty m =>
Type -> m Doc -> Type -> m Doc
prettyUnequal Type
t1 m Doc
ncmp Type
t2 = forall a (m :: * -> *).
(PrettyUnequal a, MonadPretty m) =>
a -> m Doc -> a -> m Doc
prettyUnequal (forall t a. Type'' t a -> a
unEl Type
t1) m Doc
ncmp (forall t a. Type'' t a -> a
unEl Type
t2)

instance PrettyTCM SplitError where
  prettyTCM :: forall m. MonadPretty m => SplitError -> m Doc
  prettyTCM :: forall (m :: * -> *). MonadPretty m => SplitError -> m Doc
prettyTCM SplitError
err = case SplitError
err of
    NotADatatype Closure Type
t -> forall (m :: * -> *) a c b.
(MonadTCEnv m, ReadTCState m, LensClosure a c) =>
c -> (a -> m b) -> m b
enterClosure Closure Type
t forall a b. (a -> b) -> a -> b
$ \ 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]
"Cannot split on argument of non-datatype" forall a. [a] -> [a] -> [a]
++ [forall a (m :: * -> *). (PrettyTCM a, MonadPretty m) => a -> m Doc
prettyTCM Type
t]

    BlockedType Blocker
b Closure Type
t -> forall (m :: * -> *) a c b.
(MonadTCEnv m, ReadTCState m, LensClosure a c) =>
c -> (a -> m b) -> m b
enterClosure Closure Type
t forall a b. (a -> b) -> a -> b
$ \ 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]
"Cannot split on argument of unresolved type" forall a. [a] -> [a] -> [a]
++ [forall a (m :: * -> *). (PrettyTCM a, MonadPretty m) => a -> m Doc
prettyTCM Type
t]

    ErasedDatatype Bool
causedByWithoutK Closure Type
t -> forall (m :: * -> *) a c b.
(MonadTCEnv m, ReadTCState m, LensClosure a c) =>
c -> (a -> m b) -> m b
enterClosure Closure Type
t forall a b. (a -> b) -> a -> b
$ \ 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]
"Cannot branch on erased argument of datatype" forall a. [a] -> [a] -> [a]
++
      [forall a (m :: * -> *). (PrettyTCM a, MonadPretty m) => a -> m Doc
prettyTCM Type
t] forall a. [a] -> [a] -> [a]
++
      if Bool
causedByWithoutK
      then forall (m :: * -> *). Applicative m => [Char] -> [m Doc]
pwords [Char]
"because the K rule is turned off"
      else []

    CoinductiveDatatype Closure Type
t -> forall (m :: * -> *) a c b.
(MonadTCEnv m, ReadTCState m, LensClosure a c) =>
c -> (a -> m b) -> m b
enterClosure Closure Type
t forall a b. (a -> b) -> a -> b
$ \ 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]
"Cannot pattern match on the coinductive type" forall a. [a] -> [a] -> [a]
++ [forall a (m :: * -> *). (PrettyTCM a, MonadPretty m) => a -> m Doc
prettyTCM Type
t]

{- UNUSED
    NoRecordConstructor t -> fsep $
      pwords "Cannot pattern match on record" ++ [prettyTCM t] ++
      pwords "because it has no constructor"
 -}

    UnificationStuck Maybe Blocker
b QName
c Telescope
tel Args
cIxs Args
gIxs [UnificationFailure]
errs
      | forall (t :: * -> *) a. Foldable t => t a -> Int
length Args
cIxs forall a. Eq a => a -> a -> Bool
/= forall (t :: * -> *) a. Foldable t => t a -> Int
length Args
gIxs -> forall a. HasCallStack => a
__IMPOSSIBLE__
      | Bool
otherwise                  -> forall (m :: * -> *) (t :: * -> *).
(Applicative m, Foldable t) =>
t (m Doc) -> m Doc
vcat forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall (t :: * -> *) a. Foldable t => t [a] -> [a]
concat forall a b. (a -> b) -> a -> b
$
        [ [ forall (m :: * -> *) (t :: * -> *).
(Applicative m, Foldable t) =>
t (m Doc) -> m Doc
fsep forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall (t :: * -> *) a. Foldable t => t [a] -> [a]
concat forall a b. (a -> b) -> a -> b
$
            [ forall (m :: * -> *). Applicative m => [Char] -> [m Doc]
pwords [Char]
"I'm not sure if there should be a case for the constructor"
            , [forall a (m :: * -> *). (PrettyTCM a, MonadPretty m) => a -> m Doc
prettyTCM QName
c forall a. Semigroup a => a -> a -> a
<> m Doc
","]
            , forall (m :: * -> *). Applicative m => [Char] -> [m Doc]
pwords [Char]
"because I get stuck when trying to solve the following"
            , forall (m :: * -> *). Applicative m => [Char] -> [m Doc]
pwords [Char]
"unification problems (inferred index ≟ expected index):"
            ]
          ]
        , forall a b c. (a -> b -> c) -> [a] -> [b] -> [c]
zipWith Arg Term -> Arg Term -> m Doc
prEq Args
cIxs Args
gIxs
        , if forall a. Null a => a -> Bool
null [UnificationFailure]
errs then [] else
            forall (m :: * -> *) (t :: * -> *).
(Applicative m, Foldable t) =>
t (m Doc) -> m Doc
fsep ( forall (m :: * -> *). Applicative m => [Char] -> [m Doc]
pwords [Char]
"Possible" forall a. [a] -> [a] -> [a]
++ forall (m :: * -> *). Applicative m => [Char] -> [m Doc]
pwords (forall a c. Sized a => a -> c -> c -> c
P.singPlural [UnificationFailure]
errs [Char]
"reason" [Char]
"reasons") forall a. [a] -> [a] -> [a]
++
                     forall (m :: * -> *). Applicative m => [Char] -> [m Doc]
pwords [Char]
"why unification failed:" ) forall a. a -> [a] -> [a]
:
            forall a b. (a -> b) -> [a] -> [b]
map (forall (m :: * -> *). Functor m => Int -> m Doc -> m Doc
nest Int
2 forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall a (m :: * -> *). (PrettyTCM a, MonadPretty m) => a -> m Doc
prettyTCM) [UnificationFailure]
errs
        ]
      where
        -- Andreas, 2019-08-08, issue #3943
        -- To not print hidden indices just as {_}, we strip the Arg and print
        -- the hiding information manually.
        prEq :: Arg Term -> Arg Term -> m Doc
        prEq :: Arg Term -> Arg Term -> m Doc
prEq Arg Term
cIx Arg Term
gIx = 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 :: * -> *). Functor m => Int -> m Doc -> m Doc
nest Int
2 forall a b. (a -> b) -> a -> b
$ forall (m :: * -> *) (t :: * -> *).
(Applicative m, Foldable t) =>
t (m Doc) -> m Doc
hsep [ forall {f :: * -> *} {a}.
(PrettyTCM a, MonadFresh NameId f, MonadInteractionPoints f,
 MonadStConcreteNames f, PureTCM f, IsString (f Doc), Null (f Doc),
 Semigroup (f Doc)) =>
Arg a -> f Doc
pr Arg Term
cIx , m Doc
"≟" , forall {f :: * -> *} {a}.
(PrettyTCM a, MonadFresh NameId f, MonadInteractionPoints f,
 MonadStConcreteNames f, PureTCM f, IsString (f Doc), Null (f Doc),
 Semigroup (f Doc)) =>
Arg a -> f Doc
pr Arg Term
gIx ]
        pr :: Arg a -> f Doc
pr Arg a
arg = forall a. LensRelevance a => a -> Doc -> Doc
prettyRelevance Arg a
arg forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall a. LensHiding a => a -> (Doc -> Doc) -> Doc -> Doc
prettyHiding Arg a
arg forall a. a -> a
id forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> forall a (m :: * -> *). (PrettyTCM a, MonadPretty m) => a -> m Doc
prettyTCM (forall e. Arg e -> e
unArg Arg a
arg)

    SplitError
CosplitCatchall -> 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]
"Cannot split into projections because not all clauses have a projection copattern"

    SplitError
CosplitNoTarget -> 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]
"Cannot split into projections because target type is unknown"

    CosplitNoRecordType Closure Type
t -> forall (m :: * -> *) a c b.
(MonadTCEnv m, ReadTCState m, LensClosure a c) =>
c -> (a -> m b) -> m b
enterClosure Closure Type
t forall a b. (a -> b) -> a -> b
$ \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]
"Cannot split into projections because the target 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]
" is not a record type"

    CannotCreateMissingClause QName
f (Telescope, [NamedArg DeBruijnPattern])
cl Doc
msg Closure (Abs Type)
t -> forall (m :: * -> *) (t :: * -> *).
(Applicative m, Foldable t) =>
t (m Doc) -> m Doc
fsep (
      forall (m :: * -> *). Applicative m => [Char] -> [m Doc]
pwords [Char]
"Cannot generate inferred clause for" forall a. [a] -> [a] -> [a]
++ [forall a (m :: * -> *). (PrettyTCM a, MonadPretty m) => a -> m Doc
prettyTCM QName
f forall a. Semigroup a => a -> a -> a
<> m Doc
"."] forall a. [a] -> [a] -> [a]
++
      forall (m :: * -> *). Applicative m => [Char] -> [m Doc]
pwords [Char]
"Case to handle:") 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
$ [(Telescope, [NamedArg DeBruijnPattern]) -> m Doc
display (Telescope, [NamedArg DeBruijnPattern])
cl])
                                forall (m :: * -> *). Applicative m => m Doc -> m Doc -> m Doc
$$ ((forall (f :: * -> *) a. Applicative f => a -> f a
pure Doc
msg forall (m :: * -> *). Applicative m => m Doc -> m Doc -> m Doc
<+> forall (m :: * -> *) a c b.
(MonadTCEnv m, ReadTCState m, LensClosure a c) =>
c -> (a -> m b) -> m b
enterClosure Closure (Abs Type)
t Abs Type -> m Doc
displayAbs) forall a. Semigroup a => a -> a -> a
<> m Doc
".")
        where
        displayAbs :: Abs I.Type -> m Doc
        displayAbs :: Abs Type -> m Doc
displayAbs (Abs [Char]
x Type
t) = forall b (m :: * -> *) a.
(AddContext b, MonadAddContext m) =>
b -> m a -> m a
addContext [Char]
x forall a b. (a -> b) -> a -> b
$ forall a (m :: * -> *). (PrettyTCM a, MonadPretty m) => a -> m Doc
prettyTCM Type
t
        displayAbs (NoAbs [Char]
x Type
t) = forall a (m :: * -> *). (PrettyTCM a, MonadPretty m) => a -> m Doc
prettyTCM Type
t
        display :: (Telescope, [NamedArg DeBruijnPattern]) -> m Doc
display (Telescope
tel, [NamedArg DeBruijnPattern]
ps) = forall a (m :: * -> *). (PrettyTCM a, MonadPretty m) => a -> m Doc
prettyTCM forall a b. (a -> b) -> a -> b
$ QName -> Bool -> Clause -> NamedClause
NamedClause QName
f Bool
True forall a b. (a -> b) -> a -> b
$
          forall a. Null a => a
empty { clauseTel :: Telescope
clauseTel = Telescope
tel, namedClausePats :: [NamedArg DeBruijnPattern]
namedClausePats = [NamedArg DeBruijnPattern]
ps }


    GenericSplitError [Char]
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]
"Split failed:" forall a. [a] -> [a] -> [a]
++ forall (m :: * -> *). Applicative m => [Char] -> [m Doc]
pwords [Char]
s

instance PrettyTCM NegativeUnification where
  prettyTCM :: forall (m :: * -> *). MonadPretty m => NegativeUnification -> m Doc
prettyTCM NegativeUnification
err = case NegativeUnification
err of
    UnifyConflict Telescope
tel Term
u Term
v -> 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
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]
"because unification ended with a conflicting equation "
      , 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 Term
u forall (m :: * -> *). Applicative m => m Doc -> m Doc -> m Doc
<+> m Doc
"≟" forall (m :: * -> *). Applicative m => m Doc -> m Doc -> m Doc
<+> forall a (m :: * -> *). (PrettyTCM a, MonadPretty m) => a -> m Doc
prettyTCM Term
v
      ]

    UnifyCycle Telescope
tel Int
i Term
u -> 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
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]
"because unification ended with a cyclic equation "
      , 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 (Int -> Term
var Int
i) forall (m :: * -> *). Applicative m => m Doc -> m Doc -> m Doc
<+> m Doc
"≟" forall (m :: * -> *). Applicative m => m Doc -> m Doc -> m Doc
<+> forall a (m :: * -> *). (PrettyTCM a, MonadPretty m) => a -> m Doc
prettyTCM Term
u
      ]

instance PrettyTCM UnificationFailure where
  prettyTCM :: forall (m :: * -> *). MonadPretty m => UnificationFailure -> m Doc
prettyTCM UnificationFailure
err = case UnificationFailure
err of
    UnifyIndicesNotVars Telescope
tel Type
a Term
u Term
v Args
ixs -> 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]
"Cannot apply injectivity to the equation" forall a. [a] -> [a] -> [a]
++ [forall a (m :: * -> *). (PrettyTCM a, MonadPretty m) => a -> m Doc
prettyTCM Term
u] forall a. [a] -> [a] -> [a]
++
      forall (m :: * -> *). Applicative m => [Char] -> [m Doc]
pwords [Char]
"=" 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 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]
"because I cannot generalize over the indices" forall a. [a] -> [a] -> [a]
++
      [forall (m :: * -> *) (t :: * -> *).
(Applicative m, Semigroup (m Doc), Foldable t) =>
t (m Doc) -> m Doc
prettyList (forall a b. (a -> b) -> [a] -> [b]
map forall a (m :: * -> *). (PrettyTCM a, MonadPretty m) => a -> m Doc
prettyTCM Args
ixs) forall a. Semigroup a => a -> a -> a
<> m Doc
"."]

    UnifyRecursiveEq Telescope
tel Type
a Int
i Term
u -> 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]
"Cannot solve variable " forall a. [a] -> [a] -> [a]
++ [forall a (m :: * -> *). (PrettyTCM a, MonadPretty m) => a -> m Doc
prettyTCM (Int -> Term
var Int
i)] forall a. [a] -> [a] -> [a]
++
      forall (m :: * -> *). Applicative m => [Char] -> [m Doc]
pwords [Char]
" of 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]
" with solution " forall a. [a] -> [a] -> [a]
++ [forall a (m :: * -> *). (PrettyTCM a, MonadPretty m) => a -> m Doc
prettyTCM Term
u] forall a. [a] -> [a] -> [a]
++
      forall (m :: * -> *). Applicative m => [Char] -> [m Doc]
pwords [Char]
" because the variable occurs in the solution," forall a. [a] -> [a] -> [a]
++
      forall (m :: * -> *). Applicative m => [Char] -> [m Doc]
pwords [Char]
" or in the type of one of the variables in the solution."

    UnifyReflexiveEq Telescope
tel Type
a Term
u -> 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]
"Cannot eliminate reflexive equation" forall a. [a] -> [a] -> [a]
++ [forall a (m :: * -> *). (PrettyTCM a, MonadPretty m) => a -> m Doc
prettyTCM Term
u] forall a. [a] -> [a] -> [a]
++
      forall (m :: * -> *). Applicative m => [Char] -> [m Doc]
pwords [Char]
"=" forall a. [a] -> [a] -> [a]
++ [forall a (m :: * -> *). (PrettyTCM a, MonadPretty m) => a -> m Doc
prettyTCM Term
u] forall a. [a] -> [a] -> [a]
++ forall (m :: * -> *). Applicative m => [Char] -> [m Doc]
pwords [Char]
"of 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]
"because K has been disabled."

    UnifyUnusableModality Telescope
tel Type
a Int
i Term
u Modality
mod -> 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]
"Cannot solve variable " forall a. [a] -> [a] -> [a]
++ [forall a (m :: * -> *). (PrettyTCM a, MonadPretty m) => a -> m Doc
prettyTCM (Int -> Term
var Int
i)] forall a. [a] -> [a] -> [a]
++
      forall (m :: * -> *). Applicative m => [Char] -> [m Doc]
pwords [Char]
"of 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]
"with solution " forall a. [a] -> [a] -> [a]
++ [forall a (m :: * -> *). (PrettyTCM a, MonadPretty m) => a -> m Doc
prettyTCM Term
u] forall a. [a] -> [a] -> [a]
++
      forall (m :: * -> *). Applicative m => [Char] -> [m Doc]
pwords [Char]
"because the solution cannot be used at" forall a. [a] -> [a] -> [a]
++
             [ forall (m :: * -> *). Applicative m => [Char] -> m Doc
text (forall a. Verbalize a => a -> [Char]
verbalize forall a b. (a -> b) -> a -> b
$ forall a. LensRelevance a => a -> Relevance
getRelevance Modality
mod) forall a. Semigroup a => a -> a -> a
<> m Doc
","
             , forall (m :: * -> *). Applicative m => [Char] -> m Doc
text forall a b. (a -> b) -> a -> b
$ forall a. Verbalize a => a -> [Char]
verbalize forall a b. (a -> b) -> a -> b
$ forall a. LensQuantity a => a -> Quantity
getQuantity Modality
mod ] forall a. [a] -> [a] -> [a]
++
      forall (m :: * -> *). Applicative m => [Char] -> [m Doc]
pwords [Char]
"modality"



explainWhyInScope :: forall m. MonadPretty m => WhyInScopeData -> m Doc
explainWhyInScope :: forall (m :: * -> *). MonadPretty m => WhyInScopeData -> m Doc
explainWhyInScope (WhyInScopeData QName
y [Char]
_ Maybe LocalVar
Nothing [] []) = forall (m :: * -> *). Applicative m => [Char] -> m Doc
text (forall a. Pretty a => a -> [Char]
prettyShow  QName
y forall a. [a] -> [a] -> [a]
++ [Char]
" is not in scope.")
explainWhyInScope (WhyInScopeData QName
y [Char]
_ Maybe LocalVar
v [AbstractName]
xs [AbstractModule]
ms) = forall (m :: * -> *) (t :: * -> *).
(Applicative m, Foldable t) =>
t (m Doc) -> m Doc
vcat
  [ forall (m :: * -> *). Applicative m => [Char] -> m Doc
text (forall a. Pretty a => a -> [Char]
prettyShow QName
y forall a. [a] -> [a] -> [a]
++ [Char]
" is in scope as")
  , forall (m :: * -> *). Functor m => Int -> m Doc -> m Doc
nest Int
2 forall a b. (a -> b) -> a -> b
$ forall (m :: * -> *) (t :: * -> *).
(Applicative m, Foldable t) =>
t (m Doc) -> m Doc
vcat [Maybe LocalVar -> [AbstractName] -> m Doc
variable Maybe LocalVar
v [AbstractName]
xs, [AbstractModule] -> m Doc
modules [AbstractModule]
ms]
  ]
  where
    -- variable :: Maybe _ -> [_] -> m Doc
    variable :: Maybe LocalVar -> [AbstractName] -> m Doc
variable Maybe LocalVar
Nothing [AbstractName]
vs = [AbstractName] -> m Doc
names [AbstractName]
vs
    variable (Just LocalVar
x) [AbstractName]
vs
      | forall a. Null a => a -> Bool
null [AbstractName]
vs   = m Doc
asVar
      | Bool
otherwise = 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
sep [ m Doc
asVar, forall (m :: * -> *). Functor m => Int -> m Doc -> m Doc
nest Int
2 forall a b. (a -> b) -> a -> b
$ LocalVar -> m Doc
shadowing LocalVar
x]
         , forall (m :: * -> *). Functor m => Int -> m Doc -> m Doc
nest Int
2 forall a b. (a -> b) -> a -> b
$ [AbstractName] -> m Doc
names [AbstractName]
vs
         ]
      where
        asVar :: m Doc
        asVar :: m Doc
asVar = do
          m Doc
"* a variable bound at" forall (m :: * -> *). Applicative m => m Doc -> m Doc -> m Doc
<+> forall a (m :: * -> *). (PrettyTCM a, MonadPretty m) => a -> m Doc
prettyTCM (Name -> Range
nameBindingSite forall a b. (a -> b) -> a -> b
$ LocalVar -> Name
localVar LocalVar
x)
        shadowing :: LocalVar -> m Doc
        shadowing :: LocalVar -> m Doc
shadowing (LocalVar Name
_ BindingSource
_ [])    = m Doc
"shadowing"
        shadowing LocalVar
_ = m Doc
"in conflict with"
    names :: [AbstractName] -> m Doc
names   = forall (m :: * -> *) (t :: * -> *).
(Applicative m, Foldable t) =>
t (m Doc) -> m Doc
vcat forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall a b. (a -> b) -> [a] -> [b]
map AbstractName -> m Doc
pName
    modules :: [AbstractModule] -> m Doc
modules = forall (m :: * -> *) (t :: * -> *).
(Applicative m, Foldable t) =>
t (m Doc) -> m Doc
vcat forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall a b. (a -> b) -> [a] -> [b]
map AbstractModule -> m Doc
pMod

    pKind :: KindOfName -> m Doc
pKind = \case
      KindOfName
ConName                  -> m Doc
"constructor"
      KindOfName
CoConName                -> m Doc
"coinductive constructor"
      KindOfName
FldName                  -> m Doc
"record field"
      KindOfName
PatternSynName           -> m Doc
"pattern synonym"
      KindOfName
GeneralizeName           -> m Doc
"generalizable variable"
      KindOfName
DisallowedGeneralizeName -> m Doc
"generalizable variable from let open"
      KindOfName
MacroName                -> m Doc
"macro name"
      KindOfName
QuotableName             -> m Doc
"quotable name"
      -- previously DefName:
      KindOfName
DataName                 -> m Doc
"data type"
      KindOfName
RecName                  -> m Doc
"record type"
      KindOfName
AxiomName                -> m Doc
"postulate"
      KindOfName
PrimName                 -> m Doc
"primitive function"
      KindOfName
FunName                  -> m Doc
"defined name"
      KindOfName
OtherDefName             -> m Doc
"defined name"

    pName :: AbstractName -> m Doc
    pName :: AbstractName -> m Doc
pName AbstractName
a = forall (m :: * -> *) (t :: * -> *).
(Applicative m, Foldable t) =>
t (m Doc) -> m Doc
sep
      [ m Doc
"* a"
        forall (m :: * -> *). Applicative m => m Doc -> m Doc -> m Doc
<+> KindOfName -> m Doc
pKind (AbstractName -> KindOfName
anameKind AbstractName
a)
        forall (m :: * -> *). Applicative m => m Doc -> m Doc -> m Doc
<+> forall (m :: * -> *). Applicative m => [Char] -> m Doc
text (forall a. Pretty a => a -> [Char]
prettyShow forall a b. (a -> b) -> a -> b
$ AbstractName -> QName
anameName AbstractName
a)
      , forall (m :: * -> *). Functor m => Int -> m Doc -> m Doc
nest Int
2 forall a b. (a -> b) -> a -> b
$ m Doc
"brought into scope by"
      ] forall (m :: * -> *). Applicative m => m Doc -> m Doc -> m Doc
$$
      forall (m :: * -> *). Functor m => Int -> m Doc -> m Doc
nest Int
2 (Range -> WhyInScope -> m Doc
pWhy (Name -> Range
nameBindingSite forall a b. (a -> b) -> a -> b
$ QName -> Name
qnameName forall a b. (a -> b) -> a -> b
$ AbstractName -> QName
anameName AbstractName
a) (AbstractName -> WhyInScope
anameLineage AbstractName
a))
    pMod :: AbstractModule -> m Doc
    pMod :: AbstractModule -> m Doc
pMod  AbstractModule
a = forall (m :: * -> *) (t :: * -> *).
(Applicative m, Foldable t) =>
t (m Doc) -> m Doc
sep
      [ m Doc
"* a module" forall (m :: * -> *). Applicative m => m Doc -> m Doc -> m Doc
<+> forall (m :: * -> *). Applicative m => [Char] -> m Doc
text (forall a. Pretty a => a -> [Char]
prettyShow forall a b. (a -> b) -> a -> b
$ AbstractModule -> ModuleName
amodName AbstractModule
a)
      , forall (m :: * -> *). Functor m => Int -> m Doc -> m Doc
nest Int
2 forall a b. (a -> b) -> a -> b
$ m Doc
"brought into scope by"
      ] forall (m :: * -> *). Applicative m => m Doc -> m Doc -> m Doc
$$
      forall (m :: * -> *). Functor m => Int -> m Doc -> m Doc
nest Int
2 (Range -> WhyInScope -> m Doc
pWhy (Name -> Range
nameBindingSite forall a b. (a -> b) -> a -> b
$ QName -> Name
qnameName forall a b. (a -> b) -> a -> b
$ ModuleName -> QName
mnameToQName forall a b. (a -> b) -> a -> b
$ AbstractModule -> ModuleName
amodName AbstractModule
a) (AbstractModule -> WhyInScope
amodLineage AbstractModule
a))

    pWhy :: Range -> WhyInScope -> m Doc
    pWhy :: Range -> WhyInScope -> m Doc
pWhy Range
r WhyInScope
Defined = m Doc
"- its definition at" forall (m :: * -> *). Applicative m => m Doc -> m Doc -> m Doc
<+> forall a (m :: * -> *). (PrettyTCM a, MonadPretty m) => a -> m Doc
prettyTCM Range
r
    pWhy Range
r (Opened (C.QName Name
x) WhyInScope
w) | forall a. IsNoName a => a -> Bool
isNoName Name
x = Range -> WhyInScope -> m Doc
pWhy Range
r WhyInScope
w
    pWhy Range
r (Opened QName
m WhyInScope
w) =
      m Doc
"- the opening of"
      forall (m :: * -> *). Applicative m => m Doc -> m Doc -> m Doc
<+> forall a (m :: * -> *). (PrettyTCM a, MonadPretty m) => a -> m Doc
prettyTCM QName
m
      forall (m :: * -> *). Applicative m => m Doc -> m Doc -> m Doc
<+> m Doc
"at"
      forall (m :: * -> *). Applicative m => m Doc -> m Doc -> m Doc
<+> forall a (m :: * -> *). (PrettyTCM a, MonadPretty m) => a -> m Doc
prettyTCM (forall a. HasRange a => a -> Range
getRange QName
m)
      forall (m :: * -> *). Applicative m => m Doc -> m Doc -> m Doc
$$
      Range -> WhyInScope -> m Doc
pWhy Range
r WhyInScope
w
    pWhy Range
r (Applied QName
m WhyInScope
w) =
      m Doc
"- the application of"
      forall (m :: * -> *). Applicative m => m Doc -> m Doc -> m Doc
<+> forall a (m :: * -> *). (PrettyTCM a, MonadPretty m) => a -> m Doc
prettyTCM QName
m
      forall (m :: * -> *). Applicative m => m Doc -> m Doc -> m Doc
<+> m Doc
"at"
      forall (m :: * -> *). Applicative m => m Doc -> m Doc -> m Doc
<+> forall a (m :: * -> *). (PrettyTCM a, MonadPretty m) => a -> m Doc
prettyTCM (forall a. HasRange a => a -> Range
getRange QName
m)
      forall (m :: * -> *). Applicative m => m Doc -> m Doc -> m Doc
$$
      Range -> WhyInScope -> m Doc
pWhy Range
r WhyInScope
w



---------------------------------------------------------------------------
-- * Natural language
---------------------------------------------------------------------------

class Verbalize a where
  verbalize :: a -> String

instance Verbalize Hiding where
  verbalize :: Hiding -> [Char]
verbalize Hiding
h =
    case Hiding
h of
      Hiding
Hidden     -> [Char]
"hidden"
      Hiding
NotHidden  -> [Char]
"visible"
      Instance{} -> [Char]
"instance"

instance Verbalize Relevance where
  verbalize :: Relevance -> [Char]
verbalize Relevance
r =
    case Relevance
r of
      Relevance
Relevant   -> [Char]
"relevant"
      Relevance
Irrelevant -> [Char]
"irrelevant"
      Relevance
NonStrict  -> [Char]
"shape-irrelevant"

instance Verbalize Quantity where
  verbalize :: Quantity -> [Char]
verbalize = \case
    Quantity0{} -> [Char]
"erased"
    Quantity1{} -> [Char]
"linear"
    Quantityω{} -> [Char]
"unrestricted"

instance Verbalize Cohesion where
  verbalize :: Cohesion -> [Char]
verbalize Cohesion
r =
    case Cohesion
r of
      Cohesion
Flat       -> [Char]
"flat"
      Cohesion
Continuous -> [Char]
"continuous"
      Cohesion
Squash     -> [Char]
"squashed"

instance Verbalize Modality where
  verbalize :: Modality -> [Char]
verbalize Modality
mod | Modality
mod forall a. Eq a => a -> a -> Bool
== Modality
defaultModality = [Char]
"default"
  verbalize (Modality Relevance
rel Quantity
qnt Cohesion
coh) = forall a. [a] -> [[a]] -> [a]
intercalate [Char]
"," forall a b. (a -> b) -> a -> b
$
    [ forall a. Verbalize a => a -> [Char]
verbalize Relevance
rel | Relevance
rel forall a. Eq a => a -> a -> Bool
/= Relevance
defaultRelevance ] forall a. [a] -> [a] -> [a]
++
    [ forall a. Verbalize a => a -> [Char]
verbalize Quantity
qnt | Quantity
qnt forall a. Eq a => a -> a -> Bool
/= Quantity
defaultQuantity ] forall a. [a] -> [a] -> [a]
++
    [ forall a. Verbalize a => a -> [Char]
verbalize Cohesion
coh | Cohesion
coh forall a. Eq a => a -> a -> Bool
/= Cohesion
defaultCohesion ]

-- | Indefinite article.
data Indefinite a = Indefinite a

instance Verbalize a => Verbalize (Indefinite a) where
  verbalize :: Indefinite a -> [Char]
verbalize (Indefinite a
a) =
    case forall a. Verbalize a => a -> [Char]
verbalize a
a of
      [Char]
"" -> [Char]
""
      w :: [Char]
w@(Char
c:[Char]
cs) | Char
c forall (t :: * -> *) a. (Foldable t, Eq a) => a -> t a -> Bool
`elem` [Char
'a',Char
'e',Char
'i',Char
'o'] -> [Char]
"an " forall a. [a] -> [a] -> [a]
++ [Char]
w
               | Bool
otherwise                  -> [Char]
"a " forall a. [a] -> [a] -> [a]
++ [Char]
w
      -- Aarne Ranta would whip me if he saw this.