{-# LANGUAGE NondecreasingIndentation #-}

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

module Agda.TypeChecking.Errors
  ( prettyError
  , prettyWarning
  , tcErrString
  , prettyTCWarnings'
  , prettyTCWarnings
  , tcWarningsToError
  , applyFlagsToTCWarnings'
  , applyFlagsToTCWarnings
  , dropTopLevelModule
  , topLevelModuleDropper
  , stringTCErr
  ) where

import Prelude hiding ( null )

import Data.Function
import Data.List (sortBy, isInfixOf, dropWhileEnd)
import Data.List.NonEmpty (NonEmpty(..))
import qualified Data.List.NonEmpty as NonEmpty
import Data.Maybe
import Data.Char (toLower)
import qualified Data.Set as Set
import qualified Text.PrettyPrint.Boxes as Boxes

import Agda.Syntax.Common
import Agda.Syntax.Concrete.Pretty (prettyHiding, prettyRelevance)
import Agda.Syntax.Fixity
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.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.Except ( MonadError(catchError) )
import Agda.Utils.FileName
import Agda.Utils.Float  ( toStringWithoutDotZero )
import Agda.Utils.Function
import Agda.Utils.Maybe
import Agda.Utils.Null
import Agda.Utils.Pretty ( prettyShow )
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 :: TCErr -> tcm String
prettyError err :: TCErr
err = TCM String -> tcm String
forall (tcm :: * -> *) a. MonadTCM tcm => TCM a -> tcm a
liftTCM (TCM String -> tcm String) -> TCM String -> tcm String
forall a b. (a -> b) -> a -> b
$ Doc -> String
forall a. Show a => a -> String
show (Doc -> String) -> TCMT IO Doc -> TCM String
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' err :: TCErr
err errs :: [TCErr]
errs
    | [TCErr] -> Int
forall (t :: * -> *) a. Foldable t => t a -> Int
length [TCErr]
errs Int -> Int -> Bool
forall a. Ord a => a -> a -> Bool
> 3 = [TCMT IO Doc] -> TCMT IO Doc
forall (m :: * -> *). Monad m => [m Doc] -> m Doc
fsep (
        String -> [TCMT IO Doc]
forall (m :: * -> *). Monad m => String -> [m Doc]
pwords "total panic: error when printing error from printing error from printing error." [TCMT IO Doc] -> [TCMT IO Doc] -> [TCMT IO Doc]
forall a. [a] -> [a] -> [a]
++
        String -> [TCMT IO Doc]
forall (m :: * -> *). Monad m => String -> [m Doc]
pwords "I give up! Approximations of errors (original error last):" )
        TCMT IO Doc -> TCMT IO Doc -> TCMT IO Doc
forall (m :: * -> *). Applicative m => m Doc -> m Doc -> m Doc
$$ [TCMT IO Doc] -> TCMT IO Doc
forall (m :: * -> *). Monad m => [m Doc] -> m Doc
vcat ((TCErr -> TCMT IO Doc) -> [TCErr] -> [TCMT IO Doc]
forall a b. (a -> b) -> [a] -> [b]
map (String -> TCMT IO Doc
forall (m :: * -> *). Monad m => String -> m Doc
text (String -> TCMT IO Doc)
-> (TCErr -> String) -> TCErr -> TCMT IO Doc
forall b c a. (b -> c) -> (a -> b) -> a -> c
. TCErr -> String
tcErrString) [TCErr]
errs)
    | Bool
otherwise = Bool -> (TCMT IO Doc -> TCMT IO Doc) -> TCMT IO Doc -> TCMT IO Doc
forall a. Bool -> (a -> a) -> a -> a
applyUnless ([TCErr] -> Bool
forall a. Null a => a -> Bool
null [TCErr]
errs) ("panic: error when printing error!" TCMT IO Doc -> TCMT IO Doc -> TCMT IO Doc
forall (m :: * -> *). Applicative m => m Doc -> m Doc -> m Doc
$$) (TCMT IO Doc -> TCMT IO Doc) -> TCMT IO Doc -> TCMT IO Doc
forall a b. (a -> b) -> a -> b
$ do
        (TCErr -> TCMT IO Doc
forall a (m :: * -> *). (PrettyTCM a, MonadPretty m) => a -> m Doc
prettyTCM TCErr
err TCMT IO Doc -> TCMT IO Doc -> TCMT IO Doc
forall (m :: * -> *). Applicative m => m Doc -> m Doc -> m Doc
$$ [TCMT IO Doc] -> TCMT IO Doc
forall (m :: * -> *). Monad m => [m Doc] -> m Doc
vcat ((TCErr -> TCMT IO Doc) -> [TCErr] -> [TCMT IO Doc]
forall a b. (a -> b) -> [a] -> [b]
map (String -> TCMT IO Doc
forall (m :: * -> *). Monad m => String -> m Doc
text (String -> TCMT IO Doc)
-> (TCErr -> String) -> TCErr -> TCMT IO Doc
forall b c a. (b -> c) -> (a -> b) -> a -> c
. ("when printing error " String -> String -> String
forall a. [a] -> [a] -> [a]
++) (String -> String) -> (TCErr -> String) -> TCErr -> String
forall b c a. (b -> c) -> (a -> b) -> a -> c
. TCErr -> String
tcErrString) [TCErr]
errs))
        TCMT IO Doc -> (TCErr -> TCMT IO Doc) -> TCMT IO Doc
forall e (m :: * -> *) a.
MonadError e m =>
m a -> (e -> m a) -> m a
`catchError` \ err' :: TCErr
err' -> TCErr -> [TCErr] -> TCMT IO Doc
prettyError' TCErr
err' (TCErr
errTCErr -> [TCErr] -> [TCErr]
forall a. a -> [a] -> [a]
:[TCErr]
errs)

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

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

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

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

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

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

instance PrettyTCM TCErr where
  prettyTCM :: TCErr -> m Doc
prettyTCM err :: 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 _ Closure{ clValue :: forall a. Closure a -> a
clValue = NonFatalErrors ws :: [TCWarning]
ws } -> (m Doc -> m Doc -> m Doc) -> [m Doc] -> m Doc
forall (t :: * -> *) a. Foldable t => (a -> a -> a) -> t a -> a
foldr1 m Doc -> m Doc -> m Doc
forall (m :: * -> *). Applicative m => m Doc -> m Doc -> m Doc
($$) ([m Doc] -> m Doc) -> [m Doc] -> m Doc
forall a b. (a -> b) -> a -> b
$ (TCWarning -> m Doc) -> [TCWarning] -> [m Doc]
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap TCWarning -> m Doc
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 s :: TCState
s e :: Closure TypeError
e -> (TCState -> TCState) -> m Doc -> m Doc
forall (m :: * -> *) a.
ReadTCState m =>
(TCState -> TCState) -> m a -> m a
withTCState (TCState -> TCState -> TCState
forall a b. a -> b -> a
const TCState
s) (m Doc -> m Doc) -> m Doc -> m Doc
forall a b. (a -> b) -> a -> b
$
      Range -> Maybe (Closure Call) -> m Doc -> m Doc
forall (m :: * -> *).
MonadPretty m =>
Range -> Maybe (Closure Call) -> m Doc -> m Doc
sayWhen (TCEnv -> Range
envRange (TCEnv -> Range) -> TCEnv -> Range
forall a b. (a -> b) -> a -> b
$ Closure TypeError -> TCEnv
forall a. Closure a -> TCEnv
clEnv Closure TypeError
e) (TCEnv -> Maybe (Closure Call)
envCall (TCEnv -> Maybe (Closure Call)) -> TCEnv -> Maybe (Closure Call)
forall a b. (a -> b) -> a -> b
$ Closure TypeError -> TCEnv
forall a. Closure a -> TCEnv
clEnv Closure TypeError
e) (m Doc -> m Doc) -> m Doc -> m Doc
forall a b. (a -> b) -> a -> b
$ Closure TypeError -> m Doc
forall a (m :: * -> *). (PrettyTCM a, MonadPretty m) => a -> m Doc
prettyTCM Closure TypeError
e
    Exception r :: Range
r s :: Doc
s     -> Range -> m Doc -> m Doc
forall (m :: * -> *) a.
(MonadPretty m, HasRange a) =>
a -> m Doc -> m Doc
sayWhere Range
r (m Doc -> m Doc) -> m Doc -> m Doc
forall a b. (a -> b) -> a -> b
$ Doc -> m Doc
forall (m :: * -> *) a. Monad m => a -> m a
return Doc
s
    IOException _ r :: Range
r e :: IOException
e -> Range -> m Doc -> m Doc
forall (m :: * -> *) a.
(MonadPretty m, HasRange a) =>
a -> m Doc -> m Doc
sayWhere Range
r (m Doc -> m Doc) -> m Doc -> m Doc
forall a b. (a -> b) -> a -> b
$ String -> m Doc
forall (m :: * -> *). Monad m => String -> m Doc
fwords (String -> m Doc) -> String -> m Doc
forall a b. (a -> b) -> a -> b
$ IOException -> String
forall a. Show a => a -> String
show IOException
e
    PatternErr{}      -> TCErr -> m Doc -> m Doc
forall (m :: * -> *) a.
(MonadPretty m, HasRange a) =>
a -> m Doc -> m Doc
sayWhere TCErr
err (m Doc -> m Doc) -> m Doc -> m Doc
forall a b. (a -> b) -> a -> b
$ String -> m Doc
forall (m :: * -> *). Monad m => String -> m Doc
panic "uncaught pattern violation"

