{-# LANGUAGE NondecreasingIndentation #-}

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

module Mikan.TypeChecking.Errors
  ( renderError
  , prettyError
  , prettyShadowedModule
  , tcErrString
  , prettyTCWarnings'
  , prettyTCWarnings
  , tcWarningsToError
  , applyFlagsToTCWarningsPreserving
  , applyFlagsToTCWarnings
  , getAllUnsolvedWarnings
  , getAllWarningsPreserving
  , getAllWarnings
  , getAllWarningsOfTCErr
  , dropTopLevelModule
  , topLevelModuleDropper
  , explainWhyInScope
  , Verbalize(verbalize), Indefinite(..), Ordinal(..)
  , module Mikan.TypeChecking.Monad.Diagnostic
  ) where

import Prelude hiding ( null, foldl )

import Data.Text.Short (ShortText)
import Data.Text.Short qualified as TS

import Control.Exception qualified as E
import Control.Monad ((>=>), (<=<))
import Control.Monad.Except

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

import Mikan.Interaction.Options
import Mikan.Interaction.Options.Errors

import Mikan.Syntax.Common
import Mikan.Syntax.Common.Pretty ( prettyShow, render )
import Mikan.Syntax.Common.Pretty qualified as P
import Mikan.Syntax.Concrete.Definitions (notSoNiceDeclarations, NiceDeclaration (NiceDataDef, NiceRecDef))
import Mikan.Syntax.Notation
import Mikan.Syntax.Parser (agdaFileExtensions)
import Mikan.Syntax.Position
import Mikan.Syntax.Concrete qualified as C
import Mikan.Syntax.Abstract as A
import Mikan.Syntax.Internal as I
import Mikan.Syntax.Translation.InternalToAbstract
import Mikan.Syntax.Scope.Monad (isDatatypeModule, resolveName', tryResolveName)
import Mikan.Syntax.Scope.Base
import Mikan.Syntax.TopLevelModuleName (moduleNameToFileName)

import Mikan.TypeChecking.Errors.Names (typeErrorString)
import Mikan.TypeChecking.Monad.Diagnostic
import Mikan.TypeChecking.Monad
import Mikan.TypeChecking.Pretty
import Mikan.TypeChecking.Pretty.Call
import Mikan.TypeChecking.Pretty.Warning
import Mikan.TypeChecking.Substitute
import Mikan.TypeChecking.Reduce (instantiate)

import Mikan.Interaction.Library.Base (formatLibErrors, libFile)

import Mikan.Utils.AssocList qualified as AssocList
import Mikan.Utils.CallStack ( showIOException )
import Mikan.Utils.FileName
import Mikan.Utils.Float     ( toStringWithoutDotZero )
import Mikan.Utils.Function
import Mikan.Utils.Lens
import Mikan.Utils.List      ( initLast, lastMaybe, hasElem )
import Mikan.Utils.List1     ( List1, pattern (:|) )
import Mikan.Utils.List2     ( pattern List2 )
import Mikan.Utils.List1     qualified as List1
import Mikan.Utils.List2     qualified as List2
import Mikan.Utils.Maybe
import Mikan.Utils.Monad
import Mikan.Utils.Null
import Mikan.Utils.Set1      qualified as Set1
import Mikan.Utils.Singleton
import Mikan.Utils.Size
import Mikan.Utils.String    ( rtrim )

import Mikan.Utils.Impossible
import Mikan.TypeChecking.Conversion.Errors

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

{-# SPECIALIZE renderError :: TCErr -> TCM String #-}
renderError :: MonadTCM tcm => TCErr -> tcm String
renderError :: forall (tcm :: * -> *). MonadTCM tcm => TCErr -> tcm String
renderError = (Doc -> String) -> tcm Doc -> tcm String
forall a b. (a -> b) -> tcm a -> tcm b
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap Doc -> String
forall a. Show a => a -> String
show (tcm Doc -> tcm String)
-> (TCErr -> tcm Doc) -> TCErr -> tcm String
forall b c a. (b -> c) -> (a -> b) -> a -> c
. TCErr -> tcm Doc
forall (tcm :: * -> *). MonadTCM tcm => TCErr -> tcm Doc
prettyError

{-# SPECIALIZE prettyError :: TCErr -> TCM Doc #-}
prettyError :: MonadTCM tcm => TCErr -> tcm Doc
prettyError :: forall (tcm :: * -> *). MonadTCM tcm => TCErr -> tcm Doc
prettyError = TCMT IO Doc -> tcm Doc
forall a. TCM a -> tcm a
forall (tcm :: * -> *) a. MonadTCM tcm => TCM a -> tcm a
liftTCM (TCMT IO Doc -> tcm Doc)
-> (TCErr -> TCMT IO Doc) -> TCErr -> tcm Doc
forall b c a. (b -> c) -> (a -> b) -> a -> c
. [TCErr] -> TCErr -> TCMT IO Doc
go []
  where
  go :: [TCErr] -> TCErr -> TCM Doc
  go :: [TCErr] -> TCErr -> TCMT IO Doc
go [TCErr]
errs TCErr
err
    | [TCErr] -> Int
forall a. [a] -> Int
forall (t :: * -> *) a. Foldable t => t a -> Int
length [TCErr]
errs Int -> Int -> Bool
forall a. Ord a => a -> a -> Bool
> Int
3 = [TCMT IO Doc] -> TCMT IO Doc
forall (m :: * -> *) (t :: * -> *).
(Applicative m, Foldable t) =>
t (m Doc) -> m Doc
vcat ([TCMT IO Doc] -> TCMT IO Doc) -> [TCMT IO Doc] -> TCMT IO Doc
forall a b. (a -> b) -> a -> b
$
        String -> TCMT IO Doc
forall (m :: * -> *). Applicative m => String -> m Doc
fwords (String
"total panic: error when printing error from printing error from printing error." String -> String -> String
forall a. [a] -> [a] -> [a]
++
               String
"I give up! Approximations of errors (original error last):")
        TCMT IO Doc -> [TCMT IO Doc] -> [TCMT IO Doc]
forall a. a -> [a] -> [a]
: (TCErr -> TCMT IO Doc) -> [TCErr] -> [TCMT IO Doc]
forall a b. (a -> b) -> [a] -> [b]
map (String -> TCMT IO Doc
forall (m :: * -> *). Applicative 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 b a. IsBool b => b -> (a -> a) -> a -> a
applyUnless ([TCErr] -> Bool
forall a. Null a => a -> Bool
null [TCErr]
errs)
          (\ TCMT IO Doc
d -> [TCMT IO Doc] -> TCMT IO Doc
forall (m :: * -> *) (t :: * -> *).
(Applicative m, Foldable t) =>
t (m Doc) -> m Doc
vcat ([TCMT IO Doc] -> TCMT IO Doc) -> [TCMT IO Doc] -> TCMT IO Doc
forall a b. (a -> b) -> a -> b
$
            TCMT IO Doc
"panic: error when printing error!"
            TCMT IO Doc -> [TCMT IO Doc] -> [TCMT IO Doc]
forall a. a -> [a] -> [a]
: TCMT IO Doc
d
            TCMT IO Doc -> [TCMT IO Doc] -> [TCMT IO Doc]
forall a. a -> [a] -> [a]
: (TCErr -> TCMT IO Doc) -> [TCErr] -> [TCMT IO Doc]
forall a b. (a -> b) -> [a] -> [b]
map (String -> TCMT IO Doc
forall (m :: * -> *). Applicative 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
. (String
"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)
          (TCErr -> TCMT IO Doc
forall a (m :: * -> *). (PrettyTCM a, MonadPretty m) => a -> m Doc
forall (m :: * -> *). MonadPretty m => TCErr -> m Doc
prettyTCM TCErr
err)
        TCMT IO Doc -> (TCErr -> TCMT IO Doc) -> TCMT IO Doc
forall a. TCMT IO a -> (TCErr -> TCMT IO a) -> TCMT IO a
forall e (m :: * -> *) a.
MonadError e m =>
m a -> (e -> m a) -> m a
`catchError` [TCErr] -> TCErr -> TCMT IO Doc
go (TCErr
errTCErr -> [TCErr] -> [TCErr]
forall a. a -> [a] -> [a]
:[TCErr]
errs)

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

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

nameWithBinding :: MonadPretty m => QName -> m Doc
nameWithBinding :: forall (m :: * -> *). MonadPretty m => QName -> m Doc
nameWithBinding QName
q =
  (QName -> m Doc
forall a (m :: * -> *). (PrettyTCM a, MonadPretty m) => a -> m Doc
forall (m :: * -> *). MonadPretty m => QName -> m Doc
prettyTCM QName
q m Doc -> m Doc -> m Doc
forall (m :: * -> *). Applicative m => m Doc -> 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
forall (m :: * -> *). MonadPretty m => Range -> m Doc
prettyTCM Range
r
  where
    r :: Range
r = QName -> Range
forall a. HasNameBindingSite a => a -> Range
nameBindingSite QName
q

tcErrString :: TCErr -> String
tcErrString :: TCErr -> String
tcErrString TCErr
err =
  [String] -> String
unwords ([String] -> String)
-> ([String] -> [String]) -> [String] -> String
forall b c a. (b -> c) -> (a -> b) -> a -> c
. (String -> Bool) -> [String] -> [String]
forall a. (a -> Bool) -> [a] -> [a]
filter (Bool -> Bool
not (Bool -> Bool) -> (String -> Bool) -> String -> Bool
forall b c a. (b -> c) -> (a -> b) -> a -> c
. String -> Bool
forall a. Null a => a -> Bool
null) ([String] -> [String])
-> ([String] -> [String]) -> [String] -> [String]
forall b c a. (b -> c) -> (a -> b) -> a -> c
. (Range -> String
forall a. Pretty a => a -> String
prettyShow (TCErr -> Range
forall a. HasRange a => a -> Range
getRange TCErr
err) String -> [String] -> [String]
forall a. a -> [a] -> [a]
:) ([String] -> String) -> [String] -> String
forall a b. (a -> b) -> a -> b
$
    case TCErr
err of
      TypeError CallStack
_ TCState
_ Closure SomeDiagnostic
cl     -> [ SomeDiagnostic -> String
forall a. Diagnostic a => a -> String
diagnosticString (SomeDiagnostic -> String) -> SomeDiagnostic -> String
forall a b. (a -> b) -> a -> b
$ Closure SomeDiagnostic -> SomeDiagnostic
forall a. Closure a -> a
clValue Closure SomeDiagnostic
cl ]
      ParserError ParseError
e        -> [ String
"ParserError" ]
      GenericException String
msg -> [ String
msg ]
      IOException Maybe TCState
_ Range
r IOException
e    -> [ Range -> String
forall a. Pretty a => a -> String
prettyShow Range
r, IOException -> String
forall e. Exception e => e -> String
showIOException IOException
e ]
      PatternErr{}         -> [ String
"PatternErr" ]

instance PrettyTCM TCErr where
  prettyTCM :: forall (m :: * -> *). MonadPretty m => TCErr -> m Doc
prettyTCM TCErr
err = case TCErr
err of
    -- Gallais, 2016-05-14
    -- Given where `NonFatalErrors` are created, we know for a
    -- fact that  ̀ws` is non-empty.
    TypeError CallStack
loc TCState
_ Closure{ clValue :: forall a. Closure a -> a
clValue = SomeDiagnostic
err } | Just (NonFatalErrors Set1 TCWarning
ws) <- SomeDiagnostic -> Maybe TypeError
forall a. Diagnostic a => SomeDiagnostic -> Maybe a
fromSomeDiagnostic SomeDiagnostic
err -> do
      String -> Int -> String -> m ()
forall (m :: * -> *).
MonadDebug m =>
String -> Int -> String -> m ()
reportSLn String
"error" Int
2 (String -> m ()) -> String -> m ()
forall a b. (a -> b) -> a -> b
$ String
"Error raised at " String -> String -> String
forall a. [a] -> [a] -> [a]
++ CallStack -> String
forall a. Pretty a => a -> String
prettyShow CallStack
loc
      NonEmpty (m Doc) -> m Doc
forall (m :: * -> *) (t :: * -> *).
(Applicative m, Foldable t) =>
t (m Doc) -> m Doc
vsep (NonEmpty (m Doc) -> m Doc) -> NonEmpty (m Doc) -> m Doc
forall a b. (a -> b) -> a -> b
$ (TCWarning -> m Doc) -> NonEmpty TCWarning -> NonEmpty (m Doc)
forall a b. (a -> b) -> NonEmpty a -> NonEmpty b
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap TCWarning -> m Doc
forall a (m :: * -> *). (PrettyTCM a, MonadPretty m) => a -> m Doc
forall (m :: * -> *). MonadPretty m => TCWarning -> m Doc
prettyTCM (NonEmpty TCWarning -> NonEmpty (m Doc))
-> NonEmpty TCWarning -> NonEmpty (m Doc)
forall a b. (a -> b) -> a -> b
$ Set1 TCWarning -> NonEmpty TCWarning
forall a. NESet a -> NonEmpty a
Set1.toAscList Set1 TCWarning
ws
    -- Andreas, 2014-03-23
    -- This use of withTCState seems ok since we do not collect
    -- Benchmark info during printing errors.
    TypeError CallStack
loc TCState
s Closure SomeDiagnostic
e -> (TCState -> TCState) -> m Doc -> m Doc
forall a. (TCState -> TCState) -> m a -> m a
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
$ do
      String -> Int -> String -> m ()
forall (m :: * -> *).
MonadDebug m =>
String -> Int -> String -> m ()
reportSLn String
"error" Int
2 (String -> m ()) -> String -> m ()
forall a b. (a -> b) -> a -> b
$ String
"Error raised at " String -> String -> String
forall a. [a] -> [a] -> [a]
++ CallStack -> String
forall a. Pretty a => a -> String
prettyShow CallStack
loc
      let r :: Range
r = Closure SomeDiagnostic -> TCEnv
forall a. Closure a -> TCEnv
clEnv Closure SomeDiagnostic
e TCEnv -> Getting Range TCEnv Range -> Range
forall s a. s -> Getting a s a -> a
^. Getting Range TCEnv Range
Lens' TCEnv Range
eRange
      [m Doc] -> m Doc
forall (m :: * -> *) (t :: * -> *).
(Applicative m, Foldable t) =>
t (m Doc) -> m Doc
vcat
        [ [m Doc] -> m Doc
forall (m :: * -> *) (t :: * -> *).
(Applicative m, Foldable t) =>
t (m Doc) -> m Doc
hsep
          [ if Range -> Bool
forall a. Null a => a -> Bool
null Range
r then m Doc
forall a. Null a => a
empty else Range -> m Doc
forall a (m :: * -> *). (PrettyTCM a, MonadPretty m) => a -> m Doc
forall (m :: * -> *). MonadPretty m => Range -> m Doc
prettyTCM Range
r m Doc -> m Doc -> m Doc
forall a. Semigroup a => a -> a -> a
<> m Doc
":"
          , m Doc
"error:"
          , m Doc -> m Doc
forall (m :: * -> *). Functor m => m Doc -> m Doc
brackets (String -> m Doc
forall (m :: * -> *). Applicative m => String -> m Doc
text (String -> m Doc) -> String -> m Doc
forall a b. (a -> b) -> a -> b
$ SomeDiagnostic -> String
forall a. Diagnostic a => a -> String
diagnosticString (SomeDiagnostic -> String) -> SomeDiagnostic -> String
forall a b. (a -> b) -> a -> b
$ Closure SomeDiagnostic -> SomeDiagnostic
forall a. Closure a -> a
clValue Closure SomeDiagnostic
e)
          ]
        , Closure SomeDiagnostic -> m Doc
forall a (m :: * -> *). (PrettyTCM a, MonadPretty m) => a -> m Doc
forall (m :: * -> *).
MonadPretty m =>
Closure SomeDiagnostic -> m Doc
prettyTCM Closure SomeDiagnostic
e
        , Maybe (Closure Call) -> m Doc
forall a (m :: * -> *). (PrettyTCM a, MonadPretty m) => a -> m Doc
forall (m :: * -> *).
MonadPretty m =>
Maybe (Closure Call) -> m Doc
prettyTCM (Closure SomeDiagnostic -> TCEnv
forall a. Closure a -> TCEnv
clEnv Closure SomeDiagnostic
e TCEnv
-> Getting (Maybe (Closure Call)) TCEnv (Maybe (Closure Call))
-> Maybe (Closure Call)
forall s a. s -> Getting a s a -> a
^. Getting (Maybe (Closure Call)) TCEnv (Maybe (Closure Call))
Lens' TCEnv (Maybe (Closure Call))
eCall)
        ]
    ParserError ParseError
err   -> ParseError -> m Doc
forall (m :: * -> *) a. (Applicative m, Pretty a) => a -> m Doc
pretty ParseError
err
    GenericException String
msg -> String -> m Doc
forall (m :: * -> *). Applicative m => String -> m Doc
fwords String
msg
    IOException Maybe TCState
_ Range
r 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 :: * -> *). Applicative m => String -> m Doc
fwords (String -> m Doc) -> String -> m Doc
forall a b. (a -> b) -> a -> b
$ IOException -> String
forall e. Exception e => e -> String
showIOException 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 String
"uncaught pattern violation"

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

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

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

prettyDisamb :: MonadPretty m => (QName -> Maybe (Range' SrcFile)) -> QName -> m Doc
prettyDisamb :: forall (m :: * -> *).
MonadPretty m =>
(QName -> Maybe Range) -> QName -> m Doc
prettyDisamb QName -> Maybe Range
f QName
x = do
  let d :: m Doc
d  = QName -> m Doc
forall (m :: * -> *) a. (Applicative m, Pretty a) => a -> m Doc
pretty (QName -> m Doc) -> m QName -> m Doc
forall (m :: * -> *) a b. Monad m => (a -> m b) -> m a -> m b
=<< QName -> m QName
forall (m :: * -> *). MonadPretty m => QName -> m QName
dropTopLevelModule QName
x
  Maybe Range -> m Doc -> (Range -> m Doc) -> m Doc
forall a b. Maybe a -> b -> (a -> b) -> b
caseMaybe (QName -> Maybe Range
f QName
x) m Doc
d ((Range -> m Doc) -> m Doc) -> (Range -> m Doc) -> m Doc
forall a b. (a -> b) -> a -> b
$ \ Range
r -> m Doc
d m Doc -> m Doc -> m Doc
forall (m :: * -> *). Applicative m => m Doc -> m Doc -> m Doc
<+> (m Doc
"(introduced at " m Doc -> m Doc -> m Doc
forall a. Semigroup a => a -> a -> a
<> Range -> m Doc
forall a (m :: * -> *). (PrettyTCM a, MonadPretty m) => a -> m Doc
forall (m :: * -> *). MonadPretty m => Range -> m Doc
prettyTCM Range
r m Doc -> m Doc -> m Doc
forall a. Semigroup a => a -> a -> a
<> m Doc
")")

-- | Print the last range in 'qnameModule'.
prettyDisambProj :: MonadPretty m => QName -> m Doc
prettyDisambProj :: forall (m :: * -> *). MonadPretty m => QName -> m Doc
prettyDisambProj = (QName -> Maybe Range) -> QName -> m Doc
forall (m :: * -> *).
MonadPretty m =>
(QName -> Maybe Range) -> QName -> m Doc
prettyDisamb ((QName -> Maybe Range) -> QName -> m Doc)
-> (QName -> Maybe Range) -> QName -> m Doc
forall a b. (a -> b) -> a -> b
$ [Range] -> Maybe Range
forall a. [a] -> Maybe a
lastMaybe ([Range] -> Maybe Range)
-> (QName -> [Range]) -> QName -> Maybe Range
forall b c a. (b -> c) -> (a -> b) -> a -> c
. (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]) -> (QName -> [Range]) -> QName -> [Range]
forall b c a. (b -> c) -> (a -> b) -> a -> c
. (Name -> Range) -> [Name] -> [Range]
forall a b. (a -> b) -> [a] -> [b]
map Name -> Range
forall a. HasNameBindingSite a => a -> Range
nameBindingSite ([Name] -> [Range]) -> (QName -> [Name]) -> QName -> [Range]
forall b c a. (b -> c) -> (a -> b) -> a -> c
. ModuleName -> [Name]
mnameToList (ModuleName -> [Name]) -> (QName -> ModuleName) -> QName -> [Name]
forall b c a. (b -> c) -> (a -> b) -> a -> c
. QName -> ModuleName
qnameModule

--   Print the range in 'qnameName'. This fixes the bad error message in #4130.
prettyDisambCons :: MonadPretty m => QName -> m Doc
prettyDisambCons :: forall (m :: * -> *). MonadPretty m => QName -> m Doc
prettyDisambCons = (QName -> Maybe Range) -> QName -> m Doc
forall (m :: * -> *).
MonadPretty m =>
(QName -> Maybe Range) -> QName -> m Doc
prettyDisamb ((QName -> Maybe Range) -> QName -> m Doc)
-> (QName -> Maybe Range) -> QName -> m Doc
forall a b. (a -> b) -> a -> b
$ Range -> Maybe Range
forall a. a -> Maybe a
Just (Range -> Maybe Range) -> (QName -> Range) -> QName -> Maybe Range
forall b c a. (b -> c) -> (a -> b) -> a -> c
. QName -> Range
forall a. HasNameBindingSite a => a -> Range
nameBindingSite

prepruneErrorRefinedContext :: forall m. MonadPretty m => Closure MetaId -> m Doc
prepruneErrorRefinedContext :: forall (m :: * -> *). MonadPretty m => Closure MetaId -> m Doc
prepruneErrorRefinedContext = Doc -> String -> Closure MetaId -> m Doc
forall (m :: * -> *).
MonadPretty m =>
Doc -> String -> Closure MetaId -> m Doc
prepruneError Doc
forall a. Null a => a
empty (String -> Closure MetaId -> m Doc)
-> String -> Closure MetaId -> m Doc
forall a b. (a -> b) -> a -> b
$
  String
"Failed to generalize because some of the generalized variables depend on an " String -> String -> String
forall a. [a] -> [a] -> [a]
++
  String
"unsolved meta created in a refined context (not a simple extension of the context where " String -> String -> String
forall a. [a] -> [a] -> [a]
++
  String
"generalization happens)."

prepruneErrorCyclicDependencies :: forall m. MonadPretty m => Closure MetaId -> m Doc
prepruneErrorCyclicDependencies :: forall (m :: * -> *). MonadPretty m => Closure MetaId -> m Doc
prepruneErrorCyclicDependencies = Doc -> String -> Closure MetaId -> m Doc
forall (m :: * -> *).
MonadPretty m =>
Doc -> String -> Closure MetaId -> m Doc
prepruneError Doc
forall a. Null a => a
empty (String -> Closure MetaId -> m Doc)
-> String -> Closure MetaId -> m Doc
forall a b. (a -> b) -> a -> b
$
  String
"Failed to generalize due to circular dependencies between the generalized " String -> String -> String
forall a. [a] -> [a] -> [a]
++
  String
"variables and an unsolved meta."

prepruneErrorFailedToInstantiate :: forall m. MonadPretty m => Closure MetaId -> m Doc
prepruneErrorFailedToInstantiate :: forall (m :: * -> *). MonadPretty m => Closure MetaId -> m Doc
prepruneErrorFailedToInstantiate = Doc -> String -> Closure MetaId -> m Doc
forall (m :: * -> *).
MonadPretty m =>
Doc -> String -> Closure MetaId -> m Doc
prepruneError Doc
prepruneErrorBounty (String -> Closure MetaId -> m Doc)
-> String -> Closure MetaId -> m Doc
forall a b. (a -> b) -> a -> b
$
  String
"Failed to generalize because the generalized variables depend on an unsolved meta " String -> String -> String
forall a. [a] -> [a] -> [a]
++
  String
"that could not be lifted outside the generalization."

prepruneErrorBounty :: Doc
prepruneErrorBounty :: Doc
prepruneErrorBounty = [Doc] -> Doc
forall (t :: * -> *). Foldable t => t Doc -> Doc
P.fsep ([Doc] -> Doc) -> [Doc] -> Doc
forall a b. (a -> b) -> a -> b
$ [[Doc]] -> [Doc]
forall (t :: * -> *) a. Foldable t => t [a] -> [a]
concat
  [ String -> [Doc]
P.pwords String
"Congratulations, you have hit a so far unreproduced error in generalization!"
  , String -> [Doc]
P.pwords String
"Please submit your self-contained reproducer (max 50 lines) at"
  , [ String -> Doc
P.url String
"https://github.com/agda/agda/issues/8161" ]
  , String -> [Doc]
P.pwords String
"to earn a honorable mention in the next Agda release."
  ]

prepruneError :: forall m. MonadPretty m => Doc -> String -> Closure MetaId -> m Doc
prepruneError :: forall (m :: * -> *).
MonadPretty m =>
Doc -> String -> Closure MetaId -> m Doc
prepruneError Doc
bounty String
msg Closure MetaId
x = Closure MetaId -> (MetaId -> m Doc) -> m Doc
forall (m :: * -> *) c a b.
(MonadTCEnv m, ReadTCState m, LensClosure c a) =>
c -> (a -> m b) -> m b
enterClosure Closure MetaId
x \ MetaId
x -> do
  r <- MetaId -> m Range
forall (m :: * -> *).
(HasCallStack, MonadDebug m, ReadTCState m) =>
MetaId -> m Range
getMetaRange MetaId
x
  vcat
    [ pure bounty
    , fwords $ msg ++ " The problematic unsolved meta is"
    , nest 2 $ prettyTCM (MetaV x []) <+> "at" <+> pretty r
    ]

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

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

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

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

    GeneralizationPrepruneErrorRefinedContext Closure MetaId
x ->
      Closure MetaId -> m Doc
forall (m :: * -> *). MonadPretty m => Closure MetaId -> m Doc
prepruneErrorRefinedContext Closure MetaId
x

    GeneralizationPrepruneErrorCyclicDependencies Closure MetaId
x ->
      Closure MetaId -> m Doc
forall (m :: * -> *). MonadPretty m => Closure MetaId -> m Doc
prepruneErrorCyclicDependencies Closure MetaId
x

    GeneralizationPrepruneErrorFailedToInstantiate Closure MetaId
x ->
      Closure MetaId -> m Doc
forall (m :: * -> *). MonadPretty m => Closure MetaId -> m Doc
prepruneErrorFailedToInstantiate Closure MetaId
x

    OptionError String
s -> String -> m Doc
forall (m :: * -> *). Applicative m => String -> m Doc
fwords String
s

    SyntaxError String
s -> String -> m Doc
forall (m :: * -> *). Applicative m => String -> m Doc
fwords (String -> m Doc) -> String -> m Doc
forall a b. (a -> b) -> a -> b
$ String
"Syntax error: "  String -> String -> String
forall a. [a] -> [a] -> [a]
++ String
s

    DoNotationError String
err -> String -> m Doc
forall (m :: * -> *). Applicative m => String -> m Doc
fwords String
err

    IdiomBracketError String
err -> String -> m Doc
forall (m :: * -> *). Applicative m => String -> m Doc
fwords String
err

    TypeError
InvalidDottedExpression -> String -> m Doc
forall (m :: * -> *). Applicative m => String -> m Doc
fwords String
"Invalid dotted expression"

    NoKnownRecordWithSuchFields [Name]
fields -> [m Doc] -> m Doc
forall (m :: * -> *) (t :: * -> *).
(Applicative m, Foldable t) =>
t (m Doc) -> m Doc
fsep ([m Doc] -> m Doc) -> [m Doc] -> m Doc
forall a b. (a -> b) -> a -> b
$
      case [Name]
fields of
        []  -> String -> [m Doc]
forall (m :: * -> *). Applicative m => String -> [m Doc]
pwords String
"There are no records in scope"
        [Name
f] -> String -> [m Doc]
forall (m :: * -> *). Applicative m => String -> [m Doc]
pwords String
"There is no known record with the field" [m Doc] -> [m Doc] -> [m Doc]
forall a. [a] -> [a] -> [a]
++ [ Name -> m Doc
forall (m :: * -> *) a. (Applicative m, Pretty a) => a -> m Doc
pretty Name
f ]
        [Name]
_   -> String -> [m Doc]
forall (m :: * -> *). Applicative m => String -> [m Doc]
pwords String
"There is no known record with the fields" [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. (Applicative m, Pretty a) => a -> m Doc
pretty [Name]
fields

    ShouldEndInApplicationOfTheDatatype Type
t -> [m Doc] -> m Doc
forall (m :: * -> *) (t :: * -> *).
(Applicative m, Foldable t) =>
t (m Doc) -> m Doc
fsep ([m Doc] -> m Doc) -> [m Doc] -> m Doc
forall a b. (a -> b) -> a -> b
$
      String -> [m Doc]
forall (m :: * -> *). Applicative m => String -> [m Doc]
pwords String
"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
forall (m :: * -> *). MonadPretty m => Type -> m Doc
prettyTCM Type
t] [m Doc] -> [m Doc] -> [m Doc]
forall a. [a] -> [a] -> [a]
++ String -> [m Doc]
forall (m :: * -> *). Applicative m => String -> [m Doc]
pwords String
"isn't"

    ShouldBeRecordType Type
t -> [m Doc] -> m Doc
forall (m :: * -> *) (t :: * -> *).
(Applicative m, Foldable t) =>
t (m Doc) -> m Doc
fsep ([m Doc] -> m Doc) -> [m Doc] -> m Doc
forall a b. (a -> b) -> a -> b
$
      String -> [m Doc]
forall (m :: * -> *). Applicative m => String -> [m Doc]
pwords String
"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
forall (m :: * -> *). MonadPretty m => Type -> m Doc
prettyTCM Type
t]

    TypeError
ShouldBeRecordPattern -> [m Doc] -> m Doc
forall (m :: * -> *) (t :: * -> *).
(Applicative m, Foldable t) =>
t (m Doc) -> m Doc
fsep ([m Doc] -> m Doc) -> [m Doc] -> m Doc
forall a b. (a -> b) -> a -> b
$
      String -> [m Doc]
forall (m :: * -> *). Applicative m => String -> [m Doc]
pwords String
"Expected record pattern"

    WrongHidingInLHS Hiding
h -> String -> m Doc
forall (m :: * -> *). Applicative m => String -> m Doc
fwords (String -> m Doc) -> String -> m Doc
forall a b. (a -> b) -> a -> b
$ String
"Unexpected " String -> String -> String
forall a. [a] -> [a] -> [a]
++ Hiding -> String
forall a. Verbalize a => a -> String
verbalize Hiding
h String -> String -> String
forall a. [a] -> [a] -> [a]
++ String
" argument"

    WrongHidingInLambda Hiding
h Type
t -> String -> m Doc
forall (m :: * -> *). Applicative m => String -> m Doc
fwords (String -> m Doc) -> String -> m Doc
forall a b. (a -> b) -> a -> b
$
      String
"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]
++ String
" lambda where an explicit lambda was expected"

    WrongHidingInProjection Hiding
h Hiding
h' QName
d -> [m Doc] -> m Doc
forall (m :: * -> *) (t :: * -> *).
(Applicative m, Foldable t) =>
t (m Doc) -> m Doc
fsep ([m Doc] -> m Doc) -> [m Doc] -> m Doc
forall a b. (a -> b) -> a -> b
$
      (String -> [m Doc]
forall (m :: * -> *). Applicative m => String -> [m Doc]
pwords (String -> [m Doc]) -> String -> [m Doc]
forall a b. (a -> b) -> a -> b
$ String
"Unexpected " String -> String -> String
forall a. [a] -> [a] -> [a]
++ Hiding -> String
forall a. Verbalize a => a -> String
verbalize Hiding
h String -> String -> String
forall a. [a] -> [a] -> [a]
++ String
" argument to projection")
      [m Doc] -> [m Doc] -> [m Doc]
forall a. [a] -> [a] -> [a]
++ [QName -> m Doc
forall a (m :: * -> *). (PrettyTCM a, MonadPretty m) => a -> m Doc
forall (m :: * -> *). MonadPretty m => QName -> m Doc
prettyTCM QName
d] [m Doc] -> [m Doc] -> [m Doc]
forall a. [a] -> [a] -> [a]
++
      (String -> [m Doc]
forall (m :: * -> *). Applicative m => String -> [m Doc]
pwords (String -> [m Doc]) -> String -> [m Doc]
forall a b. (a -> b) -> a -> b
$ String
"when " 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]
++ String
" argument is expected")

    IllegalHidingInPostfixProjection NamedArg Expr
arg -> [m Doc] -> m Doc
forall (m :: * -> *) (t :: * -> *).
(Applicative m, Foldable t) =>
t (m Doc) -> m Doc
fsep ([m Doc] -> m Doc) -> [m Doc] -> m Doc
forall a b. (a -> b) -> a -> b
$
      String -> [m Doc]
forall (m :: * -> *). Applicative m => String -> [m Doc]
pwords String
"Postfix projections can only be visible arguments, but"
      [m Doc] -> [m Doc] -> [m Doc]
forall a. [a] -> [a] -> [a]
++ [NamedArg Expr -> m Doc
forall (m :: * -> *) a. (Applicative m, Pretty a) => a -> m Doc
pretty NamedArg Expr
arg]
      [m Doc] -> [m Doc] -> [m Doc]
forall a. [a] -> [a] -> [a]
++ (String -> [m Doc]
forall (m :: * -> *). Applicative m => String -> [m Doc]
pwords (String -> [m Doc]) -> String -> [m Doc]
forall a b. (a -> b) -> a -> b
$ String
"is " 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 -> Indefinite Hiding) -> Hiding -> Indefinite Hiding
forall a b. (a -> b) -> a -> b
$ NamedArg Expr -> Hiding
forall a. LensHiding a => a -> Hiding
getHiding NamedArg Expr
arg) String -> String -> String
forall a. [a] -> [a] -> [a]
++ String
" argument")

    WrongNamedArgument NamedArg Expr
a List1 NamedName
xs0 -> [m Doc] -> m Doc
forall (m :: * -> *) (t :: * -> *).
(Applicative m, Foldable t) =>
t (m Doc) -> m Doc
fsep ([m Doc] -> m Doc) -> [m Doc] -> m Doc
forall a b. (a -> b) -> a -> b
$
      String -> [m Doc]
forall (m :: * -> *). Applicative m => String -> [m Doc]
pwords String
"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
forall (m :: * -> *). MonadPretty m => NamedArg Expr -> m Doc
prettyTCM NamedArg Expr
a] -- ++ pwords " (wrong argument name)"
      [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
$ [m Doc] -> m Doc
forall (m :: * -> *) (t :: * -> *).
(Applicative m, Foldable t) =>
t (m Doc) -> m Doc
fsep ([m Doc] -> m Doc) -> [m Doc] -> m Doc
forall a b. (a -> b) -> a -> b
$ String -> m Doc
forall (m :: * -> *). Applicative m => String -> m Doc
text String
"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. (Applicative m, Pretty a) => a -> m Doc
pretty [NamedName]
xs | Bool -> Bool
not ([NamedName] -> Bool
forall a. Null a => a -> Bool
null [NamedName]
xs)]
      where
      xs :: [NamedName]
xs = (NamedName -> Bool) -> List1 NamedName -> [NamedName]
forall a. (a -> Bool) -> NonEmpty a -> [a]
List1.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) List1 NamedName
xs0

    WrongHidingInApplication Hiding
h Type
t -> String -> m Doc
forall (m :: * -> *). Applicative m => String -> m Doc
fwords (String -> m Doc) -> String -> m Doc
forall a b. (a -> b) -> a -> b
$
      String
"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]
++ String
" application where an explicit application was expected"

    HidingMismatch Hiding
h Hiding
h' -> String -> m Doc
forall (m :: * -> *). Applicative m => String -> m Doc
fwords (String -> m Doc) -> String -> m Doc
forall a b. (a -> b) -> a -> b
$
      String
"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]
++ String
" 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]
++ String
" argument"

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

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

    IllformedProjectionPatternConcrete Pattern
p -> [m Doc] -> m Doc
forall (m :: * -> *) (t :: * -> *).
(Applicative m, Foldable t) =>
t (m Doc) -> m Doc
fsep ([m Doc] -> m Doc) -> [m Doc] -> m Doc
forall a b. (a -> b) -> a -> b
$
      String -> [m Doc]
forall (m :: * -> *). Applicative m => String -> [m Doc]
pwords String
"Ill-formed projection pattern" [m Doc] -> [m Doc] -> [m Doc]
forall a. [a] -> [a] -> [a]
++ [Pattern -> m Doc
forall (m :: * -> *) a. (Applicative m, Pretty a) => a -> m Doc
pretty Pattern
p]

    TypeError
LiteralTooBig -> [m Doc] -> m Doc
forall (m :: * -> *) (t :: * -> *).
(Applicative m, Foldable t) =>
t (m Doc) -> m Doc
fsep ([m Doc] -> m Doc) -> [m Doc] -> m Doc
forall a b. (a -> b) -> a -> b
$ [[m Doc]] -> [m Doc]
forall (t :: * -> *) a. Foldable t => t [a] -> [a]
concat
      [ String -> [m Doc]
forall (m :: * -> *). Applicative m => String -> [m Doc]
pwords String
"Matching on natural number literals is done by expanding"
      , String -> [m Doc]
forall (m :: * -> *). Applicative m => String -> [m Doc]
pwords String
"the literal to the corresponding constructor pattern,"
      , String -> [m Doc]
forall (m :: * -> *). Applicative m => String -> [m Doc]
pwords String
"so you probably don't want to do it this way"
      ]

    TypeError
NegativeLiteralInPattern -> [m Doc] -> m Doc
forall (m :: * -> *) (t :: * -> *).
(Applicative m, Foldable t) =>
t (m Doc) -> m Doc
fsep ([m Doc] -> m Doc) -> [m Doc] -> m Doc
forall a b. (a -> b) -> a -> b
$
      String -> [m Doc]
forall (m :: * -> *). Applicative m => String -> [m Doc]
pwords String
"Negative literals are not supported in patterns"


    WrongNumberOfConstructorArguments QName
c Int
expect Int
given -> [m Doc] -> m Doc
forall (m :: * -> *) (t :: * -> *).
(Applicative m, Foldable t) =>
t (m Doc) -> m Doc
fsep ([m Doc] -> m Doc) -> [m Doc] -> m Doc
forall a b. (a -> b) -> a -> b
$
      String -> [m Doc]
forall (m :: * -> *). Applicative m => String -> [m Doc]
pwords String
"The constructor" [m Doc] -> [m Doc] -> [m Doc]
forall a. [a] -> [a] -> [a]
++ [QName -> m Doc
forall a (m :: * -> *). (PrettyTCM a, MonadPretty m) => a -> m Doc
forall (m :: * -> *). MonadPretty m => QName -> m Doc
prettyTCM QName
c] [m Doc] -> [m Doc] -> [m Doc]
forall a. [a] -> [a] -> [a]
++
      String -> [m Doc]
forall (m :: * -> *). Applicative m => String -> [m Doc]
pwords String
"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
forall (m :: * -> *). MonadPretty m => Int -> m Doc
prettyTCM Int
expect] [m Doc] -> [m Doc] -> [m Doc]
forall a. [a] -> [a] -> [a]
++
      String -> [m Doc]
forall (m :: * -> *). Applicative m => String -> [m Doc]
pwords String
"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
forall (m :: * -> *). MonadPretty m => Int -> m Doc
prettyTCM Int
given] [m Doc] -> [m Doc] -> [m Doc]
forall a. [a] -> [a] -> [a]
++ String -> [m Doc]
forall (m :: * -> *). Applicative m => String -> [m Doc]
pwords String
"(including hidden ones)"

    CantResolveOverloadedConstructorsTargetingSameDatatype QName
d List1 QName
cs -> [m Doc] -> m Doc
forall (m :: * -> *) (t :: * -> *).
(Applicative m, Foldable t) =>
t (m Doc) -> m Doc
fsep ([m Doc] -> m Doc) -> [m Doc] -> m Doc
forall a b. (a -> b) -> a -> b
$
      String -> [m Doc]
forall (m :: * -> *). Applicative m => String -> [m Doc]
pwords String
"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 (QName -> m Doc
forall a (m :: * -> *). (PrettyTCM a, MonadPretty m) => a -> m Doc
forall (m :: * -> *). MonadPretty m => QName -> 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 :: * -> *). Applicative 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. (Applicative m, Pretty a) => a -> m Doc
pretty (List1 QName -> [Item (List1 QName)]
forall l. IsList l => l -> [Item l]
List1.toList List1 QName
cs)

    ConstructorDoesNotTargetGivenType QName
c Type
t -> [m Doc] -> m Doc
forall (m :: * -> *) (t :: * -> *).
(Applicative m, Foldable t) =>
t (m Doc) -> m Doc
fsep ([m Doc] -> m Doc) -> [m Doc] -> m Doc
forall a b. (a -> b) -> a -> b
$
      String -> [m Doc]
forall (m :: * -> *). Applicative m => String -> [m Doc]
pwords String
"The constructor" [m Doc] -> [m Doc] -> [m Doc]
forall a. [a] -> [a] -> [a]
++ [QName -> m Doc
forall a (m :: * -> *). (PrettyTCM a, MonadPretty m) => a -> m Doc
forall (m :: * -> *). MonadPretty m => QName -> m Doc
prettyTCM QName
c] [m Doc] -> [m Doc] -> [m Doc]
forall a. [a] -> [a] -> [a]
++
      String -> [m Doc]
forall (m :: * -> *). Applicative m => String -> [m Doc]
pwords String
"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
forall (m :: * -> *). MonadPretty m => Type -> m Doc
prettyTCM Type
t]

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

    ShadowedModule Name
x List1 ModuleName
ms -> m (m Doc) -> m Doc
forall (m :: * -> *) a. Monad m => m (m a) -> m a
join (m (m Doc) -> m Doc) -> m (m Doc) -> m Doc
forall a b. (a -> b) -> a -> b
$ (m Doc, Range) -> m Doc
forall a b. (a, b) -> a
fst ((m Doc, Range) -> m Doc) -> m (m Doc, Range) -> m (m Doc)
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> Name -> List1 ModuleName -> m (m Doc, Range)
forall (m :: * -> *).
MonadPretty m =>
Name -> List1 ModuleName -> m (m Doc, Range)
prettyShadowedModule Name
x List1 ModuleName
ms

    ModuleArityMismatch ModuleName
m Telescope
EmptyTel Either (List1 (NamedArg Expr)) Args
args -> [m Doc] -> m Doc
forall (m :: * -> *) (t :: * -> *).
(Applicative m, Foldable t) =>
t (m Doc) -> m Doc
fsep ([m Doc] -> m Doc) -> [m Doc] -> m Doc
forall a b. (a -> b) -> a -> b
$
      String -> [m Doc]
forall (m :: * -> *). Applicative m => String -> [m Doc]
pwords String
"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
forall (m :: * -> *). MonadPretty m => ModuleName -> m Doc
prettyTCM ModuleName
m] [m Doc] -> [m Doc] -> [m Doc]
forall a. [a] -> [a] -> [a]
++
      String -> [m Doc]
forall (m :: * -> *). Applicative m => String -> [m Doc]
pwords String
"is not parameterized, but is being applied to arguments"

    ModuleArityMismatch ModuleName
m tel :: Telescope
tel@(ExtendTel Dom Type
_ Abs Telescope
_) Either (List1 (NamedArg Expr)) Args
args -> [m Doc] -> m Doc
forall (m :: * -> *) (t :: * -> *).
(Applicative m, Foldable t) =>
t (m Doc) -> m Doc
fsep ([m Doc] -> m Doc) -> [m Doc] -> m Doc
forall a b. (a -> b) -> a -> b
$
      String -> [m Doc]
forall (m :: * -> *). Applicative m => String -> [m Doc]
pwords String
"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
forall (m :: * -> *). MonadPretty m => ModuleName -> m Doc
prettyTCM ModuleName
m] [m Doc] -> [m Doc] -> [m Doc]
forall a. [a] -> [a] -> [a]
++ String -> [m Doc]
forall (m :: * -> *). Applicative m => String -> [m Doc]
pwords String
"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
forall (m :: * -> *). MonadPretty m => Telescope -> m Doc
prettyTCM Telescope
tel]

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

    ShouldBeEmpty Type
t [DeBruijnPattern]
ps -> [m Doc] -> m Doc
forall (m :: * -> *) (t :: * -> *).
(Applicative m, Foldable t) =>
t (m Doc) -> m Doc
fsep (
      Type -> m Doc
forall a (m :: * -> *). (PrettyTCM a, MonadPretty m) => a -> m Doc
forall (m :: * -> *). MonadPretty m => Type -> m Doc
prettyTCM Type
t m Doc -> [m Doc] -> [m Doc]
forall a. a -> [a] -> [a]
:
      String -> [m Doc]
forall (m :: * -> *). Applicative m => String -> [m Doc]
pwords String
"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 Int
2 ([m Doc] -> m Doc
forall (m :: * -> *) (t :: * -> *).
(Applicative m, Foldable t) =>
t (m Doc) -> m Doc
vcat ([m Doc] -> m Doc) -> [m Doc] -> m Doc
forall a b. (a -> b) -> a -> b
$ (DeBruijnPattern -> m Doc) -> [DeBruijnPattern] -> [m Doc]
forall a b. (a -> b) -> [a] -> [b]
map (Integer -> DeBruijnPattern -> m Doc
forall a. Integer -> Pattern' a -> m Doc
prettyPat Integer
0) [DeBruijnPattern]
ps)

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

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

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

    CannotApply Expr
e Type
t -> [m Doc] -> m Doc
forall (m :: * -> *) (t :: * -> *).
(Applicative m, Foldable t) =>
t (m Doc) -> m Doc
sep
      [ m Doc
"Expression used as function but does not have function type:"
      , Int -> m Doc -> m Doc
forall (m :: * -> *). Functor m => Int -> m Doc -> m Doc
nest Int
2 (m Doc -> m Doc) -> m Doc -> m Doc
forall a b. (a -> b) -> a -> b
$ m Doc
"expr:" m Doc -> m Doc -> m Doc
forall (m :: * -> *). Applicative m => m Doc -> m Doc -> m Doc
<+> Expr -> m Doc
forall a (m :: * -> *).
(ToConcrete a, Pretty (ConOfAbs a), MonadAbsToCon m) =>
a -> m Doc
prettyA Expr
e
      , Int -> m Doc -> m Doc
forall (m :: * -> *). Functor m => Int -> m Doc -> m Doc
nest Int
2 (m Doc -> m Doc) -> m Doc -> m Doc
forall a b. (a -> b) -> a -> b
$ m Doc
"type:" m Doc -> m Doc -> m Doc
forall (m :: * -> *). Applicative m => m Doc -> m Doc -> m Doc
<+> Type -> m Doc
forall a (m :: * -> *). (PrettyTCM a, MonadPretty m) => a -> m Doc
forall (m :: * -> *). MonadPretty m => Type -> m Doc
prettyTCM Type
t
      ]

    InvalidTypeSort Sort
s -> [m Doc] -> m Doc
forall (m :: * -> *) (t :: * -> *).
(Applicative m, Foldable t) =>
t (m Doc) -> m Doc
fsep ([m Doc] -> m Doc) -> [m Doc] -> m Doc
forall a b. (a -> b) -> a -> b
$ Sort -> m Doc
forall a (m :: * -> *). (PrettyTCM a, MonadPretty m) => a -> m Doc
forall (m :: * -> *). MonadPretty m => Sort -> m Doc
prettyTCM Sort
s m Doc -> [m Doc] -> [m Doc]
forall a. a -> [a] -> [a]
: String -> [m Doc]
forall (m :: * -> *). Applicative m => String -> [m Doc]
pwords String
"is not a valid sort"

    NotLeqSort Sort
s1 Sort
s2 -> [m Doc] -> m Doc
forall (m :: * -> *) (t :: * -> *).
(Applicative m, Foldable t) =>
t (m Doc) -> m Doc
fsep ([m Doc] -> m Doc) -> [m Doc] -> m Doc
forall a b. (a -> b) -> a -> b
$
      [Sort -> m Doc
forall a (m :: * -> *). (PrettyTCM a, MonadPretty m) => a -> m Doc
forall (m :: * -> *). MonadPretty m => Sort -> m Doc
prettyTCM Sort
s1] [m Doc] -> [m Doc] -> [m Doc]
forall a. [a] -> [a] -> [a]
++ String -> [m Doc]
forall (m :: * -> *). Applicative m => String -> [m Doc]
pwords String
"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
forall (m :: * -> *). MonadPretty m => Sort -> m Doc
prettyTCM Sort
s2]

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

    DuplicateConstructors List1 Name
xs -> ([m Doc] -> m Doc
forall (m :: * -> *) (t :: * -> *).
(Applicative m, Foldable t) =>
t (m Doc) -> m Doc
fsep ([m Doc] -> m Doc) -> ([[m Doc]] -> [m Doc]) -> [[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
"Duplicate" ]
      , [ List1 Name -> m Doc -> m Doc
forall (m :: * -> *) a. (Functor m, Sized a) => a -> m Doc -> m Doc
pluralS List1 Name
xs m Doc
"constructor" ]
      , String -> [m Doc]
forall (m :: * -> *). Applicative m => String -> [m Doc]
pwords String
"in datatype:"
      ]
      m Doc -> m Doc -> m Doc
forall (m :: * -> *). Applicative m => m Doc -> m Doc -> m Doc
<?> NonEmpty (m Doc) -> m Doc
forall (m :: * -> *) (t :: * -> *).
(Applicative m, Foldable t) =>
t (m Doc) -> m Doc
fsep ((Name -> m Doc) -> List1 Name -> NonEmpty (m Doc)
forall a b. (a -> b) -> NonEmpty a -> NonEmpty b
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap Name -> m Doc
forall (m :: * -> *) a. (Applicative m, Pretty a) => a -> m Doc
pretty List1 Name
xs)

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

    DuplicateOverlapPragma QName
q OverlapMode
old OverlapMode
new -> [m Doc] -> m Doc
forall (m :: * -> *) (t :: * -> *).
(Applicative m, Foldable t) =>
t (m Doc) -> m Doc
fsep ([m Doc] -> m Doc) -> [m Doc] -> m Doc
forall a b. (a -> b) -> a -> b
$
      String -> [m Doc]
forall (m :: * -> *). Applicative m => String -> [m Doc]
pwords String
"The instance" [m Doc] -> [m Doc] -> [m Doc]
forall a. [a] -> [a] -> [a]
++ [QName -> m Doc
forall a (m :: * -> *). (PrettyTCM a, MonadPretty m) => a -> m Doc
forall (m :: * -> *). MonadPretty m => QName -> m Doc
prettyTCM QName
q] [m Doc] -> [m Doc] -> [m Doc]
forall a. [a] -> [a] -> [a]
++
      String -> [m Doc]
forall (m :: * -> *). Applicative m => String -> [m Doc]
pwords String
"was already marked" [m Doc] -> [m Doc] -> [m Doc]
forall a. [a] -> [a] -> [a]
++ [OverlapMode -> m Doc
forall (m :: * -> *) a. (Applicative m, Pretty a) => a -> m Doc
pretty OverlapMode
old m Doc -> m Doc -> m Doc
forall a. Semigroup a => a -> a -> a
<> m Doc
"."] [m Doc] -> [m Doc] -> [m Doc]
forall a. [a] -> [a] -> [a]
++
      String -> [m Doc]
forall (m :: * -> *). Applicative m => String -> [m Doc]
pwords String
"This" [m Doc] -> [m Doc] -> [m Doc]
forall a. [a] -> [a] -> [a]
++ [OverlapMode -> m Doc
forall (m :: * -> *) a. (Applicative m, Pretty a) => a -> m Doc
pretty OverlapMode
new] [m Doc] -> [m Doc] -> [m Doc]
forall a. [a] -> [a] -> [a]
++
      String -> [m Doc]
forall (m :: * -> *). Applicative m => String -> [m Doc]
pwords String
"pragma can not be applied to it."

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

    UnexpectedWithPatterns List1 Pattern
ps -> [m Doc] -> m Doc
forall (m :: * -> *) (t :: * -> *).
(Applicative m, Foldable t) =>
t (m Doc) -> m Doc
fsep ([m Doc] -> m Doc) -> [m Doc] -> m Doc
forall a b. (a -> b) -> a -> b
$
      String -> [m Doc]
forall (m :: * -> *). Applicative m => String -> [m Doc]
pwords String
"Unexpected with patterns" [m Doc] -> [m Doc] -> [m Doc]
forall a. [a] -> [a] -> [a]
++ m Doc -> NonEmpty (m Doc) -> [m Doc]
forall (m :: * -> *) (t :: * -> *).
(Applicative m, Semigroup (m Doc), Foldable t) =>
m Doc -> t (m Doc) -> [m Doc]
punctuate m Doc
" |" ((Pattern -> m Doc) -> List1 Pattern -> NonEmpty (m Doc)
forall a b. (a -> b) -> NonEmpty a -> NonEmpty b
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap Pattern -> m Doc
forall a (m :: * -> *).
(ToConcrete a, Pretty (ConOfAbs a), MonadAbsToCon m) =>
a -> m Doc
prettyA List1 Pattern
ps)

    TypeError
TooFewPatternsInWithClause -> [m Doc] -> m Doc
forall (m :: * -> *) (t :: * -> *).
(Applicative m, Foldable t) =>
t (m Doc) -> m Doc
fsep ([m Doc] -> m Doc) -> [m Doc] -> m Doc
forall a b. (a -> b) -> a -> b
$ String -> [m Doc]
forall (m :: * -> *). Applicative m => String -> [m Doc]
pwords String
"Too few arguments given in with-clause"
    TypeError
TooManyPatternsInWithClause -> [m Doc] -> m Doc
forall (m :: * -> *) (t :: * -> *).
(Applicative m, Foldable t) =>
t (m Doc) -> m Doc
fsep ([m Doc] -> m Doc) -> [m Doc] -> m Doc
forall a b. (a -> b) -> a -> b
$ String -> [m Doc]
forall (m :: * -> *). Applicative m => String -> [m Doc]
pwords String
"Too many arguments given in with-clause"

    WithClausePatternMismatch Pattern
p NamedArg DeBruijnPattern
q -> [m Doc] -> m Doc
forall (m :: * -> *) (t :: * -> *).
(Applicative m, Foldable t) =>
t (m Doc) -> m Doc
fsep ([m Doc] -> m Doc) -> [m Doc] -> m Doc
forall a b. (a -> b) -> a -> b
$
      String -> [m Doc]
forall (m :: * -> *). Applicative m => String -> [m Doc]
pwords String
"With clause pattern " [m Doc] -> [m Doc] -> [m Doc]
forall a. [a] -> [a] -> [a]
++ [Pattern -> m Doc
forall a (m :: * -> *).
(ToConcrete a, Pretty (ConOfAbs a), MonadAbsToCon m) =>
a -> m Doc
prettyA Pattern
p] [m Doc] -> [m Doc] -> [m Doc]
forall a. [a] -> [a] -> [a]
++
      String -> [m Doc]
forall (m :: * -> *). Applicative m => String -> [m Doc]
pwords String
" is not an instance of its parent pattern " [m Doc] -> [m Doc] -> [m Doc]
forall a. [a] -> [a] -> [a]
++ [[Doc] -> Doc
forall (t :: * -> *). Foldable t => t 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]]

    PathAbstractionFailed Abs Type
b -> [m Doc] -> m Doc
forall (m :: * -> *) (t :: * -> *).
(Applicative m, Foldable t) =>
t (m Doc) -> m Doc
vcat
      [ (m Doc
"Path abstraction failed for type" m Doc -> m Doc -> m Doc
forall (m :: * -> *). Applicative m => m Doc -> m Doc -> m Doc
<+> Type -> m Doc
forall a (m :: * -> *). (PrettyTCM a, MonadPretty m) => a -> m Doc
forall (m :: * -> *). MonadPretty m => Type -> m Doc
prettyTCM (Abs Type -> Type
forall a. Abs a -> a
unAbs Abs Type
b)) m Doc -> m Doc -> m Doc
forall a. Semigroup a => a -> a -> a
<> m Doc
"."
      , m Doc
"The type may be non-fibrant or its sort depends on an interval variable"
      ]

    MetaCannotDependOn MetaId
m Term
v Int
i -> [m Doc] -> m Doc
forall (m :: * -> *) (t :: * -> *).
(Applicative m, Foldable t) =>
t (m Doc) -> m Doc
fsep
      [ String -> m Doc
forall (m :: * -> *). Applicative m => String -> m Doc
text String
"Cannot instantiate the metavariable"
      , MetaId -> m Doc
forall a (m :: * -> *). (PrettyTCM a, MonadPretty m) => a -> m Doc
forall (m :: * -> *). MonadPretty m => MetaId -> m Doc
prettyTCM MetaId
m
      , m Doc
"to solution"
      , Term -> m Doc
forall a (m :: * -> *). (PrettyTCM a, MonadPretty m) => a -> m Doc
forall (m :: * -> *). MonadPretty m => Term -> m Doc
prettyTCM Term
v
      , m Doc
"since it contains the variable"
      , Term -> m Doc
forall a (m :: * -> *). (PrettyTCM a, MonadPretty m) => a -> m Doc
forall (m :: * -> *). MonadPretty m => Term -> m Doc
prettyTCM (Int -> Elims -> Term
I.Var Int
i [])
      , m Doc
"which is not in scope of the metavariable"
      ]

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

    BuiltinMustBeData BuiltinId
s Int
n -> [m Doc] -> m Doc
forall (m :: * -> *) (t :: * -> *).
(Applicative m, Foldable t) =>
t (m Doc) -> m Doc
fsep ([m Doc] -> m Doc) -> [m Doc] -> m Doc
forall a b. (a -> b) -> a -> b
$
      String -> [m Doc]
forall (m :: * -> *). Applicative m => String -> [m Doc]
pwords String
"The builtin" [m Doc] -> [m Doc] -> [m Doc]
forall a. [a] -> [a] -> [a]
++ [BuiltinId -> m Doc
forall (m :: * -> *) a. (Applicative m, Pretty a) => a -> m Doc
pretty BuiltinId
s] [m Doc] -> [m Doc] -> [m Doc]
forall a. [a] -> [a] -> [a]
++ String -> [m Doc]
forall (m :: * -> *). Applicative m => String -> [m Doc]
pwords String
"must be a datatype with" [m Doc] -> [m Doc] -> [m Doc]
forall a. [a] -> [a] -> [a]
++
      if Int
n Int -> Int -> Bool
forall a. Eq a => a -> a -> Bool
== Int
1 then String -> [m Doc]
forall (m :: * -> *). Applicative m => String -> [m Doc]
pwords String
"a single constructor or an (inductive) record type"
      else [Int -> m Doc
forall (m :: * -> *) a. (Applicative m, Pretty a) => a -> m Doc
pretty Int
n] [m Doc] -> [m Doc] -> [m Doc]
forall a. [a] -> [a] -> [a]
++ String -> [m Doc]
forall (m :: * -> *). Applicative m => String -> [m Doc]
pwords String
"constructors"

    BuiltinMustBeDef BuiltinId
s -> [m Doc] -> m Doc
forall (m :: * -> *) (t :: * -> *).
(Applicative m, Foldable t) =>
t (m Doc) -> m Doc
fsep ([m Doc] -> m Doc) -> [m Doc] -> m Doc
forall a b. (a -> b) -> a -> b
$
      String -> [m Doc]
forall (m :: * -> *). Applicative m => String -> [m Doc]
pwords String
"The argument to BUILTIN" [m Doc] -> [m Doc] -> [m Doc]
forall a. [a] -> [a] -> [a]
++ [BuiltinId -> m Doc
forall (m :: * -> *) a. (Applicative m, Pretty a) => a -> m Doc
pretty BuiltinId
s] [m Doc] -> [m Doc] -> [m Doc]
forall a. [a] -> [a] -> [a]
++ String -> [m Doc]
forall (m :: * -> *). Applicative m => String -> [m Doc]
pwords String
"must be a defined name"

    BuiltinMustBeFunction BuiltinId
s -> [m Doc] -> m Doc
forall (m :: * -> *) (t :: * -> *).
(Applicative m, Foldable t) =>
t (m Doc) -> m Doc
fsep ([m Doc] -> m Doc) -> [m Doc] -> m Doc
forall a b. (a -> b) -> a -> b
$
      String -> [m Doc]
forall (m :: * -> *). Applicative m => String -> [m Doc]
pwords String
"Builtin" [m Doc] -> [m Doc] -> [m Doc]
forall a. [a] -> [a] -> [a]
++ [BuiltinId -> m Doc
forall (m :: * -> *) a. (Applicative m, Pretty a) => a -> m Doc
pretty BuiltinId
s] [m Doc] -> [m Doc] -> [m Doc]
forall a. [a] -> [a] -> [a]
++ String -> [m Doc]
forall (m :: * -> *). Applicative m => String -> [m Doc]
pwords String
"must be bound to a function"

    BuiltinMustBePostulate BuiltinId
s -> [m Doc] -> m Doc
forall (m :: * -> *) (t :: * -> *).
(Applicative m, Foldable t) =>
t (m Doc) -> m Doc
fsep ([m Doc] -> m Doc) -> [m Doc] -> m Doc
forall a b. (a -> b) -> a -> b
$
      String -> [m Doc]
forall (m :: * -> *). Applicative m => String -> [m Doc]
pwords String
"The argument to BUILTIN" [m Doc] -> [m Doc] -> [m Doc]
forall a. [a] -> [a] -> [a]
++ [BuiltinId -> m Doc
forall (m :: * -> *) a. (Applicative m, Pretty a) => a -> m Doc
pretty BuiltinId
s] [m Doc] -> [m Doc] -> [m Doc]
forall a. [a] -> [a] -> [a]
++ String -> [m Doc]
forall (m :: * -> *). Applicative m => String -> [m Doc]
pwords String
"must be a postulated name"

    NoSuchBuiltinName ShortText
s -> [m Doc] -> m Doc
forall (m :: * -> *) (t :: * -> *).
(Applicative m, Foldable t) =>
t (m Doc) -> m Doc
fsep ([m Doc] -> m Doc) -> [m Doc] -> m Doc
forall a b. (a -> b) -> a -> b
$
      String -> [m Doc]
forall (m :: * -> *). Applicative m => String -> [m Doc]
pwords String
"There is no built-in thing called" [m Doc] -> [m Doc] -> [m Doc]
forall a. [a] -> [a] -> [a]
++ [ShortText -> m Doc
forall (m :: * -> *) a. (Applicative m, Pretty a) => a -> m Doc
pretty ShortText
s]

    InvalidBuiltin String
s -> String -> m Doc
forall (m :: * -> *). Applicative m => String -> m Doc
fwords String
s

    DuplicateBuiltinBinding BuiltinId
b Term
x Term
y -> [m Doc] -> m Doc
forall (m :: * -> *) (t :: * -> *).
(Applicative m, Foldable t) =>
t (m Doc) -> m Doc
fsep ([m Doc] -> m Doc) -> [m Doc] -> m Doc
forall a b. (a -> b) -> a -> b
$
      String -> [m Doc]
forall (m :: * -> *). Applicative m => String -> [m Doc]
pwords String
"Duplicate binding for built-in thing" [m Doc] -> [m Doc] -> [m Doc]
forall a. [a] -> [a] -> [a]
++ [BuiltinId -> m Doc
forall (m :: * -> *) a. (Applicative m, Pretty a) => a -> m Doc
pretty BuiltinId
b m Doc -> m Doc -> m Doc
forall a. Semigroup a => a -> a -> a
<> m Doc
forall (m :: * -> *). Applicative m => m Doc
comma] [m Doc] -> [m Doc] -> [m Doc]
forall a. [a] -> [a] -> [a]
++
      String -> [m Doc]
forall (m :: * -> *). Applicative m => String -> [m Doc]
pwords String
"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
forall (m :: * -> *). MonadPretty m => Term -> m Doc
prettyTCM Term
x]

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

    NoBindingForPrimitive PrimitiveId
x -> [m Doc] -> m Doc
forall (m :: * -> *) (t :: * -> *).
(Applicative m, Foldable t) =>
t (m Doc) -> m Doc
fsep ([m Doc] -> m Doc) -> [m Doc] -> m Doc
forall a b. (a -> b) -> a -> b
$
      String -> [m Doc]
forall (m :: * -> *). Applicative m => String -> [m Doc]
pwords String
"Missing binding for" [m Doc] -> [m Doc] -> [m Doc]
forall a. [a] -> [a] -> [a]
++
      [PrimitiveId -> m Doc
forall (m :: * -> *) a. (Applicative m, Pretty a) => a -> m Doc
pretty PrimitiveId
x] [m Doc] -> [m Doc] -> [m Doc]
forall a. [a] -> [a] -> [a]
++
      String -> [m Doc]
forall (m :: * -> *). Applicative m => String -> [m Doc]
pwords String
"primitive."

    DuplicatePrimitiveBinding PrimitiveId
b QName
x QName
y -> [m Doc] -> m Doc
forall (m :: * -> *) (t :: * -> *).
(Applicative m, Foldable t) =>
t (m Doc) -> m Doc
fsep ([m Doc] -> m Doc) -> [m Doc] -> m Doc
forall a b. (a -> b) -> a -> b
$
      String -> [m Doc]
forall (m :: * -> *). Applicative m => String -> [m Doc]
pwords String
"Duplicate binding for primitive thing" [m Doc] -> [m Doc] -> [m Doc]
forall a. [a] -> [a] -> [a]
++ [PrimitiveId -> m Doc
forall (m :: * -> *) a. (Applicative m, Pretty a) => a -> m Doc
pretty PrimitiveId
b m Doc -> m Doc -> m Doc
forall a. Semigroup a => a -> a -> a
<> m Doc
forall (m :: * -> *). Applicative m => m Doc
comma] [m Doc] -> [m Doc] -> [m Doc]
forall a. [a] -> [a] -> [a]
++
      String -> [m Doc]
forall (m :: * -> *). Applicative m => String -> [m Doc]
pwords String
"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
forall (m :: * -> *). MonadPretty m => QName -> m Doc
prettyTCM QName
x]

    NoSuchPrimitiveFunction ShortText
x -> [m Doc] -> m Doc
forall (m :: * -> *) (t :: * -> *).
(Applicative m, Foldable t) =>
t (m Doc) -> m Doc
fsep ([m Doc] -> m Doc) -> [m Doc] -> m Doc
forall a b. (a -> b) -> a -> b
$
      String -> [m Doc]
forall (m :: * -> *). Applicative m => String -> [m Doc]
pwords String
"There is no primitive function called" [m Doc] -> [m Doc] -> [m Doc]
forall a. [a] -> [a] -> [a]
++ [String -> m Doc
forall (m :: * -> *). Applicative m => String -> m Doc
text (ShortText -> String
TS.unpack ShortText
x)]

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

    IllegalLetInTelescope TypedBinding
tb -> [m Doc] -> m Doc
forall (m :: * -> *) (t :: * -> *).
(Applicative m, Foldable t) =>
t (m Doc) -> m Doc
fsep ([m Doc] -> m Doc) -> [m Doc] -> m Doc
forall a b. (a -> b) -> a -> b
$
      -- pwords "The binding" ++
      TypedBinding -> m Doc
forall (m :: * -> *) a. (Applicative 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 :: * -> *). Applicative m => String -> [m Doc]
pwords String
" is not allowed in a telescope here."

    IllegalPatternInTelescope Binder
bd -> [m Doc] -> m Doc
forall (m :: * -> *) (t :: * -> *).
(Applicative m, Foldable t) =>
t (m Doc) -> m Doc
fsep ([m Doc] -> m Doc) -> [m Doc] -> m Doc
forall a b. (a -> b) -> a -> b
$
      Binder -> m Doc
forall (m :: * -> *) a. (Applicative 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 :: * -> *). Applicative m => String -> [m Doc]
pwords String
" is not allowed in a telescope here."

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

    LibraryError LibErrors
err -> Doc -> m Doc
forall a. a -> m a
forall (m :: * -> *) a. Monad m => a -> m a
return (Doc -> m Doc) -> Doc -> m Doc
forall a b. (a -> b) -> a -> b
$ LibErrors -> Doc
formatLibErrors LibErrors
err

    LibTooFarDown TopLevelModuleName
m AgdaLibFile
lib -> [m Doc] -> m Doc
forall (m :: * -> *) (t :: * -> *).
(Applicative m, Foldable t) =>
t (m Doc) -> m Doc
vcat
      [ String -> m Doc
forall (m :: * -> *). Applicative m => String -> m Doc
text String
"An .agda-lib file for" m Doc -> m Doc -> m Doc
forall (m :: * -> *). Applicative m => m Doc -> m Doc -> m Doc
<+> TopLevelModuleName -> m Doc
forall (m :: * -> *) a. (Applicative m, Pretty a) => a -> m Doc
pretty TopLevelModuleName
m
      , String -> m Doc
forall (m :: * -> *). Applicative m => String -> m Doc
text String
"must not be located in the directory" m Doc -> m Doc -> m Doc
forall (m :: * -> *). Applicative m => m Doc -> m Doc -> m Doc
<+> String -> m Doc
forall (m :: * -> *). Applicative m => String -> m Doc
text (String -> String
takeDirectory (AgdaLibFile
lib AgdaLibFile -> Getting String AgdaLibFile String -> String
forall s a. s -> Getting a s a -> a
^. Getting String AgdaLibFile String
Lens' AgdaLibFile String
libFile))
      ]

    SolvedButOpenHoles TopLevelModuleNameWithSourceFile
x -> do
      [m Doc] -> m Doc
forall (m :: * -> *) (t :: * -> *).
(Applicative m, Foldable t) =>
t (m Doc) -> m Doc
vcat ([m Doc] -> m Doc) -> [m Doc] -> m Doc
forall a b. (a -> b) -> a -> b
$
        [ [m Doc] -> m Doc
forall (m :: * -> *) (t :: * -> *).
(Applicative m, Foldable t) =>
t (m Doc) -> m Doc
fsep ([m Doc] -> m Doc) -> [m Doc] -> m Doc
forall a b. (a -> b) -> a -> b
$ TopLevelModuleNameWithSourceFile -> m Doc
forall a (m :: * -> *). (PrettyTCM a, MonadPretty m) => a -> m Doc
forall (m :: * -> *).
MonadPretty m =>
TopLevelModuleNameWithSourceFile -> m Doc
prettyTCM TopLevelModuleNameWithSourceFile
x m Doc -> [m Doc] -> [m Doc]
forall a. a -> [a] -> [a]
:
            String -> [m Doc]
forall (m :: * -> *). Applicative m => String -> [m Doc]
pwords String
"cannot be imported since it has open interaction points"
        , m Doc
"(consider adding {-# OPTIONS --allow-unsolved-metas #-} to that module)"
        ]

    CyclicModuleDependency List2 TopLevelModuleName
ms0 -> do
      completer <- m (TopLevelModuleName -> TopLevelModuleNameWithSourceFile)
forall (m :: * -> *).
ReadTCState m =>
m (TopLevelModuleName -> TopLevelModuleNameWithSourceFile)
topLevelModuleNameWithSourceFileCompleter
      let List2 m0 m1 ms = completer <$> ms0
      fsep (pwords "cyclic module dependency:")
        $$ nest 2 (vcat $ (prettyTCM m0 :) $ map (("importing" <+>) . prettyTCM) (m1 : ms))

    FileNotFound TopLevelModuleName
x List1 AbsolutePath
dirs ->
      [m Doc] -> m Doc
forall (m :: * -> *) (t :: * -> *).
(Applicative m, Foldable t) =>
t (m Doc) -> m Doc
fsep ( String -> [m Doc]
forall (m :: * -> *). Applicative m => String -> [m Doc]
pwords String
"Failed to find source of module" [m Doc] -> [m Doc] -> [m Doc]
forall a. [a] -> [a] -> [a]
++ [TopLevelModuleName -> m Doc
forall (m :: * -> *) a. (Applicative 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 :: * -> *). Applicative m => String -> [m Doc]
pwords String
"in any of the following locations:"
           ) m Doc -> m Doc -> m Doc
forall (m :: * -> *). Applicative m => m Doc -> m Doc -> m Doc
$$ TopLevelModuleName -> List1 AbsolutePath -> m Doc
forall (m :: * -> *).
MonadPretty m =>
TopLevelModuleName -> List1 AbsolutePath -> m Doc
prettyPossibleFilesForModule TopLevelModuleName
x List1 AbsolutePath
dirs

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

    AmbiguousTopLevelModuleName TopLevelModuleName
x List2 AbsolutePath
files ->
      [m Doc] -> m Doc
forall (m :: * -> *) (t :: * -> *).
(Applicative m, Foldable t) =>
t (m Doc) -> m Doc
fsep ( String -> [m Doc]
forall (m :: * -> *). Applicative m => String -> [m Doc]
pwords String
"Ambiguous module name. The module name" [m Doc] -> [m Doc] -> [m Doc]
forall a. [a] -> [a] -> [a]
++
             [TopLevelModuleName -> m Doc
forall (m :: * -> *) a. (Applicative 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 :: * -> *). Applicative m => String -> [m Doc]
pwords String
"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 Int
2 (List2 (m Doc) -> m Doc
forall (m :: * -> *) (t :: * -> *).
(Applicative m, Foldable t) =>
t (m Doc) -> m Doc
vcat (List2 (m Doc) -> m Doc) -> List2 (m Doc) -> m Doc
forall a b. (a -> b) -> a -> b
$ (AbsolutePath -> m Doc) -> List2 AbsolutePath -> List2 (m Doc)
forall a b. (a -> b) -> List2 a -> List2 b
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap (String -> m Doc
forall (m :: * -> *). Applicative 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) List2 AbsolutePath
files)

    AmbiguousProjection QName
d List1 QName
disambs -> [m Doc] -> m Doc
forall (m :: * -> *) (t :: * -> *).
(Applicative m, Foldable t) =>
t (m Doc) -> m Doc
vcat
      [ m Doc
"Ambiguous projection " 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
forall (m :: * -> *). MonadPretty m => QName -> m Doc
prettyTCM QName
d m Doc -> m Doc -> m Doc
forall a. Semigroup a => a -> a -> a
<> m Doc
"."
      , m Doc
"It could refer to any of"
      , Int -> m Doc -> m Doc
forall (m :: * -> *). Functor m => Int -> m Doc -> m Doc
nest Int
2 (m Doc -> m Doc) -> m Doc -> m Doc
forall a b. (a -> b) -> a -> b
$ List2 (m Doc) -> m Doc
forall (m :: * -> *) (t :: * -> *).
(Applicative m, Foldable t) =>
t (m Doc) -> m Doc
vcat (List2 (m Doc) -> m Doc) -> List2 (m Doc) -> m Doc
forall a b. (a -> b) -> a -> b
$ (QName -> m Doc) -> List2 QName -> List2 (m Doc)
forall a b. (a -> b) -> List2 a -> List2 b
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap QName -> m Doc
forall (m :: * -> *). MonadPretty m => QName -> m Doc
prettyDisambProj (List2 QName -> List2 (m Doc)) -> List2 QName -> List2 (m Doc)
forall a b. (a -> b) -> a -> b
$ QName -> List1 QName -> List2 QName
forall a. a -> List1 a -> List2 a
List2.cons QName
d List1 QName
disambs
      ]

    AmbiguousOverloadedProjection AmbiguousQName
ds Doc
reason -> do
      let
        x :: QName
x = AmbiguousQName -> QName
headAmbQ AmbiguousQName
ds
        nameRaw :: m Doc
nameRaw = Name -> m Doc
forall (m :: * -> *) a. (Applicative m, Pretty a) => a -> m Doc
pretty (Name -> m Doc) -> Name -> m Doc
forall a b. (a -> b) -> a -> b
$ Name -> Name
A.nameConcrete (Name -> Name) -> Name -> Name
forall a b. (a -> b) -> a -> b
$ QName -> Name
A.qnameName QName
x
      [m Doc] -> m Doc
forall (m :: * -> *) (t :: * -> *).
(Applicative m, Foldable t) =>
t (m Doc) -> m Doc
vcat
        [ [m Doc] -> m Doc
forall (m :: * -> *) (t :: * -> *).
(Applicative m, Foldable t) =>
t (m Doc) -> m Doc
fsep
          [ String -> m Doc
forall (m :: * -> *). Applicative m => String -> m Doc
text String
"Cannot resolve overloaded projection"
          , m Doc
nameRaw
          , String -> m Doc
forall (m :: * -> *). Applicative m => String -> m Doc
text String
"because"
          , Doc -> m Doc
forall a. a -> m a
forall (f :: * -> *) a. Applicative f => a -> f a
pure Doc
reason
          ]
        , Int -> m Doc -> m Doc
forall (m :: * -> *). Functor m => Int -> m Doc -> m Doc
nest Int
2 (m Doc -> m Doc) -> m Doc -> m Doc
forall a b. (a -> b) -> a -> b
$ String -> m Doc
forall (m :: * -> *). Applicative m => String -> m Doc
text String
"candidates in scope:"
        , NonEmpty (m Doc) -> m Doc
forall (m :: * -> *) (t :: * -> *).
(Applicative m, Foldable t) =>
t (m Doc) -> m Doc
vcat (NonEmpty (m Doc) -> m Doc) -> NonEmpty (m Doc) -> m Doc
forall a b. (a -> b) -> a -> b
$ AmbiguousQName -> List1 QName
getAmbiguous AmbiguousQName
ds List1 QName -> (QName -> m Doc) -> NonEmpty (m Doc)
forall (f :: * -> *) a b. Functor f => f a -> (a -> b) -> f b
<&> \ QName
d -> do
            t <- QName -> m Type
forall (m :: * -> *).
(HasConstInfo m, ReadTCState m) =>
QName -> m Type
typeOfConst QName
d
            text "-" <+> nest 2 (nameRaw <+> text ":" <+> prettyTCM t)
        -- , vcat . concat $ for (unAmbQ ds) \ d ->
        --     [ text "-" <+> nest 2 (nameRaw <+> text ":" <+> (prettyTCM =<< typeOfConst (fromAmbQName d))) ]
        --       ++
        --     case d of
        --       AmbQName{} -> []
        --       AmbAbstractName x -> [ nest 2 $ prettyTCM x ]
        , case QName -> AmbiguousQName -> Maybe WhyInScopeData
whyInScopeDataFromAmbiguousQName (QName -> QName
qnameToConcrete QName
x) AmbiguousQName
ds of
            Maybe WhyInScopeData
Nothing -> m Doc
forall a. Null a => a
empty
            Just WhyInScopeData
why -> WhyInScopeData -> m Doc
forall (m :: * -> *). MonadPretty m => WhyInScopeData -> m Doc
explainWhyInScope WhyInScopeData
why
        ]

    AmbiguousConstructor QName
c List2 QName
disambs -> [m Doc] -> m Doc
forall (m :: * -> *) (t :: * -> *).
(Applicative m, Foldable t) =>
t (m Doc) -> m Doc
vcat
      [ m Doc
"Ambiguous constructor " m Doc -> m Doc -> m Doc
forall a. Semigroup a => a -> a -> a
<> Name -> m Doc
forall (m :: * -> *) a. (Applicative m, Pretty a) => a -> m Doc
pretty (QName -> Name
qnameName QName
c) m Doc -> m Doc -> m Doc
forall a. Semigroup a => a -> a -> a
<> m Doc
"."
      , m Doc
"It could refer to any of"
      , Int -> m Doc -> m Doc
forall (m :: * -> *). Functor m => Int -> m Doc -> m Doc
nest Int
2 (m Doc -> m Doc) -> m Doc -> m Doc
forall a b. (a -> b) -> a -> b
$ List2 (m Doc) -> m Doc
forall (m :: * -> *) (t :: * -> *).
(Applicative m, Foldable t) =>
t (m Doc) -> m Doc
vcat (List2 (m Doc) -> m Doc) -> List2 (m Doc) -> m Doc
forall a b. (a -> b) -> a -> b
$ (QName -> m Doc) -> List2 QName -> List2 (m Doc)
forall a b. (a -> b) -> List2 a -> List2 b
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap QName -> m Doc
forall (m :: * -> *). MonadPretty m => QName -> m Doc
prettyDisambCons List2 QName
disambs
      ]

    InvalidFileName AbsolutePath
file InvalidFileNameReason
reason -> [m Doc] -> m Doc
forall (m :: * -> *) (t :: * -> *).
(Applicative m, Foldable t) =>
t (m Doc) -> m Doc
fsep ([m Doc] -> m Doc) -> [m Doc] -> m Doc
forall a b. (a -> b) -> a -> b
$
      String -> [m Doc]
forall (m :: * -> *). Applicative m => String -> [m Doc]
pwords String
"The file name" [m Doc] -> [m Doc] -> [m Doc]
forall a. [a] -> [a] -> [a]
++ [AbsolutePath -> m Doc
forall (m :: * -> *) a. (Applicative m, Pretty a) => a -> m Doc
pretty AbsolutePath
file] [m Doc] -> [m Doc] -> [m Doc]
forall a. [a] -> [a] -> [a]
++ String -> [m Doc]
forall (m :: * -> *). Applicative m => String -> [m Doc]
pwords String
"is invalid because" [m Doc] -> [m Doc] -> [m Doc]
forall a. [a] -> [a] -> [a]
++
      case InvalidFileNameReason
reason of
        InvalidFileNameReason
DoesNotCorrespondToValidModuleName ->
          String -> [m Doc]
forall (m :: * -> *). Applicative m => String -> [m Doc]
pwords String
"it does not correspond to a valid module name."
        RootNameModuleNotAQualifiedModuleName Text
defaultName ->
          Text -> m Doc
forall (m :: * -> *) a. (Applicative m, Pretty a) => a -> m Doc
pretty Text
defaultName m Doc -> [m Doc] -> [m Doc]
forall a. a -> [a] -> [a]
: String -> [m Doc]
forall (m :: * -> *). Applicative m => String -> [m Doc]
pwords String
"is not an unqualified module name."

    ModuleDefinedInOtherFile TopLevelModuleName
mod AbsolutePath
file AbsolutePath
file' -> [m Doc] -> m Doc
forall (m :: * -> *) (t :: * -> *).
(Applicative m, Foldable t) =>
t (m Doc) -> m Doc
fsep ([m Doc] -> m Doc) -> [m Doc] -> m Doc
forall a b. (a -> b) -> a -> b
$ [[m Doc]] -> [m Doc]
forall (t :: * -> *) a. Foldable t => t [a] -> [a]
concat
      [ String -> [m Doc]
forall (m :: * -> *). Applicative m => String -> [m Doc]
pwords String
"You tried to load"
      , [ String -> m Doc
forall (m :: * -> *). Applicative m => String -> m Doc
text (AbsolutePath -> String
filePath AbsolutePath
file) ]
      , if TopLevelModuleName -> Bool
forall range. TopLevelModuleName' range -> Bool
moduleNameInferred TopLevelModuleName
mod
          then String -> [m Doc]
forall (m :: * -> *). Applicative m => String -> [m Doc]
pwords String
"which seems to define the module"
          else String -> [m Doc]
forall (m :: * -> *). Applicative m => String -> [m Doc]
pwords String
"which defines the module"
      , [ TopLevelModuleName -> m Doc
forall (m :: * -> *) a. (Applicative m, Pretty a) => a -> m Doc
pretty TopLevelModuleName
mod m Doc -> m Doc -> m Doc
forall a. Semigroup a => a -> a -> a
<> m Doc
"." ]
      , String -> [m Doc]
forall (m :: * -> *). Applicative m => String -> [m Doc]
pwords String
"However, according to the include path this module should be defined in"
      , [ String -> m Doc
forall (m :: * -> *). Applicative m => String -> m Doc
text (AbsolutePath -> String
filePath AbsolutePath
file') ]
        -- Andreas, 2025-06-21, issue #7953:
        -- We have no test that triggers this hint, not sure it can be triggered at all.
      , if TopLevelModuleName -> Bool
forall range. TopLevelModuleName' range -> Bool
moduleNameInferred TopLevelModuleName
mod then String -> [m Doc]
forall (m :: * -> *). Applicative m => String -> [m Doc]
pwords String
"(Hint: no module header was found in this file; adding one might fix this error.)"
        else [m Doc]
forall a. Null a => a
empty
      ]

    ModuleNameUnexpected TopLevelModuleNameWithSourceFile
given TopLevelModuleName
expected -> do
      let
        canon :: Doc a -> CI String
canon = String -> CI String
forall s. FoldCase s => s -> CI s
CaseInsens.mk (String -> CI String) -> (Doc a -> String) -> Doc a -> CI String
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Doc a -> String
forall a. Doc a -> String
P.render
        dExpected :: Doc
dExpected = TopLevelModuleName -> Doc
forall a. Pretty a => a -> Doc
P.pretty TopLevelModuleName
expected
      dGiven <- TopLevelModuleNameWithSourceFile -> m Doc
forall a (m :: * -> *). (PrettyTCM a, MonadPretty m) => a -> m Doc
forall (m :: * -> *).
MonadPretty m =>
TopLevelModuleNameWithSourceFile -> m Doc
prettyTCM TopLevelModuleNameWithSourceFile
given
      if| canon dGiven == canon dExpected -> fsep $ concat
          [ pwords "Case mismatch between the actual module name"
          , [ pure dGiven ]
          , pwords "and the expected module name"
          , [ pure dExpected ]
          ]
        | otherwise -> fsep $ concat
          [ pwords "The name of the top level module does not match the file name."
          , if moduleNameInferred (fileModuleName given) then
              pwords "The unnamed module" ++
              [ do
                  path <- srcFilePath $ fileModuleSourceFile given
                  let r = AbsolutePath -> Range
rangeFromAbsolutePath AbsolutePath
path
                  parens ("at" <> prettyTCM r)
              ]
            else pwords "The module" ++ [ pure dGiven ]
          , pwords "should probably be named"
          , [ pure dExpected ]
          ]

    ModuleNameHashCollision RawTopLevelModuleName
raw Maybe RawTopLevelModuleName
raw' -> String -> m Doc
forall (m :: * -> *). Applicative m => String -> m Doc
fwords (String -> m Doc) -> String -> m Doc
forall a b. (a -> b) -> a -> b
$ case Maybe RawTopLevelModuleName
raw' of
      Maybe RawTopLevelModuleName
Nothing ->
        String
"The module name " String -> String -> String
forall a. [a] -> [a] -> [a]
++ RawTopLevelModuleName -> String
forall a. Pretty a => a -> String
prettyShow RawTopLevelModuleName
raw String -> String -> String
forall a. [a] -> [a] -> [a]
++ String
" has a reserved " String -> String -> String
forall a. [a] -> [a] -> [a]
++
        String
"hash (you may want to consider renaming the module with this name)"
      Just RawTopLevelModuleName
raw' ->
        String
"Module name hash collision for " String -> String -> String
forall a. [a] -> [a] -> [a]
++ RawTopLevelModuleName -> String
forall a. Pretty a => a -> String
prettyShow RawTopLevelModuleName
raw String -> String -> String
forall a. [a] -> [a] -> [a]
++
        String
" and " String -> String -> String
forall a. [a] -> [a] -> [a]
++ RawTopLevelModuleName -> String
forall a. Pretty a => a -> String
prettyShow RawTopLevelModuleName
raw' String -> String -> String
forall a. [a] -> [a] -> [a]
++ String
" (you may want to consider " String -> String -> String
forall a. [a] -> [a] -> [a]
++
        String
"renaming one of these modules)"

    ModuleNameDoesntMatchFileName TopLevelModuleName
given List1 AbsolutePath
dirs -> [m Doc] -> m Doc
forall (m :: * -> *) (t :: * -> *).
(Applicative m, Foldable t) =>
t (m Doc) -> m Doc
vcat
      [ [m Doc] -> m Doc
forall (m :: * -> *) (t :: * -> *).
(Applicative m, Foldable t) =>
t (m Doc) -> m Doc
fsep ([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
"The" ]
        , [ m Doc
"inferred" | TopLevelModuleName -> Bool
forall range. TopLevelModuleName' range -> Bool
moduleNameInferred TopLevelModuleName
given ]
        , [ m Doc
"name" ]
        , [ m Doc
"`" m Doc -> m Doc -> m Doc
forall a. Semigroup a => a -> a -> a
<> TopLevelModuleName -> m Doc
forall (m :: * -> *) a. (Applicative m, Pretty a) => a -> m Doc
pretty TopLevelModuleName
given m Doc -> m Doc -> m Doc
forall a. Semigroup a => a -> a -> a
<> m Doc
"`"]
        , String -> [m Doc]
forall (m :: * -> *). Applicative m => String -> [m Doc]
pwords String
"of the top level module"
        , String -> [m Doc]
forall (m :: * -> *). Applicative m => String -> [m Doc]
pwords String
"does not match the file name."
        , String -> [m Doc]
forall (m :: * -> *). Applicative m => String -> [m Doc]
pwords String
"A such named module should be defined in one of the following files:"
        ]
      , TopLevelModuleName -> List1 AbsolutePath -> m Doc
forall (m :: * -> *).
MonadPretty m =>
TopLevelModuleName -> List1 AbsolutePath -> m Doc
prettyPossibleFilesForModule TopLevelModuleName
given List1 AbsolutePath
dirs
      , if TopLevelModuleName -> Bool
forall range. TopLevelModuleName' range -> Bool
moduleNameInferred TopLevelModuleName
given then [m Doc] -> m Doc
forall (m :: * -> *) (t :: * -> *).
(Applicative m, Foldable t) =>
t (m Doc) -> m Doc
fsep ([m Doc] -> m Doc) -> [m Doc] -> m Doc
forall a b. (a -> b) -> a -> b
$
          String -> [m Doc]
forall (m :: * -> *). Applicative m => String -> [m Doc]
pwords String
"(Hint: no module header was found in this file; adding one might fix this error.)"
        else m Doc
forall a. Null a => a
empty
      ]

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

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

    CopatternHeadNotProjection QName
x -> [m Doc] -> m Doc
forall (m :: * -> *) (t :: * -> *).
(Applicative m, Foldable t) =>
t (m Doc) -> m Doc
fsep ([m Doc] -> m Doc) -> [m Doc] -> m Doc
forall a b. (a -> b) -> a -> b
$ [[m Doc]] -> [m Doc]
forall (t :: * -> *) a. Foldable t => t [a] -> [a]
concat
      [ String -> [m Doc]
forall (m :: * -> *). Applicative m => String -> [m Doc]
pwords String
"Head of copattern needs to be a projection, but"
      , [ QName -> m Doc
forall a (m :: * -> *). (PrettyTCM a, MonadPretty m) => a -> m Doc
forall (m :: * -> *). MonadPretty m => QName -> m Doc
prettyTCM QName
x ]
      , String -> [m Doc]
forall (m :: * -> *). Applicative m => String -> [m Doc]
pwords String
"isn't one"
      ]

    NotAllowedInDotPatterns NotAllowedInDotPatterns
what -> [m Doc] -> m Doc
forall (m :: * -> *) (t :: * -> *).
(Applicative m, Foldable t) =>
t (m Doc) -> m Doc
fsep ([m Doc] -> m Doc) -> [m Doc] -> m Doc
forall a b. (a -> b) -> a -> b
$ NotAllowedInDotPatterns -> [m Doc]
verb NotAllowedInDotPatterns
what [m Doc] -> [m Doc] -> [m Doc]
forall a. [a] -> [a] -> [a]
++ String -> [m Doc]
forall (m :: * -> *). Applicative m => String -> [m Doc]
pwords String
"are not allowed in dot patterns"
      where
      verb :: NotAllowedInDotPatterns -> [m Doc]
verb = \case
        NotAllowedInDotPatterns
LetExpressions -> String -> [m Doc]
forall (m :: * -> *). Applicative m => String -> [m Doc]
pwords String
"Let expressions"
        NotAllowedInDotPatterns
PatternLambdas -> String -> [m Doc]
forall (m :: * -> *). Applicative m => String -> [m Doc]
pwords String
"Pattern lambdas"

    NotInScope QName
x ->
      -- using the warning version to avoid code duplication
      Warning -> m Doc
forall (m :: * -> *). MonadPretty m => Warning -> m Doc
prettyWarning (Warning -> m Doc) -> Warning -> m Doc
forall a b. (a -> b) -> a -> b
$ QName -> Warning
NotInScopeW QName
x

    NoSuchModule QName
x -> do
      -- Andreas, 2025-10-18, issue #8144
      -- In the situation
      -- @
      --   mutual
      --     record R : Type where ...
      --     open R
      -- @
      -- which desugars to
      -- @
      --   record R : Type
      --   open R
      --   record R where ...
      -- @
      -- we want to give some hint that while record R is defined,
      -- its module R is not defined yet.
      hint <- do
        ExceptT NameResolutionError m ResolvedName
-> m (Either NameResolutionError ResolvedName)
forall e (m :: * -> *) a. ExceptT e m a -> m (Either e a)
runExceptT (KindsOfNames
-> Maybe (Set1 Name)
-> QName
-> ExceptT NameResolutionError m ResolvedName
forall (m :: * -> *).
(ReadTCState m, HasBuiltins m, HasConstInfo m,
 MonadError NameResolutionError m) =>
KindsOfNames -> Maybe (Set1 Name) -> QName -> m ResolvedName
tryResolveName ([KindOfName] -> KindsOfNames
someKindsOfNames [KindOfName
DataName, KindOfName
RecName]) Maybe (Set1 Name)
forall a. Maybe a
Nothing QName
x) m (Either NameResolutionError ResolvedName)
-> (Either NameResolutionError ResolvedName -> m String)
-> m String
forall a b. m a -> (a -> m b) -> m b
forall (m :: * -> *) a b. Monad m => m a -> (a -> m b) -> m b
>>= \case
          Right (DefinedName Access
_ (AbsName QName
y KindOfName
DataName WhyInScope
_ NameMetadata
_) Suffix
_) -> do
            String -> m String
forall a. a -> m a
forall (m :: * -> *) a. Monad m => a -> m a
return String
"---but a data type of that name is in scope whose data module is either not defined yet or hidden"
          Right (DefinedName Access
_ (AbsName QName
y KindOfName
RecName  WhyInScope
_ NameMetadata
_) Suffix
_) -> do
            String -> m String
forall a. a -> m a
forall (m :: * -> *) a. Monad m => a -> m a
return String
"---but a record type of that name is in scope whose record module is either not defined yet or hidden (note that records defined in a `mutual' block cannot be opened in the same block)"
          Either NameResolutionError ResolvedName
_ -> String -> m String
forall a. a -> m a
forall (m :: * -> *) a. Monad m => a -> m a
return String
""
      fsep $ pwords "No module" ++ [pretty x] ++ pwords ("in scope" ++ hint)

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

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

    AmbiguousField Name
field List2 ModuleName
modules -> [m Doc] -> m Doc
forall (m :: * -> *) (t :: * -> *).
(Applicative m, Foldable t) =>
t (m Doc) -> m Doc
vcat ([m Doc] -> m Doc) -> [m Doc] -> m Doc
forall a b. (a -> b) -> a -> b
$
      [m Doc] -> m Doc
forall (m :: * -> *) (t :: * -> *).
(Applicative m, Foldable t) =>
t (m Doc) -> m Doc
hsep [ m Doc
"Ambiguity: the field", Name -> m Doc
forall a (m :: * -> *). (PrettyTCM a, MonadPretty m) => a -> m Doc
forall (m :: * -> *). MonadPretty m => Name -> m Doc
prettyTCM Name
field, m Doc
"appears in the following modules:" ]
      m Doc -> [m Doc] -> [m Doc]
forall a. a -> [a] -> [a]
: (ModuleName -> m Doc) -> [ModuleName] -> [m Doc]
forall a b. (a -> b) -> [a] -> [b]
map ModuleName -> m Doc
forall a (m :: * -> *). (PrettyTCM a, MonadPretty m) => a -> m Doc
forall (m :: * -> *). MonadPretty m => ModuleName -> m Doc
prettyTCM (List2 ModuleName -> [Item (List2 ModuleName)]
forall l. IsList l => l -> [Item l]
List2.toList List2 ModuleName
modules)

    ClashingDefinition QName
x ClashingName
y Maybe NiceDeclaration
suggestion -> [m Doc] -> m Doc
forall (m :: * -> *) (t :: * -> *).
(Applicative m, Foldable t) =>
t (m Doc) -> m Doc
vcat
      [ [m Doc] -> m Doc
forall (m :: * -> *) (t :: * -> *).
(Applicative m, Foldable t) =>
t (m Doc) -> m Doc
fsep ([m Doc] -> m Doc) -> [m Doc] -> m Doc
forall a b. (a -> b) -> a -> b
$ String -> [m Doc]
forall (m :: * -> *). Applicative m => String -> [m Doc]
pwords String
"Multiple definitions of" [m Doc] -> [m Doc] -> [m Doc]
forall a. [a] -> [a] -> [a]
++ [ QName -> m Doc
forall (m :: * -> *) a. (Applicative m, Pretty a) => a -> m Doc
pretty QName
x m Doc -> m Doc -> m Doc
forall a. Semigroup a => a -> a -> a
<> m Doc
"." ] [m Doc] -> [m Doc] -> [m Doc]
forall a. [a] -> [a] -> [a]
++ ClashingName -> [m Doc]
clashingWith ClashingName
y
      , m Doc -> Maybe (m Doc) -> m Doc
forall a. a -> Maybe a -> a
fromMaybe m Doc
forall a. Null a => a
empty (Maybe (m Doc) -> m Doc) -> Maybe (m Doc) -> m Doc
forall a b. (a -> b) -> a -> b
$ (NiceDeclaration -> m Doc)
-> Maybe NiceDeclaration -> Maybe (m Doc)
forall a b. (a -> b) -> Maybe a -> Maybe b
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap NiceDeclaration -> m Doc
forall {m :: * -> *}.
(IsString (m Doc), Semigroup (m Doc), MonadTCEnv m) =>
NiceDeclaration -> m Doc
hint Maybe NiceDeclaration
suggestion
      ]
      where
        clashingWith :: ClashingName -> [m Doc]
clashingWith = \case
          ClashingAbstractName AbstractName
y -> do
            String -> [m Doc]
forall (m :: * -> *). Applicative m => String -> [m Doc]
pwords String
"Previous definition" [m Doc] -> [m Doc] -> [m Doc]
forall a. [a] -> [a] -> [a]
++ [WhyInScopeData -> m Doc
forall (m :: * -> *). MonadPretty m => WhyInScopeData -> m Doc
explainWhyInScope (WhyInScopeData -> m Doc) -> WhyInScopeData -> m Doc
forall a b. (a -> b) -> a -> b
$ QName -> AbstractName -> WhyInScopeData
whyInScopeDataFromAbstractName QName
x AbstractName
y]
          ClashingQName QName
y ->
            String -> [m Doc]
forall (m :: * -> *). Applicative m => String -> [m Doc]
pwords String
"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
forall (m :: * -> *). MonadPretty m => Range -> m Doc
prettyTCM (Range -> m Doc) -> Range -> m Doc
forall a b. (a -> b) -> a -> b
$ QName -> Range
forall a. HasNameBindingSite a => a -> Range
nameBindingSite QName
y]
        hint :: NiceDeclaration -> m Doc
hint NiceDeclaration
d = do
          let dataOrRecord :: m Doc
dataOrRecord = case NiceDeclaration
d of
                NiceDataDef{} -> m Doc
"data"
                NiceRecDef{}  -> m Doc
"record"
                NiceDeclaration
_ -> m Doc
forall a. HasCallStack => a
__IMPOSSIBLE__
          [m Doc] -> m Doc
forall (m :: * -> *) (t :: * -> *).
(Applicative m, Foldable t) =>
t (m Doc) -> m Doc
vcat
            [ m Doc
"Perhaps you meant to write"
            , Int -> m Doc -> m Doc
forall (m :: * -> *). Functor m => Int -> m Doc -> m Doc
nest Int
2 (m Doc
"'" m Doc -> m Doc -> m Doc
forall a. Semigroup a => a -> a -> a
<> List1 Declaration -> m Doc
forall (m :: * -> *) a. (Applicative m, Pretty a) => a -> m Doc
pretty (NiceDeclaration -> List1 Declaration
notSoNiceDeclarations NiceDeclaration
d) m Doc -> m Doc -> m Doc
forall a. Semigroup a => a -> a -> a
<> 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. (Applicative m, Pretty a) => a -> m Doc
pretty (Range -> m Doc) -> (TCEnv -> Range) -> TCEnv -> m Doc
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Getting Range TCEnv Range -> TCEnv -> Range
forall s (m :: * -> *) a. MonadReader s m => Getting a s a -> m a
view Getting Range TCEnv Range
Lens' TCEnv Range
eRange (TCEnv -> m Doc) -> m TCEnv -> m Doc
forall (m :: * -> *) a b. Monad m => (a -> m b) -> m a -> m b
=<< m TCEnv
forall (m :: * -> *). MonadTCEnv m => m TCEnv
askTC)) m Doc -> m Doc -> m Doc
forall a. Semigroup a => a -> a -> a
<> m Doc
"?"
            , [m Doc] -> m Doc
forall (m :: * -> *) (t :: * -> *).
(Applicative m, Foldable t) =>
t (m Doc) -> m Doc
fsep ([m Doc] -> m Doc) -> [m Doc] -> m Doc
forall a b. (a -> b) -> a -> b
$ [[m Doc]] -> [m Doc]
forall (t :: * -> *) a. Foldable t => t [a] -> [a]
concat
              [ [ m Doc
"In", m Doc
dataOrRecord ]
              , String -> [m Doc]
forall (m :: * -> *). Applicative m => String -> [m Doc]
pwords String
"definitions separate from their"
              , [ m Doc
dataOrRecord ]
              , String -> [m Doc]
forall (m :: * -> *). Applicative m => String -> [m Doc]
pwords String
"declaration, the ':' and type must be omitted"
            ] ]

    ClashingModule ModuleName
m1 ModuleName
m2 -> [m Doc] -> m Doc
forall (m :: * -> *) (t :: * -> *).
(Applicative m, Foldable t) =>
t (m Doc) -> m Doc
fsep ([m Doc] -> m Doc) -> [m Doc] -> m Doc
forall a b. (a -> b) -> a -> b
$
      String -> [m Doc]
forall (m :: * -> *). Applicative m => String -> [m Doc]
pwords String
"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
forall (m :: * -> *). MonadPretty m => ModuleName -> m Doc
prettyTCM ModuleName
m1, m Doc
"and", ModuleName -> m Doc
forall a (m :: * -> *). (PrettyTCM a, MonadPretty m) => a -> m Doc
forall (m :: * -> *). MonadPretty m => ModuleName -> m Doc
prettyTCM ModuleName
m2]
      [m Doc] -> [m Doc] -> [m Doc]
forall a. [a] -> [a] -> [a]
++ String -> [m Doc]
forall (m :: * -> *). Applicative m => String -> [m Doc]
pwords String
"clash."

    DuplicateImports QName
m List1 ImportedName
xs ->
      [m Doc] -> m Doc
forall (m :: * -> *) (t :: * -> *).
(Applicative m, Foldable t) =>
t (m Doc) -> m Doc
fsep (String -> [m Doc]
forall (m :: * -> *). Applicative m => String -> [m Doc]
pwords String
"Ambiguous imports from module" [m Doc] -> [m Doc] -> [m Doc]
forall a. [a] -> [a] -> [a]
++ [QName -> m Doc
forall (m :: * -> *) a. (Applicative m, Pretty a) => a -> m Doc
pretty QName
m] [m Doc] -> [m Doc] -> [m Doc]
forall a. [a] -> [a] -> [a]
++ String -> [m Doc]
forall (m :: * -> *). Applicative m => String -> [m Doc]
pwords String
"for identifiers:")
      m Doc -> m Doc -> m Doc
forall (m :: * -> *). Applicative m => m Doc -> m Doc -> m Doc
<?> [m Doc] -> m Doc
forall (m :: * -> *) (t :: * -> *).
(Applicative m, Foldable t) =>
t (m Doc) -> m Doc
fsep (m Doc -> NonEmpty (m Doc) -> [m Doc]
forall (m :: * -> *) (t :: * -> *).
(Applicative m, Semigroup (m Doc), Foldable t) =>
m Doc -> t (m Doc) -> [m Doc]
punctuate m Doc
";" (NonEmpty (m Doc) -> [m Doc]) -> NonEmpty (m Doc) -> [m Doc]
forall a b. (a -> b) -> a -> b
$ (ImportedName -> m Doc) -> List1 ImportedName -> NonEmpty (m Doc)
forall a b. (a -> b) -> NonEmpty a -> NonEmpty b
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap ImportedName -> m Doc
forall (m :: * -> *) a. (Applicative m, Pretty a) => a -> m Doc
pretty List1 ImportedName
xs)
        -- Andreas, 2026-02-14 punctuate with semicolon since xs may contain "module M" or even ","

    DefinitionInDifferentModule QName
_x -> [m Doc] -> m Doc
forall (m :: * -> *) (t :: * -> *).
(Applicative m, Foldable t) =>
t (m Doc) -> m Doc
fsep ([m Doc] -> m Doc) -> [m Doc] -> m Doc
forall a b. (a -> b) -> a -> b
$
      String -> [m Doc]
forall (m :: * -> *). Applicative m => String -> [m Doc]
pwords String
"Definition in different module than its type signature"

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

    InvalidPun ConstructorOrPatternSynonym
kind QName
x -> [m Doc] -> m Doc
forall (m :: * -> *) (t :: * -> *).
(Applicative m, Foldable t) =>
t (m Doc) -> m Doc
fsep ([m Doc] -> m Doc) -> [m Doc] -> m Doc
forall a b. (a -> b) -> a -> b
$ [[m Doc]] -> [m Doc]
forall (t :: * -> *) a. Foldable t => t [a] -> [a]
concat
      [ String -> [m Doc]
forall (m :: * -> *). Applicative m => String -> [m Doc]
pwords String
"A pun must not use the"
      , [ Doc -> m Doc
forall a. a -> m a
forall (f :: * -> *) a. Applicative f => a -> f a
pure (Doc -> m Doc) -> Doc -> m Doc
forall a b. (a -> b) -> a -> b
$ ConstructorOrPatternSynonym -> Doc
forall a. Pretty a => a -> Doc
P.pretty ConstructorOrPatternSynonym
kind ]
      , [ QName -> m Doc
forall a (m :: * -> *). (PrettyTCM a, MonadPretty m) => a -> m Doc
forall (m :: * -> *). MonadPretty m => QName -> m Doc
prettyTCM QName
x ]
      ]

    RepeatedVariablesInPattern List1 Name
xs -> [m Doc] -> m Doc
forall (m :: * -> *) (t :: * -> *).
(Applicative m, Foldable t) =>
t (m Doc) -> m Doc
fsep ([m Doc] -> m Doc) -> [m Doc] -> m Doc
forall a b. (a -> b) -> a -> b
$
      String -> [m Doc]
forall (m :: * -> *). Applicative m => String -> [m Doc]
pwords String
"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. (Applicative m, Pretty a) => a -> m Doc
pretty (List1 Name -> [Item (List1 Name)]
forall l. IsList l => l -> [Item l]
List1.toList List1 Name
xs)

    RepeatedNamesInImportDirective List1 (List2 ImportedName)
yss ->
      ([m Doc] -> m Doc
forall (m :: * -> *) (t :: * -> *).
(Applicative m, Foldable t) =>
t (m Doc) -> m Doc
fsep ([m Doc] -> m Doc) -> ([[m Doc]] -> [m Doc]) -> [[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
"Repeated" , List1 (List2 ImportedName) -> m Doc -> m Doc
forall (m :: * -> *) a. (Functor m, Sized a) => a -> m Doc -> m Doc
pluralS List1 (List2 ImportedName)
yss m Doc
"name" ]
         , String -> [m Doc]
forall (m :: * -> *). Applicative m => String -> [m Doc]
pwords String
"in import directive:"
         ]
      m Doc -> m Doc -> m Doc
forall (m :: * -> *). Applicative m => m Doc -> m Doc -> m Doc
<?> [m Doc] -> m Doc
forall (m :: * -> *) (t :: * -> *).
(Applicative m, Foldable t) =>
t (m Doc) -> m Doc
fsep (m Doc -> NonEmpty (m Doc) -> [m Doc]
forall (m :: * -> *) (t :: * -> *).
(Applicative m, Semigroup (m Doc), Foldable t) =>
m Doc -> t (m Doc) -> [m Doc]
punctuate m Doc
";" (NonEmpty (m Doc) -> [m Doc]) -> NonEmpty (m Doc) -> [m Doc]
forall a b. (a -> b) -> a -> b
$ (List2 ImportedName -> m Doc)
-> List1 (List2 ImportedName) -> NonEmpty (m Doc)
forall a b. (a -> b) -> NonEmpty a -> NonEmpty b
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap (ImportedName -> m Doc
forall a (m :: * -> *). (PrettyTCM a, MonadPretty m) => a -> m Doc
forall (m :: * -> *). MonadPretty m => ImportedName -> m Doc
prettyTCM (ImportedName -> m Doc)
-> (List2 ImportedName -> ImportedName)
-> List2 ImportedName
-> m Doc
forall b c a. (b -> c) -> (a -> b) -> a -> c
. List2 ImportedName -> ImportedName
forall a. List2 a -> a
List2.head) List1 (List2 ImportedName)
yss)
        -- Andreas, 2026-02-14 punctuate with semicolon since list may contain "module M" or even ","

    TypeError
DeclarationsAfterTopLevelModule -> String -> m Doc
forall (m :: * -> *). Applicative m => String -> m Doc
fwords (String -> m Doc) -> String -> m Doc
forall a b. (a -> b) -> a -> b
$ String
"No declarations allowed after top-level module."

    TypeError
IllegalDeclarationBeforeTopLevelModule -> String -> m Doc
forall (m :: * -> *). Applicative m => String -> m Doc
fwords (String -> m Doc) -> String -> m Doc
forall a b. (a -> b) -> a -> b
$ String
"Illegal declaration(s) before top-level module"

    MissingTypeSignature MissingTypeSignatureInfo
info -> String -> m Doc
forall (m :: * -> *). Applicative m => String -> m Doc
fwords String
"Missing type signature for" m Doc -> m Doc -> m Doc
forall (m :: * -> *). Applicative m => m Doc -> m Doc -> m Doc
<+> MissingTypeSignatureInfo -> m Doc
forall a (m :: * -> *). (PrettyTCM a, MonadPretty m) => a -> m Doc
forall (m :: * -> *).
MonadPretty m =>
MissingTypeSignatureInfo -> m Doc
prettyTCM MissingTypeSignatureInfo
info

    NotAnExpression Expr
e -> [m Doc] -> m Doc
forall (m :: * -> *) (t :: * -> *).
(Applicative m, Foldable t) =>
t (m Doc) -> m Doc
fsep ([m Doc] -> m Doc) -> [m Doc] -> m Doc
forall a b. (a -> b) -> a -> b
$
      Expr -> m Doc
forall (m :: * -> *) a. (Applicative 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 :: * -> *). Applicative m => String -> [m Doc]
pwords String
"is not a valid expression."

    NotAValidLetBinding Maybe NotAValidLetBinding
Nothing -> String -> m Doc
forall (m :: * -> *). Applicative m => String -> m Doc
fwords (String -> m Doc) -> String -> m Doc
forall a b. (a -> b) -> a -> b
$ String
"Not a valid let binding"
    NotAValidLetBinding (Just NotAValidLetBinding
err) -> String -> m Doc
forall (m :: * -> *). Applicative m => String -> m Doc
fwords (String -> m Doc) -> String -> m Doc
forall a b. (a -> b) -> a -> b
$ NotAValidLetBinding -> String
verbalizeNotAValidLetBinding NotAValidLetBinding
err

    NotAValidLetExpression NotAValidLetExpression
err -> String -> m Doc
forall (m :: * -> *). Applicative m => String -> m Doc
fwords (String -> m Doc) -> String -> m Doc
forall a b. (a -> b) -> a -> b
$ NotAValidLetExpression -> String
verbalizeNotAValidLetExpression NotAValidLetExpression
err

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

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

        pretty' :: C.Expr -> m Doc
        pretty' :: Expr -> m Doc
pretty' Expr
e = do
          p1 <- m Doc
pretty_es
          p2 <- pretty e
          if render p1 == render p2 then unambiguous e else return p2

        unambiguous :: C.Expr -> m Doc
        unambiguous :: Expr -> m Doc
unambiguous e :: Expr
e@(C.OpApp Range
r QName
op Set1 Name
_ OpAppArgs
xs)
          | (NamedArg (MaybePlaceholder (OpApp Expr)) -> Bool)
-> OpAppArgs -> 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) OpAppArgs
xs =
            Expr -> m Doc
forall (m :: * -> *) a. (Applicative 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 -> NonEmpty (NamedArg Expr) -> Expr
forall b a. (b -> a -> b) -> b -> NonEmpty a -> b
forall (t :: * -> *) b a.
Foldable t =>
(b -> a -> b) -> b -> t a -> b
foldl (Range -> Expr -> NamedArg Expr -> Expr
C.App Range
r) (QName -> Expr
C.Ident QName
op) (NonEmpty (NamedArg Expr) -> Expr)
-> NonEmpty (NamedArg Expr) -> Expr
forall a b. (a -> b) -> a -> b
$
                ((NamedArg (MaybePlaceholder (OpApp Expr)) -> NamedArg Expr)
-> OpAppArgs -> NonEmpty (NamedArg Expr)
forall a b. (a -> b) -> NonEmpty a -> NonEmpty b
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap ((NamedArg (MaybePlaceholder (OpApp Expr)) -> NamedArg Expr)
 -> OpAppArgs -> NonEmpty (NamedArg Expr))
-> ((MaybePlaceholder (OpApp Expr) -> Expr)
    -> NamedArg (MaybePlaceholder (OpApp Expr)) -> NamedArg Expr)
-> (MaybePlaceholder (OpApp Expr) -> Expr)
-> OpAppArgs
-> NonEmpty (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 a b. (a -> b) -> Arg a -> Arg b
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 a b. (a -> b) -> Named NamedName a -> Named NamedName b
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap) MaybePlaceholder (OpApp Expr) -> Expr
forall e. MaybePlaceholder (OpApp e) -> e
fromOrdinary OpAppArgs
xs
          | (NamedArg (MaybePlaceholder (OpApp Expr)) -> Bool)
-> OpAppArgs -> 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) OpAppArgs
xs =
              Expr -> m Doc
forall (m :: * -> *) a. (Applicative 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
<+> m Doc
"(section)"
        unambiguous Expr
e = Expr -> m Doc
forall (m :: * -> *) a. (Applicative m, Pretty a) => a -> m Doc
pretty Expr
e

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

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

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


    NoParseForLHS LHSOrPatSyn
lhsOrPatSyn [Pattern]
errs Pattern
p -> [m Doc] -> m Doc
forall (m :: * -> *) (t :: * -> *).
(Applicative m, Foldable t) =>
t (m Doc) -> m Doc
vcat
      [ [m Doc] -> m Doc
forall (m :: * -> *) (t :: * -> *).
(Applicative m, Foldable t) =>
t (m Doc) -> m Doc
fsep ([m Doc] -> m Doc) -> [m Doc] -> m Doc
forall a b. (a -> b) -> a -> b
$ String -> [m Doc]
forall (m :: * -> *). Applicative m => String -> [m Doc]
pwords String
"Could not parse the" [m Doc] -> [m Doc] -> [m Doc]
forall a. [a] -> [a] -> [a]
++ [m Doc]
prettyLhsOrPatSyn [m Doc] -> [m Doc] -> [m Doc]
forall a. [a] -> [a] -> [a]
++ [Pattern -> m Doc
forall (m :: * -> *) a. (Applicative m, Pretty a) => a -> m Doc
pretty Pattern
p]
      , m Doc
prettyErrs
      ]
      where
      prettyLhsOrPatSyn :: [m Doc]
prettyLhsOrPatSyn = String -> [m Doc]
forall (m :: * -> *). Applicative m => String -> [m Doc]
pwords (String -> [m Doc]) -> String -> [m Doc]
forall a b. (a -> b) -> a -> b
$ case LHSOrPatSyn
lhsOrPatSyn of
        LHSOrPatSyn
IsLHS    -> String
"left-hand side"
        LHSOrPatSyn
IsPatSyn -> String
"pattern synonym right-hand side"
      prettyErrs :: m Doc
prettyErrs = case [Pattern]
errs of
        []     -> m Doc
forall a. Null a => a
empty
        Pattern
p0 : [Pattern]
_ -> [m Doc] -> m Doc
forall (m :: * -> *) (t :: * -> *).
(Applicative m, Foldable t) =>
t (m Doc) -> m Doc
fsep ([m Doc] -> m Doc) -> [m Doc] -> m Doc
forall a b. (a -> b) -> a -> b
$ String -> [m Doc]
forall (m :: * -> *). Applicative m => String -> [m Doc]
pwords String
"Problematic expression:" [m Doc] -> [m Doc] -> [m Doc]
forall a. [a] -> [a] -> [a]
++ [Pattern -> m Doc
forall (m :: * -> *) a. (Applicative m, Pretty a) => a -> m Doc
pretty Pattern
p0]

    AmbiguousParseForLHS LHSOrPatSyn
lhsOrPatSyn Pattern
p List2 Pattern
ps -> do
      d <- Pattern -> m Doc
forall (m :: * -> *) a. (Applicative m, Pretty a) => a -> m Doc
pretty Pattern
p
      vcat $
        [ fsep $
            pwords "Don't know how to parse" ++ [pure d <> "."] ++
            pwords "Could mean any one of:"
        ]
          ++
        map (nest 2 . pretty' d) (List2.toList ps)
      where
        pretty' :: Doc -> C.Pattern -> m Doc
        pretty' :: Doc -> Pattern -> m Doc
pretty' Doc
d1 Pattern
p' = do
          d2 <- Pattern -> m Doc
forall (m :: * -> *) a. (Applicative m, Pretty a) => a -> m Doc
pretty Pattern
p'
          if render d1 == render d2 then pretty $ unambiguousP p' else return d2

        -- the entire pattern is shown, not just the ambiguous part,
        -- so we need to dig in order to find the OpAppP's.
        unambiguousP :: C.Pattern -> C.Pattern
        unambiguousP :: Pattern -> Pattern
unambiguousP (C.AppP Pattern
x 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 a b. (a -> b) -> Arg a -> Arg b
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 a b. (a -> b) -> Named NamedName a -> Named NamedName b
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap) Pattern -> Pattern
unambiguousP NamedArg Pattern
y
        unambiguousP (C.HiddenP Range
r 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 a b. (a -> b) -> Named NamedName a -> Named NamedName b
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap Pattern -> Pattern
unambiguousP Named NamedName Pattern
x
        unambiguousP (C.InstanceP Range
r Named NamedName Pattern
x)    = Range -> Named NamedName Pattern -> Pattern
C.InstanceP Range
r (Named NamedName Pattern -> Pattern)
-> Named NamedName Pattern -> Pattern
forall a b. (a -> b) -> a -> b
$ (Pattern -> Pattern)
-> Named NamedName Pattern -> Named NamedName Pattern
forall a b. (a -> b) -> Named NamedName a -> Named NamedName b
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap Pattern -> Pattern
unambiguousP Named NamedName Pattern
x
        unambiguousP (C.ParenP Range
r Pattern
x)       = Range -> Pattern -> Pattern
C.ParenP Range
r (Pattern -> Pattern) -> Pattern -> Pattern
forall a b. (a -> b) -> a -> b
$ Pattern -> Pattern
unambiguousP Pattern
x
        unambiguousP (C.AsP Range
r Name
n Pattern
x)        = Range -> Name -> Pattern -> Pattern
C.AsP Range
r Name
n (Pattern -> Pattern) -> Pattern -> Pattern
forall a b. (a -> b) -> a -> b
$ Pattern -> Pattern
unambiguousP Pattern
x
        unambiguousP (C.OpAppP Range
r QName
op Set1 Name
_ List1 (NamedArg Pattern)
xs) = (Pattern -> NamedArg Pattern -> Pattern)
-> Pattern -> List1 (NamedArg Pattern) -> Pattern
forall b a. (b -> a -> b) -> b -> NonEmpty a -> b
forall (t :: * -> *) b a.
Foldable t =>
(b -> a -> b) -> b -> t a -> b
foldl Pattern -> NamedArg Pattern -> Pattern
C.AppP (Bool -> QName -> Pattern
C.IdentP Bool
True QName
op) List1 (NamedArg Pattern)
xs
        unambiguousP Pattern
e                    = Pattern
e

    OperatorInformation [NotationSection]
sects (OpScope Bool
_ Map QName (List1 AbstractName)
globals AssocList Name Name
locals) TypeError
err ->
      TypeError -> m Doc
forall a (m :: * -> *). (PrettyTCM a, MonadPretty m) => a -> m Doc
forall (m :: * -> *). MonadPretty m => TypeError -> 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 :: * -> *) (t :: * -> *).
(Applicative m, Foldable t) =>
t (m Doc) -> m Doc
fsep (String -> [m Doc]
forall (m :: * -> *). Applicative m => String -> [m Doc]
pwords String
"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 Int
2
        (if [NotationSection] -> Bool
forall a. Null a => a -> Bool
null [NotationSection]
sects then m Doc
"None" else
         [m Doc] -> m Doc
forall (m :: * -> *) (t :: * -> *).
(Applicative m, Foldable t) =>
t (m Doc) -> m Doc
vcat ((String -> m Doc) -> [String] -> [m Doc]
forall a b. (a -> b) -> [a] -> [b]
map (String -> m Doc
forall (m :: * -> *). Applicative m => String -> m Doc
text (String -> m Doc) -> (String -> String) -> String -> m Doc
forall b c a. (b -> c) -> (a -> b) -> a -> c
. String -> String
rtrim) ([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
$
               (\([Box]
col1, [Box]
col2, [Box]
col3) ->
                   Int -> Alignment -> [Box] -> Box
forall (f :: * -> *).
Foldable f =>
Int -> Alignment -> f Box -> Box
Boxes.hsep Int
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. Pretty a => a -> String
prettyShow (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]
properSects))
        m Doc -> m Doc -> m Doc
forall (m :: * -> *). Applicative m => m Doc -> m Doc -> m Doc
$$
      if [ShortText] -> Bool
forall a. Null a => a -> Bool
null [ShortText]
relevantSimpleNames then m Doc
forall a. Null a => a
empty else do
        [m Doc] -> m Doc
forall (m :: * -> *) (t :: * -> *).
(Applicative m, Foldable t) =>
t (m Doc) -> m Doc
fsep (String -> [m Doc]
forall (m :: * -> *). Applicative m => String -> [m Doc]
pwords String
"Identifiers used in the grammar that overlap with the operators:")
          m Doc -> m Doc -> m Doc
forall (m :: * -> *). Applicative m => m Doc -> m Doc -> m Doc
$$
          Int -> m Doc -> m Doc
forall (m :: * -> *). Functor m => Int -> m Doc -> m Doc
nest Int
2 ([m Doc] -> m Doc
forall (m :: * -> *) (t :: * -> *).
(Applicative m, Foldable t) =>
t (m Doc) -> m Doc
fsep ((ShortText -> m Doc) -> [ShortText] -> [m Doc]
forall a b. (a -> b) -> [a] -> [b]
map (ShortText -> m Doc
forall (m :: * -> *) a. (Applicative m, Pretty a) => a -> m Doc
pretty) [ShortText]
relevantSimpleNames))

      where
      -- Andreas, 2025-12-17, issue #3677
      -- Prepare a list of names in scope that might clash with the operators.
      -- For now, disregard qualified names.
      relevantSimpleNames :: [ShortText]
relevantSimpleNames = [ShortText] -> [ShortText]
forall a. Ord a => [a] -> [a]
List.sort ([ShortText] -> [ShortText]) -> [ShortText] -> [ShortText]
forall a b. (a -> b) -> a -> b
$ (ShortText -> Bool) -> [ShortText] -> [ShortText]
forall a. (a -> Bool) -> [a] -> [a]
filter ([ShortText] -> ShortText -> Bool
forall a. Ord a => [a] -> a -> Bool
hasElem [ShortText]
operatorParts) [ShortText]
simpleNames
      simpleNames :: [ShortText]
simpleNames =
        (QName -> Maybe ShortText) -> [QName] -> [ShortText]
forall a b. (a -> Maybe b) -> [a] -> [b]
mapMaybe (Name -> Maybe ShortText
C.isSimpleName (Name -> Maybe ShortText)
-> (QName -> Maybe Name) -> QName -> Maybe ShortText
forall (m :: * -> *) b c a.
Monad m =>
(b -> m c) -> (a -> m b) -> a -> m c
<=< QName -> Maybe Name
C.isUnqualified) (Map QName (List1 AbstractName) -> [QName]
forall k a. Map k a -> [k]
Map.keys Map QName (List1 AbstractName)
globals) [ShortText] -> [ShortText] -> [ShortText]
forall a. [a] -> [a] -> [a]
++
        (Name -> Maybe ShortText) -> [Name] -> [ShortText]
forall a b. (a -> Maybe b) -> [a] -> [b]
mapMaybe Name -> Maybe ShortText
C.isSimpleName (AssocList Name Name -> [Name]
forall k v. AssocList k v -> [k]
AssocList.keys AssocList Name Name
locals)
      operatorParts :: [ShortText]
operatorParts = (NotationSection -> [ShortText])
-> [NotationSection] -> [ShortText]
forall (t :: * -> *) a b. Foldable t => (a -> [b]) -> t a -> [b]
concatMap (Notation -> [ShortText]
stringParts (Notation -> [ShortText])
-> (NotationSection -> Notation) -> NotationSection -> [ShortText]
forall b c a. (b -> c) -> (a -> b) -> a -> c
. NewNotation -> Notation
notation (NewNotation -> Notation)
-> (NotationSection -> NewNotation) -> NotationSection -> Notation
forall b c a. (b -> c) -> (a -> b) -> a -> c
. NotationSection -> NewNotation
sectNotation) [NotationSection]
properSects

      properSects :: [NotationSection]
properSects = (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

      trimLeft :: Notation -> Notation
trimLeft  = (NotationPart -> Bool) -> Notation -> Notation
forall a. (a -> Bool) -> [a] -> [a]
dropWhile NotationPart -> Bool
isAHole
      trimRight :: Notation -> Notation
trimRight = (NotationPart -> Bool) -> Notation -> Notation
forall a. (a -> Bool) -> [a] -> [a]
dropWhileEnd NotationPart -> Bool
isAHole

      closedWithoutHoles :: NotationSection -> Bool
closedWithoutHoles 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 [ () | HolePart{} <- Notation -> Notation
trimLeft (Notation -> Notation) -> Notation -> Notation
forall a b. (a -> b) -> a -> b
$ Notation -> Notation
trimRight (Notation -> Notation) -> Notation -> Notation
forall a b. (a -> b) -> a -> b
$
                                    NewNotation -> Notation
notation (NotationSection -> NewNotation
sectNotation NotationSection
sect) ]

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

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

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

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

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

        ([Name]
names, Name
name) = List1 Name -> ([Name], Name)
forall a. List1 a -> ([a], a)
List1.initLast (List1 Name -> ([Name], Name)) -> List1 Name -> ([Name], Name)
forall a b. (a -> b) -> a -> b
$ Set1 Name -> List1 Name
forall a. NESet a -> NonEmpty a
Set1.toList (Set1 Name -> List1 Name) -> Set1 Name -> List1 Name
forall a b. (a -> b) -> a -> b
$ NewNotation -> Set1 Name
notaNames NewNotation
nota

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

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

    ImpossibleConstructor QName
c NegativeUnification
neg -> [m Doc] -> m Doc
forall (m :: * -> *) (t :: * -> *).
(Applicative m, Foldable t) =>
t (m Doc) -> m Doc
fsep ([m Doc] -> m Doc) -> [m Doc] -> m Doc
forall a b. (a -> b) -> a -> b
$
      String -> [m Doc]
forall (m :: * -> *). Applicative m => String -> [m Doc]
pwords String
"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
forall (m :: * -> *). MonadPretty m => QName -> m Doc
prettyTCM QName
c] [m Doc] -> [m Doc] -> [m Doc]
forall a. [a] -> [a] -> [a]
++
      String -> [m Doc]
forall (m :: * -> *). Applicative m => String -> [m Doc]
pwords String
" 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
forall (m :: * -> *). MonadPretty m => NegativeUnification -> m Doc
prettyTCM NegativeUnification
neg] [m Doc] -> [m Doc] -> [m Doc]
forall a. [a] -> [a] -> [a]
++
      String -> [m Doc]
forall (m :: * -> *). Applicative m => String -> [m Doc]
pwords String
"Possible solution: remove the clause, or use an absurd pattern ()."

    DeBruijnIndexOutOfScope Int
i Telescope
EmptyTel [] -> [m Doc] -> m Doc
forall (m :: * -> *) (t :: * -> *).
(Applicative m, Foldable t) =>
t (m Doc) -> m Doc
fsep ([m Doc] -> m Doc) -> [m Doc] -> m Doc
forall a b. (a -> b) -> a -> b
$
        String -> [m Doc]
forall (m :: * -> *). Applicative m => String -> [m Doc]
pwords (String -> [m Doc]) -> String -> [m Doc]
forall a b. (a -> b) -> a -> b
$ String
"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]
++ String
" is not in scope in the empty context"
    DeBruijnIndexOutOfScope Int
i Telescope
cxt [Name]
names ->
        [m Doc] -> m Doc
forall (m :: * -> *) (t :: * -> *).
(Applicative m, Foldable t) =>
t (m Doc) -> m Doc
sep [ String -> m Doc
forall (m :: * -> *). Applicative m => String -> m Doc
text (String
"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]
++ String
" 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
$ ShortText -> m Doc -> m Doc
forall b (m :: * -> *) a.
(AddContext b, MonadAddContext m) =>
b -> m a -> m a
forall (m :: * -> *) a.
MonadAddContext m =>
ShortText -> m a -> m a
addContext (ShortText
"_" :: ShortText) (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
forall (m :: * -> *). MonadPretty m => Telescope -> 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 a. Subst 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 (Name
x : [Name]
xs) = Dom Type -> Abs Telescope -> Telescope
forall a. a -> Abs (Tele a) -> Tele a
ExtendTel (Type -> Dom Type
forall a t. a -> Dom' t 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 Int
0)) (Abs Telescope -> Telescope) -> Abs Telescope -> Telescope
forall a b. (a -> b) -> a -> b
$
          ShortText -> Telescope -> Abs Telescope
forall a. ShortText -> a -> Abs a
Abs (String -> ShortText
TS.pack (String -> ShortText) -> String -> ShortText
forall a b. (a -> b) -> a -> b
$ 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

    MissingBindingsForTelescopeVariables List1 ShortText
xs -> [m Doc] -> m Doc
forall (m :: * -> *) (t :: * -> *).
(Applicative m, Foldable t) =>
t (m Doc) -> m Doc
vcat
      [ [m Doc] -> m Doc
forall (m :: * -> *) (t :: * -> *).
(Applicative m, Foldable t) =>
t (m Doc) -> m Doc
fsep [ m Doc
"Missing", List1 ShortText -> m Doc -> m Doc
forall (m :: * -> *) a. (Functor m, Sized a) => a -> m Doc -> m Doc
pluralS List1 ShortText
xs m Doc
"binding", m Doc
"for", m Doc
"telescope", List1 ShortText -> m Doc -> m Doc
forall (m :: * -> *) a. (Functor m, Sized a) => a -> m Doc -> m Doc
pluralS List1 ShortText
xs m Doc
"variable" m Doc -> m Doc -> m Doc
forall a. Semigroup a => a -> a -> a
<> m Doc
forall (m :: * -> *). Applicative m => m Doc
colon ]
        m Doc -> m Doc -> m Doc
forall (m :: * -> *). Applicative m => m Doc -> m Doc -> m Doc
<?> (NonEmpty (m Doc) -> m Doc
forall (m :: * -> *) (t :: * -> *).
(Applicative m, Foldable t) =>
t (m Doc) -> m Doc
fsep ((ShortText -> m Doc) -> List1 ShortText -> NonEmpty (m Doc)
forall a b. (a -> b) -> NonEmpty a -> NonEmpty b
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap (ShortText -> m Doc
forall (m :: * -> *) a. (Applicative m, Pretty a) => a -> m Doc
pretty) List1 ShortText
xs))
      , m Doc
"All variables in the clause telescope must be bound in the left-hand side."
      ]

    TypeError
NeedOptionAllowExec -> [m Doc] -> m Doc
forall (m :: * -> *) (t :: * -> *).
(Applicative m, Foldable t) =>
t (m Doc) -> m Doc
fsep ([m Doc] -> m Doc) -> [m Doc] -> m Doc
forall a b. (a -> b) -> a -> b
$
      String -> [m Doc]
forall (m :: * -> *). Applicative m => String -> [m Doc]
pwords String
"Option --allow-exec needed to call external commands from macros"

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

    TypeError
NeedOptionPatternMatching -> [m Doc] -> m Doc
forall (m :: * -> *) (t :: * -> *).
(Applicative m, Foldable t) =>
t (m Doc) -> m Doc
fsep ([m Doc] -> m Doc) -> [m Doc] -> m Doc
forall a b. (a -> b) -> a -> b
$
      String -> [m Doc]
forall (m :: * -> *). Applicative m => String -> [m Doc]
pwords String
"Pattern matching is disabled (use option --pattern-matching to enable it)"

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

    CannotGeneralizeEtaExpandable QName
x Type
mt ->
      (m Doc
"Cannot generalize over" m Doc -> m Doc -> m Doc
forall (m :: * -> *). Applicative m => m Doc -> m Doc -> m Doc
<+> QName -> m Doc
forall a (m :: * -> *). (PrettyTCM a, MonadPretty m) => a -> m Doc
forall (m :: * -> *). MonadPretty m => QName -> m Doc
prettyTCM QName
x m Doc -> m Doc -> m Doc
forall (m :: * -> *). Applicative m => m Doc -> m Doc -> m Doc
<+> m Doc
"of eta-expandable type") m Doc -> m Doc -> m Doc
forall (m :: * -> *). Applicative m => m Doc -> m Doc -> m Doc
<?> Type -> m Doc
forall a (m :: * -> *). (PrettyTCM a, MonadPretty m) => a -> m Doc
forall (m :: * -> *). MonadPretty m => Type -> m Doc
prettyTCM Type
mt

    GeneralizeNotSupportedHere QName
x -> [m Doc] -> m Doc
forall (m :: * -> *) (t :: * -> *).
(Applicative m, Foldable t) =>
t (m Doc) -> m Doc
fsep ([m Doc] -> m Doc) -> [m Doc] -> m Doc
forall a b. (a -> b) -> a -> b
$
      String -> [m Doc]
forall (m :: * -> *). Applicative m => String -> [m Doc]
pwords (String -> [m Doc]) -> String -> [m Doc]
forall a b. (a -> b) -> a -> b
$ String
"Generalizable variable " String -> String -> String
forall a. [a] -> [a] -> [a]
++ QName -> String
forall a. Pretty a => a -> String
prettyShow QName
x String -> String -> String
forall a. [a] -> [a] -> [a]
++ String
" is not supported here"

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

    GeneralizedVarInLetOpenedModule QName
x -> [m Doc] -> m Doc
forall (m :: * -> *) (t :: * -> *).
(Applicative m, Foldable t) =>
t (m Doc) -> m Doc
fsep ([m Doc] -> m Doc) -> [m Doc] -> m Doc
forall a b. (a -> b) -> a -> b
$
      String -> [m Doc]
forall (m :: * -> *). Applicative m => String -> [m Doc]
pwords String
"Cannot use generalized variable from let-opened module: " [m Doc] -> [m Doc] -> [m Doc]
forall a. [a] -> [a] -> [a]
++
      [QName -> m Doc
forall a (m :: * -> *). (PrettyTCM a, MonadPretty m) => a -> m Doc
forall (m :: * -> *). MonadPretty m => QName -> m Doc
prettyTCM QName
x]

    MultipleFixityDecls List1 (Name, Pair Fixity')
xs ->
      [m Doc] -> m Doc
forall (m :: * -> *) (t :: * -> *).
(Applicative m, Foldable t) =>
t (m Doc) -> m Doc
sep [ [m Doc] -> m Doc
forall (m :: * -> *) (t :: * -> *).
(Applicative m, Foldable t) =>
t (m Doc) -> m Doc
fsep ([m Doc] -> m Doc) -> [m Doc] -> m Doc
forall a b. (a -> b) -> a -> b
$ String -> [m Doc]
forall (m :: * -> *). Applicative m => String -> [m Doc]
pwords String
"Multiple fixity or syntax declarations for"
          , NonEmpty (m Doc) -> m Doc
forall (m :: * -> *) (t :: * -> *).
(Applicative m, Foldable t) =>
t (m Doc) -> m Doc
vcat (NonEmpty (m Doc) -> m Doc) -> NonEmpty (m Doc) -> m Doc
forall a b. (a -> b) -> a -> b
$ ((Name, Pair Fixity') -> m Doc)
-> List1 (Name, Pair Fixity') -> NonEmpty (m Doc)
forall a b. (a -> b) -> NonEmpty a -> NonEmpty b
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap (Name, Pair Fixity') -> m Doc
forall {m :: * -> *} {t :: * -> *} {a} {a}.
(Semigroup (m Doc), Applicative m, IsString (m Doc), Foldable t,
 Pretty a, Pretty a, HasRange a, Functor t) =>
(a, t a) -> m Doc
f List1 (Name, Pair Fixity')
xs
          ]
      where
        f :: (a, t a) -> m Doc
f (a
x, t a
fs) = (a -> m Doc
forall (m :: * -> *) a. (Applicative 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 -> m Doc
forall (m :: * -> *). Applicative m => m Doc -> m Doc -> m Doc
<+> t (m Doc) -> m Doc
forall (m :: * -> *) (t :: * -> *).
(Applicative m, Foldable t) =>
t (m Doc) -> m Doc
fsep ((a -> m Doc) -> t a -> t (m Doc)
forall a b. (a -> b) -> t a -> t b
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap (PrintRange a -> m Doc
forall (m :: * -> *) a. (Applicative m, Pretty a) => a -> m Doc
pretty (PrintRange a -> m Doc) -> (a -> PrintRange a) -> a -> m Doc
forall b c a. (b -> c) -> (a -> b) -> a -> c
. a -> PrintRange a
forall a. a -> PrintRange a
PrintRange) t a
fs)

    MultiplePolarityPragmas List1 Name
xs -> [m Doc] -> m Doc
forall (m :: * -> *) (t :: * -> *).
(Applicative m, Foldable t) =>
t (m Doc) -> m Doc
fsep ([m Doc] -> m Doc) -> [m Doc] -> m Doc
forall a b. (a -> b) -> a -> b
$
      String -> [m Doc]
forall (m :: * -> *). Applicative m => String -> [m Doc]
pwords String
"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. (Applicative m, Pretty a) => a -> m Doc
pretty (List1 Name -> [Item (List1 Name)]
forall l. IsList l => l -> [Item l]
List1.toList List1 Name
xs)

    CannotQuote CannotQuote
what -> do
      String -> m Doc
forall (m :: * -> *). Applicative m => String -> m Doc
fwords String
"`quote' expects an unambiguous defined name," m Doc -> m Doc -> m Doc
forall (m :: * -> *). Applicative m => m Doc -> m Doc -> m Doc
$$ do
      [m Doc] -> m Doc
forall (m :: * -> *) (t :: * -> *).
(Applicative m, Foldable t) =>
t (m Doc) -> m Doc
fsep ([m Doc] -> m Doc) -> [m Doc] -> m Doc
forall a b. (a -> b) -> a -> b
$ String -> [m Doc]
forall (m :: * -> *). Applicative m => String -> [m Doc]
pwords String
"but here the argument is" [m Doc] -> [m Doc] -> [m Doc]
forall a. [a] -> [a] -> [a]
++
        case CannotQuote
what of
          CannotQuote
CannotQuoteNothing ->
            String -> [m Doc]
forall (m :: * -> *). Applicative m => String -> [m Doc]
pwords String
"missing"
          CannotQuote
CannotQuoteHidden ->
            String -> [m Doc]
forall (m :: * -> *). Applicative m => String -> [m Doc]
pwords String
"implicit"
          CannotQuoteAmbiguous AmbiguousQName
xs ->
            String -> [m Doc]
forall (m :: * -> *). Applicative m => String -> [m Doc]
pwords String
"ambiguous:" [m Doc] -> [m Doc] -> [m Doc]
forall a. [a] -> [a] -> [a]
++ [ AmbiguousQName -> m Doc
forall (m :: * -> *) a. (Applicative m, Pretty a) => a -> m Doc
pretty AmbiguousQName
xs ]
          CannotQuoteExpression Expr
e -> case Expr
e of
            -- These expression can be quoted:
            A.Def' QName
_ Suffix
NoSuffix -> [m Doc]
forall a. HasCallStack => a
__IMPOSSIBLE__
              -- Andreas, 2024-09-27, issue #7514:
              -- Why only quote suffix-free universes?
            A.Macro        {} -> [m Doc]
forall a. HasCallStack => a
__IMPOSSIBLE__
            A.Proj         {} -> [m Doc]
forall a. HasCallStack => a
__IMPOSSIBLE__
            A.Con          {} -> [m Doc]
forall a. HasCallStack => a
__IMPOSSIBLE__
            A.DontCare     {} -> [m Doc]
forall a. HasCallStack => a
__IMPOSSIBLE__
            A.ScopedExpr   {} -> [m Doc]
forall a. HasCallStack => a
__IMPOSSIBLE__
            -- These cannot:
            A.PatternSyn   {} -> String -> [m Doc]
other String
"a pattern synonym:"
            A.Var          {} -> String -> [m Doc]
other String
"a variable:"
            A.Lit          {} -> String -> [m Doc]
other String
"a literal:"
            A.QuestionMark {} -> String -> [m Doc]
forall (m :: * -> *). Applicative m => String -> [m Doc]
pwords String
"a metavariable"
            A.Underscore   {} -> String -> [m Doc]
forall (m :: * -> *). Applicative m => String -> [m Doc]
pwords String
"a metavariable"
            Expr
_ ->
              String -> [m Doc]
forall (m :: * -> *). Applicative m => String -> [m Doc]
pwords String
"a compound expression"
            where
              other :: String -> [m Doc]
other String
s = String -> [m Doc]
forall (m :: * -> *). Applicative m => String -> [m Doc]
pwords String
s [m Doc] -> [m Doc] -> [m Doc]
forall a. [a] -> [a] -> [a]
++ [ Expr -> m Doc
forall a (m :: * -> *). (PrettyTCM a, MonadPretty m) => a -> m Doc
forall (m :: * -> *). MonadPretty m => Expr -> m Doc
prettyTCM Expr
e]
          CannotQuotePattern NamedArg Pattern
p -> case NamedArg Pattern -> Pattern
forall a. NamedArg a -> a
namedArg NamedArg Pattern
p of
            C.IdentP    {} -> [m Doc]
forall a. HasCallStack => a
__IMPOSSIBLE__
            C.HiddenP   {} -> [m Doc]
forall a. HasCallStack => a
__IMPOSSIBLE__
            C.InstanceP {} -> [m Doc]
forall a. HasCallStack => a
__IMPOSSIBLE__
            C.RawAppP   {} -> [m Doc]
forall a. HasCallStack => a
__IMPOSSIBLE__
            C.AbsurdP   {} -> String -> [m Doc]
forall (m :: * -> *). Applicative m => String -> [m Doc]
pwords String
"an absurd pattern"
            C.LitP      {} -> String -> [m Doc]
forall (m :: * -> *). Applicative m => String -> [m Doc]
pwords String
"a literal pattern"
            C.WildP     {} -> String -> [m Doc]
forall (m :: * -> *). Applicative m => String -> [m Doc]
pwords String
"a wildcard pattern"
            Pattern
_ ->
              String -> [m Doc]
forall (m :: * -> *). Applicative m => String -> [m Doc]
pwords String
"a compound pattern"

    CannotQuoteTerm CannotQuoteTerm
what -> do
      String -> m Doc
forall (m :: * -> *). Applicative m => String -> m Doc
fwords String
"`quoteTerm' expects a single visible argument," m Doc -> m Doc -> m Doc
forall (m :: * -> *). Applicative m => m Doc -> m Doc -> m Doc
$$ do
      [m Doc] -> m Doc
forall (m :: * -> *) (t :: * -> *).
(Applicative m, Foldable t) =>
t (m Doc) -> m Doc
fsep ([m Doc] -> m Doc) -> [m Doc] -> m Doc
forall a b. (a -> b) -> a -> b
$ String -> [m Doc]
forall (m :: * -> *). Applicative m => String -> [m Doc]
pwords String
"but has been given" [m Doc] -> [m Doc] -> [m Doc]
forall a. [a] -> [a] -> [a]
++
        case CannotQuoteTerm
what of
          CannotQuoteTerm
CannotQuoteTermNothing ->
            String -> [m Doc]
forall (m :: * -> *). Applicative m => String -> [m Doc]
pwords String
"none"
          CannotQuoteTermHidden Hiding
h ->
            String -> [m Doc]
forall (m :: * -> *). Applicative m => String -> [m Doc]
pwords (String -> [m Doc]) -> String -> [m Doc]
forall a b. (a -> b) -> a -> b
$ 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]
++ String
" one"


    ConstructorNameOfNonRecord ResolvedName
res | DefinedName Access
_ AbstractName
nm Suffix
_ <- ResolvedName
res, KindOfName
RecName <- AbstractName -> KindOfName
anameKind AbstractName
nm ->
      [m Doc] -> m Doc
forall (m :: * -> *) (t :: * -> *).
(Applicative m, Foldable t) =>
t (m Doc) -> m Doc
fsep ([m Doc] -> m Doc) -> [m Doc] -> m Doc
forall a b. (a -> b) -> a -> b
$ String -> [m Doc]
forall (m :: * -> *). Applicative m => String -> [m Doc]
pwords String
"The constructor for record type" [m Doc] -> [m Doc] -> [m Doc]
forall a. [a] -> [a] -> [a]
++ [AbstractName -> m Doc
forall a (m :: * -> *). (PrettyTCM a, MonadPretty m) => a -> m Doc
forall (m :: * -> *). MonadPretty m => AbstractName -> m Doc
prettyTCM AbstractName
nm] [m Doc] -> [m Doc] -> [m Doc]
forall a. [a] -> [a] -> [a]
++ String -> [m Doc]
forall (m :: * -> *). Applicative m => String -> [m Doc]
pwords String
"is not in scope in the types of its fields."

    ConstructorNameOfNonRecord ResolvedName
res -> case ResolvedName
res of
      ResolvedName
UnknownName -> m Doc
forall a. HasCallStack => a
__IMPOSSIBLE__ -- Turned into NotInScope when the name is resolved
      ResolvedName
name ->
        let
          qn :: m Doc
          (m Doc
qn, String
whatis) = case ResolvedName
name of
            DefinedName Access
_ AbstractName
nm Suffix
_ -> (AbstractName -> m Doc
forall a (m :: * -> *). (PrettyTCM a, MonadPretty m) => a -> m Doc
forall (m :: * -> *). MonadPretty m => AbstractName -> m Doc
prettyTCM AbstractName
nm,) case AbstractName -> KindOfName
anameKind AbstractName
nm of
              KindOfName
RecName                  -> String
forall a. HasCallStack => a
__IMPOSSIBLE__
              KindOfName
ConName                  -> String
forall a. HasCallStack => a
__IMPOSSIBLE__
              KindOfName
CoConName                -> String
forall a. HasCallStack => a
__IMPOSSIBLE__
              KindOfName
FldName                  -> String
forall a. HasCallStack => a
__IMPOSSIBLE__
              KindOfName
PatternSynName           -> String
forall a. HasCallStack => a
__IMPOSSIBLE__

              KindOfName
GeneralizeName           -> String
"a generalized variable"
              KindOfName
DisallowedGeneralizeName -> String
"a generalized variable"
              KindOfName
MacroName                -> String
"a macro"
              KindOfName
QuotableName             -> String
"a quotable name"

              KindOfName
DataName                 -> String
"a data type"
              KindOfName
FunName                  -> String
"a function"
              KindOfName
AxiomName                -> String
"a postulate"
              KindOfName
PrimName                 -> String
"a primitive"
              KindOfName
OtherDefName             -> String
"a defined symbol"
            VarName Name
a BindingSource
_ -> (Name -> m Doc
forall a (m :: * -> *). (PrettyTCM a, MonadPretty m) => a -> m Doc
forall (m :: * -> *). MonadPretty m => Name -> m Doc
prettyTCM Name
a, String
"a local variable")
            FieldName (AbstractName
a :| [AbstractName]
_) -> (AbstractName -> m Doc
forall a (m :: * -> *). (PrettyTCM a, MonadPretty m) => a -> m Doc
forall (m :: * -> *). MonadPretty m => AbstractName -> m Doc
prettyTCM AbstractName
a, String
"a projection")
            ConstructorName Set1 Induction
_ (AbstractName
a :| [AbstractName]
_) -> (AbstractName -> m Doc
forall a (m :: * -> *). (PrettyTCM a, MonadPretty m) => a -> m Doc
forall (m :: * -> *). MonadPretty m => AbstractName -> m Doc
prettyTCM AbstractName
a, String
"a constructor")
            PatternSynResName (AbstractName
a :| [AbstractName]
_) -> (AbstractName -> m Doc
forall a (m :: * -> *). (PrettyTCM a, MonadPretty m) => a -> m Doc
forall (m :: * -> *). MonadPretty m => AbstractName -> m Doc
prettyTCM AbstractName
a, String
"a pattern synonym")
        in [m Doc] -> m Doc
forall (m :: * -> *) (t :: * -> *).
(Applicative m, Foldable t) =>
t (m Doc) -> m Doc
fsep ([m Doc] -> m Doc) -> [m Doc] -> m Doc
forall a b. (a -> b) -> a -> b
$ String -> [m Doc]
forall (m :: * -> *). Applicative m => String -> [m Doc]
pwords String
"Only record types have constructor names, but" [m Doc] -> [m Doc] -> [m Doc]
forall a. [a] -> [a] -> [a]
++ [m Doc
qn, m Doc
"is"] [m Doc] -> [m Doc] -> [m Doc]
forall a. [a] -> [a] -> [a]
++ String -> [m Doc]
forall (m :: * -> *). Applicative m => String -> [m Doc]
pwords (String
whatis String -> String -> String
forall a. Semigroup a => a -> a -> a
<> String
".")

    NonFatalErrors Set1 TCWarning
ws -> NonEmpty (m Doc) -> m Doc
forall (m :: * -> *) (t :: * -> *).
(Applicative m, Foldable t) =>
t (m Doc) -> m Doc
vsep (NonEmpty (m Doc) -> m Doc) -> NonEmpty (m Doc) -> m Doc
forall a b. (a -> b) -> a -> b
$ (TCWarning -> m Doc) -> NonEmpty TCWarning -> NonEmpty (m Doc)
forall a b. (a -> b) -> NonEmpty a -> NonEmpty b
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap TCWarning -> m Doc
forall a (m :: * -> *). (PrettyTCM a, MonadPretty m) => a -> m Doc
forall (m :: * -> *). MonadPretty m => TCWarning -> m Doc
prettyTCM (NonEmpty TCWarning -> NonEmpty (m Doc))
-> NonEmpty TCWarning -> NonEmpty (m Doc)
forall a b. (a -> b) -> a -> b
$ Set1 TCWarning -> NonEmpty TCWarning
forall a. NESet a -> NonEmpty a
Set1.toAscList Set1 TCWarning
ws

    TriedToCopyConstrainedPrim QName
q -> [m Doc] -> m Doc
forall (m :: * -> *) (t :: * -> *).
(Applicative m, Foldable t) =>
t (m Doc) -> m Doc
fsep ([m Doc] -> m Doc) -> [m Doc] -> m Doc
forall a b. (a -> b) -> a -> b
$
      String -> [m Doc]
forall (m :: * -> *). Applicative m => String -> [m Doc]
pwords String
"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
forall (m :: * -> *). MonadPretty m => QName -> m Doc
prettyTCM QName
q]

    MismatchedProjectionsError QName
left QName
right -> [m Doc] -> m Doc
forall (m :: * -> *) (t :: * -> *).
(Applicative m, Foldable t) =>
t (m Doc) -> m Doc
fsep ([m Doc] -> m Doc) -> [m Doc] -> m Doc
forall a b. (a -> b) -> a -> b
$
      String -> [m Doc]
forall (m :: * -> *). Applicative m => String -> [m Doc]
pwords String
"The projections" [m Doc] -> [m Doc] -> [m Doc]
forall a. [a] -> [a] -> [a]
++ [QName -> m Doc
forall a (m :: * -> *). (PrettyTCM a, MonadPretty m) => a -> m Doc
forall (m :: * -> *). MonadPretty m => QName -> m Doc
prettyTCM QName
left] [m Doc] -> [m Doc] -> [m Doc]
forall a. [a] -> [a] -> [a]
++
      String -> [m Doc]
forall (m :: * -> *). Applicative m => String -> [m Doc]
pwords String
"and" [m Doc] -> [m Doc] -> [m Doc]
forall a. [a] -> [a] -> [a]
++ [QName -> m Doc
forall a (m :: * -> *). (PrettyTCM a, MonadPretty m) => a -> m Doc
forall (m :: * -> *). MonadPretty m => QName -> m Doc
prettyTCM QName
right] [m Doc] -> [m Doc] -> [m Doc]
forall a. [a] -> [a] -> [a]
++
      String -> [m Doc]
forall (m :: * -> *). Applicative m => String -> [m Doc]
pwords String
"do not match"

    InvalidProjectionParameter NamedArg Expr
arg -> [m Doc] -> m Doc
forall (m :: * -> *) (t :: * -> *).
(Applicative m, Foldable t) =>
t (m Doc) -> m Doc
fsep ([m Doc] -> m Doc) -> [m Doc] -> m Doc
forall a b. (a -> b) -> a -> b
$
      String -> [m Doc]
forall (m :: * -> *). Applicative m => String -> [m Doc]
pwords String
"Invalid projection parameter " [m Doc] -> [m Doc] -> [m Doc]
forall a. [a] -> [a] -> [a]
++
      [NamedArg Expr -> m Doc
forall a (m :: * -> *).
(ToConcrete a, Pretty (ConOfAbs a), MonadAbsToCon m) =>
a -> m Doc
prettyA NamedArg Expr
arg]

    TypeError
TacticAttributeNotAllowed -> [m Doc] -> m Doc
forall (m :: * -> *) (t :: * -> *).
(Applicative m, Foldable t) =>
t (m Doc) -> m Doc
fsep ([m Doc] -> m Doc) -> [m Doc] -> m Doc
forall a b. (a -> b) -> a -> b
$
      String -> [m Doc]
forall (m :: * -> *). Applicative m => String -> [m Doc]
pwords String
"The @tactic attribute is not allowed here"

    CannotRewriteByNonEquation Type
t ->
      m Doc
"Cannot rewrite by equation of type" m Doc -> m Doc -> m Doc
forall (m :: * -> *). Applicative m => m Doc -> m Doc -> m Doc
<+> Type -> m Doc
forall a (m :: * -> *). (PrettyTCM a, MonadPretty m) => a -> m Doc
forall (m :: * -> *). MonadPretty m => Type -> m Doc
prettyTCM Type
t

    MacroResultTypeMismatch Type
expectedType ->
      [m Doc] -> m Doc
forall (m :: * -> *) (t :: * -> *).
(Applicative m, Foldable t) =>
t (m Doc) -> m Doc
sep [ m Doc
"Result type of a macro must be", Int -> m Doc -> m Doc
forall (m :: * -> *). Functor m => Int -> m Doc -> m Doc
nest Int
2 (m Doc -> m Doc) -> m Doc -> m Doc
forall a b. (a -> b) -> a -> b
$ Type -> m Doc
forall a (m :: * -> *). (PrettyTCM a, MonadPretty m) => a -> m Doc
forall (m :: * -> *). MonadPretty m => Type -> m Doc
prettyTCM Type
expectedType ]

    NonLocalWhereModuleInRefinedContext [Term]
args [ShortText]
names -> do
      let pr :: ShortText -> a -> m Doc
pr ShortText
x a
v = String -> m Doc
forall (m :: * -> *). Applicative m => String -> m Doc
text (ShortText -> String
TS.unpack ShortText
x String -> String -> String
forall a. [a] -> [a] -> [a]
++ String
" =") m Doc -> m Doc -> m Doc
forall (m :: * -> *). Applicative m => m Doc -> m Doc -> m Doc
<+> a -> m Doc
forall a (m :: * -> *). (PrettyTCM a, MonadPretty m) => a -> m Doc
forall (m :: * -> *). MonadPretty m => a -> m Doc
prettyTCM a
v
      [m Doc] -> m Doc
forall (m :: * -> *) (t :: * -> *).
(Applicative m, Foldable t) =>
t (m Doc) -> m Doc
vcat
        [ [m Doc] -> m Doc
forall (m :: * -> *) (t :: * -> *).
(Applicative m, Foldable t) =>
t (m Doc) -> m Doc
fsep ([m Doc] -> m Doc) -> [m Doc] -> m Doc
forall a b. (a -> b) -> a -> b
$ String -> [m Doc]
forall (m :: * -> *). Applicative m => String -> [m Doc]
pwords (String -> [m Doc]) -> String -> [m Doc]
forall a b. (a -> b) -> a -> b
$ String
"Non-local where-modules are not allowed when module parameters have been refined by pattern matching."
        , m Doc
"(See" m Doc -> m Doc -> m Doc
forall (m :: * -> *). Applicative m => m Doc -> m Doc -> m Doc
<+> (Int -> m Doc
forall (m :: * -> *). Applicative m => Int -> m Doc
githubIssue Int
2897 m Doc -> m Doc -> m Doc
forall a. Semigroup a => a -> a -> a
<> m Doc
".)")
        , String -> m Doc
forall (m :: * -> *). Applicative m => String -> m Doc
text (String -> m Doc) -> String -> m Doc
forall a b. (a -> b) -> a -> b
$ String
"In this case the module parameter" String -> String -> String
forall a. [a] -> [a] -> [a]
++
                  (if Bool -> Bool
not ([Term] -> Bool
forall a. Null a => a -> Bool
null [Term]
args) then String
"s have" else String
" has") String -> String -> String
forall a. [a] -> [a] -> [a]
++
                  String
" been refined to"
        , Int -> m Doc -> m Doc
forall (m :: * -> *). Functor m => Int -> m Doc -> m Doc
nest Int
2 (m Doc -> m Doc) -> m Doc -> m Doc
forall a b. (a -> b) -> a -> b
$ [m Doc] -> m Doc
forall (m :: * -> *) (t :: * -> *).
(Applicative m, Foldable t) =>
t (m Doc) -> m Doc
vcat ([m Doc] -> m Doc) -> [m Doc] -> m Doc
forall a b. (a -> b) -> a -> b
$ (ShortText -> Term -> m Doc) -> [ShortText] -> [Term] -> [m Doc]
forall a b c. (a -> b -> c) -> [a] -> [b] -> [c]
zipWith ShortText -> Term -> m Doc
forall {m :: * -> *} {a}.
(PrettyTCM a, MonadFresh NameId m, MonadInteractionPoints m,
 MonadStConcreteNames m, PureTCM m, IsString (m Doc), Null (m Doc),
 Semigroup (m Doc)) =>
ShortText -> a -> m Doc
pr [ShortText]
names [Term]
args
        ]

    CannotGenerateTransportClause QName
f Closure (Abs Type)
clos ->
      Closure (Abs Type) -> (Abs Type -> m Doc) -> m Doc
forall (m :: * -> *) c a b.
(MonadTCEnv m, ReadTCState m, LensClosure c a) =>
c -> (a -> m b) -> m b
enterClosure Closure (Abs Type)
clos \ Abs Type
failed_t -> (ShortText, Dom Type) -> m Doc -> m Doc
forall b (m :: * -> *) a.
(AddContext b, MonadAddContext m) =>
b -> m a -> m a
forall (m :: * -> *) a.
MonadAddContext m =>
(ShortText, Dom Type) -> m a -> m a
addContext (ShortText
"i" :: ShortText, Dom Type
HasCallStack => Dom Type
__DUMMY_DOM__) (m Doc -> m Doc) -> m Doc -> m Doc
forall a b. (a -> b) -> a -> b
$ [m Doc] -> m Doc
forall (m :: * -> *) (t :: * -> *).
(Applicative m, Foldable t) =>
t (m Doc) -> m Doc
vcat
        [ m Doc
"Could not generate a transport clause for" m Doc -> m Doc -> m Doc
forall (m :: * -> *). Applicative m => m Doc -> m Doc -> m Doc
<+> QName -> m Doc
forall a (m :: * -> *). (PrettyTCM a, MonadPretty m) => a -> m Doc
forall (m :: * -> *). MonadPretty m => QName -> m Doc
prettyTCM QName
f
        , m Doc
"because a term of type" m Doc -> m Doc -> m Doc
forall (m :: * -> *). Applicative m => m Doc -> m Doc -> m Doc
<+> Type -> m Doc
forall a (m :: * -> *). (PrettyTCM a, MonadPretty m) => a -> m Doc
forall (m :: * -> *). MonadPretty m => Type -> m Doc
prettyTCM (Abs Type -> Type
forall a. Abs a -> a
unAbs Abs Type
failed_t)
        , m Doc
"lives in the sort" m Doc -> m Doc -> m Doc
forall (m :: * -> *). Applicative m => m Doc -> m Doc -> m Doc
<+> Sort -> m Doc
forall a (m :: * -> *). (PrettyTCM a, MonadPretty m) => a -> m Doc
forall (m :: * -> *). MonadPretty m => Sort -> m Doc
prettyTCM (Type -> Sort
forall a. LensSort a => a -> Sort
getSort (Abs Type -> Type
forall a. Abs a -> a
unAbs Abs Type
failed_t))
        , m Doc
"and thus can not be transported"
        ]

    CubicalPrimitiveNotFullyApplied QName
c ->
      QName -> m Doc
forall a (m :: * -> *). (PrettyTCM a, MonadPretty m) => a -> m Doc
forall (m :: * -> *). MonadPretty m => QName -> m Doc
prettyTCM QName
c m Doc -> m Doc -> m Doc
forall (m :: * -> *). Applicative m => m Doc -> m Doc -> m Doc
<+> m Doc
"must be fully applied"

    ExpectedIntervalLiteral Expr
e -> do
      i0 <- Term -> Maybe Term -> Term
forall a. a -> Maybe a -> a
fromMaybe Term
forall a. HasCallStack => a
__IMPOSSIBLE__ (Maybe Term -> Term) -> m (Maybe Term) -> m Term
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> BuiltinId -> m (Maybe Term)
forall (m :: * -> *). HasBuiltins m => BuiltinId -> m (Maybe Term)
getBuiltin' BuiltinId
builtinIZero
      i1 <- fromMaybe __IMPOSSIBLE__ <$> getBuiltin' builtinIOne
      fsep $ concat
        [ pwords "Expected an interval literal"
        , [ parens $ fsep [ prettyTCM i0, "or", prettyTCM i1 ] ]
        , pwords "but found:"
        , [ prettyTCM e ]
        ]

    TypeError
PatternInPathLambda ->
      String -> m Doc
forall (m :: * -> *). Applicative m => String -> m Doc
fwords String
"Patterns are not allowed in Path-lambdas"

    TypeError
PatternInSystem ->
      String -> m Doc
forall (m :: * -> *). Applicative m => String -> m Doc
fwords String
"Pattern matching or path copatterns not allowed in systems"

    TypeError
FaceConstraintDisjunction ->
      String -> m Doc
forall (m :: * -> *). Applicative m => String -> m Doc
fwords String
"Cannot have disjunctions in a face constraint"

    TypeError
FaceConstraintUnsatisfiable ->
      String -> m Doc
forall (m :: * -> *). Applicative m => String -> m Doc
fwords String
"The face constraint is unsatisfiable"

    IllTypedPatternAfterWithAbstraction Pattern
p -> [m Doc] -> m Doc
forall (m :: * -> *) (t :: * -> *).
(Applicative m, Foldable t) =>
t (m Doc) -> m Doc
vcat
      [ m Doc
"Ill-typed pattern after with abstraction: " m Doc -> m Doc -> m Doc
forall (m :: * -> *). Applicative m => m Doc -> m Doc -> m Doc
<+> Pattern -> m Doc
forall a (m :: * -> *).
(ToConcrete a, Pretty (ConOfAbs a), MonadAbsToCon m) =>
a -> m Doc
prettyA Pattern
p
      , m Doc
"(perhaps you can replace it by `_`?)"
      ]

    ComatchingDisabledForRecord QName
recName ->
      m Doc
"Copattern matching is disabled for record" m Doc -> m Doc -> m Doc
forall (m :: * -> *). Applicative m => m Doc -> m Doc -> m Doc
<+> QName -> m Doc
forall a (m :: * -> *). (PrettyTCM a, MonadPretty m) => a -> m Doc
forall (m :: * -> *). MonadPretty m => QName -> m Doc
prettyTCM QName
recName

    UnexpectedParameter LamBinding
par -> do
      String -> m Doc
forall (m :: * -> *). Applicative m => String -> m Doc
text String
"Unexpected parameter" m Doc -> m Doc -> m Doc
forall (m :: * -> *). Applicative m => m Doc -> m Doc -> m Doc
<+> LamBinding -> m Doc
forall a (m :: * -> *).
(ToConcrete a, Pretty (ConOfAbs a), MonadAbsToCon m) =>
a -> m Doc
prettyA LamBinding
par

    NoParameterOfName ShortText
x -> do
      String -> m Doc
forall (m :: * -> *). Applicative m => String -> m Doc
text (String
"No parameter of name " String -> String -> String
forall a. [a] -> [a] -> [a]
++ ShortText -> String
TS.unpack ShortText
x)

    SortDoesNotAdmitDataDefinitions QName
name Sort
s ->[m Doc] -> m Doc
forall (m :: * -> *) (t :: * -> *).
(Applicative m, Foldable t) =>
t (m Doc) -> m Doc
fsep
      [ m Doc
"The universe"
      , Sort -> m Doc
forall a (m :: * -> *). (PrettyTCM a, MonadPretty m) => a -> m Doc
forall (m :: * -> *). MonadPretty m => Sort -> m Doc
prettyTCM Sort
s
      , m Doc
"of"
      , QName -> m Doc
forall a (m :: * -> *). (PrettyTCM a, MonadPretty m) => a -> m Doc
forall (m :: * -> *). MonadPretty m => QName -> m Doc
prettyTCM QName
name
      , m Doc
"does not admit data or record declarations"
      ]

    SortCannotDependOnItsIndex QName
name Type
t -> [m Doc] -> m Doc
forall (m :: * -> *) (t :: * -> *).
(Applicative m, Foldable t) =>
t (m Doc) -> m Doc
fsep
      [ m Doc
"The sort of" m Doc -> m Doc -> m Doc
forall (m :: * -> *). Applicative m => m Doc -> m Doc -> m Doc
<+> QName -> m Doc
forall a (m :: * -> *). (PrettyTCM a, MonadPretty m) => a -> m Doc
forall (m :: * -> *). MonadPretty m => QName -> m Doc
prettyTCM QName
name
      , m Doc
"cannot depend on its indices in the type"
      , Type -> m Doc
forall a (m :: * -> *). (PrettyTCM a, MonadPretty m) => a -> m Doc
forall (m :: * -> *). MonadPretty m => Type -> m Doc
prettyTCM Type
t
      ]

    UnexpectedTypeSignatureForParameter List1 (NamedArg Binder)
xs -> do
      [m Doc] -> m Doc
forall (m :: * -> *) (t :: * -> *).
(Applicative m, Foldable t) =>
t (m Doc) -> m Doc
fsep (String -> [m Doc]
forall (m :: * -> *). Applicative m => String -> [m Doc]
pwords String
"Unexpected type signature for" [m Doc] -> [m Doc] -> [m Doc]
forall a. [a] -> [a] -> [a]
++ [ List1 (NamedArg Binder) -> m Doc -> m Doc
forall (m :: * -> *) a. (Functor m, Sized a) => a -> m Doc -> m Doc
pluralS List1 (NamedArg Binder)
xs m Doc
"parameter" ]) m Doc -> m Doc -> m Doc
forall (m :: * -> *). Applicative m => m Doc -> m Doc -> m Doc
<+> NonEmpty (m Doc) -> m Doc
forall (m :: * -> *) (t :: * -> *).
(Applicative m, Foldable t) =>
t (m Doc) -> m Doc
sep ((NamedArg Binder -> m Doc)
-> List1 (NamedArg Binder) -> NonEmpty (m Doc)
forall a b. (a -> b) -> NonEmpty a -> NonEmpty b
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap NamedArg Binder -> m Doc
forall a (m :: * -> *).
(ToConcrete a, Pretty (ConOfAbs a), MonadAbsToCon m) =>
a -> m Doc
prettyA List1 (NamedArg Binder)
xs)

    TypeError
QualifiedLocalModule -> String -> m Doc
forall (m :: * -> *). Applicative m => String -> m Doc
fwords String
"Local modules cannot have qualified names"

    BackendDoesNotSupportOnlyScopeChecking ShortText
backend -> [m Doc] -> m Doc
forall (m :: * -> *) (t :: * -> *).
(Applicative m, Foldable t) =>
t (m Doc) -> m Doc
fsep ([m Doc] -> m Doc) -> [m Doc] -> m Doc
forall a b. (a -> b) -> a -> b
$ [[m Doc]] -> [m Doc]
forall (t :: * -> *) a. Foldable t => t [a] -> [a]
concat
      [ String -> [m Doc]
forall (m :: * -> *). Applicative m => String -> [m Doc]
pwords String
"The backend"
      , [ ShortText -> m Doc
forall a (m :: * -> *). (PrettyTCM a, MonadPretty m) => a -> m Doc
forall (m :: * -> *). MonadPretty m => ShortText -> m Doc
prettyTCM ShortText
backend ]
      , String -> [m Doc]
forall (m :: * -> *). Applicative m => String -> [m Doc]
pwords String
"does not support --only-scope-checking."
      ]

    UnknownBackend ShortText
backend Set ShortText
backends -> Doc -> m Doc
forall a. a -> m a
forall (f :: * -> *) a. Applicative f => a -> f a
pure (Doc -> m Doc) -> Doc -> m Doc
forall a b. (a -> b) -> a -> b
$ [Doc] -> Doc
forall (t :: * -> *). Foldable t => t Doc -> Doc
P.vcat ([Doc] -> Doc) -> [Doc] -> Doc
forall a b. (a -> b) -> a -> b
$ [[Doc]] -> [Doc]
forall (t :: * -> *) a. Foldable t => t [a] -> [a]
concat
      [ [ [Doc] -> Doc
forall (t :: * -> *). Foldable t => t Doc -> Doc
P.hcat [ Doc
"No backend called '", ShortText -> Doc
forall a. Pretty a => a -> Doc
P.pretty ShortText
backend, Doc
"' " ] ]
      , [ Doc
"Installed backend(s):" ]
      , (ShortText -> Doc) -> [ShortText] -> [Doc]
forall a b. (a -> b) -> [a] -> [b]
map ((Doc
"-" Doc -> Doc -> Doc
forall a. Doc a -> Doc a -> Doc a
P.<+>) (Doc -> Doc) -> (ShortText -> Doc) -> ShortText -> Doc
forall b c a. (b -> c) -> (a -> b) -> a -> c
. ShortText -> Doc
forall a. Pretty a => a -> Doc
P.pretty) ([ShortText] -> [Doc]) -> [ShortText] -> [Doc]
forall a b. (a -> b) -> a -> b
$ Set ShortText -> [ShortText]
forall a. Set a -> [a]
Set.toAscList Set ShortText
backends
      ]

    CustomBackendError ShortText
backend Doc
err -> (ShortText -> m Doc
forall (m :: * -> *) a. (Applicative m, Pretty a) => a -> m Doc
pretty ShortText
backend m Doc -> m Doc -> m Doc
forall a. Semigroup a => a -> a -> a
<> m Doc
":") m Doc -> m Doc -> m Doc
forall (m :: * -> *). Applicative m => m Doc -> m Doc -> m Doc
<?> Doc -> m Doc
forall a. a -> m a
forall (f :: * -> *) a. Applicative f => a -> f a
pure Doc
err

    where
    mpar :: a -> a -> m Doc -> m Doc
mpar a
n a
args
      | a
n a -> a -> Bool
forall a. Ord a => a -> a -> Bool
> a
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 :: Arg (I.Pattern' a) -> m Doc
    prettyArg :: forall a. Arg (Pattern' a) -> m Doc
prettyArg (Arg ArgInfo
info Pattern' a
x) = case ArgInfo -> Hiding
forall a. LensHiding a => a -> Hiding
getHiding ArgInfo
info of
      Hiding
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 a. Integer -> Pattern' a -> m Doc
prettyPat Integer
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 a. Integer -> Pattern' a -> m Doc
prettyPat Integer
0 Pattern' a
x
      Hiding
NotHidden  -> Integer -> Pattern' a -> m Doc
forall a. Integer -> Pattern' a -> m Doc
prettyPat Integer
1 Pattern' a
x

    prettyPat :: Integer -> (I.Pattern' a) -> m Doc
    prettyPat :: forall a. Integer -> Pattern' a -> m Doc
prettyPat Integer
_ (I.VarP PatternInfo
_ a
_) = m Doc
"_"
    prettyPat Integer
_ (I.DotP PatternInfo
_ Term
_) = m Doc
"._"
    prettyPat Integer
n (I.ConP ConHead
c ConPatternInfo
_ [NamedArg (Pattern' a)]
args) =
      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
forall (m :: * -> *). MonadPretty m => ConHead -> 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 :: * -> *) (t :: * -> *).
(Applicative m, Foldable t) =>
t (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 a. 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 a b. (a -> b) -> Arg a -> Arg b
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 Integer
n (I.DefP PatternInfo
o QName
q [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
forall (m :: * -> *). MonadPretty m => QName -> 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 :: * -> *) (t :: * -> *).
(Applicative m, Foldable t) =>
t (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 a. 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 a b. (a -> b) -> Arg a -> Arg b
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 Integer
_ (I.LitP PatternInfo
_ Literal
l) = Literal -> m Doc
forall a (m :: * -> *). (PrettyTCM a, MonadPretty m) => a -> m Doc
forall (m :: * -> *). MonadPretty m => Literal -> m Doc
prettyTCM Literal
l
    prettyPat Integer
_ (I.ProjP ProjOrigin
_ QName
p) = m Doc
"." 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
forall (m :: * -> *). MonadPretty m => QName -> m Doc
prettyTCM QName
p
    prettyPat Integer
_ (I.IApplyP PatternInfo
_ Term
_ Term
_ a
_) = m Doc
"_"
    prettyPat Integer
n (I.MaskP Pattern' a
p) = Integer -> Pattern' a -> m Doc
forall a. Integer -> Pattern' a -> m Doc
prettyPat Integer
n Pattern' a
p

{-# SPECIALIZE prettyPossibleFilesForModule :: TopLevelModuleName -> List1 AbsolutePath -> TCM Doc #-}
prettyPossibleFilesForModule :: MonadPretty m => TopLevelModuleName -> List1 AbsolutePath -> m Doc
prettyPossibleFilesForModule :: forall (m :: * -> *).
MonadPretty m =>
TopLevelModuleName -> List1 AbsolutePath -> m Doc
prettyPossibleFilesForModule TopLevelModuleName
m List1 AbsolutePath
dirs = [m Doc] -> m Doc
forall (m :: * -> *) (t :: * -> *).
(Applicative m, Foldable t) =>
t (m Doc) -> m Doc
vcat
    [ Int -> m Doc -> m Doc
forall (m :: * -> *). Functor m => Int -> m Doc -> m Doc
nest Int
2 (m Doc -> m Doc) -> m Doc -> m Doc
forall a b. (a -> b) -> a -> b
$ [m Doc] -> m Doc
forall (m :: * -> *) (t :: * -> *).
(Applicative m, Foldable t) =>
t (m Doc) -> m Doc
vcat ([m Doc] -> m Doc) -> [m Doc] -> m Doc
forall a b. (a -> b) -> a -> b
$ (String -> m Doc) -> [String] -> [m Doc]
forall a b. (a -> b) -> [a] -> [b]
map String -> m Doc
forall (m :: * -> *). Applicative m => String -> m Doc
text ([String] -> [m Doc]) -> [String] -> [m Doc]
forall a b. (a -> b) -> a -> b
$
      [ AbsolutePath -> String
filePath AbsolutePath
dir String -> String -> String
</> TopLevelModuleName -> String -> String
moduleNameToFileName TopLevelModuleName
m String
".AGDA"
      | AbsolutePath
dir  <- List1 AbsolutePath -> [Item (List1 AbsolutePath)]
forall l. IsList l => l -> [Item l]
List1.toList List1 AbsolutePath
dirs
      ]
    , m Doc
"where .AGDA denotes a legal extension for an Agda file"
    , 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 :: * -> *) (t :: * -> *).
(Applicative m, Foldable t) =>
t (m Doc) -> m Doc
fsep ([m Doc] -> m Doc) -> [m Doc] -> m Doc
forall a b. (a -> b) -> a -> b
$ String -> [m Doc]
forall (m :: * -> *). Applicative m => String -> [m Doc]
pwords String
"i.e., one of" [m Doc] -> [m Doc] -> [m Doc]
forall a. [a] -> [a] -> [a]
++ (String -> m Doc) -> [String] -> [m Doc]
forall a b. (a -> b) -> [a] -> [b]
map String -> m Doc
forall (m :: * -> *). Applicative m => String -> m Doc
text [String]
agdaFileExtensions
    ]

-- | Pretty-print error 'ShadowedModule' and return the range of the shadowed module.
{-# SPECIALIZE prettyShadowedModule :: C.Name -> List1 A.ModuleName -> TCM (TCM Doc, Range) #-}
prettyShadowedModule :: MonadPretty m => C.Name -> List1 A.ModuleName -> m (m Doc, Range)
prettyShadowedModule :: forall (m :: * -> *).
MonadPretty m =>
Name -> List1 ModuleName -> m (m Doc, Range)
prettyShadowedModule Name
x ms :: List1 ModuleName
ms@(ModuleName
m0 :| [ModuleName]
_) = do
      -- Clash! Concrete module name x already points to the abstract names ms.
      (r, m) <- do
        -- Andreas, 2017-07-28, issue #719.
        -- First, we try to find whether one of the abstract names @ms@ points back to @x@
        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 = NonEmpty [(QName, ModuleName)] -> [(QName, ModuleName)]
forall (t :: * -> *) a. Foldable t => t [a] -> [a]
concat (NonEmpty [(QName, ModuleName)] -> [(QName, ModuleName)])
-> NonEmpty [(QName, ModuleName)] -> [(QName, ModuleName)]
forall a b. (a -> b) -> a -> b
$ List1 ModuleName
ms List1 ModuleName
-> (ModuleName -> [(QName, ModuleName)])
-> NonEmpty [(QName, ModuleName)]
forall (f :: * -> *) a b. Functor f => f a -> (a -> b) -> f b
<&> \ 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
        reportSLn "scope.clash.error" 30 $ "candidates = " ++ prettyShow xms0

        -- Try to find x (which will have a different Range, if it has one (#2649)).
        let xms = ((QName, ModuleName) -> Bool)
-> [(QName, ModuleName)] -> [(QName, ModuleName)]
forall a. (a -> Bool) -> [a] -> [a]
filter ((\ 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 a. HasRange a => a -> 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
        reportSLn "scope.class.error" 30 $ "filtered candidates = " ++ prettyShow xms

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

        -- If that failed, we pick the first m from ms which has a nameBindingSite.
        let rms = NonEmpty [(Range, ModuleName)] -> [(Range, ModuleName)]
forall (t :: * -> *) a. Foldable t => t [a] -> [a]
concat (NonEmpty [(Range, ModuleName)] -> [(Range, ModuleName)])
-> NonEmpty [(Range, ModuleName)] -> [(Range, ModuleName)]
forall a b. (a -> b) -> a -> b
$ List1 ModuleName
ms List1 ModuleName
-> (ModuleName -> [(Range, ModuleName)])
-> NonEmpty [(Range, ModuleName)]
forall (f :: * -> *) a b. Functor f => f a -> (a -> b) -> f b
<&> \ 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
forall a. HasNameBindingSite a => a -> 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.
        reportSLn "scope.class.error" 30 $ "rangeful clashing modules = " ++ prettyShow rms

        -- If even this fails, we pick the first m and give no range.
        return $ fromMaybe (noRange, m0) $ listToMaybe rms

      return . (,r) . fsep $
        pwords "Duplicate definition of module" ++ [prettyTCM x <> "."] ++
        pwords "Previous definition of" ++ [help m] ++ pwords "module" ++ [prettyTCM x] ++
        pwords "at" ++ [prettyTCM r]
      where
        help :: MonadPretty m => ModuleName -> m Doc
        help :: forall (m :: * -> *). MonadPretty m => ModuleName -> m Doc
help ModuleName
m = m (Maybe DataOrRecordModule)
-> m Doc -> (DataOrRecordModule -> m Doc) -> m Doc
forall (m :: * -> *) a b.
Monad m =>
m (Maybe a) -> m b -> (a -> m b) -> m b
caseMaybeM (ModuleName -> m (Maybe DataOrRecordModule)
forall (m :: * -> *).
ReadTCState m =>
ModuleName -> m (Maybe DataOrRecordModule)
isDatatypeModule ModuleName
m) m Doc
forall a. Null a => a
empty ((DataOrRecordModule -> m Doc) -> m Doc)
-> (DataOrRecordModule -> m Doc) -> m Doc
forall a b. (a -> b) -> a -> b
$ \case
          DataOrRecordModule
IsDataModule   -> m Doc
"(datatype)"
          DataOrRecordModule
IsRecordModule -> m Doc
"(record)"

instance PrettyTCM TopLevelModuleNameWithSourceFile where
  prettyTCM :: forall (m :: * -> *).
MonadPretty m =>
TopLevelModuleNameWithSourceFile -> m Doc
prettyTCM (TopLevelModuleNameWithSourceFile TopLevelModuleName
x SourceFile
file) = do
    path <- SourceFile -> m AbsolutePath
forall (m :: * -> *). MonadFileId m => SourceFile -> m AbsolutePath
srcFilePath SourceFile
file
    let x' = Range -> TopLevelModuleName -> TopLevelModuleName
forall a. SetRange a => Range -> a -> a
setRange (AbsolutePath -> Range
rangeFromAbsolutePath AbsolutePath
path) TopLevelModuleName
x
    pretty (PrintRange x')

instance PrettyTCM MissingTypeSignatureInfo where
  prettyTCM :: forall (m :: * -> *).
MonadPretty m =>
MissingTypeSignatureInfo -> m Doc
prettyTCM = \case
    MissingDataSignature Name
x       -> [m Doc] -> m Doc
forall (m :: * -> *) (t :: * -> *).
(Applicative m, Foldable t) =>
t (m Doc) -> m Doc
fsep [ m Doc
"data"  , m Doc
"definition", Name -> m Doc
forall a (m :: * -> *). (PrettyTCM a, MonadPretty m) => a -> m Doc
forall (m :: * -> *). MonadPretty m => Name -> m Doc
prettyTCM Name
x ]
    MissingRecordSignature Name
x     -> [m Doc] -> m Doc
forall (m :: * -> *) (t :: * -> *).
(Applicative m, Foldable t) =>
t (m Doc) -> m Doc
fsep [ m Doc
"record", m Doc
"definition", Name -> m Doc
forall a (m :: * -> *). (PrettyTCM a, MonadPretty m) => a -> m Doc
forall (m :: * -> *). MonadPretty m => Name -> m Doc
prettyTCM Name
x ]
    MissingFunctionSignature LHS
lhs -> [m Doc] -> m Doc
forall (m :: * -> *) (t :: * -> *).
(Applicative m, Foldable t) =>
t (m Doc) -> m Doc
fsep [ m Doc
"left", m Doc
"hand", m Doc
"side", LHS -> m Doc
forall a (m :: * -> *). (PrettyTCM a, MonadPretty m) => a -> m Doc
forall (m :: * -> *). MonadPretty m => LHS -> m Doc
prettyTCM LHS
lhs ]

notCmp :: MonadPretty m => Comparison -> m Doc
notCmp :: forall (m :: * -> *). MonadPretty m => Comparison -> m Doc
notCmp Comparison
cmp = m Doc
"!" 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
forall (m :: * -> *). MonadPretty m => Comparison -> m Doc
prettyTCM Comparison
cmp
instance PrettyTCM NegativeUnification where
  prettyTCM :: forall (m :: * -> *). MonadPretty m => NegativeUnification -> m Doc
prettyTCM NegativeUnification
err = case NegativeUnification
err of
    UnifyConflict Telescope
tel Term
u Term
v -> Telescope -> m Doc -> m Doc
forall b (m :: * -> *) a.
(AddContext b, MonadAddContext m) =>
b -> m a -> m a
forall (m :: * -> *) a.
MonadAddContext m =>
Telescope -> m a -> m a
addContext Telescope
tel (m Doc -> m Doc) -> m Doc -> m Doc
forall a b. (a -> b) -> a -> b
$ [m Doc] -> m Doc
forall (m :: * -> *) (t :: * -> *).
(Applicative m, Foldable t) =>
t (m Doc) -> m Doc
vcat ([m Doc] -> m Doc) -> [m Doc] -> m Doc
forall a b. (a -> b) -> a -> b
$
      [ [m Doc] -> m Doc
forall (m :: * -> *) (t :: * -> *).
(Applicative m, Foldable t) =>
t (m Doc) -> m Doc
fsep ([m Doc] -> m Doc) -> [m Doc] -> m Doc
forall a b. (a -> b) -> a -> b
$ String -> [m Doc]
forall (m :: * -> *). Applicative m => String -> [m Doc]
pwords String
"because unification ended with a conflicting equation "
      , Int -> m Doc -> m Doc
forall (m :: * -> *). Functor m => Int -> m Doc -> m Doc
nest Int
2 (m Doc -> m Doc) -> m Doc -> m Doc
forall a b. (a -> b) -> a -> b
$ Term -> m Doc
forall a (m :: * -> *). (PrettyTCM a, MonadPretty m) => a -> m Doc
forall (m :: * -> *). MonadPretty m => Term -> 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 -> 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
forall (m :: * -> *). MonadPretty m => Term -> m Doc
prettyTCM Term
v
      ]

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

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

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

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

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



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

class Verbalize a where
  verbalize :: a -> String

instance Verbalize Hiding where
  verbalize :: Hiding -> String
verbalize = Hiding -> String
hidingToString

-- | Indefinite article.
newtype Indefinite a = Indefinite a

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

-- | Number rendered as an ordinal (@1st@, @2nd@, etc)
newtype Ordinal = Ordinal Int
instance Verbalize Ordinal where
  verbalize :: Ordinal -> String
verbalize (Ordinal Int
n) = case Int
n Int -> Int -> Int
forall a. Integral a => a -> a -> a
`mod` Int
10 of
    Int
1 -> Int -> String
forall a. Show a => a -> String
show Int
n String -> String -> String
forall a. Semigroup a => a -> a -> a
<> String
"st"
    Int
2 -> Int -> String
forall a. Show a => a -> String
show Int
n String -> String -> String
forall a. Semigroup a => a -> a -> a
<> String
"nd"
    Int
3 -> Int -> String
forall a. Show a => a -> String
show Int
n String -> String -> String
forall a. Semigroup a => a -> a -> a
<> String
"rd"
    Int
_ -> Int -> String
forall a. Show a => a -> String
show Int
n String -> String -> String
forall a. Semigroup a => a -> a -> a
<> String
"th"