-- | Drops given amount of leading components of the qualified name.
dropTopLevelModule' :: Int -> QName -> QName
dropTopLevelModule' :: Int -> QName -> QName
dropTopLevelModule' k :: Int
k (QName (MName ns :: [Name]
ns) n :: Name
n) = ModuleName -> Name -> QName
QName ([Name] -> ModuleName
MName (Int -> [Name] -> [Name]
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 q :: QName
q = ((QName -> QName) -> QName -> QName
forall a b. (a -> b) -> a -> b
$ QName
q) ((QName -> QName) -> QName)
-> TCMT IO (QName -> QName) -> TCM QName
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> TCMT IO (QName -> QName)
forall (m :: * -> *).
(MonadTCEnv m, ReadTCState m) =>
m (QName -> QName)
topLevelModuleDropper

-- | Produces a function which drops the filename component of the qualified name.
topLevelModuleDropper :: (MonadTCEnv m, ReadTCState m) => m (QName -> QName)
topLevelModuleDropper :: m (QName -> QName)
topLevelModuleDropper = do
  m (Maybe AbsolutePath)
-> m (QName -> QName)
-> (AbsolutePath -> m (QName -> QName))
-> m (QName -> QName)
forall (m :: * -> *) a b.
Monad m =>
m (Maybe a) -> m b -> (a -> m b) -> m b
caseMaybeM ((TCEnv -> Maybe AbsolutePath) -> m (Maybe AbsolutePath)
forall (m :: * -> *) a. MonadTCEnv m => (TCEnv -> a) -> m a
asksTC TCEnv -> Maybe AbsolutePath
envCurrentPath) ((QName -> QName) -> m (QName -> QName)
forall (m :: * -> *) a. Monad m => a -> m a
return QName -> QName
forall a. a -> a
id) ((AbsolutePath -> m (QName -> QName)) -> m (QName -> QName))
-> (AbsolutePath -> m (QName -> QName)) -> m (QName -> QName)
forall a b. (a -> b) -> a -> b
$ \ f :: AbsolutePath
f -> do
  TopLevelModuleName
m <- TopLevelModuleName
-> Maybe TopLevelModuleName -> TopLevelModuleName
forall a. a -> Maybe a -> a
fromMaybe TopLevelModuleName
forall a. HasCallStack => a
__IMPOSSIBLE__ (Maybe TopLevelModuleName -> TopLevelModuleName)
-> m (Maybe TopLevelModuleName) -> m TopLevelModuleName
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> AbsolutePath -> m (Maybe TopLevelModuleName)
forall (m :: * -> *).
ReadTCState m =>
AbsolutePath -> m (Maybe TopLevelModuleName)
lookupModuleFromSource AbsolutePath
f
  (QName -> QName) -> m (QName -> QName)
forall (m :: * -> *) a. Monad m => a -> m a
return ((QName -> QName) -> m (QName -> QName))
-> (QName -> QName) -> m (QName -> QName)
forall a b. (a -> b) -> a -> b
$ Int -> QName -> QName
dropTopLevelModule' (Int -> QName -> QName) -> Int -> QName -> QName
forall a b. (a -> b) -> a -> b
$ TopLevelModuleName -> Int
forall a. Sized a => a -> Int
size TopLevelModuleName
m

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

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

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

    CompilationError s :: String
s -> [m Doc] -> m Doc
forall (m :: * -> *). Monad m => [m Doc] -> m Doc
sep [String -> m Doc
forall (m :: * -> *). Monad m => String -> m Doc
fwords "Compilation error:", String -> m Doc
forall (m :: * -> *). Monad m => String -> m Doc
text String
s]

    GenericError s :: String
s -> String -> m Doc
forall (m :: * -> *). Monad m => String -> m Doc
fwords String
s

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

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

    DataMustEndInSort t :: Term
t -> [m Doc] -> m Doc
forall (m :: * -> *). Monad m => [m Doc] -> m Doc
fsep ([m Doc] -> m Doc) -> [m Doc] -> m Doc
forall a b. (a -> b) -> a -> b
$
      String -> [m Doc]
forall (m :: * -> *). Monad m => String -> [m Doc]
pwords "The type of a datatype must end in a sort."
      [m Doc] -> [m Doc] -> [m Doc]
forall a. [a] -> [a] -> [a]
++ [Term -> m Doc
forall a (m :: * -> *). (PrettyTCM a, MonadPretty m) => a -> m Doc
prettyTCM Term
t] [m Doc] -> [m Doc] -> [m Doc]
forall a. [a] -> [a] -> [a]
++ String -> [m Doc]
forall (m :: * -> *). Monad m => String -> [m Doc]
pwords "isn't a sort."

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

    ShouldEndInApplicationOfTheDatatype t :: Type
t -> [m Doc] -> m Doc
forall (m :: * -> *). Monad m => [m Doc] -> m Doc
fsep ([m Doc] -> m Doc) -> [m Doc] -> m Doc
forall a b. (a -> b) -> a -> b
$
      String -> [m Doc]
forall (m :: * -> *). Monad m => String -> [m Doc]
pwords "The target of a constructor must be the datatype applied to its parameters,"
      [m Doc] -> [m Doc] -> [m Doc]
forall a. [a] -> [a] -> [a]
++ [Type -> m Doc
forall a (m :: * -> *). (PrettyTCM a, MonadPretty m) => a -> m Doc
prettyTCM Type
t] [m Doc] -> [m Doc] -> [m Doc]
forall a. [a] -> [a] -> [a]
++ String -> [m Doc]
forall (m :: * -> *). Monad m => String -> [m Doc]
pwords "isn't"

    ShouldBeAppliedToTheDatatypeParameters s :: Term
s t :: Term
t -> [m Doc] -> m Doc
forall (m :: * -> *). Monad m => [m Doc] -> m Doc
fsep ([m Doc] -> m Doc) -> [m Doc] -> m Doc
forall a b. (a -> b) -> a -> b
$
      String -> [m Doc]
forall (m :: * -> *). Monad m => String -> [m Doc]
pwords "The target of the constructor should be" [m Doc] -> [m Doc] -> [m Doc]
forall a. [a] -> [a] -> [a]
++ [Term -> m Doc
forall a (m :: * -> *). (PrettyTCM a, MonadPretty m) => a -> m Doc
prettyTCM Term
s] [m Doc] -> [m Doc] -> [m Doc]
forall a. [a] -> [a] -> [a]
++
      String -> [m Doc]
forall (m :: * -> *). Monad m => String -> [m Doc]
pwords "instead of" [m Doc] -> [m Doc] -> [m Doc]
forall a. [a] -> [a] -> [a]
++ [Term -> m Doc
forall a (m :: * -> *). (PrettyTCM a, MonadPretty m) => a -> m Doc
prettyTCM Term
t]

    ShouldBeApplicationOf t :: Type
t q :: QName
q -> [m Doc] -> m Doc
forall (m :: * -> *). Monad m => [m Doc] -> m Doc
fsep ([m Doc] -> m Doc) -> [m Doc] -> m Doc
forall a b. (a -> b) -> a -> b
$
      String -> [m Doc]
forall (m :: * -> *). Monad m => String -> [m Doc]
pwords "The pattern constructs an element of" [m Doc] -> [m Doc] -> [m Doc]
forall a. [a] -> [a] -> [a]
++ [QName -> m Doc
forall a (m :: * -> *). (PrettyTCM a, MonadPretty m) => a -> m Doc
prettyTCM QName
q] [m Doc] -> [m Doc] -> [m Doc]
forall a. [a] -> [a] -> [a]
++
      String -> [m Doc]
forall (m :: * -> *). Monad m => String -> [m Doc]
pwords "which is not the right datatype"

    ShouldBeRecordType t :: Type
t -> [m Doc] -> m Doc
forall (m :: * -> *). Monad m => [m Doc] -> m Doc
fsep ([m Doc] -> m Doc) -> [m Doc] -> m Doc
forall a b. (a -> b) -> a -> b
$
      String -> [m Doc]
forall (m :: * -> *). Monad m => String -> [m Doc]
pwords "Expected non-abstract record type, found " [m Doc] -> [m Doc] -> [m Doc]
forall a. [a] -> [a] -> [a]
++ [Type -> m Doc
forall a (m :: * -> *). (PrettyTCM a, MonadPretty m) => a -> m Doc
prettyTCM Type
t]

    ShouldBeRecordPattern p :: DeBruijnPattern
p -> [m Doc] -> m Doc
forall (m :: * -> *). Monad m => [m Doc] -> m Doc
fsep ([m Doc] -> m Doc) -> [m Doc] -> m Doc
forall a b. (a -> b) -> a -> b
$
      String -> [m Doc]
forall (m :: * -> *). Monad m => String -> [m Doc]
pwords "Expected record pattern" -- ", found " ++ [prettyTCM p]

    NotAProjectionPattern p :: NamedArg Pattern
p -> [m Doc] -> m Doc
forall (m :: * -> *). Monad m => [m Doc] -> m Doc
fsep ([m Doc] -> m Doc) -> [m Doc] -> m Doc
forall a b. (a -> b) -> a -> b
$
      String -> [m Doc]
forall (m :: * -> *). Monad m => String -> [m Doc]
pwords "Not a valid projection for a copattern: " [m Doc] -> [m Doc] -> [m Doc]
forall a. [a] -> [a] -> [a]
++ [ NamedArg Pattern -> m Doc
forall c a (m :: * -> *).
(Pretty c, ToConcrete a c, MonadAbsToCon m) =>
a -> m Doc
prettyA NamedArg Pattern
p ]

    WrongHidingInLHS -> String -> m Doc
forall (m :: * -> *). Monad m => String -> m Doc
fwords "Unexpected implicit argument"

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

    WrongIrrelevanceInLambda ->
      String -> m Doc
forall (m :: * -> *). Monad m => String -> m Doc
fwords "Found a non-strict lambda where a irrelevant lambda was expected"

    WrongQuantityInLambda ->
      String -> m Doc
forall (m :: * -> *). Monad m => String -> m Doc
fwords "Incorrect quantity annotation in lambda"

    WrongCohesionInLambda ->
      String -> m Doc
forall (m :: * -> *). Monad m => String -> m Doc
fwords "Incorrect cohesion annotation in lambda"

    WrongNamedArgument a :: NamedArg Expr
a xs0 :: [NamedName]
xs0 -> [m Doc] -> m Doc
forall (m :: * -> *). Monad m => [m Doc] -> m Doc
fsep ([m Doc] -> m Doc) -> [m Doc] -> m Doc
forall a b. (a -> b) -> a -> b
$
      String -> [m Doc]
forall (m :: * -> *). Monad m => String -> [m Doc]
pwords "Function does not accept argument "
      [m Doc] -> [m Doc] -> [m Doc]
forall a. [a] -> [a] -> [a]
++ [NamedArg Expr -> m Doc
forall a (m :: * -> *). (PrettyTCM a, MonadPretty m) => a -> m Doc
prettyTCM NamedArg Expr
a] -- ++ pwords " (wrong argument name)"
      [m Doc] -> [m Doc] -> [m Doc]
forall a. [a] -> [a] -> [a]
++ if [NamedName] -> Bool
forall a. Null a => a -> Bool
null [NamedName]
xs then [] else
         [m Doc -> m Doc
forall (m :: * -> *). Functor m => m Doc -> m Doc
parens (m Doc -> m Doc) -> m Doc -> m Doc
forall a b. (a -> b) -> a -> b
$ [m Doc] -> m Doc
forall (m :: * -> *). Monad m => [m Doc] -> m Doc
fsep ([m Doc] -> m Doc) -> [m Doc] -> m Doc
forall a b. (a -> b) -> a -> b
$ String -> m Doc
forall (m :: * -> *). Monad m => String -> m Doc
text "possible arguments:" m Doc -> [m Doc] -> [m Doc]
forall a. a -> [a] -> [a]
: (NamedName -> m Doc) -> [NamedName] -> [m Doc]
forall a b. (a -> b) -> [a] -> [b]
map NamedName -> m Doc
forall (m :: * -> *) a. (Monad m, Pretty a) => a -> m Doc
pretty [NamedName]
xs]
      where
      xs :: [NamedName]
xs = (NamedName -> Bool) -> [NamedName] -> [NamedName]
forall a. (a -> Bool) -> [a] -> [a]
filter (Bool -> Bool
not (Bool -> Bool) -> (NamedName -> Bool) -> NamedName -> Bool
forall b c a. (b -> c) -> (a -> b) -> a -> c
. NamedName -> Bool
forall a. IsNoName a => a -> Bool
isNoName) [NamedName]
xs0

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

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

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

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

    UninstantiatedDotPattern e :: Expr
e -> [m Doc] -> m Doc
forall (m :: * -> *). Monad m => [m Doc] -> m Doc
fsep ([m Doc] -> m Doc) -> [m Doc] -> m Doc
forall a b. (a -> b) -> a -> b
$
      String -> [m Doc]
forall (m :: * -> *). Monad m => String -> [m Doc]
pwords "Failed to infer the value of dotted pattern"

    ForcedConstructorNotInstantiated p :: Pattern
p -> [m Doc] -> m Doc
forall (m :: * -> *). Monad m => [m Doc] -> m Doc
fsep ([m Doc] -> m Doc) -> [m Doc] -> m Doc
forall a b. (a -> b) -> a -> b
$
      String -> [m Doc]
forall (m :: * -> *). Monad m => String -> [m Doc]
pwords "Failed to infer that constructor pattern "
      [m Doc] -> [m Doc] -> [m Doc]
forall a. [a] -> [a] -> [a]
++ [Pattern -> m Doc
forall c a (m :: * -> *).
(Pretty c, ToConcrete a c, MonadAbsToCon m) =>
a -> m Doc
prettyA Pattern
p] [m Doc] -> [m Doc] -> [m Doc]
forall a. [a] -> [a] -> [a]
++ String -> [m Doc]
forall (m :: * -> *). Monad m => String -> [m Doc]
pwords " is forced"

    IlltypedPattern p :: Pattern
p a :: Type
a -> do
      let ho :: p -> p -> m Doc
ho _ _ = [m Doc] -> m Doc
forall (m :: * -> *). Monad m => [m Doc] -> m Doc
fsep ([m Doc] -> m Doc) -> [m Doc] -> m Doc
forall a b. (a -> b) -> a -> b
$ String -> [m Doc]
forall (m :: * -> *). Monad m => String -> [m Doc]
pwords "Cannot pattern match on functions"
      Type -> (Dom Type -> Abs Type -> m Doc) -> (Type -> m Doc) -> m Doc
forall (m :: * -> *) a.
MonadReduce m =>
Type -> (Dom Type -> Abs Type -> m a) -> (Type -> m a) -> m a
ifPiType Type
a Dom Type -> Abs Type -> m Doc
forall (m :: * -> *) p p. Monad m => p -> p -> m Doc
ho ((Type -> m Doc) -> m Doc) -> (Type -> m Doc) -> m Doc
forall a b. (a -> b) -> a -> b
$ {- else -} \ _ -> do
        [m Doc] -> m Doc
forall (m :: * -> *). Monad m => [m Doc] -> m Doc
fsep ([m Doc] -> m Doc) -> [m Doc] -> m Doc
forall a b. (a -> b) -> a -> b
$ String -> [m Doc]
forall (m :: * -> *). Monad m => String -> [m Doc]
pwords "Type mismatch"

    IllformedProjectionPattern p :: Pattern
p -> [m Doc] -> m Doc
forall (m :: * -> *). Monad m => [m Doc] -> m Doc
fsep ([m Doc] -> m Doc) -> [m Doc] -> m Doc
forall a b. (a -> b) -> a -> b
$
      String -> [m Doc]
forall (m :: * -> *). Monad m => String -> [m Doc]
pwords "Ill-formed projection pattern " [m Doc] -> [m Doc] -> [m Doc]
forall a. [a] -> [a] -> [a]
++ [Pattern -> m Doc
forall c a (m :: * -> *).
(Pretty c, ToConcrete a c, MonadAbsToCon m) =>
a -> m Doc
prettyA Pattern
p]

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

    WrongNumberOfConstructorArguments c :: QName
c expect :: Int
expect given :: Int
given -> [m Doc] -> m Doc
forall (m :: * -> *). Monad m => [m Doc] -> m Doc
fsep ([m Doc] -> m Doc) -> [m Doc] -> m Doc
forall a b. (a -> b) -> a -> b
$
      String -> [m Doc]
forall (m :: * -> *). Monad m => String -> [m Doc]
pwords "The constructor" [m Doc] -> [m Doc] -> [m Doc]
forall a. [a] -> [a] -> [a]
++ [QName -> m Doc
forall a (m :: * -> *). (PrettyTCM a, MonadPretty m) => a -> m Doc
prettyTCM QName
c] [m Doc] -> [m Doc] -> [m Doc]
forall a. [a] -> [a] -> [a]
++
      String -> [m Doc]
forall (m :: * -> *). Monad m => String -> [m Doc]
pwords "expects" [m Doc] -> [m Doc] -> [m Doc]
forall a. [a] -> [a] -> [a]
++ [Int -> m Doc
forall a (m :: * -> *). (PrettyTCM a, MonadPretty m) => a -> m Doc
prettyTCM Int
expect] [m Doc] -> [m Doc] -> [m Doc]
forall a. [a] -> [a] -> [a]
++
      String -> [m Doc]
forall (m :: * -> *). Monad m => String -> [m Doc]
pwords "arguments (including hidden ones), but has been given"
      [m Doc] -> [m Doc] -> [m Doc]
forall a. [a] -> [a] -> [a]
++ [Int -> m Doc
forall a (m :: * -> *). (PrettyTCM a, MonadPretty m) => a -> m Doc
prettyTCM Int
given] [m Doc] -> [m Doc] -> [m Doc]
forall a. [a] -> [a] -> [a]
++ String -> [m Doc]
forall (m :: * -> *). Monad m => String -> [m Doc]
pwords "(including hidden ones)"

    CantResolveOverloadedConstructorsTargetingSameDatatype d :: QName
d cs :: [QName]
cs -> [m Doc] -> m Doc
forall (m :: * -> *). Monad m => [m Doc] -> m Doc
fsep ([m Doc] -> m Doc) -> [m Doc] -> m Doc
forall a b. (a -> b) -> a -> b
$
      String -> [m Doc]
forall (m :: * -> *). Monad m => String -> [m Doc]
pwords "Can't resolve overloaded constructors targeting the same datatype"
      [m Doc] -> [m Doc] -> [m Doc]
forall a. [a] -> [a] -> [a]
++ [(m Doc -> m Doc
forall (m :: * -> *). Functor m => m Doc -> m Doc
parens (m Doc -> m Doc) -> m Doc -> m Doc
forall a b. (a -> b) -> a -> b
$ QName -> m Doc
forall a (m :: * -> *). (PrettyTCM a, MonadPretty m) => a -> m Doc
prettyTCM (QName -> QName
qnameToConcrete QName
d)) m Doc -> m Doc -> m Doc
forall a. Semigroup a => a -> a -> a
<> m Doc
forall (m :: * -> *). Monad m => m Doc
colon]
      [m Doc] -> [m Doc] -> [m Doc]
forall a. [a] -> [a] -> [a]
++ (QName -> m Doc) -> [QName] -> [m Doc]
forall a b. (a -> b) -> [a] -> [b]
map QName -> m Doc
forall (m :: * -> *) a. (Monad m, Pretty a) => a -> m Doc
pretty [QName]
cs

    DoesNotConstructAnElementOf c :: QName
c t :: Type
t -> [m Doc] -> m Doc
forall (m :: * -> *). Monad m => [m Doc] -> m Doc
fsep ([m Doc] -> m Doc) -> [m Doc] -> m Doc
forall a b. (a -> b) -> a -> b
$
      String -> [m Doc]
forall (m :: * -> *). Monad m => String -> [m Doc]
pwords "The constructor" [m Doc] -> [m Doc] -> [m Doc]
forall a. [a] -> [a] -> [a]
++ [QName -> m Doc
forall a (m :: * -> *). (PrettyTCM a, MonadPretty m) => a -> m Doc
prettyTCM QName
c] [m Doc] -> [m Doc] -> [m Doc]
forall a. [a] -> [a] -> [a]
++
      String -> [m Doc]
forall (m :: * -> *). Monad m => String -> [m Doc]
pwords "does not construct an element of" [m Doc] -> [m Doc] -> [m Doc]
forall a. [a] -> [a] -> [a]
++ [Type -> m Doc
forall a (m :: * -> *). (PrettyTCM a, MonadPretty m) => a -> m Doc
prettyTCM Type
t]

    ConstructorPatternInWrongDatatype c :: QName
c d :: QName
d -> [m Doc] -> m Doc
forall (m :: * -> *). Monad m => [m Doc] -> m Doc
fsep ([m Doc] -> m Doc) -> [m Doc] -> m Doc
forall a b. (a -> b) -> a -> b
$
      [QName -> m Doc
forall a (m :: * -> *). (PrettyTCM a, MonadPretty m) => a -> m Doc
prettyTCM QName
c] [m Doc] -> [m Doc] -> [m Doc]
forall a. [a] -> [a] -> [a]
++ String -> [m Doc]
forall (m :: * -> *). Monad m => String -> [m Doc]
pwords "is not a constructor of the datatype"
      [m Doc] -> [m Doc] -> [m Doc]
forall a. [a] -> [a] -> [a]
++ [QName -> m Doc
forall a (m :: * -> *). (PrettyTCM a, MonadPretty m) => a -> m Doc
prettyTCM QName
d]

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

    ShadowedModule x :: Name
x ms :: [ModuleName]
ms@(m0 :: ModuleName
m0 : _) -> do
      -- Clash! Concrete module name x already points to the abstract names ms.
      (r :: Range
r, m :: 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 <- m ScopeInfo
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 [ModuleName]
-> (ModuleName -> [(QName, ModuleName)]) -> [(QName, ModuleName)]
forall (m :: * -> *) a b. Monad m => m a -> (a -> m b) -> m b
>>= \ m :: ModuleName
m -> (QName -> (QName, ModuleName)) -> [QName] -> [(QName, ModuleName)]
forall a b. (a -> b) -> [a] -> [b]
map (,ModuleName
m) ([QName] -> [(QName, ModuleName)])
-> [QName] -> [(QName, ModuleName)]
forall a b. (a -> b) -> a -> b
$ ModuleName -> ScopeInfo -> [QName]
inverseScopeLookupModule ModuleName
m ScopeInfo
scope
        String -> Int -> String -> m ()
forall (m :: * -> *).
MonadDebug m =>
String -> Int -> String -> m ()
reportSLn "scope.clash.error" 30 (String -> m ()) -> String -> m ()
forall a b. (a -> b) -> a -> b
$ "candidates = " String -> String -> String
forall a. [a] -> [a] -> [a]
++ [(QName, ModuleName)] -> String
forall a. Pretty a => a -> String
prettyShow [(QName, ModuleName)]
xms0

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

        -- If we found a copy of x with non-empty range, great!
        Maybe (QName, ModuleName)
-> ((QName, ModuleName) -> m (Range, ModuleName))
-> m (Range, ModuleName)
-> m (Range, ModuleName)
forall a b. Maybe a -> (a -> b) -> b -> b
ifJust ([(QName, ModuleName)] -> Maybe (QName, ModuleName)
forall a. [a] -> Maybe a
listToMaybe [(QName, ModuleName)]
xms) (\ (x' :: QName
x', m :: ModuleName
m) -> (Range, ModuleName) -> m (Range, ModuleName)
forall (m :: * -> *) a. Monad m => a -> m a
return (QName -> Range
forall t. HasRange t => t -> Range
getRange QName
x', ModuleName
m)) (m (Range, ModuleName) -> m (Range, ModuleName))
-> m (Range, ModuleName) -> m (Range, ModuleName)
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 [ModuleName]
-> (ModuleName -> [(Range, ModuleName)]) -> [(Range, ModuleName)]
forall (m :: * -> *) a b. Monad m => m a -> (a -> m b) -> m b
>>= \ m :: ModuleName
m -> (Range -> (Range, ModuleName)) -> [Range] -> [(Range, ModuleName)]
forall a b. (a -> b) -> [a] -> [b]
map (,ModuleName
m) ([Range] -> [(Range, ModuleName)])
-> [Range] -> [(Range, ModuleName)]
forall a b. (a -> b) -> a -> b
$
              (Range -> Bool) -> [Range] -> [Range]
forall a. (a -> Bool) -> [a] -> [a]
filter (Range
forall a. Range' a
noRange Range -> Range -> Bool
forall a. Eq a => a -> a -> Bool
/=) ([Range] -> [Range]) -> [Range] -> [Range]
forall a b. (a -> b) -> a -> b
$ (Name -> Range) -> [Name] -> [Range]
forall a b. (a -> b) -> [a] -> [b]
map Name -> Range
nameBindingSite ([Name] -> [Range]) -> [Name] -> [Range]
forall a b. (a -> b) -> a -> b
$ [Name] -> [Name]
forall a. [a] -> [a]
reverse ([Name] -> [Name]) -> [Name] -> [Name]
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.
        String -> Int -> String -> m ()
forall (m :: * -> *).
MonadDebug m =>
String -> Int -> String -> m ()
reportSLn "scope.class.error" 30 (String -> m ()) -> String -> m ()
forall a b. (a -> b) -> a -> b
$ "rangeful clashing modules = " String -> String -> String
forall a. [a] -> [a] -> [a]
++ [(Range, ModuleName)] -> String
forall a. Pretty a => a -> String
prettyShow [(Range, ModuleName)]
rms

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

      [m Doc] -> m Doc
forall (m :: * -> *). Monad m => [m Doc] -> m Doc
fsep ([m Doc] -> m Doc) -> [m Doc] -> m Doc
forall a b. (a -> b) -> a -> b
$
        String -> [m Doc]
forall (m :: * -> *). Monad m => String -> [m Doc]
pwords "Duplicate definition of module" [m Doc] -> [m Doc] -> [m Doc]
forall a. [a] -> [a] -> [a]
++ [Name -> m Doc
forall a (m :: * -> *). (PrettyTCM a, MonadPretty m) => a -> m Doc
prettyTCM Name
x m Doc -> m Doc -> m Doc
forall a. Semigroup a => a -> a -> a
<> "."] [m Doc] -> [m Doc] -> [m Doc]
forall a. [a] -> [a] -> [a]
++
        String -> [m Doc]
forall (m :: * -> *). Monad m => String -> [m Doc]
pwords "Previous definition of" [m Doc] -> [m Doc] -> [m Doc]
forall a. [a] -> [a] -> [a]
++ [ModuleName -> m Doc
forall (m :: * -> *) b.
(ReadTCState m, Null (m b), IsString (m b)) =>
ModuleName -> m b
help ModuleName
m] [m Doc] -> [m Doc] -> [m Doc]
forall a. [a] -> [a] -> [a]
++ String -> [m Doc]
forall (m :: * -> *). Monad m => String -> [m Doc]
pwords "module" [m Doc] -> [m Doc] -> [m Doc]
forall a. [a] -> [a] -> [a]
++ [Name -> m Doc
forall a (m :: * -> *). (PrettyTCM a, MonadPretty m) => a -> m Doc
prettyTCM Name
x] [m Doc] -> [m Doc] -> [m Doc]
forall a. [a] -> [a] -> [a]
++
        String -> [m Doc]
forall (m :: * -> *). Monad m => String -> [m Doc]
pwords "at" [m Doc] -> [m Doc] -> [m Doc]
forall a. [a] -> [a] -> [a]
++ [Range -> m Doc
forall a (m :: * -> *). (PrettyTCM a, MonadPretty m) => a -> m Doc
prettyTCM Range
r]
      where
        help :: ModuleName -> m b
help m :: ModuleName
m = m (Maybe DataOrRecord) -> m b -> (DataOrRecord -> m b) -> m b
forall (m :: * -> *) a b.
Monad m =>
m (Maybe a) -> m b -> (a -> m b) -> m b
caseMaybeM (ModuleName -> m (Maybe DataOrRecord)
forall (m :: * -> *).
ReadTCState m =>
ModuleName -> m (Maybe DataOrRecord)
isDatatypeModule ModuleName
m) m b
forall a. Null a => a
empty ((DataOrRecord -> m b) -> m b) -> (DataOrRecord -> m b) -> m b
forall a b. (a -> b) -> a -> b
$ \case
          IsData   -> "(datatype)"
          IsRecord -> "(record)"

    ModuleArityMismatch m :: ModuleName
m EmptyTel args :: [NamedArg Expr]
args -> [m Doc] -> m Doc
forall (m :: * -> *). Monad m => [m Doc] -> m Doc
fsep ([m Doc] -> m Doc) -> [m Doc] -> m Doc
forall a b. (a -> b) -> a -> b
$
      String -> [m Doc]
forall (m :: * -> *). Monad m => String -> [m Doc]
pwords "The module" [m Doc] -> [m Doc] -> [m Doc]
forall a. [a] -> [a] -> [a]
++ [ModuleName -> m Doc
forall a (m :: * -> *). (PrettyTCM a, MonadPretty m) => a -> m Doc
prettyTCM ModuleName
m] [m Doc] -> [m Doc] -> [m Doc]
forall a. [a] -> [a] -> [a]
++
      String -> [m Doc]
forall (m :: * -> *). Monad m => String -> [m Doc]
pwords "is not parameterized, but is being applied to arguments"

    ModuleArityMismatch m :: ModuleName
m tel :: Telescope
tel@(ExtendTel _ _) args :: [NamedArg Expr]
args -> [m Doc] -> m Doc
forall (m :: * -> *). Monad m => [m Doc] -> m Doc
fsep ([m Doc] -> m Doc) -> [m Doc] -> m Doc
forall a b. (a -> b) -> a -> b
$
      String -> [m Doc]
forall (m :: * -> *). Monad m => String -> [m Doc]
pwords "The arguments to " [m Doc] -> [m Doc] -> [m Doc]
forall a. [a] -> [a] -> [a]
++ [ModuleName -> m Doc
forall a (m :: * -> *). (PrettyTCM a, MonadPretty m) => a -> m Doc
prettyTCM ModuleName
m] [m Doc] -> [m Doc] -> [m Doc]
forall a. [a] -> [a] -> [a]
++ String -> [m Doc]
forall (m :: * -> *). Monad m => String -> [m Doc]
pwords "do not fit the telescope" [m Doc] -> [m Doc] -> [m Doc]
forall a. [a] -> [a] -> [a]
++
      [Telescope -> m Doc
forall a (m :: * -> *). (PrettyTCM a, MonadPretty m) => a -> m Doc
prettyTCM Telescope
tel]

    ShouldBeEmpty t :: Type
t [] -> [m Doc] -> m Doc
forall (m :: * -> *). Monad m => [m Doc] -> m Doc
fsep ([m Doc] -> m Doc) -> [m Doc] -> m Doc
forall a b. (a -> b) -> a -> b
$
       [Type -> m Doc
forall a (m :: * -> *). (PrettyTCM a, MonadPretty m) => a -> m Doc
prettyTCM Type
t] [m Doc] -> [m Doc] -> [m Doc]
forall a. [a] -> [a] -> [a]
++ String -> [m Doc]
forall (m :: * -> *). Monad m => String -> [m Doc]
pwords "should be empty, but that's not obvious to me"

    ShouldBeEmpty t :: Type
t ps :: [DeBruijnPattern]
ps -> [m Doc] -> m Doc
forall (m :: * -> *). Monad m => [m Doc] -> m Doc
fsep (
      [Type -> m Doc
forall a (m :: * -> *). (PrettyTCM a, MonadPretty m) => a -> m Doc
prettyTCM Type
t] [m Doc] -> [m Doc] -> [m Doc]
forall a. [a] -> [a] -> [a]
++
      String -> [m Doc]
forall (m :: * -> *). Monad m => String -> [m Doc]
pwords "should be empty, but the following constructor patterns are valid:"
      ) m Doc -> m Doc -> m Doc
forall (m :: * -> *). Applicative m => m Doc -> m Doc -> m Doc
$$ Int -> m Doc -> m Doc
forall (m :: * -> *). Functor m => Int -> m Doc -> m Doc
nest 2 ([m Doc] -> m Doc
forall (m :: * -> *). Monad m => [m Doc] -> m Doc
vcat ([m Doc] -> m Doc) -> [m Doc] -> m Doc
forall a b. (a -> b) -> a -> b
$ (DeBruijnPattern -> m Doc) -> [DeBruijnPattern] -> [m Doc]
forall a b. (a -> b) -> [a] -> [b]
map (Integer -> DeBruijnPattern -> m Doc
forall (m :: * -> *) a.
MonadPretty m =>
Integer -> Pattern' a -> m Doc
prettyPat 0) [DeBruijnPattern]
ps)

    ShouldBeASort t :: Type
t -> [m Doc] -> m Doc
forall (m :: * -> *). Monad m => [m Doc] -> m Doc
fsep ([m Doc] -> m Doc) -> [m Doc] -> m Doc
forall a b. (a -> b) -> a -> b
$
      [Type -> m Doc
forall a (m :: * -> *). (PrettyTCM a, MonadPretty m) => a -> m Doc
prettyTCM Type
t] [m Doc] -> [m Doc] -> [m Doc]
forall a. [a] -> [a] -> [a]
++ String -> [m Doc]
forall (m :: * -> *). Monad m => String -> [m Doc]
pwords "should be a sort, but it isn't"

    ShouldBePi t :: Type
t -> [m Doc] -> m Doc
forall (m :: * -> *). Monad m => [m Doc] -> m Doc
fsep ([m Doc] -> m Doc) -> [m Doc] -> m Doc
forall a b. (a -> b) -> a -> b
$
      [Type -> m Doc
forall a (m :: * -> *). (PrettyTCM a, MonadPretty m) => a -> m Doc
prettyTCM Type
t] [m Doc] -> [m Doc] -> [m Doc]
forall a. [a] -> [a] -> [a]
++ String -> [m Doc]
forall (m :: * -> *). Monad m => String -> [m Doc]
pwords "should be a function type, but it isn't"

    ShouldBePath t :: Type
t -> [m Doc] -> m Doc
forall (m :: * -> *). Monad m => [m Doc] -> m Doc
fsep ([m Doc] -> m Doc) -> [m Doc] -> m Doc
forall a b. (a -> b) -> a -> b
$
      [Type -> m Doc
forall a (m :: * -> *). (PrettyTCM a, MonadPretty m) => a -> m Doc
prettyTCM Type
t] [m Doc] -> [m Doc] -> [m Doc]
forall a. [a] -> [a] -> [a]
++ String -> [m Doc]
forall (m :: * -> *). Monad m => String -> [m Doc]
pwords "should be a Path or PathP type, but it isn't"

    NotAProperTerm -> String -> m Doc
forall (m :: * -> *). Monad m => String -> m Doc
fwords "Found a malformed term"

    InvalidTypeSort s :: Sort
s -> [m Doc] -> m Doc
forall (m :: * -> *). Monad m => [m Doc] -> m Doc
fsep ([m Doc] -> m Doc) -> [m Doc] -> m Doc
forall a b. (a -> b) -> a -> b
$ [Sort -> m Doc
forall a (m :: * -> *). (PrettyTCM a, MonadPretty m) => a -> m Doc
prettyTCM Sort
s] [m Doc] -> [m Doc] -> [m Doc]
forall a. [a] -> [a] -> [a]
++ String -> [m Doc]
forall (m :: * -> *). Monad m => String -> [m Doc]
pwords "is not a valid type"
    InvalidType v :: Term
v -> [m Doc] -> m Doc
forall (m :: * -> *). Monad m => [m Doc] -> m Doc
fsep ([m Doc] -> m Doc) -> [m Doc] -> m Doc
forall a b. (a -> b) -> a -> b
$ [Term -> m Doc
forall a (m :: * -> *). (PrettyTCM a, MonadPretty m) => a -> m Doc
prettyTCM Term
v] [m Doc] -> [m Doc] -> [m Doc]
forall a. [a] -> [a] -> [a]
++ String -> [m Doc]
forall (m :: * -> *). Monad m => String -> [m Doc]
pwords "is not a valid type"

    FunctionTypeInSizeUniv v :: Term
v -> [m Doc] -> m Doc
forall (m :: * -> *). Monad m => [m Doc] -> m Doc
fsep ([m Doc] -> m Doc) -> [m Doc] -> m Doc
forall a b. (a -> b) -> a -> b
$
      String -> [m Doc]
forall (m :: * -> *). Monad m => String -> [m Doc]
pwords "Functions may not return sizes, thus, function type " [m Doc] -> [m Doc] -> [m Doc]
forall a. [a] -> [a] -> [a]
++
      [ Term -> m Doc
forall a (m :: * -> *). (PrettyTCM a, MonadPretty m) => a -> m Doc
prettyTCM Term
v ] [m Doc] -> [m Doc] -> [m Doc]
forall a. [a] -> [a] -> [a]
++ String -> [m Doc]
forall (m :: * -> *). Monad m => String -> [m Doc]
pwords " is illegal"

    SplitOnIrrelevant t :: Dom Type
t -> [m Doc] -> m Doc
forall (m :: * -> *). Monad m => [m Doc] -> m Doc
fsep ([m Doc] -> m Doc) -> [m Doc] -> m Doc
forall a b. (a -> b) -> a -> b
$
      String -> [m Doc]
forall (m :: * -> *). Monad m => String -> [m Doc]
pwords "Cannot pattern match against" [m Doc] -> [m Doc] -> [m Doc]
forall a. [a] -> [a] -> [a]
++ [String -> m Doc
forall (m :: * -> *). Monad m => String -> m Doc
text (String -> m Doc) -> String -> m Doc
forall a b. (a -> b) -> a -> b
$ Relevance -> String
forall a. Verbalize a => a -> String
verbalize (Relevance -> String) -> Relevance -> String
forall a b. (a -> b) -> a -> b
$ Dom Type -> Relevance
forall a. LensRelevance a => a -> Relevance
getRelevance Dom Type
t] [m Doc] -> [m Doc] -> [m Doc]
forall a. [a] -> [a] -> [a]
++
      String -> [m Doc]
forall (m :: * -> *). Monad m => String -> [m Doc]
pwords "argument of type" [m Doc] -> [m Doc] -> [m Doc]
forall a. [a] -> [a] -> [a]
++ [Type -> m Doc
forall a (m :: * -> *). (PrettyTCM a, MonadPretty m) => a -> m Doc
prettyTCM (Type -> m Doc) -> Type -> m Doc
forall a b. (a -> b) -> a -> b
$ Dom Type -> Type
forall t e. Dom' t e -> e
unDom Dom Type
t]

    SplitOnUnusableCohesion t :: Dom Type
t -> [m Doc] -> m Doc
forall (m :: * -> *). Monad m => [m Doc] -> m Doc
fsep ([m Doc] -> m Doc) -> [m Doc] -> m Doc
forall a b. (a -> b) -> a -> b
$
      String -> [m Doc]
forall (m :: * -> *). Monad m => String -> [m Doc]
pwords "Cannot pattern match against" [m Doc] -> [m Doc] -> [m Doc]
forall a. [a] -> [a] -> [a]
++ [String -> m Doc
forall (m :: * -> *). Monad m => String -> m Doc
text (String -> m Doc) -> String -> m Doc
forall a b. (a -> b) -> a -> b
$ Cohesion -> String
forall a. Verbalize a => a -> String
verbalize (Cohesion -> String) -> Cohesion -> String
forall a b. (a -> b) -> a -> b
$ Dom Type -> Cohesion
forall a. LensCohesion a => a -> Cohesion
getCohesion Dom Type
t] [m Doc] -> [m Doc] -> [m Doc]
forall a. [a] -> [a] -> [a]
++
      String -> [m Doc]
forall (m :: * -> *). Monad m => String -> [m Doc]
pwords "argument of type" [m Doc] -> [m Doc] -> [m Doc]
forall a. [a] -> [a] -> [a]
++ [Type -> m Doc
forall a (m :: * -> *). (PrettyTCM a, MonadPretty m) => a -> m Doc
prettyTCM (Type -> m Doc) -> Type -> m Doc
forall a b. (a -> b) -> a -> b
$ Dom Type -> Type
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 v :: Term
v t :: Type
t -> [m Doc] -> m Doc
forall (m :: * -> *). Monad m => [m Doc] -> m Doc
fsep ([m Doc] -> m Doc) -> [m Doc] -> m Doc
forall a b. (a -> b) -> a -> b
$
      String -> [m Doc]
forall (m :: * -> *). Monad m => String -> [m Doc]
pwords "Cannot pattern match because the (refined) argument " [m Doc] -> [m Doc] -> [m Doc]
forall a. [a] -> [a] -> [a]
++
      [ Term -> m Doc
forall a (m :: * -> *). (PrettyTCM a, MonadPretty m) => a -> m Doc
prettyTCM Term
v ] [m Doc] -> [m Doc] -> [m Doc]
forall a. [a] -> [a] -> [a]
++ String -> [m Doc]
forall (m :: * -> *). Monad m => String -> [m Doc]
pwords " is not a variable."

    DefinitionIsIrrelevant x :: QName
x -> [m Doc] -> m Doc
forall (m :: * -> *). Monad m => [m Doc] -> m Doc
fsep ([m Doc] -> m Doc) -> [m Doc] -> m Doc
forall a b. (a -> b) -> a -> b
$
      "Identifier" m Doc -> [m Doc] -> [m Doc]
forall a. a -> [a] -> [a]
: QName -> m Doc
forall a (m :: * -> *). (PrettyTCM a, MonadPretty m) => a -> m Doc
prettyTCM QName
x m Doc -> [m Doc] -> [m Doc]
forall a. a -> [a] -> [a]
: String -> [m Doc]
forall (m :: * -> *). Monad m => String -> [m Doc]
pwords "is declared irrelevant, so it cannot be used here"

    DefinitionIsErased x :: QName
x -> [m Doc] -> m Doc
forall (m :: * -> *). Monad m => [m Doc] -> m Doc
fsep ([m Doc] -> m Doc) -> [m Doc] -> m Doc
forall a b. (a -> b) -> a -> b
$
      "Identifier" m Doc -> [m Doc] -> [m Doc]
forall a. a -> [a] -> [a]
: QName -> m Doc
forall a (m :: * -> *). (PrettyTCM a, MonadPretty m) => a -> m Doc
prettyTCM QName
x m Doc -> [m Doc] -> [m Doc]
forall a. a -> [a] -> [a]
: String -> [m Doc]
forall (m :: * -> *). Monad m => String -> [m Doc]
pwords "is declared erased, so it cannot be used here"

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

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

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

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

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

    UnequalLevel cmp :: Comparison
cmp s :: Level
s t :: Level
t -> [m Doc] -> m Doc
forall (m :: * -> *). Monad m => [m Doc] -> m Doc
fsep ([m Doc] -> m Doc) -> [m Doc] -> m Doc
forall a b. (a -> b) -> a -> b
$
      [Level -> m Doc
forall a (m :: * -> *). (PrettyTCM a, MonadPretty m) => a -> m Doc
prettyTCM Level
s, Comparison -> m Doc
forall (m :: * -> *). MonadPretty m => Comparison -> m Doc
notCmp Comparison
cmp, Level -> m Doc
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 cmp :: Comparison
cmp a :: Type
a b :: Type
b -> Type -> m Doc -> Type -> m Doc
forall a (m :: * -> *).
(PrettyUnequal a, MonadPretty m) =>
a -> m Doc -> a -> m Doc
prettyUnequal Type
a (Comparison -> m Doc
forall (m :: * -> *). MonadPretty m => Comparison -> m Doc
notCmp Comparison
cmp) Type
b
--              fsep $ [prettyTCM a, notCmp cmp, prettyTCM b]

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

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

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

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

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

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

    TooManyFields r :: QName
r missing :: [Name]
missing xs :: [Name]
xs -> [m Doc] -> m Doc
forall (m :: * -> *). Monad m => [m Doc] -> m Doc
fsep ([m Doc] -> m Doc) -> [m Doc] -> m Doc
forall a b. (a -> b) -> a -> b
$
      String -> [m Doc]
forall (m :: * -> *). Monad m => String -> [m Doc]
pwords "The record type" [m Doc] -> [m Doc] -> [m Doc]
forall a. [a] -> [a] -> [a]
++ [QName -> m Doc
forall a (m :: * -> *). (PrettyTCM a, MonadPretty m) => a -> m Doc
prettyTCM QName
r] [m Doc] -> [m Doc] -> [m Doc]
forall a. [a] -> [a] -> [a]
++
      String -> [m Doc]
forall (m :: * -> *). Monad m => String -> [m Doc]
pwords "does not have the fields" [m Doc] -> [m Doc] -> [m Doc]
forall a. [a] -> [a] -> [a]
++ m Doc -> [m Doc] -> [m Doc]
forall (m :: * -> *).
(Applicative m, Semigroup (m Doc)) =>
m Doc -> [m Doc] -> [m Doc]
punctuate m Doc
forall (m :: * -> *). Monad m => m Doc
comma ((Name -> m Doc) -> [Name] -> [m Doc]
forall a b. (a -> b) -> [a] -> [b]
map Name -> m Doc
forall (m :: * -> *) a. (Monad m, Pretty a) => a -> m Doc
pretty [Name]
xs) [m Doc] -> [m Doc] -> [m Doc]
forall a. [a] -> [a] -> [a]
++
      if [Name] -> Bool
forall a. Null a => a -> Bool
null [Name]
missing then [] else
        String -> [m Doc]
forall (m :: * -> *). Monad m => String -> [m Doc]
pwords "but it would have the fields"  [m Doc] -> [m Doc] -> [m Doc]
forall a. [a] -> [a] -> [a]
++ m Doc -> [m Doc] -> [m Doc]
forall (m :: * -> *).
(Applicative m, Semigroup (m Doc)) =>
m Doc -> [m Doc] -> [m Doc]
punctuate m Doc
forall (m :: * -> *). Monad m => m Doc
comma ((Name -> m Doc) -> [Name] -> [m Doc]
forall a b. (a -> b) -> [a] -> [b]
map Name -> m Doc
forall (m :: * -> *) a. (Monad m, Pretty a) => a -> m Doc
pretty [Name]
missing)

    DuplicateConstructors xs :: [Name]
xs -> [m Doc] -> m Doc
forall (m :: * -> *). Monad m => [m Doc] -> m Doc
fsep ([m Doc] -> m Doc) -> [m Doc] -> m Doc
forall a b. (a -> b) -> a -> b
$
      String -> [m Doc]
forall (m :: * -> *). Monad m => String -> [m Doc]
pwords "Duplicate constructors" [m Doc] -> [m Doc] -> [m Doc]
forall a. [a] -> [a] -> [a]
++ m Doc -> [m Doc] -> [m Doc]
forall (m :: * -> *).
(Applicative m, Semigroup (m Doc)) =>
m Doc -> [m Doc] -> [m Doc]
punctuate m Doc
forall (m :: * -> *). Monad m => m Doc
comma ((Name -> m Doc) -> [Name] -> [m Doc]
forall a b. (a -> b) -> [a] -> [b]
map Name -> m Doc
forall (m :: * -> *) a. (Monad m, Pretty a) => a -> m Doc
pretty [Name]
xs) [m Doc] -> [m Doc] -> [m Doc]
forall a. [a] -> [a] -> [a]
++
      String -> [m Doc]
forall (m :: * -> *). Monad m => String -> [m Doc]
pwords "in datatype"

    DuplicateFields xs :: [Name]
xs -> [m Doc] -> m Doc
forall (m :: * -> *). Monad m => [m Doc] -> m Doc
fsep ([m Doc] -> m Doc) -> [m Doc] -> m Doc
forall a b. (a -> b) -> a -> b
$
      String -> [m Doc]
forall (m :: * -> *). Monad m => String -> [m Doc]
pwords "Duplicate fields" [m Doc] -> [m Doc] -> [m Doc]
forall a. [a] -> [a] -> [a]
++ m Doc -> [m Doc] -> [m Doc]
forall (m :: * -> *).
(Applicative m, Semigroup (m Doc)) =>
m Doc -> [m Doc] -> [m Doc]
punctuate m Doc
forall (m :: * -> *). Monad m => m Doc
comma ((Name -> m Doc) -> [Name] -> [m Doc]
forall a b. (a -> b) -> [a] -> [b]
map Name -> m Doc
forall (m :: * -> *) a. (Monad m, Pretty a) => a -> m Doc
pretty [Name]
xs) [m Doc] -> [m Doc] -> [m Doc]
forall a. [a] -> [a] -> [a]
++
      String -> [m Doc]
forall (m :: * -> *). Monad m => String -> [m Doc]
pwords "in record"

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

    UnexpectedWithPatterns ps :: [Pattern]
ps -> [m Doc] -> m Doc
forall (m :: * -> *). Monad m => [m Doc] -> m Doc
fsep ([m Doc] -> m Doc) -> [m Doc] -> m Doc
forall a b. (a -> b) -> a -> b
$
      String -> [m Doc]
forall (m :: * -> *). Monad m => String -> [m Doc]
pwords "Unexpected with patterns" [m Doc] -> [m Doc] -> [m Doc]
forall a. [a] -> [a] -> [a]
++ (m Doc -> [m Doc] -> [m Doc]
forall (m :: * -> *).
(Applicative m, Semigroup (m Doc)) =>
m Doc -> [m Doc] -> [m Doc]
punctuate " |" ([m Doc] -> [m Doc]) -> [m Doc] -> [m Doc]
forall a b. (a -> b) -> a -> b
$ (Pattern -> m Doc) -> [Pattern] -> [m Doc]
forall a b. (a -> b) -> [a] -> [b]
map Pattern -> m Doc
forall c a (m :: * -> *).
(Pretty c, ToConcrete a c, MonadAbsToCon m) =>
a -> m Doc
prettyA [Pattern]
ps)

    WithClausePatternMismatch p :: Pattern
p q :: NamedArg DeBruijnPattern
q -> [m Doc] -> m Doc
forall (m :: * -> *). Monad m => [m Doc] -> m Doc
fsep ([m Doc] -> m Doc) -> [m Doc] -> m Doc
forall a b. (a -> b) -> a -> b
$
      String -> [m Doc]
forall (m :: * -> *). Monad m => String -> [m Doc]
pwords "With clause pattern " [m Doc] -> [m Doc] -> [m Doc]
forall a. [a] -> [a] -> [a]
++ [Pattern -> m Doc
forall c a (m :: * -> *).
(Pretty c, ToConcrete a c, MonadAbsToCon m) =>
a -> m Doc
prettyA Pattern
p] [m Doc] -> [m Doc] -> [m Doc]
forall a. [a] -> [a] -> [a]
++
      String -> [m Doc]
forall (m :: * -> *). Monad m => String -> [m Doc]
pwords " is not an instance of its parent pattern " [m Doc] -> [m Doc] -> [m Doc]
forall a. [a] -> [a] -> [a]
++ [[Doc] -> Doc
P.fsep ([Doc] -> Doc) -> m [Doc] -> m Doc
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> [NamedArg DeBruijnPattern] -> m [Doc]
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 m :: MetaId
m {- ps -} i :: Int
i -> [m Doc] -> m Doc
forall (m :: * -> *). Monad m => [m Doc] -> m Doc
fsep ([m Doc] -> m Doc) -> [m Doc] -> m Doc
forall a b. (a -> b) -> a -> b
$
      String -> [m Doc]
forall (m :: * -> *). Monad m => String -> [m Doc]
pwords "The metavariable" [m Doc] -> [m Doc] -> [m Doc]
forall a. [a] -> [a] -> [a]
++ [Term -> m Doc
forall a (m :: * -> *). (PrettyTCM a, MonadPretty m) => a -> m Doc
prettyTCM (Term -> m Doc) -> Term -> m Doc
forall a b. (a -> b) -> a -> b
$ MetaId -> Elims -> Term
MetaV MetaId
m []] [m Doc] -> [m Doc] -> [m Doc]
forall a. [a] -> [a] -> [a]
++
      String -> [m Doc]
forall (m :: * -> *). Monad m => String -> [m Doc]
pwords "cannot depend on" [m Doc] -> [m Doc] -> [m Doc]
forall a. [a] -> [a] -> [a]
++ [Int -> m Doc
pvar Int
i] [m Doc] -> [m Doc] -> [m Doc]
forall a. [a] -> [a] -> [a]
++
      [] -- pwords "because it" ++ deps
        where
          pvar :: Int -> m Doc
pvar = Term -> m Doc
forall a (m :: * -> *). (PrettyTCM a, MonadPretty m) => a -> m Doc
prettyTCM (Term -> m Doc) -> (Int -> Term) -> Int -> m Doc
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 m :: MetaId
m -> [m Doc] -> m Doc
forall (m :: * -> *). Monad m => [m Doc] -> m Doc
fsep ([m Doc] -> m Doc) -> [m Doc] -> m Doc
forall a b. (a -> b) -> a -> b
$
      String -> [m Doc]
forall (m :: * -> *). Monad m => String -> [m Doc]
pwords "Cannot construct infinite solution of metavariable" [m Doc] -> [m Doc] -> [m Doc]
forall a. [a] -> [a] -> [a]
++ [Term -> m Doc
forall a (m :: * -> *). (PrettyTCM a, MonadPretty m) => a -> m Doc
prettyTCM (Term -> m Doc) -> Term -> m Doc
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 m :: MetaId
m _ -> [m Doc] -> m Doc
forall (m :: * -> *). Monad m => [m Doc] -> m Doc
fsep ([m Doc] -> m Doc) -> [m Doc] -> m Doc
forall a b. (a -> b) -> a -> b
$
      String -> [m Doc]
forall (m :: * -> *). Monad m => String -> [m Doc]
pwords "Cannot instantiate the metavariable because (part of) the" [m Doc] -> [m Doc] -> [m Doc]
forall a. [a] -> [a] -> [a]
++
      String -> [m Doc]
forall (m :: * -> *). Monad m => String -> [m Doc]
pwords "solution was created in an irrelevant context."

    -- The following error is caught and reraised as GenericDocError in Occurs.hs
    MetaErasedSolution m :: MetaId
m _ -> [m Doc] -> m Doc
forall (m :: * -> *). Monad m => [m Doc] -> m Doc
fsep ([m Doc] -> m Doc) -> [m Doc] -> m Doc
forall a b. (a -> b) -> a -> b
$
      String -> [m Doc]
forall (m :: * -> *). Monad m => String -> [m Doc]
pwords "Cannot instantiate the metavariable because (part of) the" [m Doc] -> [m Doc] -> [m Doc]
forall a. [a] -> [a] -> [a]
++
      String -> [m Doc]
forall (m :: * -> *). Monad m => String -> [m Doc]
pwords "solution was created in an erased context."

    BuiltinMustBeConstructor s :: String
s e :: Expr
e -> [m Doc] -> m Doc
forall (m :: * -> *). Monad m => [m Doc] -> m Doc
fsep ([m Doc] -> m Doc) -> [m Doc] -> m Doc
forall a b. (a -> b) -> a -> b
$
      [Expr -> m Doc
forall c a (m :: * -> *).
(Pretty c, ToConcrete a c, MonadAbsToCon m) =>
a -> m Doc
prettyA Expr
e] [m Doc] -> [m Doc] -> [m Doc]
forall a. [a] -> [a] -> [a]
++ String -> [m Doc]
forall (m :: * -> *). Monad m => String -> [m Doc]
pwords "must be a constructor in the binding to builtin" [m Doc] -> [m Doc] -> [m Doc]
forall a. [a] -> [a] -> [a]
++ [String -> m Doc
forall (m :: * -> *). Monad m => String -> m Doc
text String
s]

    NoSuchBuiltinName s :: String
s -> [m Doc] -> m Doc
forall (m :: * -> *). Monad m => [m Doc] -> m Doc
fsep ([m Doc] -> m Doc) -> [m Doc] -> m Doc
forall a b. (a -> b) -> a -> b
$
      String -> [m Doc]
forall (m :: * -> *). Monad m => String -> [m Doc]
pwords "There is no built-in thing called" [m Doc] -> [m Doc] -> [m Doc]
forall a. [a] -> [a] -> [a]
++ [String -> m Doc
forall (m :: * -> *). Monad m => String -> m Doc
text String
s]

    DuplicateBuiltinBinding b :: String
b x :: Term
x y :: Term
y -> [m Doc] -> m Doc
forall (m :: * -> *). Monad m => [m Doc] -> m Doc
fsep ([m Doc] -> m Doc) -> [m Doc] -> m Doc
forall a b. (a -> b) -> a -> b
$
      String -> [m Doc]
forall (m :: * -> *). Monad m => String -> [m Doc]
pwords "Duplicate binding for built-in thing" [m Doc] -> [m Doc] -> [m Doc]
forall a. [a] -> [a] -> [a]
++ [String -> m Doc
forall (m :: * -> *). Monad m => String -> m Doc
text String
b m Doc -> m Doc -> m Doc
forall a. Semigroup a => a -> a -> a
<> m Doc
forall (m :: * -> *). Monad m => m Doc
comma] [m Doc] -> [m Doc] -> [m Doc]
forall a. [a] -> [a] -> [a]
++
      String -> [m Doc]
forall (m :: * -> *). Monad m => String -> [m Doc]
pwords "previous binding to" [m Doc] -> [m Doc] -> [m Doc]
forall a. [a] -> [a] -> [a]
++ [Term -> m Doc
forall a (m :: * -> *). (PrettyTCM a, MonadPretty m) => a -> m Doc
prettyTCM Term
x]

    NoBindingForBuiltin x :: String
x
      | String
x String -> [String] -> Bool
forall (t :: * -> *) a. (Foldable t, Eq a) => a -> t a -> Bool
`elem` [String
builtinZero, String
builtinSuc] -> [m Doc] -> m Doc
forall (m :: * -> *). Monad m => [m Doc] -> m Doc
fsep ([m Doc] -> m Doc) -> [m Doc] -> m Doc
forall a b. (a -> b) -> a -> b
$
        String -> [m Doc]
forall (m :: * -> *). Monad m => String -> [m Doc]
pwords "No binding for builtin " [m Doc] -> [m Doc] -> [m Doc]
forall a. [a] -> [a] -> [a]
++ [String -> m Doc
forall (m :: * -> *). Monad m => String -> m Doc
text String
x m Doc -> m Doc -> m Doc
forall a. Semigroup a => a -> a -> a
<> m Doc
forall (m :: * -> *). Monad m => m Doc
comma] [m Doc] -> [m Doc] -> [m Doc]
forall a. [a] -> [a] -> [a]
++
        String -> [m Doc]
forall (m :: * -> *). Monad m => String -> [m Doc]
pwords ("use {-# BUILTIN " String -> String -> String
forall a. [a] -> [a] -> [a]
++ String
builtinNat String -> String -> String
forall a. [a] -> [a] -> [a]
++ " name #-} to bind builtin natural " String -> String -> String
forall a. [a] -> [a] -> [a]
++
                "numbers to the type 'name'")
      | Bool
otherwise -> [m Doc] -> m Doc
forall (m :: * -> *). Monad m => [m Doc] -> m Doc
fsep ([m Doc] -> m Doc) -> [m Doc] -> m Doc
forall a b. (a -> b) -> a -> b
$
        String -> [m Doc]
forall (m :: * -> *). Monad m => String -> [m Doc]
pwords "No binding for builtin thing" [m Doc] -> [m Doc] -> [m Doc]
forall a. [a] -> [a] -> [a]
++ [String -> m Doc
forall (m :: * -> *). Monad m => String -> m Doc
text String
x m Doc -> m Doc -> m Doc
forall a. Semigroup a => a -> a -> a
<> m Doc
forall (m :: * -> *). Monad m => m Doc
comma] [m Doc] -> [m Doc] -> [m Doc]
forall a. [a] -> [a] -> [a]
++
        String -> [m Doc]
forall (m :: * -> *). Monad m => String -> [m Doc]
pwords ("use {-# BUILTIN " String -> String -> String
forall a. [a] -> [a] -> [a]
++ String
x String -> String -> String
forall a. [a] -> [a] -> [a]
++ " name #-} to bind it to 'name'")

    DuplicatePrimitiveBinding b :: String
b x :: QName
x y :: QName
y -> [m Doc] -> m Doc
forall (m :: * -> *). Monad m => [m Doc] -> m Doc
fsep ([m Doc] -> m Doc) -> [m Doc] -> m Doc
forall a b. (a -> b) -> a -> b
$
      String -> [m Doc]
forall (m :: * -> *). Monad m => String -> [m Doc]
pwords "Duplicate binding for primitive thing" [m Doc] -> [m Doc] -> [m Doc]
forall a. [a] -> [a] -> [a]
++ [String -> m Doc
forall (m :: * -> *). Monad m => String -> m Doc
text String
b m Doc -> m Doc -> m Doc
forall a. Semigroup a => a -> a -> a
<> m Doc
forall (m :: * -> *). Monad m => m Doc
comma] [m Doc] -> [m Doc] -> [m Doc]
forall a. [a] -> [a] -> [a]
++
      String -> [m Doc]
forall (m :: * -> *). Monad m => String -> [m Doc]
pwords "previous binding to" [m Doc] -> [m Doc] -> [m Doc]
forall a. [a] -> [a] -> [a]
++ [QName -> m Doc
forall a (m :: * -> *). (PrettyTCM a, MonadPretty m) => a -> m Doc
prettyTCM QName
x]

    NoSuchPrimitiveFunction x :: String
x -> [m Doc] -> m Doc
forall (m :: * -> *). Monad m => [m Doc] -> m Doc
fsep ([m Doc] -> m Doc) -> [m Doc] -> m Doc
forall a b. (a -> b) -> a -> b
$
      String -> [m Doc]
forall (m :: * -> *). Monad m => String -> [m Doc]
pwords "There is no primitive function called" [m Doc] -> [m Doc] -> [m Doc]
forall a. [a] -> [a] -> [a]
++ [String -> m Doc
forall (m :: * -> *). Monad m => String -> m Doc
text String
x]

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

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

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

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

    LocalVsImportedModuleClash m :: ModuleName
m -> [m Doc] -> m Doc
forall (m :: * -> *). Monad m => [m Doc] -> m Doc
fsep ([m Doc] -> m Doc) -> [m Doc] -> m Doc
forall a b. (a -> b) -> a -> b
$
      String -> [m Doc]
forall (m :: * -> *). Monad m => String -> [m Doc]
pwords "The module" [m Doc] -> [m Doc] -> [m Doc]
forall a. [a] -> [a] -> [a]
++ [ModuleName -> m Doc
forall a (m :: * -> *). (PrettyTCM a, MonadPretty m) => a -> m Doc
prettyTCM ModuleName
m] [m Doc] -> [m Doc] -> [m Doc]
forall a. [a] -> [a] -> [a]
++
      String -> [m Doc]
forall (m :: * -> *). Monad m => String -> [m Doc]
pwords "can refer to either a local module or an imported module"

    SolvedButOpenHoles -> [m Doc] -> m Doc
forall (m :: * -> *). Monad m => [m Doc] -> m Doc
fsep ([m Doc] -> m Doc) -> [m Doc] -> m Doc
forall a b. (a -> b) -> a -> b
$
      String -> [m Doc]
forall (m :: * -> *). Monad m => String -> [m Doc]
pwords "Module cannot be imported since it has open interaction points" [m Doc] -> [m Doc] -> [m Doc]
forall a. [a] -> [a] -> [a]
++
      String -> [m Doc]
forall (m :: * -> *). Monad m => String -> [m Doc]
pwords "(consider adding {-# OPTIONS --allow-unsolved-metas #-} to this module)"

    CyclicModuleDependency ms :: [TopLevelModuleName]
ms ->
      [m Doc] -> m Doc
forall (m :: * -> *). Monad m => [m Doc] -> m Doc
fsep (String -> [m Doc]
forall (m :: * -> *). Monad m => String -> [m Doc]
pwords "cyclic module dependency:")
      m Doc -> m Doc -> m Doc
forall (m :: * -> *). Applicative m => m Doc -> m Doc -> m Doc
$$ Int -> m Doc -> m Doc
forall (m :: * -> *). Functor m => Int -> m Doc -> m Doc
nest 2 ([m Doc] -> m Doc
forall (m :: * -> *). Monad m => [m Doc] -> m Doc
vcat ([m Doc] -> m Doc) -> [m Doc] -> m Doc
forall a b. (a -> b) -> a -> b
$ (TopLevelModuleName -> m Doc) -> [TopLevelModuleName] -> [m Doc]
forall a b. (a -> b) -> [a] -> [b]
map TopLevelModuleName -> m Doc
forall (m :: * -> *) a. (Monad m, Pretty a) => a -> m Doc
pretty [TopLevelModuleName]
ms)

    FileNotFound x :: TopLevelModuleName
x files :: [AbsolutePath]
files ->
      [m Doc] -> m Doc
forall (m :: * -> *). Monad m => [m Doc] -> m Doc
fsep ( String -> [m Doc]
forall (m :: * -> *). Monad m => String -> [m Doc]
pwords "Failed to find source of module" [m Doc] -> [m Doc] -> [m Doc]
forall a. [a] -> [a] -> [a]
++ [TopLevelModuleName -> m Doc
forall (m :: * -> *) a. (Monad m, Pretty a) => a -> m Doc
pretty TopLevelModuleName
x] [m Doc] -> [m Doc] -> [m Doc]
forall a. [a] -> [a] -> [a]
++
             String -> [m Doc]
forall (m :: * -> *). Monad m => String -> [m Doc]
pwords "in any of the following locations:"
           ) m Doc -> m Doc -> m Doc
forall (m :: * -> *). Applicative m => m Doc -> m Doc -> m Doc
$$ Int -> m Doc -> m Doc
forall (m :: * -> *). Functor m => Int -> m Doc -> m Doc
nest 2 ([m Doc] -> m Doc
forall (m :: * -> *). Monad m => [m Doc] -> m Doc
vcat ([m Doc] -> m Doc) -> [m Doc] -> m Doc
forall a b. (a -> b) -> a -> b
$ (AbsolutePath -> m Doc) -> [AbsolutePath] -> [m Doc]
forall a b. (a -> b) -> [a] -> [b]
map (String -> m Doc
forall (m :: * -> *). Monad m => String -> m Doc
text (String -> m Doc)
-> (AbsolutePath -> String) -> AbsolutePath -> m Doc
forall b c a. (b -> c) -> (a -> b) -> a -> c
. AbsolutePath -> String
filePath) [AbsolutePath]
files)

    OverlappingProjects f :: AbsolutePath
f m1 :: TopLevelModuleName
m1 m2 :: TopLevelModuleName
m2 ->
      [m Doc] -> m Doc
forall (m :: * -> *). Monad m => [m Doc] -> m Doc
fsep ( String -> [m Doc]
forall (m :: * -> *). Monad m => String -> [m Doc]
pwords "The file" [m Doc] -> [m Doc] -> [m Doc]
forall a. [a] -> [a] -> [a]
++ [String -> m Doc
forall (m :: * -> *). Monad m => String -> m Doc
text (AbsolutePath -> String
filePath AbsolutePath
f)] [m Doc] -> [m Doc] -> [m Doc]
forall a. [a] -> [a] -> [a]
++
             String -> [m Doc]
forall (m :: * -> *). Monad m => String -> [m Doc]
pwords "can be accessed via several project roots. Both" [m Doc] -> [m Doc] -> [m Doc]
forall a. [a] -> [a] -> [a]
++
             [TopLevelModuleName -> m Doc
forall (m :: * -> *) a. (Monad m, Pretty a) => a -> m Doc
pretty TopLevelModuleName
m1] [m Doc] -> [m Doc] -> [m Doc]
forall a. [a] -> [a] -> [a]
++ String -> [m Doc]
forall (m :: * -> *). Monad m => String -> [m Doc]
pwords "and" [m Doc] -> [m Doc] -> [m Doc]
forall a. [a] -> [a] -> [a]
++ [TopLevelModuleName -> m Doc
forall (m :: * -> *) a. (Monad m, Pretty a) => a -> m Doc
pretty TopLevelModuleName
m2] [m Doc] -> [m Doc] -> [m Doc]
forall a. [a] -> [a] -> [a]
++
             String -> [m Doc]
forall (m :: * -> *). Monad m => String -> [m Doc]
pwords "point to this file."
           )

    AmbiguousTopLevelModuleName x :: TopLevelModuleName
x files :: [AbsolutePath]
files ->
      [m Doc] -> m Doc
forall (m :: * -> *). Monad m => [m Doc] -> m Doc
fsep ( String -> [m Doc]
forall (m :: * -> *). Monad m => String -> [m Doc]
pwords "Ambiguous module name. The module name" [m Doc] -> [m Doc] -> [m Doc]
forall a. [a] -> [a] -> [a]
++
             [TopLevelModuleName -> m Doc
forall (m :: * -> *) a. (Monad m, Pretty a) => a -> m Doc
pretty TopLevelModuleName
x] [m Doc] -> [m Doc] -> [m Doc]
forall a. [a] -> [a] -> [a]
++
             String -> [m Doc]
forall (m :: * -> *). Monad m => String -> [m Doc]
pwords "could refer to any of the following files:"
           ) m Doc -> m Doc -> m Doc
forall (m :: * -> *). Applicative m => m Doc -> m Doc -> m Doc
$$ Int -> m Doc -> m Doc
forall (m :: * -> *). Functor m => Int -> m Doc -> m Doc
nest 2 ([m Doc] -> m Doc
forall (m :: * -> *). Monad m => [m Doc] -> m Doc
vcat ([m Doc] -> m Doc) -> [m Doc] -> m Doc
forall a b. (a -> b) -> a -> b
$ (AbsolutePath -> m Doc) -> [AbsolutePath] -> [m Doc]
forall a b. (a -> b) -> [a] -> [b]
map (String -> m Doc
forall (m :: * -> *). Monad m => String -> m Doc
text (String -> m Doc)
-> (AbsolutePath -> String) -> AbsolutePath -> m Doc
forall b c a. (b -> c) -> (a -> b) -> a -> c
. AbsolutePath -> String
filePath) [AbsolutePath]
files)

    ClashingFileNamesFor x :: ModuleName
x files :: [AbsolutePath]
files ->
      [m Doc] -> m Doc
forall (m :: * -> *). Monad m => [m Doc] -> m Doc
fsep ( String -> [m Doc]
forall (m :: * -> *). Monad m => String -> [m Doc]
pwords "Multiple possible sources for module"
             [m Doc] -> [m Doc] -> [m Doc]
forall a. [a] -> [a] -> [a]
++ [ModuleName -> m Doc
forall a (m :: * -> *). (PrettyTCM a, MonadPretty m) => a -> m Doc
prettyTCM ModuleName
x] [m Doc] -> [m Doc] -> [m Doc]
forall a. [a] -> [a] -> [a]
++ String -> [m Doc]
forall (m :: * -> *). Monad m => String -> [m Doc]
pwords "found:"
           ) m Doc -> m Doc -> m Doc
forall (m :: * -> *). Applicative m => m Doc -> m Doc -> m Doc
$$ Int -> m Doc -> m Doc
forall (m :: * -> *). Functor m => Int -> m Doc -> m Doc
nest 2 ([m Doc] -> m Doc
forall (m :: * -> *). Monad m => [m Doc] -> m Doc
vcat ([m Doc] -> m Doc) -> [m Doc] -> m Doc
forall a b. (a -> b) -> a -> b
$ (AbsolutePath -> m Doc) -> [AbsolutePath] -> [m Doc]
forall a b. (a -> b) -> [a] -> [b]
map (String -> m Doc
forall (m :: * -> *). Monad m => String -> m Doc
text (String -> m Doc)
-> (AbsolutePath -> String) -> AbsolutePath -> m Doc
forall b c a. (b -> c) -> (a -> b) -> a -> c
. AbsolutePath -> String
filePath) [AbsolutePath]
files)

    ModuleDefinedInOtherFile mod :: TopLevelModuleName
mod file :: AbsolutePath
file file' :: AbsolutePath
file' -> [m Doc] -> m Doc
forall (m :: * -> *). Monad m => [m Doc] -> m Doc
fsep ([m Doc] -> m Doc) -> [m Doc] -> m Doc
forall a b. (a -> b) -> a -> b
$
      String -> [m Doc]
forall (m :: * -> *). Monad m => String -> [m Doc]
pwords "You tried to load" [m Doc] -> [m Doc] -> [m Doc]
forall a. [a] -> [a] -> [a]
++ [String -> m Doc
forall (m :: * -> *). Monad m => String -> m Doc
text (AbsolutePath -> String
filePath AbsolutePath
file)] [m Doc] -> [m Doc] -> [m Doc]
forall a. [a] -> [a] -> [a]
++
      String -> [m Doc]
forall (m :: * -> *). Monad m => String -> [m Doc]
pwords "which defines the module" [m Doc] -> [m Doc] -> [m Doc]
forall a. [a] -> [a] -> [a]
++ [TopLevelModuleName -> m Doc
forall (m :: * -> *) a. (Monad m, Pretty a) => a -> m Doc
pretty TopLevelModuleName
mod m Doc -> m Doc -> m Doc
forall a. Semigroup a => a -> a -> a
<> "."] [m Doc] -> [m Doc] -> [m Doc]
forall a. [a] -> [a] -> [a]
++
      String -> [m Doc]
forall (m :: * -> *). Monad m => String -> [m Doc]
pwords "However, according to the include path this module should" [m Doc] -> [m Doc] -> [m Doc]
forall a. [a] -> [a] -> [a]
++
      String -> [m Doc]
forall (m :: * -> *). Monad m => String -> [m Doc]
pwords "be defined in" [m Doc] -> [m Doc] -> [m Doc]
forall a. [a] -> [a] -> [a]
++ [String -> m Doc
forall (m :: * -> *). Monad m => String -> m Doc
text (AbsolutePath -> String
filePath AbsolutePath
file') m Doc -> m Doc -> m Doc
forall a. Semigroup a => a -> a -> a
<> "."]

    ModuleNameUnexpected given :: TopLevelModuleName
given expected :: TopLevelModuleName
expected -> [m Doc] -> m Doc
forall (m :: * -> *). Monad m => [m Doc] -> m Doc
fsep ([m Doc] -> m Doc) -> [m Doc] -> m Doc
forall a b. (a -> b) -> a -> b
$
      String -> [m Doc]
forall (m :: * -> *). Monad m => String -> [m Doc]
pwords "The name of the top level module does not match the file name. The module" [m Doc] -> [m Doc] -> [m Doc]
forall a. [a] -> [a] -> [a]
++
      [ TopLevelModuleName -> m Doc
forall (m :: * -> *) a. (Monad m, Pretty a) => a -> m Doc
pretty TopLevelModuleName
given ] [m Doc] -> [m Doc] -> [m Doc]
forall a. [a] -> [a] -> [a]
++
      String -> [m Doc]
forall (m :: * -> *). Monad m => String -> [m Doc]
pwords "should probably be named" [m Doc] -> [m Doc] -> [m Doc]
forall a. [a] -> [a] -> [a]
++
      [ TopLevelModuleName -> m Doc
forall (m :: * -> *) a. (Monad m, Pretty a) => a -> m Doc
pretty TopLevelModuleName
expected ]

    ModuleNameDoesntMatchFileName given :: TopLevelModuleName
given files :: [AbsolutePath]
files ->
      [m Doc] -> m Doc
forall (m :: * -> *). Monad m => [m Doc] -> m Doc
fsep (String -> [m Doc]
forall (m :: * -> *). Monad m => String -> [m Doc]
pwords "The name of the top level module does not match the file name. The module" [m Doc] -> [m Doc] -> [m Doc]
forall a. [a] -> [a] -> [a]
++
           [ TopLevelModuleName -> m Doc
forall (m :: * -> *) a. (Monad m, Pretty a) => a -> m Doc
pretty TopLevelModuleName
given ] [m Doc] -> [m Doc] -> [m Doc]
forall a. [a] -> [a] -> [a]
++ String -> [m Doc]
forall (m :: * -> *). Monad m => String -> [m Doc]
pwords "should be defined in one of the following files:")
      m Doc -> m Doc -> m Doc
forall (m :: * -> *). Applicative m => m Doc -> m Doc -> m Doc
$$ Int -> m Doc -> m Doc
forall (m :: * -> *). Functor m => Int -> m Doc -> m Doc
nest 2 ([m Doc] -> m Doc
forall (m :: * -> *). Monad m => [m Doc] -> m Doc
vcat ([m Doc] -> m Doc) -> [m Doc] -> m Doc
forall a b. (a -> b) -> a -> b
$ (AbsolutePath -> m Doc) -> [AbsolutePath] -> [m Doc]
forall a b. (a -> b) -> [a] -> [b]
map (String -> m Doc
forall (m :: * -> *). Monad m => String -> m Doc
text (String -> m Doc)
-> (AbsolutePath -> String) -> AbsolutePath -> m Doc
forall b c a. (b -> c) -> (a -> b) -> a -> c
. AbsolutePath -> String
filePath) [AbsolutePath]
files)

    BothWithAndRHS -> [m Doc] -> m Doc
forall (m :: * -> *). Monad m => [m Doc] -> m Doc
fsep ([m Doc] -> m Doc) -> [m Doc] -> m Doc
forall a b. (a -> b) -> a -> b
$ String -> [m Doc]
forall (m :: * -> *). Monad m => String -> [m Doc]
pwords "Unexpected right hand side"

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

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

    NoSuchModule x :: QName
x -> [m Doc] -> m Doc
forall (m :: * -> *). Monad m => [m Doc] -> m Doc
fsep ([m Doc] -> m Doc) -> [m Doc] -> m Doc
forall a b. (a -> b) -> a -> b
$ String -> [m Doc]
forall (m :: * -> *). Monad m => String -> [m Doc]
pwords "No module" [m Doc] -> [m Doc] -> [m Doc]
forall a. [a] -> [a] -> [a]
++ [QName -> m Doc
forall (m :: * -> *) a. (Monad m, Pretty a) => a -> m Doc
pretty QName
x] [m Doc] -> [m Doc] -> [m Doc]
forall a. [a] -> [a] -> [a]
++ String -> [m Doc]
forall (m :: * -> *). Monad m => String -> [m Doc]
pwords "in scope"

    AmbiguousName x :: QName
x ys :: NonEmpty QName
ys -> [m Doc] -> m Doc
forall (m :: * -> *). Monad m => [m Doc] -> m Doc
vcat
      [ [m Doc] -> m Doc
forall (m :: * -> *). Monad m => [m Doc] -> m Doc
fsep ([m Doc] -> m Doc) -> [m Doc] -> m Doc
forall a b. (a -> b) -> a -> b
$ String -> [m Doc]
forall (m :: * -> *). Monad m => String -> [m Doc]
pwords "Ambiguous name" [m Doc] -> [m Doc] -> [m Doc]
forall a. [a] -> [a] -> [a]
++ [QName -> m Doc
forall (m :: * -> *) a. (Monad m, Pretty a) => a -> m Doc
pretty QName
x m Doc -> m Doc -> m Doc
forall a. Semigroup a => a -> a -> a
<> "."] [m Doc] -> [m Doc] -> [m Doc]
forall a. [a] -> [a] -> [a]
++
               String -> [m Doc]
forall (m :: * -> *). Monad m => String -> [m Doc]
pwords "It could refer to any one of"
      , Int -> m Doc -> m Doc
forall (m :: * -> *). Functor m => Int -> m Doc -> m Doc
nest 2 (m Doc -> m Doc) -> m Doc -> m Doc
forall a b. (a -> b) -> a -> b
$ [m Doc] -> m Doc
forall (m :: * -> *). Monad m => [m Doc] -> m Doc
vcat ([m Doc] -> m Doc) -> [m Doc] -> m Doc
forall a b. (a -> b) -> a -> b
$ (QName -> m Doc) -> [QName] -> [m Doc]
forall a b. (a -> b) -> [a] -> [b]
map QName -> m Doc
forall (m :: * -> *). MonadPretty m => QName -> m Doc
nameWithBinding (NonEmpty QName -> [QName]
forall a. NonEmpty a -> [a]
NonEmpty.toList NonEmpty QName
ys)
      , String -> m Doc
forall (m :: * -> *). Monad m => String -> m Doc
fwords "(hint: Use C-c C-w (in Emacs) if you want to know why)"
      ]

    AmbiguousModule x :: QName
x ys :: NonEmpty ModuleName
ys -> [m Doc] -> m Doc
forall (m :: * -> *). Monad m => [m Doc] -> m Doc
vcat
      [ [m Doc] -> m Doc
forall (m :: * -> *). Monad m => [m Doc] -> m Doc
fsep ([m Doc] -> m Doc) -> [m Doc] -> m Doc
forall a b. (a -> b) -> a -> b
$ String -> [m Doc]
forall (m :: * -> *). Monad m => String -> [m Doc]
pwords "Ambiguous module name" [m Doc] -> [m Doc] -> [m Doc]
forall a. [a] -> [a] -> [a]
++ [QName -> m Doc
forall (m :: * -> *) a. (Monad m, Pretty a) => a -> m Doc
pretty QName
x m Doc -> m Doc -> m Doc
forall a. Semigroup a => a -> a -> a
<> "."] [m Doc] -> [m Doc] -> [m Doc]
forall a. [a] -> [a] -> [a]
++
               String -> [m Doc]
forall (m :: * -> *). Monad m => String -> [m Doc]
pwords "It could refer to any one of"
      , Int -> m Doc -> m Doc
forall (m :: * -> *). Functor m => Int -> m Doc -> m Doc
nest 2 (m Doc -> m Doc) -> m Doc -> m Doc
forall a b. (a -> b) -> a -> b
$ [m Doc] -> m Doc
forall (m :: * -> *). Monad m => [m Doc] -> m Doc
vcat ([m Doc] -> m Doc) -> [m Doc] -> m Doc
forall a b. (a -> b) -> a -> b
$ (ModuleName -> m Doc) -> [ModuleName] -> [m Doc]
forall a b. (a -> b) -> [a] -> [b]
map ModuleName -> m Doc
forall (m :: * -> *). MonadPretty m => ModuleName -> m Doc
help (NonEmpty ModuleName -> [ModuleName]
forall a. NonEmpty a -> [a]
NonEmpty.toList NonEmpty ModuleName
ys)
      , String -> m Doc
forall (m :: * -> *). Monad m => String -> m Doc
fwords "(hint: Use C-c C-w (in Emacs) if you want to know why)"
      ]
      where
        help :: MonadPretty m => ModuleName -> m Doc
        help :: ModuleName -> m Doc
help m :: ModuleName
m = do
          m Doc
anno <- m (Maybe DataOrRecord)
-> m (m Doc) -> (DataOrRecord -> m (m Doc)) -> m (m Doc)
forall (m :: * -> *) a b.
Monad m =>
m (Maybe a) -> m b -> (a -> m b) -> m b
caseMaybeM (ModuleName -> m (Maybe DataOrRecord)
forall (m :: * -> *).
ReadTCState m =>
ModuleName -> m (Maybe DataOrRecord)
isDatatypeModule ModuleName
m) (m Doc -> m (m Doc)
forall (m :: * -> *) a. Monad m => a -> m a
return m Doc
forall a. Null a => a
empty) ((DataOrRecord -> m (m Doc)) -> m (m Doc))
-> (DataOrRecord -> m (m Doc)) -> m (m Doc)
forall a b. (a -> b) -> a -> b
$ \case
            IsData   -> m Doc -> m (m Doc)
forall (m :: * -> *) a. Monad m => a -> m a
return (m Doc -> m (m Doc)) -> m Doc -> m (m Doc)
forall a b. (a -> b) -> a -> b
$ "(datatype module)"
            IsRecord -> m Doc -> m (m Doc)
forall (m :: * -> *) a. Monad m => a -> m a
return (m Doc -> m (m Doc)) -> m Doc -> m (m Doc)
forall a b. (a -> b) -> a -> b
$ "(record module)"
          [m Doc] -> m Doc
forall (m :: * -> *). Monad m => [m Doc] -> m Doc
sep [ModuleName -> m Doc
forall a (m :: * -> *). (PrettyTCM a, MonadPretty m) => a -> m Doc
prettyTCM ModuleName
m, m Doc
anno ]

    ClashingDefinition x :: QName
x y :: QName
y -> [m Doc] -> m Doc
forall (m :: * -> *). Monad m => [m Doc] -> m Doc
fsep ([m Doc] -> m Doc) -> [m Doc] -> m Doc
forall a b. (a -> b) -> a -> b
$
      String -> [m Doc]
forall (m :: * -> *). Monad m => String -> [m Doc]
pwords "Multiple definitions of" [m Doc] -> [m Doc] -> [m Doc]
forall a. [a] -> [a] -> [a]
++ [QName -> m Doc
forall (m :: * -> *) a. (Monad m, Pretty a) => a -> m Doc
pretty QName
x m Doc -> m Doc -> m Doc
forall a. Semigroup a => a -> a -> a
<> "."] [m Doc] -> [m Doc] -> [m Doc]
forall a. [a] -> [a] -> [a]
++
      String -> [m Doc]
forall (m :: * -> *). Monad m => String -> [m Doc]
pwords "Previous definition at"
      [m Doc] -> [m Doc] -> [m Doc]
forall a. [a] -> [a] -> [a]
++ [Range -> m Doc
forall a (m :: * -> *). (PrettyTCM a, MonadPretty m) => a -> m Doc
prettyTCM (Range -> m Doc) -> Range -> m Doc
forall a b. (a -> b) -> a -> b
$ Name -> Range
nameBindingSite (Name -> Range) -> Name -> Range
forall a b. (a -> b) -> a -> b
$ QName -> Name
qnameName QName
y]

    ClashingModule m1 :: ModuleName
m1 m2 :: ModuleName
m2 -> [m Doc] -> m Doc
forall (m :: * -> *). Monad m => [m Doc] -> m Doc
fsep ([m Doc] -> m Doc) -> [m Doc] -> m Doc
forall a b. (a -> b) -> a -> b
$
      String -> [m Doc]
forall (m :: * -> *). Monad m => String -> [m Doc]
pwords "The modules" [m Doc] -> [m Doc] -> [m Doc]
forall a. [a] -> [a] -> [a]
++ [ModuleName -> m Doc
forall a (m :: * -> *). (PrettyTCM a, MonadPretty m) => a -> m Doc
prettyTCM ModuleName
m1, "and", ModuleName -> m Doc
forall a (m :: * -> *). (PrettyTCM a, MonadPretty m) => a -> m Doc
prettyTCM ModuleName
m2]
      [m Doc] -> [m Doc] -> [m Doc]
forall a. [a] -> [a] -> [a]
++ String -> [m Doc]
forall (m :: * -> *). Monad m => String -> [m Doc]
pwords "clash."

    ClashingImport x :: Name
x y :: QName
y -> [m Doc] -> m Doc
forall (m :: * -> *). Monad m => [m Doc] -> m Doc
fsep ([m Doc] -> m Doc) -> [m Doc] -> m Doc
forall a b. (a -> b) -> a -> b
$
      String -> [m Doc]
forall (m :: * -> *). Monad m => String -> [m Doc]
pwords "Import clash between" [m Doc] -> [m Doc] -> [m Doc]
forall a. [a] -> [a] -> [a]
++ [Name -> m Doc
forall (m :: * -> *) a. (Monad m, Pretty a) => a -> m Doc
pretty Name
x, "and", QName -> m Doc
forall a (m :: * -> *). (PrettyTCM a, MonadPretty m) => a -> m Doc
prettyTCM QName
y]

    ClashingModuleImport x :: Name
x y :: ModuleName
y -> [m Doc] -> m Doc
forall (m :: * -> *). Monad m => [m Doc] -> m Doc
fsep ([m Doc] -> m Doc) -> [m Doc] -> m Doc
forall a b. (a -> b) -> a -> b
$
      String -> [m Doc]
forall (m :: * -> *). Monad m => String -> [m Doc]
pwords "Module import clash between" [m Doc] -> [m Doc] -> [m Doc]
forall a. [a] -> [a] -> [a]
++ [Name -> m Doc
forall (m :: * -> *) a. (Monad m, Pretty a) => a -> m Doc
pretty Name
x, "and", ModuleName -> m Doc
forall a (m :: * -> *). (PrettyTCM a, MonadPretty m) => a -> m Doc
prettyTCM ModuleName
y]

    PatternShadowsConstructor x :: Name
x c :: QName
c -> [m Doc] -> m Doc
forall (m :: * -> *). Monad m => [m Doc] -> m Doc
fsep ([m Doc] -> m Doc) -> [m Doc] -> m Doc
forall a b. (a -> b) -> a -> b
$
      String -> [m Doc]
forall (m :: * -> *). Monad m => String -> [m Doc]
pwords "The pattern variable" [m Doc] -> [m Doc] -> [m Doc]
forall a. [a] -> [a] -> [a]
++ [Name -> m Doc
forall a (m :: * -> *). (PrettyTCM a, MonadPretty m) => a -> m Doc
prettyTCM Name
x] [m Doc] -> [m Doc] -> [m Doc]
forall a. [a] -> [a] -> [a]
++
      String -> [m Doc]
forall (m :: * -> *). Monad m => String -> [m Doc]
pwords "has the same name as the constructor" [m Doc] -> [m Doc] -> [m Doc]
forall a. [a] -> [a] -> [a]
++ [QName -> m Doc
forall a (m :: * -> *). (PrettyTCM a, MonadPretty m) => a -> m Doc
prettyTCM QName
c]

    DuplicateImports m :: QName
m xs :: [ImportedName]
xs -> [m Doc] -> m Doc
forall (m :: * -> *). Monad m => [m Doc] -> m Doc
fsep ([m Doc] -> m Doc) -> [m Doc] -> m Doc
forall a b. (a -> b) -> a -> b
$
      String -> [m Doc]
forall (m :: * -> *). Monad m => String -> [m Doc]
pwords "Ambiguous imports from module" [m Doc] -> [m Doc] -> [m Doc]
forall a. [a] -> [a] -> [a]
++ [QName -> m Doc
forall (m :: * -> *) a. (Monad m, Pretty a) => a -> m Doc
pretty QName
m] [m Doc] -> [m Doc] -> [m Doc]
forall a. [a] -> [a] -> [a]
++ String -> [m Doc]
forall (m :: * -> *). Monad m => String -> [m Doc]
pwords "for" [m Doc] -> [m Doc] -> [m Doc]
forall a. [a] -> [a] -> [a]
++
      m Doc -> [m Doc] -> [m Doc]
forall (m :: * -> *).
(Applicative m, Semigroup (m Doc)) =>
m Doc -> [m Doc] -> [m Doc]
punctuate m Doc
forall (m :: * -> *). Monad m => m Doc
comma ((ImportedName -> m Doc) -> [ImportedName] -> [m Doc]
forall a b. (a -> b) -> [a] -> [b]
map ImportedName -> m Doc
forall (m :: * -> *) a. (Monad m, Pretty a) => a -> m Doc
pretty [ImportedName]
xs)

    NotAModuleExpr e :: Expr
e -> [m Doc] -> m Doc
forall (m :: * -> *). Monad m => [m Doc] -> m Doc
fsep ([m Doc] -> m Doc) -> [m Doc] -> m Doc
forall a b. (a -> b) -> a -> b
$
      String -> [m Doc]
forall (m :: * -> *). Monad m => String -> [m Doc]
pwords "The right-hand side of a module definition must have the form 'M e1 .. en'" [m Doc] -> [m Doc] -> [m Doc]
forall a. [a] -> [a] -> [a]
++
      String -> [m Doc]
forall (m :: * -> *). Monad m => String -> [m Doc]
pwords "where M is a module name. The expression"
      [m Doc] -> [m Doc] -> [m Doc]
forall a. [a] -> [a] -> [a]
++ [Expr -> m Doc
forall (m :: * -> *) a. (Monad m, Pretty a) => a -> m Doc
pretty Expr
e, "doesn't."]

    FieldOutsideRecord -> [m Doc] -> m Doc
forall (m :: * -> *). Monad m => [m Doc] -> m Doc
fsep ([m Doc] -> m Doc) -> [m Doc] -> m Doc
forall a b. (a -> b) -> a -> b
$
      String -> [m Doc]
forall (m :: * -> *). Monad m => String -> [m Doc]
pwords "Field appearing outside record declaration."

    InvalidPattern p :: Pattern
p -> [m Doc] -> m Doc
forall (m :: * -> *). Monad m => [m Doc] -> m Doc
fsep ([m Doc] -> m Doc) -> [m Doc] -> m Doc
forall a b. (a -> b) -> a -> b
$
      Pattern -> m Doc
forall (m :: * -> *) a. (Monad m, Pretty a) => a -> m Doc
pretty Pattern
p m Doc -> [m Doc] -> [m Doc]
forall a. a -> [a] -> [a]
: String -> [m Doc]
forall (m :: * -> *). Monad m => String -> [m Doc]
pwords "is not a valid pattern"

    RepeatedVariablesInPattern xs :: [Name]
xs -> [m Doc] -> m Doc
forall (m :: * -> *). Monad m => [m Doc] -> m Doc
fsep ([m Doc] -> m Doc) -> [m Doc] -> m Doc
forall a b. (a -> b) -> a -> b
$
      String -> [m Doc]
forall (m :: * -> *). Monad m => String -> [m Doc]
pwords "Repeated variables in pattern:" [m Doc] -> [m Doc] -> [m Doc]
forall a. [a] -> [a] -> [a]
++ (Name -> m Doc) -> [Name] -> [m Doc]
forall a b. (a -> b) -> [a] -> [b]
map Name -> m Doc
forall (m :: * -> *) a. (Monad m, Pretty a) => a -> m Doc
pretty [Name]
xs

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

    NotAValidLetBinding nd :: NiceDeclaration
nd -> String -> m Doc
forall (m :: * -> *). Monad m => String -> m Doc
fwords (String -> m Doc) -> String -> m Doc
forall a b. (a -> b) -> a -> b
$
      "Not a valid let-declaration"

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

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

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

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

    AmbiguousParseForApplication es :: [Expr]
es es' :: [Expr]
es' -> [m Doc] -> m Doc
forall (m :: * -> *). Monad m => [m Doc] -> m Doc
fsep (
      String -> [m Doc]
forall (m :: * -> *). Monad m => String -> [m Doc]
pwords "Don't know how to parse" [m Doc] -> [m Doc] -> [m Doc]
forall a. [a] -> [a] -> [a]
++ [m Doc
forall (m :: * -> *). MonadPretty m => m Doc
pretty_es m Doc -> m Doc -> m Doc
forall a. Semigroup a => a -> a -> a
<> "."] [m Doc] -> [m Doc] -> [m Doc]
forall a. [a] -> [a] -> [a]
++
      String -> [m Doc]
forall (m :: * -> *). Monad m => String -> [m Doc]
pwords "Could mean any one of:"
      ) m Doc -> m Doc -> m Doc
forall (m :: * -> *). Applicative m => m Doc -> m Doc -> m Doc
$$ Int -> m Doc -> m Doc
forall (m :: * -> *). Functor m => Int -> m Doc -> m Doc
nest 2 ([m Doc] -> m Doc
forall (m :: * -> *). Monad m => [m Doc] -> m Doc
vcat ([m Doc] -> m Doc) -> [m Doc] -> m Doc
forall a b. (a -> b) -> a -> b
$ (Expr -> m Doc) -> [Expr] -> [m Doc]
forall a b. (a -> b) -> [a] -> [b]
map Expr -> m Doc
forall (m :: * -> *). MonadPretty m => Expr -> m Doc
pretty' [Expr]
es')
      where
        pretty_es :: MonadPretty m => m Doc
        pretty_es :: m Doc
pretty_es = Expr -> m Doc
forall (m :: * -> *) a. (Monad m, Pretty a) => a -> m Doc
pretty (Expr -> m Doc) -> Expr -> m Doc
forall a b. (a -> b) -> a -> b
$ Range -> [Expr] -> Expr
C.RawApp Range
forall a. Range' a
noRange [Expr]
es

        pretty' :: MonadPretty m => C.Expr -> m Doc
        pretty' :: Expr -> m Doc
pretty' e :: Expr
e = do
          Doc
p1 <- m Doc
forall (m :: * -> *). MonadPretty m => m Doc
pretty_es
          Doc
p2 <- Expr -> m Doc
forall (m :: * -> *) a. (Monad m, Pretty a) => a -> m Doc
pretty Expr
e
          if Doc -> String
forall a. Show a => a -> String
show Doc
p1 String -> String -> Bool
forall a. Eq a => a -> a -> Bool
== Doc -> String
forall a. Show a => a -> String
show Doc
p2 then Expr -> m Doc
forall (m :: * -> *). MonadPretty m => Expr -> m Doc
unambiguous Expr
e else Expr -> m Doc
forall (m :: * -> *) a. (Monad m, Pretty a) => a -> m Doc
pretty Expr
e

        unambiguous :: MonadPretty m => C.Expr -> m Doc
        unambiguous :: Expr -> m Doc
unambiguous e :: Expr
e@(C.OpApp r :: Range
r op :: QName
op _ xs :: [NamedArg (MaybePlaceholder (OpApp Expr))]
xs)
          | (NamedArg (MaybePlaceholder (OpApp Expr)) -> Bool)
-> [NamedArg (MaybePlaceholder (OpApp Expr))] -> Bool
forall (t :: * -> *) a. Foldable t => (a -> Bool) -> t a -> Bool
all (MaybePlaceholder (OpApp Expr) -> Bool
forall e. MaybePlaceholder (OpApp e) -> Bool
isOrdinary (MaybePlaceholder (OpApp Expr) -> Bool)
-> (NamedArg (MaybePlaceholder (OpApp Expr))
    -> MaybePlaceholder (OpApp Expr))
-> NamedArg (MaybePlaceholder (OpApp Expr))
-> Bool
forall b c a. (b -> c) -> (a -> b) -> a -> c
. NamedArg (MaybePlaceholder (OpApp Expr))
-> MaybePlaceholder (OpApp Expr)
forall a. NamedArg a -> a
namedArg) [NamedArg (MaybePlaceholder (OpApp Expr))]
xs =
            Expr -> m Doc
forall (m :: * -> *) a. (Monad m, Pretty a) => a -> m Doc
pretty (Expr -> m Doc) -> Expr -> m Doc
forall a b. (a -> b) -> a -> b
$
              (Expr -> NamedArg Expr -> Expr) -> Expr -> [NamedArg Expr] -> Expr
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) ([NamedArg Expr] -> Expr) -> [NamedArg Expr] -> Expr
forall a b. (a -> b) -> a -> b
$
                ((NamedArg (MaybePlaceholder (OpApp Expr)) -> NamedArg Expr)
-> [NamedArg (MaybePlaceholder (OpApp Expr))] -> [NamedArg Expr]
forall a b. (a -> b) -> [a] -> [b]
map ((NamedArg (MaybePlaceholder (OpApp Expr)) -> NamedArg Expr)
 -> [NamedArg (MaybePlaceholder (OpApp Expr))] -> [NamedArg Expr])
-> ((MaybePlaceholder (OpApp Expr) -> Expr)
    -> NamedArg (MaybePlaceholder (OpApp Expr)) -> NamedArg Expr)
-> (MaybePlaceholder (OpApp Expr) -> Expr)
-> [NamedArg (MaybePlaceholder (OpApp Expr))]
-> [NamedArg Expr]
forall b c a. (b -> c) -> (a -> b) -> a -> c
. (Named NamedName (MaybePlaceholder (OpApp Expr))
 -> Named NamedName Expr)
-> NamedArg (MaybePlaceholder (OpApp Expr)) -> NamedArg Expr
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap ((Named NamedName (MaybePlaceholder (OpApp Expr))
  -> Named NamedName Expr)
 -> NamedArg (MaybePlaceholder (OpApp Expr)) -> NamedArg Expr)
-> ((MaybePlaceholder (OpApp Expr) -> Expr)
    -> Named NamedName (MaybePlaceholder (OpApp Expr))
    -> Named NamedName Expr)
-> (MaybePlaceholder (OpApp Expr) -> Expr)
-> NamedArg (MaybePlaceholder (OpApp Expr))
-> NamedArg Expr
forall b c a. (b -> c) -> (a -> b) -> a -> c
. (MaybePlaceholder (OpApp Expr) -> Expr)
-> Named NamedName (MaybePlaceholder (OpApp Expr))
-> Named NamedName Expr
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap) MaybePlaceholder (OpApp Expr) -> Expr
forall e. MaybePlaceholder (OpApp e) -> e
fromOrdinary [NamedArg (MaybePlaceholder (OpApp Expr))]
xs
          | (NamedArg (MaybePlaceholder (OpApp Expr)) -> Bool)
-> [NamedArg (MaybePlaceholder (OpApp Expr))] -> Bool
forall (t :: * -> *) a. Foldable t => (a -> Bool) -> t a -> Bool
any (MaybePlaceholder (OpApp Expr) -> Bool
forall a. MaybePlaceholder a -> Bool
isPlaceholder (MaybePlaceholder (OpApp Expr) -> Bool)
-> (NamedArg (MaybePlaceholder (OpApp Expr))
    -> MaybePlaceholder (OpApp Expr))
-> NamedArg (MaybePlaceholder (OpApp Expr))
-> Bool
forall b c a. (b -> c) -> (a -> b) -> a -> c
. NamedArg (MaybePlaceholder (OpApp Expr))
-> MaybePlaceholder (OpApp Expr)
forall a. NamedArg a -> a
namedArg) [NamedArg (MaybePlaceholder (OpApp Expr))]
xs =
              Expr -> m Doc
forall (m :: * -> *) a. (Monad m, Pretty a) => a -> m Doc
pretty Expr
e m Doc -> m Doc -> m Doc
forall (m :: * -> *). Applicative m => m Doc -> m Doc -> m Doc
<+> "(section)"
        unambiguous e :: Expr
e = Expr -> m Doc
forall (m :: * -> *) a. (Monad m, Pretty a) => a -> m Doc
pretty Expr
e

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

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

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

    BadArgumentsToPatternSynonym x :: AmbiguousQName
x -> [m Doc] -> m Doc
forall (m :: * -> *). Monad m => [m Doc] -> m Doc
fsep ([m Doc] -> m Doc) -> [m Doc] -> m Doc
forall a b. (a -> b) -> a -> b
$
      String -> [m Doc]
forall (m :: * -> *). Monad m => String -> [m Doc]
pwords "Bad arguments to pattern synonym " [m Doc] -> [m Doc] -> [m Doc]
forall a. [a] -> [a] -> [a]
++ [QName -> m Doc
forall a (m :: * -> *). (PrettyTCM a, MonadPretty m) => a -> m Doc
prettyTCM (QName -> m Doc) -> QName -> m Doc
forall a b. (a -> b) -> a -> b
$ AmbiguousQName -> QName
headAmbQ AmbiguousQName
x]

    TooFewArgumentsToPatternSynonym x :: AmbiguousQName
x -> [m Doc] -> m Doc
forall (m :: * -> *). Monad m => [m Doc] -> m Doc
fsep ([m Doc] -> m Doc) -> [m Doc] -> m Doc
forall a b. (a -> b) -> a -> b
$
      String -> [m Doc]
forall (m :: * -> *). Monad m => String -> [m Doc]
pwords "Too few arguments to pattern synonym " [m Doc] -> [m Doc] -> [m Doc]
forall a. [a] -> [a] -> [a]
++ [QName -> m Doc
forall a (m :: * -> *). (PrettyTCM a, MonadPretty m) => a -> m Doc
prettyTCM (QName -> m Doc) -> QName -> m Doc
forall a b. (a -> b) -> a -> b
$ AmbiguousQName -> QName
headAmbQ AmbiguousQName
x]

    CannotResolveAmbiguousPatternSynonym defs :: NonEmpty (QName, PatternSynDefn)
defs -> [m Doc] -> m Doc
forall (m :: * -> *). Monad m => [m Doc] -> m Doc
vcat
      [ [m Doc] -> m Doc
forall (m :: * -> *). Monad m => [m Doc] -> m Doc
fsep ([m Doc] -> m Doc) -> [m Doc] -> m Doc
forall a b. (a -> b) -> a -> b
$ String -> [m Doc]
forall (m :: * -> *). Monad m => String -> [m Doc]
pwords "Cannot resolve overloaded pattern synonym" [m Doc] -> [m Doc] -> [m Doc]
forall a. [a] -> [a] -> [a]
++ [QName -> m Doc
forall a (m :: * -> *). (PrettyTCM a, MonadPretty m) => a -> m Doc
prettyTCM QName
x m Doc -> m Doc -> m Doc
forall a. Semigroup a => a -> a -> a
<> m Doc
forall (m :: * -> *). Monad m => m Doc
comma] [m Doc] -> [m Doc] -> [m Doc]
forall a. [a] -> [a] -> [a]
++
               String -> [m Doc]
forall (m :: * -> *). Monad m => String -> [m Doc]
pwords "since candidates have different shapes:"
      , Int -> m Doc -> m Doc
forall (m :: * -> *). Functor m => Int -> m Doc -> m Doc
nest 2 (m Doc -> m Doc) -> m Doc -> m Doc
forall a b. (a -> b) -> a -> b
$ [m Doc] -> m Doc
forall (m :: * -> *). Monad m => [m Doc] -> m Doc
vcat ([m Doc] -> m Doc) -> [m Doc] -> m Doc
forall a b. (a -> b) -> a -> b
$ ((QName, PatternSynDefn) -> m Doc)
-> [(QName, PatternSynDefn)] -> [m Doc]
forall a b. (a -> b) -> [a] -> [b]
map (QName, PatternSynDefn) -> m Doc
forall (m :: * -> *).
(MonadTCEnv m, ReadTCState m, MonadStConcreteNames m, HasOptions m,
 HasBuiltins m, MonadDebug m, IsString (m Doc)) =>
(QName, PatternSynDefn) -> m Doc
prDef (NonEmpty (QName, PatternSynDefn) -> [(QName, PatternSynDefn)]
forall a. NonEmpty a -> [a]
NonEmpty.toList NonEmpty (QName, PatternSynDefn)
defs)
      , [m Doc] -> m Doc
forall (m :: * -> *). Monad m => [m Doc] -> m Doc
fsep ([m Doc] -> m Doc) -> [m Doc] -> m Doc
forall a b. (a -> b) -> a -> b
$ String -> [m Doc]
forall (m :: * -> *). Monad m => String -> [m Doc]
pwords "(hint: overloaded pattern synonyms must be equal up to variable and constructor names)"
      ]
      where
        (x :: QName
x, _) = NonEmpty (QName, PatternSynDefn) -> (QName, PatternSynDefn)
forall a. NonEmpty a -> a
NonEmpty.head NonEmpty (QName, PatternSynDefn)
defs
        prDef :: (QName, PatternSynDefn) -> m Doc
prDef (x :: QName
x, (xs :: [Arg Name]
xs, p :: Pattern' Void
p)) = Declaration -> m Doc
forall c a (m :: * -> *).
(Pretty c, ToConcrete a c, MonadAbsToCon m) =>
a -> m Doc
prettyA (QName -> [Arg Name] -> Pattern' Void -> Declaration
A.PatternSynDef QName
x [Arg Name]
xs Pattern' Void
p) m Doc -> m Doc -> m Doc
forall (m :: * -> *). Applicative m => m Doc -> m Doc -> m Doc
<?> ("at" m Doc -> m Doc -> m Doc
forall (m :: * -> *). Applicative m => m Doc -> m Doc -> m Doc
<+> Range -> m Doc
forall (m :: * -> *) a. (Monad m, Pretty a) => a -> m Doc
pretty Range
r)
          where r :: Range
r = Name -> Range
nameBindingSite (Name -> Range) -> Name -> Range
forall a b. (a -> b) -> a -> b
$ QName -> Name
qnameName QName
x

    UnusedVariableInPatternSynonym -> [m Doc] -> m Doc
forall (m :: * -> *). Monad m => [m Doc] -> m Doc
fsep ([m Doc] -> m Doc) -> [m Doc] -> m Doc
forall a b. (a -> b) -> a -> b
$
      String -> [m Doc]
forall (m :: * -> *). Monad m => String -> [m Doc]
pwords "Unused variable in pattern synonym."

    NoParseForLHS IsLHS p :: Pattern
p -> [m Doc] -> m Doc
forall (m :: * -> *). Monad m => [m Doc] -> m Doc
fsep (
      String -> [m Doc]
forall (m :: * -> *). Monad m => String -> [m Doc]
pwords "Could not parse the left-hand side" [m Doc] -> [m Doc] -> [m Doc]
forall a. [a] -> [a] -> [a]
++ [Pattern -> m Doc
forall (m :: * -> *) a. (Monad m, Pretty a) => a -> m Doc
pretty Pattern
p])

    NoParseForLHS IsPatSyn p :: Pattern
p -> [m Doc] -> m Doc
forall (m :: * -> *). Monad m => [m Doc] -> m Doc
fsep (
      String -> [m Doc]
forall (m :: * -> *). Monad m => String -> [m Doc]
pwords "Could not parse the pattern synonym" [m Doc] -> [m Doc] -> [m Doc]
forall a. [a] -> [a] -> [a]
++ [Pattern -> m Doc
forall (m :: * -> *) a. (Monad m, Pretty a) => a -> m Doc
pretty Pattern
p])

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

    AmbiguousParseForLHS lhsOrPatSyn :: LHSOrPatSyn
lhsOrPatSyn p :: Pattern
p ps :: [Pattern]
ps -> [m Doc] -> m Doc
forall (m :: * -> *). Monad m => [m Doc] -> m Doc
fsep (
      String -> [m Doc]
forall (m :: * -> *). Monad m => String -> [m Doc]
pwords "Don't know how to parse" [m Doc] -> [m Doc] -> [m Doc]
forall a. [a] -> [a] -> [a]
++ [m Doc
forall (m :: * -> *). MonadPretty m => m Doc
pretty_p m Doc -> m Doc -> m Doc
forall a. Semigroup a => a -> a -> a
<> "."] [m Doc] -> [m Doc] -> [m Doc]
forall a. [a] -> [a] -> [a]
++
      String -> [m Doc]
forall (m :: * -> *). Monad m => String -> [m Doc]
pwords "Could mean any one of:"
      ) m Doc -> m Doc -> m Doc
forall (m :: * -> *). Applicative m => m Doc -> m Doc -> m Doc
$$ Int -> m Doc -> m Doc
forall (m :: * -> *). Functor m => Int -> m Doc -> m Doc
nest 2 ([m Doc] -> m Doc
forall (m :: * -> *). Monad m => [m Doc] -> m Doc
vcat ([m Doc] -> m Doc) -> [m Doc] -> m Doc
forall a b. (a -> b) -> a -> b
$ (Pattern -> m Doc) -> [Pattern] -> [m Doc]
forall a b. (a -> b) -> [a] -> [b]
map Pattern -> m Doc
forall (m :: * -> *). MonadPretty m => Pattern -> m Doc
pretty' [Pattern]
ps)
      where
        pretty_p :: MonadPretty m => m Doc
        pretty_p :: m Doc
pretty_p = Pattern -> m Doc
forall (m :: * -> *) a. (Monad m, Pretty a) => a -> m Doc
pretty Pattern
p

        pretty' :: MonadPretty m => C.Pattern -> m Doc
        pretty' :: Pattern -> m Doc
pretty' p' :: Pattern
p' = do
          Doc
p1 <- m Doc
forall (m :: * -> *). MonadPretty m => m Doc
pretty_p
          Doc
p2 <- Pattern -> m Doc
forall (m :: * -> *) a. (Monad m, Pretty a) => a -> m Doc
pretty Pattern
p'
          Pattern -> m Doc
forall (m :: * -> *) a. (Monad m, Pretty a) => a -> m Doc
pretty (Pattern -> m Doc) -> Pattern -> m Doc
forall a b. (a -> b) -> a -> b
$ if Doc -> String
forall a. Show a => a -> String
show Doc
p1 String -> String -> Bool
forall a. Eq a => a -> a -> Bool
== Doc -> String
forall a. Show a => a -> String
show Doc
p2 then Pattern -> Pattern
unambiguousP Pattern
p' else Pattern
p'

        -- 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 x :: Pattern
x y :: NamedArg Pattern
y)         = Pattern -> NamedArg Pattern -> Pattern
C.AppP (Pattern -> Pattern
unambiguousP Pattern
x) (NamedArg Pattern -> Pattern) -> NamedArg Pattern -> Pattern
forall a b. (a -> b) -> a -> b
$ ((Named NamedName Pattern -> Named NamedName Pattern)
-> NamedArg Pattern -> NamedArg Pattern
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap((Named NamedName Pattern -> Named NamedName Pattern)
 -> NamedArg Pattern -> NamedArg Pattern)
-> ((Pattern -> Pattern)
    -> Named NamedName Pattern -> Named NamedName Pattern)
-> (Pattern -> Pattern)
-> NamedArg Pattern
-> NamedArg Pattern
forall b c a. (b -> c) -> (a -> b) -> a -> c
.(Pattern -> Pattern)
-> Named NamedName Pattern -> Named NamedName Pattern
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap) Pattern -> Pattern
unambiguousP NamedArg Pattern
y
        unambiguousP (C.HiddenP r :: Range
r x :: Named NamedName Pattern
x)      = Range -> Named NamedName Pattern -> Pattern
C.HiddenP Range
r (Named NamedName Pattern -> Pattern)
-> Named NamedName Pattern -> Pattern
forall a b. (a -> b) -> a -> b
$ (Pattern -> Pattern)
-> Named NamedName Pattern -> Named NamedName Pattern
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap Pattern -> Pattern
unambiguousP Named NamedName Pattern
x
        unambiguousP (C.InstanceP r :: Range
r x :: Named NamedName Pattern
x)    = Range -> Named NamedName Pattern -> Pattern
C.InstanceP Range
r (Named NamedName Pattern -> Pattern)
-> Named NamedName Pattern -> Pattern
forall a b. (a -> b) -> a -> b
$ (Pattern -> Pattern)
-> Named NamedName Pattern -> Named NamedName Pattern
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap Pattern -> Pattern
unambiguousP Named NamedName Pattern
x
        unambiguousP (C.ParenP r :: Range
r x :: Pattern
x)       = Range -> Pattern -> Pattern
C.ParenP Range
r (Pattern -> Pattern) -> Pattern -> Pattern
forall a b. (a -> b) -> a -> b
$ Pattern -> Pattern
unambiguousP Pattern
x
        unambiguousP (C.AsP r :: Range
r n :: Name
n x :: Pattern
x)        = Range -> Name -> Pattern -> Pattern
C.AsP Range
r Name
n (Pattern -> Pattern) -> Pattern -> Pattern
forall a b. (a -> b) -> a -> b
$ Pattern -> Pattern
unambiguousP Pattern
x
        unambiguousP (C.OpAppP r :: Range
r op :: QName
op _ xs :: [NamedArg Pattern]
xs) = (Pattern -> NamedArg Pattern -> Pattern)
-> Pattern -> [NamedArg Pattern] -> Pattern
forall (t :: * -> *) b a.
Foldable t =>
(b -> a -> b) -> b -> t a -> b
foldl Pattern -> NamedArg Pattern -> Pattern
C.AppP (QName -> Pattern
C.IdentP QName
op) [NamedArg Pattern]
xs
        unambiguousP e :: Pattern
e                    = Pattern
e

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

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

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

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

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

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

        (names :: [Name]
names, name :: Name
name) = case Set Name -> [Name]
forall a. Set a -> [a]
Set.toList (Set Name -> [Name]) -> Set Name -> [Name]
forall a b. (a -> b) -> a -> b
$ NewNotation -> Set Name
notaNames NewNotation
nota of
          [] -> ([Name], Name)
forall a. HasCallStack => a
__IMPOSSIBLE__
          ns :: [Name]
ns -> ([Name] -> [Name]
forall a. [a] -> [a]
init [Name]
ns, [Name] -> Name
forall a. [a] -> a
last [Name]
ns)

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

        kind :: String
kind = case NotationSection -> NotationKind
sectKind NotationSection
sect of
          PrefixNotation  -> "prefix"
          PostfixNotation -> "postfix"
          NonfixNotation  -> "closed"
          NoNotation      -> String
forall a. HasCallStack => a
__IMPOSSIBLE__
          InfixNotation   ->
            case Fixity -> Associativity
fixityAssoc (Fixity -> Associativity) -> Fixity -> Associativity
forall a b. (a -> b) -> a -> b
$ NewNotation -> Fixity
notaFixity NewNotation
nota of
              NonAssoc   -> "infix"
              LeftAssoc  -> "infixl"
              RightAssoc -> "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 e :: SplitError
e -> SplitError -> m Doc
forall a (m :: * -> *). (PrettyTCM a, MonadPretty m) => a -> m Doc
prettyTCM SplitError
e

    ImpossibleConstructor c :: QName
c neg :: NegativeUnification
neg -> [m Doc] -> m Doc
forall (m :: * -> *). Monad m => [m Doc] -> m Doc
fsep ([m Doc] -> m Doc) -> [m Doc] -> m Doc
forall a b. (a -> b) -> a -> b
$
      String -> [m Doc]
forall (m :: * -> *). Monad m => String -> [m Doc]
pwords "The case for the constructor " [m Doc] -> [m Doc] -> [m Doc]
forall a. [a] -> [a] -> [a]
++ [QName -> m Doc
forall a (m :: * -> *). (PrettyTCM a, MonadPretty m) => a -> m Doc
prettyTCM QName
c] [m Doc] -> [m Doc] -> [m Doc]
forall a. [a] -> [a] -> [a]
++
      String -> [m Doc]
forall (m :: * -> *). Monad m => String -> [m Doc]
pwords " is impossible" [m Doc] -> [m Doc] -> [m Doc]
forall a. [a] -> [a] -> [a]
++ [NegativeUnification -> m Doc
forall a (m :: * -> *). (PrettyTCM a, MonadPretty m) => a -> m Doc
prettyTCM NegativeUnification
neg] [m Doc] -> [m Doc] -> [m Doc]
forall a. [a] -> [a] -> [a]
++
      String -> [m Doc]
forall (m :: * -> *). Monad m => String -> [m Doc]
pwords "Possible solution: remove the clause, or use an absurd pattern ()."

    TooManyPolarities x :: QName
x n :: Int
n -> [m Doc] -> m Doc
forall (m :: * -> *). Monad m => [m Doc] -> m Doc
fsep ([m Doc] -> m Doc) -> [m Doc] -> m Doc
forall a b. (a -> b) -> a -> b
$
      String -> [m Doc]
forall (m :: * -> *). Monad m => String -> [m Doc]
pwords "Too many polarities given in the POLARITY pragma for" [m Doc] -> [m Doc] -> [m Doc]
forall a. [a] -> [a] -> [a]
++
      [QName -> m Doc
forall a (m :: * -> *). (PrettyTCM a, MonadPretty m) => a -> m Doc
prettyTCM QName
x] [m Doc] -> [m Doc] -> [m Doc]
forall a. [a] -> [a] -> [a]
++
      String -> [m Doc]
forall (m :: * -> *). Monad m => String -> [m Doc]
pwords "(at most" [m Doc] -> [m Doc] -> [m Doc]
forall a. [a] -> [a] -> [a]
++ [String -> m Doc
forall (m :: * -> *). Monad m => String -> m Doc
text (Int -> String
forall a. Show a => a -> String
show Int
n)] [m Doc] -> [m Doc] -> [m Doc]
forall a. [a] -> [a] -> [a]
++ String -> [m Doc]
forall (m :: * -> *). Monad m => String -> [m Doc]
pwords "allowed)."

    InstanceNoCandidate t :: Type
t errs :: [(Term, TCErr)]
errs -> [m Doc] -> m Doc
forall (m :: * -> *). Monad m => [m Doc] -> m Doc
vcat ([m Doc] -> m Doc) -> [m Doc] -> m Doc
forall a b. (a -> b) -> a -> b
$
      [ [m Doc] -> m Doc
forall (m :: * -> *). Monad m => [m Doc] -> m Doc
fsep ([m Doc] -> m Doc) -> [m Doc] -> m Doc
forall a b. (a -> b) -> a -> b
$ String -> [m Doc]
forall (m :: * -> *). Monad m => String -> [m Doc]
pwords "No instance of type" [m Doc] -> [m Doc] -> [m Doc]
forall a. [a] -> [a] -> [a]
++ [Type -> m Doc
forall a (m :: * -> *). (PrettyTCM a, MonadPretty m) => a -> m Doc
prettyTCM Type
t] [m Doc] -> [m Doc] -> [m Doc]
forall a. [a] -> [a] -> [a]
++ String -> [m Doc]
forall (m :: * -> *). Monad m => String -> [m Doc]
pwords "was found in scope."
      , [m Doc] -> m Doc
forall (m :: * -> *). Monad m => [m Doc] -> m Doc
vcat ([m Doc] -> m Doc) -> [m Doc] -> m Doc
forall a b. (a -> b) -> a -> b
$ ((Term, TCErr) -> m Doc) -> [(Term, TCErr)] -> [m Doc]
forall a b. (a -> b) -> [a] -> [b]
map (Term, TCErr) -> m Doc
forall (m :: * -> *) a a.
(MonadReduce m, MonadAddContext m, MonadInteractionPoints m,
 MonadFresh NameId m, HasConstInfo m, HasBuiltins m,
 MonadStConcreteNames 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 (term :: a
term, err :: a
err) =
          String -> m Doc
forall (m :: * -> *). Monad m => String -> m Doc
text "-" m Doc -> m Doc -> m Doc
forall (m :: * -> *). Applicative m => m Doc -> m Doc -> m Doc
<+>
            [m Doc] -> m Doc
forall (m :: * -> *). Monad m => [m Doc] -> m Doc
vcat [ a -> m Doc
forall a (m :: * -> *). (PrettyTCM a, MonadPretty m) => a -> m Doc
prettyTCM a
term m Doc -> m Doc -> m Doc
forall (m :: * -> *). Applicative m => m Doc -> m Doc -> m Doc
<?> String -> m Doc
forall (m :: * -> *). Monad m => String -> m Doc
text "was ruled out because"
                 , a -> m Doc
forall a (m :: * -> *). (PrettyTCM a, MonadPretty m) => a -> m Doc
prettyTCM a
err ]

    UnquoteFailed e :: UnquoteError
e -> case UnquoteError
e of
      BadVisibility msg :: String
msg arg :: Arg Term
arg -> [m Doc] -> m Doc
forall (m :: * -> *). Monad m => [m Doc] -> m Doc
fsep ([m Doc] -> m Doc) -> [m Doc] -> m Doc
forall a b. (a -> b) -> a -> b
$
        String -> [m Doc]
forall (m :: * -> *). Monad m => String -> [m Doc]
pwords (String -> [m Doc]) -> String -> [m Doc]
forall a b. (a -> b) -> a -> b
$ "Unable to unquote the argument. It should be `" String -> String -> String
forall a. [a] -> [a] -> [a]
++ String
msg String -> String -> String
forall a. [a] -> [a] -> [a]
++ "'."

      ConInsteadOfDef x :: QName
x def :: String
def con :: String
con -> [m Doc] -> m Doc
forall (m :: * -> *). Monad m => [m Doc] -> m Doc
fsep ([m Doc] -> m Doc) -> [m Doc] -> m Doc
forall a b. (a -> b) -> a -> b
$
        String -> [m Doc]
forall (m :: * -> *). Monad m => String -> [m Doc]
pwords ("Use " String -> String -> String
forall a. [a] -> [a] -> [a]
++ String
con String -> String -> String
forall a. [a] -> [a] -> [a]
++ " instead of " String -> String -> String
forall a. [a] -> [a] -> [a]
++ String
def String -> String -> String
forall a. [a] -> [a] -> [a]
++ " for constructor") [m Doc] -> [m Doc] -> [m Doc]
forall a. [a] -> [a] -> [a]
++
        [QName -> m Doc
forall a (m :: * -> *). (PrettyTCM a, MonadPretty m) => a -> m Doc
prettyTCM QName
x]

      DefInsteadOfCon x :: QName
x def :: String
def con :: String
con -> [m Doc] -> m Doc
forall (m :: * -> *). Monad m => [m Doc] -> m Doc
fsep ([m Doc] -> m Doc) -> [m Doc] -> m Doc
forall a b. (a -> b) -> a -> b
$
        String -> [m Doc]
forall (m :: * -> *). Monad m => String -> [m Doc]
pwords ("Use " String -> String -> String
forall a. [a] -> [a] -> [a]
++ String
def String -> String -> String
forall a. [a] -> [a] -> [a]
++ " instead of " String -> String -> String
forall a. [a] -> [a] -> [a]
++ String
con String -> String -> String
forall a. [a] -> [a] -> [a]
++ " for non-constructor")
        [m Doc] -> [m Doc] -> [m Doc]
forall a. [a] -> [a] -> [a]
++ [QName -> m Doc
forall a (m :: * -> *). (PrettyTCM a, MonadPretty m) => a -> m Doc
prettyTCM QName
x]

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

      BlockedOnMeta _ m :: MetaId
m -> [m Doc] -> m Doc
forall (m :: * -> *). Monad m => [m Doc] -> m Doc
fsep ([m Doc] -> m Doc) -> [m Doc] -> m Doc
forall a b. (a -> b) -> a -> b
$
        String -> [m Doc]
forall (m :: * -> *). Monad m => String -> [m Doc]
pwords (String -> [m Doc]) -> String -> [m Doc]
forall a b. (a -> b) -> a -> b
$ "Unquote failed because of unsolved meta variables."

      UnquotePanic err :: String
err -> m Doc
forall a. HasCallStack => a
__IMPOSSIBLE__

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

    NeedOptionCopatterns -> [m Doc] -> m Doc
forall (m :: * -> *). Monad m => [m Doc] -> m Doc
fsep ([m Doc] -> m Doc) -> [m Doc] -> m Doc
forall a b. (a -> b) -> a -> b
$
      String -> [m Doc]
forall (m :: * -> *). Monad m => String -> [m Doc]
pwords "Option --copatterns needed to enable destructor patterns"

    NeedOptionRewriting  -> [m Doc] -> m Doc
forall (m :: * -> *). Monad m => [m Doc] -> m Doc
fsep ([m Doc] -> m Doc) -> [m Doc] -> m Doc
forall a b. (a -> b) -> a -> b
$
      String -> [m Doc]
forall (m :: * -> *). Monad m => String -> [m Doc]
pwords "Option --rewriting needed to add and use rewrite rules"

    NeedOptionProp       -> [m Doc] -> m Doc
forall (m :: * -> *). Monad m => [m Doc] -> m Doc
fsep ([m Doc] -> m Doc) -> [m Doc] -> m Doc
forall a b. (a -> b) -> a -> b
$
      String -> [m Doc]
forall (m :: * -> *). Monad m => String -> [m Doc]
pwords "Universe Prop is disabled (use options --prop and --no-prop to enable/disable Prop)"

    GeneralizeNotSupportedHere x :: QName
x -> [m Doc] -> m Doc
forall (m :: * -> *). Monad m => [m Doc] -> m Doc
fsep ([m Doc] -> m Doc) -> [m Doc] -> m Doc
forall a b. (a -> b) -> a -> b
$
      String -> [m Doc]
forall (m :: * -> *). Monad m => String -> [m Doc]
pwords (String -> [m Doc]) -> String -> [m Doc]
forall a b. (a -> b) -> a -> b
$ "Generalizable variable " String -> String -> String
forall a. [a] -> [a] -> [a]
++ QName -> String
forall a. Show a => a -> String
show QName
x String -> String -> String
forall a. [a] -> [a] -> [a]
++ " is not supported here"

    GeneralizeCyclicDependency -> [m Doc] -> m Doc
forall (m :: * -> *). Monad m => [m Doc] -> m Doc
fsep ([m Doc] -> m Doc) -> [m Doc] -> m Doc
forall a b. (a -> b) -> a -> b
$
      String -> [m Doc]
forall (m :: * -> *). Monad m => String -> [m Doc]
pwords "Cyclic dependency between generalized variables"

    GeneralizeUnsolvedMeta -> [m Doc] -> m Doc
forall (m :: * -> *). Monad m => [m Doc] -> m Doc
fsep ([m Doc] -> m Doc) -> [m Doc] -> m Doc
forall a b. (a -> b) -> a -> b
$
      String -> [m Doc]
forall (m :: * -> *). Monad m => String -> [m Doc]
pwords "Unsolved meta not generalized"

    MultipleFixityDecls xs :: [(Name, [Fixity'])]
xs ->
      [m Doc] -> m Doc
forall (m :: * -> *). Monad m => [m Doc] -> m Doc
sep [ [m Doc] -> m Doc
forall (m :: * -> *). Monad m => [m Doc] -> m Doc
fsep ([m Doc] -> m Doc) -> [m Doc] -> m Doc
forall a b. (a -> b) -> a -> b
$ String -> [m Doc]
forall (m :: * -> *). Monad m => String -> [m Doc]
pwords "Multiple fixity or syntax declarations for"
          , [m Doc] -> m Doc
forall (m :: * -> *). Monad m => [m Doc] -> m Doc
vcat ([m Doc] -> m Doc) -> [m Doc] -> m Doc
forall a b. (a -> b) -> a -> b
$ ((Name, [Fixity']) -> m Doc) -> [(Name, [Fixity'])] -> [m Doc]
forall a b. (a -> b) -> [a] -> [b]
map (Name, [Fixity']) -> m Doc
forall (m :: * -> *) a a.
(Semigroup (m Doc), Monad m, IsString (m Doc), Pretty a,
 Pretty a) =>
(a, [a]) -> m Doc
f [(Name, [Fixity'])]
xs
          ]
      where
        f :: (a, [a]) -> m Doc
f (x :: a
x, fs :: [a]
fs) = (a -> m Doc
forall (m :: * -> *) a. (Monad m, Pretty a) => a -> m Doc
pretty a
x m Doc -> m Doc -> m Doc
forall a. Semigroup a => a -> a -> a
<> ": ") m Doc -> m Doc -> m Doc
forall (m :: * -> *). Applicative m => m Doc -> m Doc -> m Doc
<+> [m Doc] -> m Doc
forall (m :: * -> *). Monad m => [m Doc] -> m Doc
fsep ((a -> m Doc) -> [a] -> [m Doc]
forall a b. (a -> b) -> [a] -> [b]
map a -> m Doc
forall (m :: * -> *) a. (Monad m, Pretty a) => a -> m Doc
pretty [a]
fs)

    MultiplePolarityPragmas xs :: [Name]
xs -> [m Doc] -> m Doc
forall (m :: * -> *). Monad m => [m Doc] -> m Doc
fsep ([m Doc] -> m Doc) -> [m Doc] -> m Doc
forall a b. (a -> b) -> a -> b
$
      String -> [m Doc]
forall (m :: * -> *). Monad m => String -> [m Doc]
pwords "Multiple polarity pragmas for" [m Doc] -> [m Doc] -> [m Doc]
forall a. [a] -> [a] -> [a]
++ (Name -> m Doc) -> [Name] -> [m Doc]
forall a b. (a -> b) -> [a] -> [b]
map Name -> m Doc
forall (m :: * -> *) a. (Monad m, Pretty a) => a -> m Doc
pretty [Name]
xs

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

    InstanceSearchDepthExhausted c :: Term
c a :: Type
a d :: Int
d -> [m Doc] -> m Doc
forall (m :: * -> *). Monad m => [m Doc] -> m Doc
fsep ([m Doc] -> m Doc) -> [m Doc] -> m Doc
forall a b. (a -> b) -> a -> b
$
      String -> [m Doc]
forall (m :: * -> *). Monad m => String -> [m Doc]
pwords ("Instance search depth exhausted (max depth: " String -> String -> String
forall a. [a] -> [a] -> [a]
++ Int -> String
forall a. Show a => a -> String
show Int
d String -> String -> String
forall a. [a] -> [a] -> [a]
++ ") for candidate") [m Doc] -> [m Doc] -> [m Doc]
forall a. [a] -> [a] -> [a]
++
      [m Doc -> Int -> m Doc -> m Doc
forall (m :: * -> *).
Applicative m =>
m Doc -> Int -> m Doc -> m Doc
hang (Term -> m Doc
forall a (m :: * -> *). (PrettyTCM a, MonadPretty m) => a -> m Doc
prettyTCM Term
c m Doc -> m Doc -> m Doc
forall (m :: * -> *). Applicative m => m Doc -> m Doc -> m Doc
<+> ":") 2 (Type -> m Doc
forall a (m :: * -> *). (PrettyTCM a, MonadPretty m) => a -> m Doc
prettyTCM Type
a)]

    TriedToCopyConstrainedPrim q :: QName
q -> [m Doc] -> m Doc
forall (m :: * -> *). Monad m => [m Doc] -> m Doc
fsep ([m Doc] -> m Doc) -> [m Doc] -> m Doc
forall a b. (a -> b) -> a -> b
$
      String -> [m Doc]
forall (m :: * -> *). Monad m => String -> [m Doc]
pwords "Cannot create a module containing a copy of" [m Doc] -> [m Doc] -> [m Doc]
forall a. [a] -> [a] -> [a]
++ [QName -> m Doc
forall a (m :: * -> *). (PrettyTCM a, MonadPretty m) => a -> m Doc
prettyTCM QName
q]

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

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

    prettyPat :: MonadPretty m => Integer -> (I.Pattern' a) -> m Doc
    prettyPat :: Integer -> Pattern' a -> m Doc
prettyPat _ (I.VarP _ _) = "_"
    prettyPat _ (I.DotP _ _) = "._"
    prettyPat n :: Integer
n (I.ConP c :: ConHead
c _ args :: [NamedArg (Pattern' a)]
args) =
      Integer -> [NamedArg (Pattern' a)] -> m Doc -> m Doc
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 (m Doc -> m Doc) -> m Doc -> m Doc
forall a b. (a -> b) -> a -> b
$
        ConHead -> m Doc
forall a (m :: * -> *). (PrettyTCM a, MonadPretty m) => a -> m Doc
prettyTCM ConHead
c m Doc -> m Doc -> m Doc
forall (m :: * -> *). Applicative m => m Doc -> m Doc -> m Doc
<+> [m Doc] -> m Doc
forall (m :: * -> *). Monad m => [m Doc] -> m Doc
fsep ((NamedArg (Pattern' a) -> m Doc)
-> [NamedArg (Pattern' a)] -> [m Doc]
forall a b. (a -> b) -> [a] -> [b]
map (Arg (Pattern' a) -> m Doc
forall (m :: * -> *) a. MonadPretty m => Arg (Pattern' a) -> m Doc
prettyArg (Arg (Pattern' a) -> m Doc)
-> (NamedArg (Pattern' a) -> Arg (Pattern' a))
-> NamedArg (Pattern' a)
-> m Doc
forall b c a. (b -> c) -> (a -> b) -> a -> c
. (Named NamedName (Pattern' a) -> Pattern' a)
-> NamedArg (Pattern' a) -> Arg (Pattern' a)
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap Named NamedName (Pattern' a) -> Pattern' a
forall name a. Named name a -> a
namedThing) [NamedArg (Pattern' a)]
args)
    prettyPat n :: Integer
n (I.DefP o :: PatternInfo
o q :: QName
q args :: [NamedArg (Pattern' a)]
args) =
      Integer -> [NamedArg (Pattern' a)] -> m Doc -> m Doc
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 (m Doc -> m Doc) -> m Doc -> m Doc
forall a b. (a -> b) -> a -> b
$
        QName -> m Doc
forall a (m :: * -> *). (PrettyTCM a, MonadPretty m) => a -> m Doc
prettyTCM QName
q m Doc -> m Doc -> m Doc
forall (m :: * -> *). Applicative m => m Doc -> m Doc -> m Doc
<+> [m Doc] -> m Doc
forall (m :: * -> *). Monad m => [m Doc] -> m Doc
fsep ((NamedArg (Pattern' a) -> m Doc)
-> [NamedArg (Pattern' a)] -> [m Doc]
forall a b. (a -> b) -> [a] -> [b]
map (Arg (Pattern' a) -> m Doc
forall (m :: * -> *) a. MonadPretty m => Arg (Pattern' a) -> m Doc
prettyArg (Arg (Pattern' a) -> m Doc)
-> (NamedArg (Pattern' a) -> Arg (Pattern' a))
-> NamedArg (Pattern' a)
-> m Doc
forall b c a. (b -> c) -> (a -> b) -> a -> c
. (Named NamedName (Pattern' a) -> Pattern' a)
-> NamedArg (Pattern' a) -> Arg (Pattern' a)
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap Named NamedName (Pattern' a) -> Pattern' a
forall name a. Named name a -> a
namedThing) [NamedArg (Pattern' a)]
args)
    prettyPat _ (I.LitP _ l :: Literal
l) = Literal -> m Doc
forall a (m :: * -> *). (PrettyTCM a, MonadPretty m) => a -> m Doc
prettyTCM Literal
l
    prettyPat _ (I.ProjP _ p :: QName
p) = "." m Doc -> m Doc -> m Doc
forall a. Semigroup a => a -> a -> a
<> QName -> m Doc
forall a (m :: * -> *). (PrettyTCM a, MonadPretty m) => a -> m Doc
prettyTCM QName
p
    prettyPat _ (I.IApplyP _ _ _ _) = "_"

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

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

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

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

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

    IrrelevantDatatype t :: Closure Type
t -> Closure Type -> (Type -> m Doc) -> m Doc
forall (m :: * -> *) a c b.
(MonadTCEnv m, ReadTCState m, LensClosure a c) =>
c -> (a -> m b) -> m b
enterClosure Closure Type
t ((Type -> m Doc) -> m Doc) -> (Type -> m Doc) -> m Doc
forall a b. (a -> b) -> a -> b
$ \ t :: Type
t -> [m Doc] -> m Doc
forall (m :: * -> *). Monad m => [m Doc] -> m Doc
fsep ([m Doc] -> m Doc) -> [m Doc] -> m Doc
forall a b. (a -> b) -> a -> b
$
      String -> [m Doc]
forall (m :: * -> *). Monad m => String -> [m Doc]
pwords "Cannot split on argument of irrelevant datatype" [m Doc] -> [m Doc] -> [m Doc]
forall a. [a] -> [a] -> [a]
++ [Type -> m Doc
forall a (m :: * -> *). (PrettyTCM a, MonadPretty m) => a -> m Doc
prettyTCM Type
t]

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

    CoinductiveDatatype t :: Closure Type
t -> Closure Type -> (Type -> m Doc) -> m Doc
forall (m :: * -> *) a c b.
(MonadTCEnv m, ReadTCState m, LensClosure a c) =>
c -> (a -> m b) -> m b
enterClosure Closure Type
t ((Type -> m Doc) -> m Doc) -> (Type -> m Doc) -> m Doc
forall a b. (a -> b) -> a -> b
$ \ t :: Type
t -> [m Doc] -> m Doc
forall (m :: * -> *). Monad m => [m Doc] -> m Doc
fsep ([m Doc] -> m Doc) -> [m Doc] -> m Doc
forall a b. (a -> b) -> a -> b
$
      String -> [m Doc]
forall (m :: * -> *). Monad m => String -> [m Doc]
pwords "Cannot pattern match on the coinductive type" [m Doc] -> [m Doc] -> [m Doc]
forall a. [a] -> [a] -> [a]
++ [Type -> m Doc
forall a (m :: * -> *). (PrettyTCM a, MonadPretty m) => a -> m Doc
prettyTCM Type
t]

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

    UnificationStuck c :: QName
c tel :: Telescope
tel cIxs :: Args
cIxs gIxs :: Args
gIxs errs :: [UnificationFailure]
errs
      | Args -> Int
forall (t :: * -> *) a. Foldable t => t a -> Int
length Args
cIxs Int -> Int -> Bool
forall a. Eq a => a -> a -> Bool
/= Args -> Int
forall (t :: * -> *) a. Foldable t => t a -> Int
length Args
gIxs -> m Doc
forall a. HasCallStack => a
__IMPOSSIBLE__
      | Bool
otherwise                  -> [m Doc] -> m Doc
forall (m :: * -> *). Monad m => [m Doc] -> m Doc
vcat ([m Doc] -> m Doc) -> ([[m Doc]] -> [m Doc]) -> [[m Doc]] -> m Doc
forall b c a. (b -> c) -> (a -> b) -> a -> c
. [[m Doc]] -> [m Doc]
forall (t :: * -> *) a. Foldable t => t [a] -> [a]
concat ([[m Doc]] -> m Doc) -> [[m Doc]] -> m Doc
forall a b. (a -> b) -> a -> b
$
        [ [ [m Doc] -> m Doc
forall (m :: * -> *). Monad m => [m Doc] -> m Doc
fsep ([m Doc] -> m Doc) -> ([[m Doc]] -> [m Doc]) -> [[m Doc]] -> m Doc
forall b c a. (b -> c) -> (a -> b) -> a -> c
. [[m Doc]] -> [m Doc]
forall (t :: * -> *) a. Foldable t => t [a] -> [a]
concat ([[m Doc]] -> m Doc) -> [[m Doc]] -> m Doc
forall a b. (a -> b) -> a -> b
$
            [ String -> [m Doc]
forall (m :: * -> *). Monad m => String -> [m Doc]
pwords "I'm not sure if there should be a case for the constructor"
            , [QName -> m Doc
forall a (m :: * -> *). (PrettyTCM a, MonadPretty m) => a -> m Doc
prettyTCM QName
c m Doc -> m Doc -> m Doc
forall a. Semigroup a => a -> a -> a
<> ","]
            , String -> [m Doc]
forall (m :: * -> *). Monad m => String -> [m Doc]
pwords "because I get stuck when trying to solve the following"
            , String -> [m Doc]
forall (m :: * -> *). Monad m => String -> [m Doc]
pwords "unification problems (inferred index ≟ expected index):"
            ]
          ]
        , (Arg Term -> Arg Term -> m Doc) -> Args -> Args -> [m Doc]
forall a b c. (a -> b -> c) -> [a] -> [b] -> [c]
zipWith Arg Term -> Arg Term -> m Doc
forall (m :: * -> *) a a.
(MonadAddContext m, MonadReduce m, MonadInteractionPoints m,
 MonadFresh NameId m, HasConstInfo m, HasBuiltins m,
 MonadStConcreteNames m, IsString (m Doc), Null (m Doc),
 Semigroup (m Doc), PrettyTCM a, PrettyTCM a) =>
Arg a -> Arg a -> m Doc
prEq Args
cIxs Args
gIxs
        , if [UnificationFailure] -> Bool
forall a. Null a => a -> Bool
null [UnificationFailure]
errs then [] else
            [ [m Doc] -> m Doc
forall (m :: * -> *). Monad m => [m Doc] -> m Doc
fsep ([m Doc] -> m Doc) -> [m Doc] -> m Doc
forall a b. (a -> b) -> a -> b
$ String -> [m Doc]
forall (m :: * -> *). Monad m => String -> [m Doc]
pwords "Possible" [m Doc] -> [m Doc] -> [m Doc]
forall a. [a] -> [a] -> [a]
++ String -> [m Doc]
forall (m :: * -> *). Monad m => String -> [m Doc]
pwords ([UnificationFailure] -> String -> String -> String
forall a c. Sized a => a -> c -> c -> c
P.singPlural [UnificationFailure]
errs "reason" "reasons") [m Doc] -> [m Doc] -> [m Doc]
forall a. [a] -> [a] -> [a]
++
                     String -> [m Doc]
forall (m :: * -> *). Monad m => String -> [m Doc]
pwords "why unification failed:" ] [m Doc] -> [m Doc] -> [m Doc]
forall a. [a] -> [a] -> [a]
++
            (UnificationFailure -> m Doc) -> [UnificationFailure] -> [m Doc]
forall a b. (a -> b) -> [a] -> [b]
map (Int -> m Doc -> m Doc
forall (m :: * -> *). Functor m => Int -> m Doc -> m Doc
nest 2 (m Doc -> m Doc)
-> (UnificationFailure -> m Doc) -> UnificationFailure -> m Doc
forall b c a. (b -> c) -> (a -> b) -> a -> c
. UnificationFailure -> m Doc
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 a -> Arg a -> m Doc
prEq cIx :: Arg a
cIx gIx :: Arg a
gIx = Telescope -> m Doc -> m Doc
forall b (m :: * -> *) a.
(AddContext b, MonadAddContext m) =>
b -> m a -> m a
addContext Telescope
tel (m Doc -> m Doc) -> m Doc -> m Doc
forall a b. (a -> b) -> a -> b
$ Int -> m Doc -> m Doc
forall (m :: * -> *). Functor m => Int -> m Doc -> m Doc
nest 2 (m Doc -> m Doc) -> m Doc -> m Doc
forall a b. (a -> b) -> a -> b
$ [m Doc] -> m Doc
forall (m :: * -> *). Monad m => [m Doc] -> m Doc
hsep [ Arg a -> m Doc
forall (f :: * -> *) a.
(PrettyTCM a, MonadReduce f, MonadAddContext f,
 MonadInteractionPoints f, MonadFresh NameId f, HasConstInfo f,
 HasBuiltins f, MonadStConcreteNames f, IsString (f Doc),
 Null (f Doc), Semigroup (f Doc)) =>
Arg a -> f Doc
pr Arg a
cIx , "≟" , Arg a -> m Doc
forall (f :: * -> *) a.
(PrettyTCM a, MonadReduce f, MonadAddContext f,
 MonadInteractionPoints f, MonadFresh NameId f, HasConstInfo f,
 HasBuiltins f, MonadStConcreteNames f, IsString (f Doc),
 Null (f Doc), Semigroup (f Doc)) =>
Arg a -> f Doc
pr Arg a
gIx ]
        pr :: Arg a -> f Doc
pr arg :: Arg a
arg = Arg a -> Doc -> Doc
forall a. LensRelevance a => a -> Doc -> Doc
prettyRelevance Arg a
arg (Doc -> Doc) -> (Doc -> Doc) -> Doc -> Doc
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Arg a -> (Doc -> Doc) -> Doc -> Doc
forall a. LensHiding a => a -> (Doc -> Doc) -> Doc -> Doc
prettyHiding Arg a
arg Doc -> Doc
forall a. a -> a
id (Doc -> Doc) -> f Doc -> f Doc
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> a -> f Doc
forall a (m :: * -> *). (PrettyTCM a, MonadPretty m) => a -> m Doc
prettyTCM (Arg a -> a
forall e. Arg e -> e
unArg Arg a
arg)

    CosplitCatchall -> [m Doc] -> m Doc
forall (m :: * -> *). Monad m => [m Doc] -> m Doc
fsep ([m Doc] -> m Doc) -> [m Doc] -> m Doc
forall a b. (a -> b) -> a -> b
$
      String -> [m Doc]
forall (m :: * -> *). Monad m => String -> [m Doc]
pwords "Cannot split into projections because not all clauses have a projection copattern"

    CosplitNoTarget -> [m Doc] -> m Doc
forall (m :: * -> *). Monad m => [m Doc] -> m Doc
fsep ([m Doc] -> m Doc) -> [m Doc] -> m Doc
forall a b. (a -> b) -> a -> b
$
      String -> [m Doc]
forall (m :: * -> *). Monad m => String -> [m Doc]
pwords "Cannot split into projections because target type is unknown"

    CosplitNoRecordType t :: Closure Type
t -> Closure Type -> (Type -> m Doc) -> m Doc
forall (m :: * -> *) a c b.
(MonadTCEnv m, ReadTCState m, LensClosure a c) =>
c -> (a -> m b) -> m b
enterClosure Closure Type
t ((Type -> m Doc) -> m Doc) -> (Type -> m Doc) -> m Doc
forall a b. (a -> b) -> a -> b
$ \t :: Type
t -> [m Doc] -> m Doc
forall (m :: * -> *). Monad m => [m Doc] -> m Doc
fsep ([m Doc] -> m Doc) -> [m Doc] -> m Doc
forall a b. (a -> b) -> a -> b
$
      String -> [m Doc]
forall (m :: * -> *). Monad m => String -> [m Doc]
pwords "Cannot split into projections because the target type "
      [m Doc] -> [m Doc] -> [m Doc]
forall a. [a] -> [a] -> [a]
++ [Type -> m Doc
forall a (m :: * -> *). (PrettyTCM a, MonadPretty m) => a -> m Doc
prettyTCM Type
t] [m Doc] -> [m Doc] -> [m Doc]
forall a. [a] -> [a] -> [a]
++ String -> [m Doc]
forall (m :: * -> *). Monad m => String -> [m Doc]
pwords " is not a record type"

    CannotCreateMissingClause f :: QName
f cl :: (Telescope, [NamedArg DeBruijnPattern])
cl msg :: Doc
msg t :: Closure (Abs Type)
t -> [m Doc] -> m Doc
forall (m :: * -> *). Monad m => [m Doc] -> m Doc
fsep (
      String -> [m Doc]
forall (m :: * -> *). Monad m => String -> [m Doc]
pwords "Cannot generate inferred clause for" [m Doc] -> [m Doc] -> [m Doc]
forall a. [a] -> [a] -> [a]
++ [QName -> m Doc
forall a (m :: * -> *). (PrettyTCM a, MonadPretty m) => a -> m Doc
prettyTCM QName
f m Doc -> m Doc -> m Doc
forall a. Semigroup a => a -> a -> a
<> "."] [m Doc] -> [m Doc] -> [m Doc]
forall a. [a] -> [a] -> [a]
++
      String -> [m Doc]
forall (m :: * -> *). Monad m => String -> [m Doc]
pwords "Case to handle:") m Doc -> m Doc -> m Doc
forall (m :: * -> *). Applicative m => m Doc -> m Doc -> m Doc
$$ Int -> m Doc -> m Doc
forall (m :: * -> *). Functor m => Int -> m Doc -> m Doc
nest 2 ([m Doc] -> m Doc
forall (m :: * -> *). Monad m => [m Doc] -> m Doc
vcat ([m Doc] -> m Doc) -> [m Doc] -> m Doc
forall a b. (a -> b) -> a -> b
$ [(Telescope, [NamedArg DeBruijnPattern]) -> m Doc
forall (m :: * -> *).
(MonadReduce m, MonadAddContext m, MonadInteractionPoints m,
 MonadFresh NameId m, HasConstInfo m, HasBuiltins m,
 MonadStConcreteNames m, IsString (m Doc), Null (m Doc),
 Semigroup (m Doc)) =>
(Telescope, [NamedArg DeBruijnPattern]) -> m Doc
display (Telescope, [NamedArg DeBruijnPattern])
cl])
                                m Doc -> m Doc -> m Doc
forall (m :: * -> *). Applicative m => m Doc -> m Doc -> m Doc
$$ ((Doc -> m Doc
forall (f :: * -> *) a. Applicative f => a -> f a
pure Doc
msg m Doc -> m Doc -> m Doc
forall (m :: * -> *). Applicative m => m Doc -> m Doc -> m Doc
<+> Closure (Abs Type) -> (Abs Type -> 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
forall (m :: * -> *) a.
(MonadAddContext m, PrettyTCM a, MonadReduce m,
 MonadInteractionPoints m, MonadFresh NameId m, HasConstInfo m,
 HasBuiltins m, MonadStConcreteNames m, IsString (m Doc),
 Null (m Doc), Semigroup (m Doc)) =>
Abs a -> m Doc
displayAbs) m Doc -> m Doc -> m Doc
forall a. Semigroup a => a -> a -> a
<> ".")
        where
        displayAbs :: Abs a -> m Doc
displayAbs (Abs x :: String
x t :: a
t) = String -> m Doc -> m Doc
forall b (m :: * -> *) a.
(AddContext b, MonadAddContext m) =>
b -> m a -> m a
addContext String
x (m Doc -> m Doc) -> m Doc -> m Doc
forall a b. (a -> b) -> a -> b
$ a -> m Doc
forall a (m :: * -> *). (PrettyTCM a, MonadPretty m) => a -> m Doc
prettyTCM a
t
        displayAbs (NoAbs x :: String
x t :: a
t) = a -> m Doc
forall a (m :: * -> *). (PrettyTCM a, MonadPretty m) => a -> m Doc
prettyTCM a
t
        display :: (Telescope, [NamedArg DeBruijnPattern]) -> m Doc
display (tel :: Telescope
tel, ps :: [NamedArg DeBruijnPattern]
ps) = NamedClause -> m Doc
forall a (m :: * -> *). (PrettyTCM a, MonadPretty m) => a -> m Doc
prettyTCM (NamedClause -> m Doc) -> NamedClause -> m Doc
forall a b. (a -> b) -> a -> b
$ QName -> Bool -> Clause -> NamedClause
NamedClause QName
f Bool
True (Clause -> NamedClause) -> Clause -> NamedClause
forall a b. (a -> b) -> a -> b
$
          Clause
forall a. Null a => a
empty { clauseTel :: Telescope
clauseTel = Telescope
tel, namedClausePats :: [NamedArg DeBruijnPattern]
namedClausePats = [NamedArg DeBruijnPattern]
ps }


    GenericSplitError s :: String
s -> [m Doc] -> m Doc
forall (m :: * -> *). Monad m => [m Doc] -> m Doc
fsep ([m Doc] -> m Doc) -> [m Doc] -> m Doc
forall a b. (a -> b) -> a -> b
$ String -> [m Doc]
forall (m :: * -> *). Monad m => String -> [m Doc]
pwords "Split failed:" [m Doc] -> [m Doc] -> [m Doc]
forall a. [a] -> [a] -> [a]
++ String -> [m Doc]
forall (m :: * -> *). Monad m => String -> [m Doc]
pwords String
s

instance PrettyTCM NegativeUnification where
  prettyTCM :: NegativeUnification -> m Doc
prettyTCM err :: NegativeUnification
err = case NegativeUnification
err of
    UnifyConflict tel :: Telescope
tel u :: Term
u v :: Term
v -> Telescope -> m Doc -> m Doc
forall b (m :: * -> *) a.
(AddContext b, MonadAddContext m) =>
b -> m a -> m a
addContext Telescope
tel (m Doc -> m Doc) -> m Doc -> m Doc
forall a b. (a -> b) -> a -> b
$ [m Doc] -> m Doc
forall (m :: * -> *). Monad m => [m Doc] -> m Doc
vcat ([m Doc] -> m Doc) -> [m Doc] -> m Doc
forall a b. (a -> b) -> a -> b
$
      [ [m Doc] -> m Doc
forall (m :: * -> *). Monad m => [m Doc] -> m Doc
fsep ([m Doc] -> m Doc) -> [m Doc] -> m Doc
forall a b. (a -> b) -> a -> b
$ String -> [m Doc]
forall (m :: * -> *). Monad m => String -> [m Doc]
pwords "because unification ended with a conflicting equation "
      , Int -> m Doc -> m Doc
forall (m :: * -> *). Functor m => Int -> m Doc -> m Doc
nest 2 (m Doc -> m Doc) -> m Doc -> m Doc
forall a b. (a -> b) -> a -> b
$ Term -> m Doc
forall a (m :: * -> *). (PrettyTCM a, MonadPretty m) => a -> m Doc
prettyTCM Term
u m Doc -> m Doc -> m Doc
forall (m :: * -> *). Applicative m => m Doc -> m Doc -> m Doc
<+> "≟" m Doc -> m Doc -> m Doc
forall (m :: * -> *). Applicative m => m Doc -> m Doc -> m Doc
<+> Term -> m Doc
forall a (m :: * -> *). (PrettyTCM a, MonadPretty m) => a -> m Doc
prettyTCM Term
v
      ]

    UnifyCycle tel :: Telescope
tel i :: Int
i u :: Term
u -> Telescope -> m Doc -> m Doc
forall b (m :: * -> *) a.
(AddContext b, MonadAddContext m) =>
b -> m a -> m a
addContext Telescope
tel (m Doc -> m Doc) -> m Doc -> m Doc
forall a b. (a -> b) -> a -> b
$ [m Doc] -> m Doc
forall (m :: * -> *). Monad m => [m Doc] -> m Doc
vcat ([m Doc] -> m Doc) -> [m Doc] -> m Doc
forall a b. (a -> b) -> a -> b
$
      [ [m Doc] -> m Doc
forall (m :: * -> *). Monad m => [m Doc] -> m Doc
fsep ([m Doc] -> m Doc) -> [m Doc] -> m Doc
forall a b. (a -> b) -> a -> b
$ String -> [m Doc]
forall (m :: * -> *). Monad m => String -> [m Doc]
pwords "because unification ended with a cyclic equation "
      , Int -> m Doc -> m Doc
forall (m :: * -> *). Functor m => Int -> m Doc -> m Doc
nest 2 (m Doc -> m Doc) -> m Doc -> m Doc
forall a b. (a -> b) -> a -> b
$ Term -> m Doc
forall a (m :: * -> *). (PrettyTCM a, MonadPretty m) => a -> m Doc
prettyTCM (Int -> Term
var Int
i) m Doc -> m Doc -> m Doc
forall (m :: * -> *). Applicative m => m Doc -> m Doc -> m Doc
<+> "≟" m Doc -> m Doc -> m Doc
forall (m :: * -> *). Applicative m => m Doc -> m Doc -> m Doc
<+> Term -> m Doc
forall a (m :: * -> *). (PrettyTCM a, MonadPretty m) => a -> m Doc
prettyTCM Term
u
      ]

instance PrettyTCM UnificationFailure where
  prettyTCM :: UnificationFailure -> m Doc
prettyTCM err :: UnificationFailure
err = case UnificationFailure
err of
    UnifyIndicesNotVars tel :: Telescope
tel a :: Type
a u :: Term
u v :: Term
v ixs :: Args
ixs -> Telescope -> m Doc -> m Doc
forall b (m :: * -> *) a.
(AddContext b, MonadAddContext m) =>
b -> m a -> m a
addContext Telescope
tel (m Doc -> m Doc) -> m Doc -> m Doc
forall a b. (a -> b) -> a -> b
$ [m Doc] -> m Doc
forall (m :: * -> *). Monad m => [m Doc] -> m Doc
fsep ([m Doc] -> m Doc) -> [m Doc] -> m Doc
forall a b. (a -> b) -> a -> b
$
      String -> [m Doc]
forall (m :: * -> *). Monad m => String -> [m Doc]
pwords "Cannot apply injectivity to the equation" [m Doc] -> [m Doc] -> [m Doc]
forall a. [a] -> [a] -> [a]
++ [Term -> m Doc
forall a (m :: * -> *). (PrettyTCM a, MonadPretty m) => a -> m Doc
prettyTCM Term
u] [m Doc] -> [m Doc] -> [m Doc]
forall a. [a] -> [a] -> [a]
++
      String -> [m Doc]
forall (m :: * -> *). Monad m => String -> [m Doc]
pwords "=" [m Doc] -> [m Doc] -> [m Doc]
forall a. [a] -> [a] -> [a]
++ [Term -> m Doc
forall a (m :: * -> *). (PrettyTCM a, MonadPretty m) => a -> m Doc
prettyTCM Term
v] [m Doc] -> [m Doc] -> [m Doc]
forall a. [a] -> [a] -> [a]
++ String -> [m Doc]
forall (m :: * -> *). Monad m => String -> [m Doc]
pwords "of type" [m Doc] -> [m Doc] -> [m Doc]
forall a. [a] -> [a] -> [a]
++ [Type -> m Doc
forall a (m :: * -> *). (PrettyTCM a, MonadPretty m) => a -> m Doc
prettyTCM Type
a] [m Doc] -> [m Doc] -> [m Doc]
forall a. [a] -> [a] -> [a]
++
      String -> [m Doc]
forall (m :: * -> *). Monad m => String -> [m Doc]
pwords "because I cannot generalize over the indices" [m Doc] -> [m Doc] -> [m Doc]
forall a. [a] -> [a] -> [a]
++
      [[m Doc] -> m Doc
forall (m :: * -> *).
(Monad m, Semigroup (m Doc)) =>
[m Doc] -> m Doc
prettyList ((Arg Term -> m Doc) -> Args -> [m Doc]
forall a b. (a -> b) -> [a] -> [b]
map Arg Term -> m Doc
forall a (m :: * -> *). (PrettyTCM a, MonadPretty m) => a -> m Doc
prettyTCM Args
ixs) m Doc -> m Doc -> m Doc
forall a. Semigroup a => a -> a -> a
<> "."]

    UnifyRecursiveEq tel :: Telescope
tel a :: Type
a i :: Int
i u :: Term
u -> Telescope -> m Doc -> m Doc
forall b (m :: * -> *) a.
(AddContext b, MonadAddContext m) =>
b -> m a -> m a
addContext Telescope
tel (m Doc -> m Doc) -> m Doc -> m Doc
forall a b. (a -> b) -> a -> b
$ [m Doc] -> m Doc
forall (m :: * -> *). Monad m => [m Doc] -> m Doc
fsep ([m Doc] -> m Doc) -> [m Doc] -> m Doc
forall a b. (a -> b) -> a -> b
$
      String -> [m Doc]
forall (m :: * -> *). Monad m => String -> [m Doc]
pwords "Cannot solve variable " [m Doc] -> [m Doc] -> [m Doc]
forall a. [a] -> [a] -> [a]
++ [Term -> m Doc
forall a (m :: * -> *). (PrettyTCM a, MonadPretty m) => a -> m Doc
prettyTCM (Int -> Term
var Int
i)] [m Doc] -> [m Doc] -> [m Doc]
forall a. [a] -> [a] -> [a]
++
      String -> [m Doc]
forall (m :: * -> *). Monad m => String -> [m Doc]
pwords " of type " [m Doc] -> [m Doc] -> [m Doc]
forall a. [a] -> [a] -> [a]
++ [Type -> m Doc
forall a (m :: * -> *). (PrettyTCM a, MonadPretty m) => a -> m Doc
prettyTCM Type
a] [m Doc] -> [m Doc] -> [m Doc]
forall a. [a] -> [a] -> [a]
++
      String -> [m Doc]
forall (m :: * -> *). Monad m => String -> [m Doc]
pwords " with solution " [m Doc] -> [m Doc] -> [m Doc]
forall a. [a] -> [a] -> [a]
++ [Term -> m Doc
forall a (m :: * -> *). (PrettyTCM a, MonadPretty m) => a -> m Doc
prettyTCM Term
u] [m Doc] -> [m Doc] -> [m Doc]
forall a. [a] -> [a] -> [a]
++
      String -> [m Doc]
forall (m :: * -> *). Monad m => String -> [m Doc]
pwords " because the variable occurs in the solution," [m Doc] -> [m Doc] -> [m Doc]
forall a. [a] -> [a] -> [a]
++
      String -> [m Doc]
forall (m :: * -> *). Monad m => String -> [m Doc]
pwords " or in the type of one of the variables in the solution."

    UnifyReflexiveEq tel :: Telescope
tel a :: Type
a u :: Term
u -> Telescope -> m Doc -> m Doc
forall b (m :: * -> *) a.
(AddContext b, MonadAddContext m) =>
b -> m a -> m a
addContext Telescope
tel (m Doc -> m Doc) -> m Doc -> m Doc
forall a b. (a -> b) -> a -> b
$ [m Doc] -> m Doc
forall (m :: * -> *). Monad m => [m Doc] -> m Doc
fsep ([m Doc] -> m Doc) -> [m Doc] -> m Doc
forall a b. (a -> b) -> a -> b
$
      String -> [m Doc]
forall (m :: * -> *). Monad m => String -> [m Doc]
pwords "Cannot eliminate reflexive equation" [m Doc] -> [m Doc] -> [m Doc]
forall a. [a] -> [a] -> [a]
++ [Term -> m Doc
forall a (m :: * -> *). (PrettyTCM a, MonadPretty m) => a -> m Doc
prettyTCM Term
u] [m Doc] -> [m Doc] -> [m Doc]
forall a. [a] -> [a] -> [a]
++
      String -> [m Doc]
forall (m :: * -> *). Monad m => String -> [m Doc]
pwords "=" [m Doc] -> [m Doc] -> [m Doc]
forall a. [a] -> [a] -> [a]
++ [Term -> m Doc
forall a (m :: * -> *). (PrettyTCM a, MonadPretty m) => a -> m Doc
prettyTCM Term
u] [m Doc] -> [m Doc] -> [m Doc]
forall a. [a] -> [a] -> [a]
++ String -> [m Doc]
forall (m :: * -> *). Monad m => String -> [m Doc]
pwords "of type" [m Doc] -> [m Doc] -> [m Doc]
forall a. [a] -> [a] -> [a]
++ [Type -> m Doc
forall a (m :: * -> *). (PrettyTCM a, MonadPretty m) => a -> m Doc
prettyTCM Type
a] [m Doc] -> [m Doc] -> [m Doc]
forall a. [a] -> [a] -> [a]
++
      String -> [m Doc]
forall (m :: * -> *). Monad m => String -> [m Doc]
pwords "because K has been disabled."

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


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

class Verbalize a where
  verbalize :: a -> String

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

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

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

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

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

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