module Agda.TypeChecking.Pretty.Warning
  ( applyFlagsToTCWarnings
  , applyFlagsToTCWarningsPreserving
  , filterTCWarnings
  , getAllUnsolvedWarnings
  , getAllWarnings
  , getAllWarningsOfTCErr
  , getAllWarningsPreserving
  , prettyDuplicateFields
  , prettyTCWarnings
  , prettyTCWarnings'
  , prettyTooManyFields
  , prettyWarning
  , tcWarningsToError
  )
where

import Prelude hiding ( null )

import Control.Monad ( guard, filterM, forM, (<=<) )

import Data.Char ( toLower )
import qualified Data.Foldable as Fold
import Data.Function (on)
import qualified Data.List as List
import Data.Maybe
import Data.Set (Set)
import qualified Data.Set  as Set
import qualified Data.Text as T

import Agda.TypeChecking.Monad.Base
import qualified Agda.TypeChecking.Monad.Base.Warning as W
import Agda.TypeChecking.Monad.Builtin
import {-# SOURCE #-} Agda.TypeChecking.Errors
import Agda.TypeChecking.Monad.MetaVars
import Agda.TypeChecking.Monad.Options
import Agda.TypeChecking.Monad.Debug
import Agda.TypeChecking.Monad.Constraints
import Agda.TypeChecking.Monad.State ( getScope )
import Agda.TypeChecking.Monad ( localTCState, enterClosure )
import Agda.TypeChecking.Positivity () --instance only
import Agda.TypeChecking.Pretty
import Agda.TypeChecking.Pretty.Call () -- instance PrettyTCM CallInfo
import {-# SOURCE #-} Agda.TypeChecking.Pretty.Constraint (prettyInterestingConstraints, interestingConstraint)
import Agda.TypeChecking.Warnings (MonadWarning, isUnsolvedWarning, onlyShowIfUnsolved, classifyWarning, WhichWarnings(..), warning_)
import {-# SOURCE #-} Agda.TypeChecking.MetaVars

import Agda.Syntax.Common
  ( ImportedName'(..), fromImportedName, partitionImportedNames
  , IsOpaque(OpaqueDef, TransparentDef)
  , ProjOrigin(..)
  , getHiding
  )
import Agda.Syntax.Common.Pretty ( Pretty, prettyShow, singPlural )
import qualified Agda.Syntax.Common.Pretty as P
import qualified Agda.Syntax.Concrete as C
import Agda.Syntax.Internal
import Agda.Syntax.Position
import Agda.Syntax.Scope.Base ( concreteNamesInScope, NameOrModule(..) )
import Agda.Syntax.Translation.InternalToAbstract

import Agda.Interaction.Options
import Agda.Interaction.Options.Errors
import Agda.Interaction.Options.Warnings

import Agda.Utils.Boolean  ( toBool )
import Agda.Utils.FileName ( filePath )
import Agda.Utils.Functor  ( (<.>) )
import Agda.Utils.Lens
import Agda.Utils.List ( editDistance )
import Agda.Utils.List1 ( List1, pattern (:|), (<|) )
import qualified Agda.Utils.List1 as List1
import Agda.Utils.Monad ( anyM, ifM )
import Agda.Utils.Null
import Agda.Utils.Singleton
import qualified Agda.Utils.Set1 as Set1
import Agda.Utils.WithDefault  ( pattern Value )
import qualified Agda.Utils.VarSet as VarSet

import Agda.Utils.Impossible

instance PrettyTCM TCWarning where
  prettyTCM :: forall (m :: * -> *). MonadPretty m => TCWarning -> m Doc
prettyTCM w :: TCWarning
w@(TCWarning CallStack
loc Range
_ Warning
_ Doc
doc [Char]
_ Bool
_) = Doc
doc Doc -> m () -> m Doc
forall a b. a -> m b -> m a
forall (f :: * -> *) a b. Functor f => a -> f b -> f a
<$ do
    [Char] -> VerboseLevel -> [Char] -> m ()
forall (m :: * -> *).
MonadDebug m =>
[Char] -> VerboseLevel -> [Char] -> m ()
reportSLn [Char]
"warning" VerboseLevel
2 ([Char] -> m ()) -> [Char] -> m ()
forall a b. (a -> b) -> a -> b
$ [Char]
"Warning raised at " [Char] -> [Char] -> [Char]
forall a. [a] -> [a] -> [a]
++ CallStack -> [Char]
forall a. Pretty a => a -> [Char]
prettyShow CallStack
loc

instance PrettyTCM Warning where
  prettyTCM :: forall (m :: * -> *). MonadPretty m => Warning -> m Doc
prettyTCM = Warning -> m Doc
forall (m :: * -> *). MonadPretty m => Warning -> m Doc
prettyWarning

{-# SPECIALIZE prettyWarning :: Warning -> TCM Doc #-}
prettyWarning :: MonadPretty m => Warning -> m Doc
prettyWarning :: forall (m :: * -> *). MonadPretty m => Warning -> m Doc
prettyWarning = \case

    UnsolvedMetaVariables Set1 Range
ms  ->
      [m Doc] -> m Doc
forall (m :: * -> *) (t :: * -> *).
(Applicative m, Foldable t) =>
t (m Doc) -> m Doc
fsep ( [Char] -> [m Doc]
forall (m :: * -> *). Applicative m => [Char] -> [m Doc]
pwords [Char]
"Unsolved metas at the following locations:" )
      m Doc -> m Doc -> m Doc
forall (m :: * -> *). Applicative m => m Doc -> m Doc -> m Doc
$$ VerboseLevel -> m Doc -> m Doc
forall (m :: * -> *). Functor m => VerboseLevel -> m Doc -> m Doc
nest VerboseLevel
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
$ (Range -> m Doc) -> List1 Range -> 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 Range -> m Doc
forall a (m :: * -> *). (PrettyTCM a, MonadPretty m) => a -> m Doc
forall (m :: * -> *). MonadPretty m => Range -> m Doc
prettyTCM (List1 Range -> NonEmpty (m Doc))
-> List1 Range -> NonEmpty (m Doc)
forall a b. (a -> b) -> a -> b
$ Set1 Range -> List1 Range
forall a. NESet a -> NonEmpty a
Set1.toAscList Set1 Range
ms)

    UnsolvedInteractionMetas Set1 Range
is ->
      [m Doc] -> m Doc
forall (m :: * -> *) (t :: * -> *).
(Applicative m, Foldable t) =>
t (m Doc) -> m Doc
fsep ( [Char] -> [m Doc]
forall (m :: * -> *). Applicative m => [Char] -> [m Doc]
pwords [Char]
"Unsolved interaction metas at the following locations:" )
      m Doc -> m Doc -> m Doc
forall (m :: * -> *). Applicative m => m Doc -> m Doc -> m Doc
$$ VerboseLevel -> m Doc -> m Doc
forall (m :: * -> *). Functor m => VerboseLevel -> m Doc -> m Doc
nest VerboseLevel
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
$ (Range -> m Doc) -> List1 Range -> 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 Range -> m Doc
forall a (m :: * -> *). (PrettyTCM a, MonadPretty m) => a -> m Doc
forall (m :: * -> *). MonadPretty m => Range -> m Doc
prettyTCM (List1 Range -> NonEmpty (m Doc))
-> List1 Range -> NonEmpty (m Doc)
forall a b. (a -> b) -> a -> b
$ Set1 Range -> List1 Range
forall a. NESet a -> NonEmpty a
Set1.toAscList Set1 Range
is)

    InteractionMetaBoundaries Set1 Range
is ->
      [m Doc] -> m Doc
forall (m :: * -> *) (t :: * -> *).
(Applicative m, Foldable t) =>
t (m Doc) -> m Doc
fsep ( [Char] -> [m Doc]
forall (m :: * -> *). Applicative m => [Char] -> [m Doc]
pwords [Char]
"Interaction meta(s) at the following location(s) have unsolved boundary constraints:" )
      m Doc -> m Doc -> m Doc
forall (m :: * -> *). Applicative m => m Doc -> m Doc -> m Doc
$$ VerboseLevel -> m Doc -> m Doc
forall (m :: * -> *). Functor m => VerboseLevel -> m Doc -> m Doc
nest VerboseLevel
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
$ (Range -> m Doc) -> List1 Range -> 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 Range -> m Doc
forall a (m :: * -> *). (PrettyTCM a, MonadPretty m) => a -> m Doc
forall (m :: * -> *). MonadPretty m => Range -> m Doc
prettyTCM (List1 Range -> NonEmpty (m Doc))
-> List1 Range -> NonEmpty (m Doc)
forall a b. (a -> b) -> a -> b
$ Set1 Range -> List1 Range
forall a. NESet a -> NonEmpty a
Set1.toAscList Set1 Range
is)

    UnsolvedConstraints List1 ProblemConstraint
cs -> do
      pcs <- [ProblemConstraint] -> m [Doc]
forall (m :: * -> *).
MonadPretty m =>
[ProblemConstraint] -> m [Doc]
prettyInterestingConstraints ([ProblemConstraint] -> m [Doc]) -> [ProblemConstraint] -> m [Doc]
forall a b. (a -> b) -> a -> b
$ List1 ProblemConstraint -> [Item (List1 ProblemConstraint)]
forall l. IsList l => l -> [Item l]
List1.toList List1 ProblemConstraint
cs
      if null pcs
        then fsep $ pwords "Unsolved constraints"  -- #4065: keep minimal warning text
        else vcat
          [ fsep $ pwords "Failed to solve the following constraints:"
          , nest 2 $ return $ P.vcat $ List.nub pcs
          ]

    TerminationIssue List1 TerminationError
errs1 -> do
      dropTopLevel <- m (QName -> QName)
forall (m :: * -> *).
(MonadDebug m, MonadTCEnv m, ReadTCState m) =>
m (QName -> QName)
topLevelModuleDropper
      let errs = List1 TerminationError -> [Item (List1 TerminationError)]
forall l. IsList l => l -> [Item l]
List1.toList List1 TerminationError
errs1
      let (guardednessHelps, guardednessHelpsNot) =
            List.partition (toBool . termErrGuardednessHelps) errs
      let report [Char]
hint [TerminationError]
because = if [TerminationError] -> Bool
forall a. Null a => a -> Bool
null [TerminationError]
because 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
vcat
              [ [Char] -> m Doc
forall (m :: * -> *). Applicative m => [Char] -> m Doc
fwords [Char]
"Termination checking failed for the following functions:"
              , [Char] -> m Doc
forall (m :: * -> *). Applicative m => [Char] -> m Doc
fwords [Char]
hint
              , VerboseLevel -> m Doc -> m Doc
forall (m :: * -> *). Functor m => VerboseLevel -> m Doc -> m Doc
nest VerboseLevel
2 (m Doc -> m Doc) -> m Doc -> m Doc
forall a b. (a -> b) -> a -> b
$ [m Doc] -> m Doc
forall (m :: * -> *) (t :: * -> *).
(Applicative m, Foldable t) =>
t (m Doc) -> m Doc
fsep ([m Doc] -> m Doc) -> [m Doc] -> m Doc
forall a b. (a -> b) -> a -> b
$ m Doc -> [m Doc] -> [m Doc]
forall (m :: * -> *) (t :: * -> *).
(Applicative m, Semigroup (m Doc), Foldable t) =>
m Doc -> t (m Doc) -> [m Doc]
punctuate m Doc
forall (m :: * -> *). Applicative m => m Doc
comma ([m Doc] -> [m Doc]) -> [m Doc] -> [m Doc]
forall a b. (a -> b) -> a -> b
$
                  (QName -> m Doc) -> [QName] -> [m Doc]
forall a b. (a -> b) -> [a] -> [b]
map (QName -> m Doc
forall (m :: * -> *) a. (Applicative m, Pretty a) => a -> m Doc
pretty (QName -> m Doc) -> (QName -> QName) -> QName -> m Doc
forall b c a. (b -> c) -> (a -> b) -> a -> c
. QName -> QName
dropTopLevel) ([QName] -> [m Doc]) -> [QName] -> [m Doc]
forall a b. (a -> b) -> a -> b
$
                    (TerminationError -> [QName]) -> [TerminationError] -> [QName]
forall (t :: * -> *) a b. Foldable t => (a -> [b]) -> t a -> [b]
concatMap TerminationError -> [QName]
termErrFunctions [TerminationError]
because
              , [Char] -> m Doc
forall (m :: * -> *). Applicative m => [Char] -> m Doc
fwords [Char]
"Problematic calls:"
              , VerboseLevel -> m Doc -> m Doc
forall (m :: * -> *). Functor m => VerboseLevel -> m Doc -> m Doc
nest VerboseLevel
2 (m Doc -> m Doc) -> m Doc -> m Doc
forall a b. (a -> b) -> a -> b
$ ([Doc] -> Doc) -> m [Doc] -> m Doc
forall a b. (a -> b) -> m a -> m b
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap ([Doc] -> Doc
forall (t :: * -> *). Foldable t => t Doc -> Doc
P.vcat ([Doc] -> Doc) -> ([Doc] -> [Doc]) -> [Doc] -> Doc
forall b c a. (b -> c) -> (a -> b) -> a -> c
. [Doc] -> [Doc]
forall a. Eq a => [a] -> [a]
List.nub) (m [Doc] -> m Doc) -> m [Doc] -> m Doc
forall a b. (a -> b) -> a -> b
$
                  (CallInfo -> m Doc) -> [CallInfo] -> m [Doc]
forall (t :: * -> *) (m :: * -> *) a b.
(Traversable t, Monad m) =>
(a -> m b) -> t a -> m (t b)
forall (m :: * -> *) a b. Monad m => (a -> m b) -> [a] -> m [b]
mapM CallInfo -> m Doc
forall a (m :: * -> *). (PrettyTCM a, MonadPretty m) => a -> m Doc
forall (m :: * -> *). MonadPretty m => CallInfo -> m Doc
prettyTCM ([CallInfo] -> m [Doc]) -> [CallInfo] -> m [Doc]
forall a b. (a -> b) -> a -> b
$ (CallInfo -> Range) -> [CallInfo] -> [CallInfo]
forall b a. Ord b => (a -> b) -> [a] -> [a]
List.sortOn CallInfo -> Range
forall a. HasRange a => a -> Range
getRange ([CallInfo] -> [CallInfo]) -> [CallInfo] -> [CallInfo]
forall a b. (a -> b) -> a -> b
$
                    (TerminationError -> [CallInfo])
-> [TerminationError] -> [CallInfo]
forall (t :: * -> *) a b. Foldable t => (a -> [b]) -> t a -> [b]
concatMap TerminationError -> [CallInfo]
termErrCalls [TerminationError]
because
              ]
      -- Andreas, 2025-04-01, issue #6657
      -- Hint towards --guardedness where appropriate, but not when --sized-types is on.
      -- Andreas, 2025-04-12, issue #7796
      -- Also not when --no-guardedness is explicitly given (rather than the default).
      opts <- pragmaOptions
      let haveSizedTypes = PragmaOptions -> Bool
optSizedTypes PragmaOptions
opts
      let guardedness    = PragmaOptions -> WithDefault 'False
_optGuardedness PragmaOptions
opts
      reportSDoc "tc.warning.termination" 50 $ vcat
        [ "printing TerminationIssue"
        , "sized-types = " <+> (text . show) haveSizedTypes
        , "guardedness = " <+> (text . show) guardedness
        ]
      if guardedness == Value False then report empty errs else do
        let
          hint = [[Char]] -> [Char]
forall (t :: * -> *) a. Foldable t => t [a] -> [a]
concat ([[Char]] -> [Char]) -> [[Char]] -> [Char]
forall a b. (a -> b) -> a -> b
$ [[[Char]]] -> [[Char]]
forall (t :: * -> *) a. Foldable t => t [a] -> [a]
concat
            [ [ [Char]
"(Option --guardedness might fix this problem" ]
            , [ [Char]
", but it is not --safe to use with --sized-types" | Bool
haveSizedTypes ]
            , [ [Char]
".)" ]
            ]
        vcat [ report hint guardednessHelps
             , report empty guardednessHelpsNot
             ]

    UnreachableClauses QName
_f List1 Range
pss -> m Doc
"Unreachable" m Doc -> m Doc -> m Doc
forall (m :: * -> *). Applicative m => m Doc -> m Doc -> m Doc
<+> List1 Range -> m Doc -> m Doc
forall (m :: * -> *) a. (Functor m, Sized a) => a -> m Doc -> m Doc
pluralS List1 Range
pss m Doc
"clause"

    CoverageIssue QName
f List1 (Telescope, [NamedArg DeBruijnPattern])
pss -> [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
          [ [Char] -> [m Doc]
forall (m :: * -> *). Applicative m => [Char] -> [m Doc]
pwords [Char]
"Incomplete pattern matching for"
          , [ 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 -> m Doc -> m Doc
forall a. Semigroup a => a -> a -> a
<> m Doc
"." ]
          , [Char] -> [m Doc]
forall (m :: * -> *). Applicative m => [Char] -> [m Doc]
pwords [Char]
"Missing cases:"
          ]
        , VerboseLevel -> m Doc -> m Doc
forall (m :: * -> *). Functor m => VerboseLevel -> m Doc -> m Doc
nest VerboseLevel
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
$ ((Telescope, [NamedArg DeBruijnPattern]) -> m Doc)
-> List1 (Telescope, [NamedArg DeBruijnPattern])
-> 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 (Telescope, [NamedArg DeBruijnPattern]) -> m Doc
display List1 (Telescope, [NamedArg DeBruijnPattern])
pss
        ]
      where
        display :: (Telescope, [NamedArg DeBruijnPattern]) -> m Doc
display (Telescope
tel, [NamedArg DeBruijnPattern]
ps) = NamedClause -> m Doc
forall a (m :: * -> *). (PrettyTCM a, MonadPretty m) => a -> m Doc
forall (m :: * -> *). MonadPretty m => NamedClause -> m Doc
prettyTCM (NamedClause -> m Doc) -> NamedClause -> m Doc
forall a b. (a -> b) -> a -> b
$ QName -> Bool -> Clause -> NamedClause
NamedClause QName
f Bool
True (Clause -> NamedClause) -> Clause -> NamedClause
forall a b. (a -> b) -> a -> b
$
          Clause
forall a. Null a => a
empty { clauseTel = tel, namedClausePats = ps }

    CoverageNoExactSplit QName
f List1 Clause
cs -> 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
$
      [m Doc] -> m Doc
forall (m :: * -> *) (t :: * -> *).
(Applicative m, Foldable t) =>
t (m Doc) -> m Doc
fsep ([Char] -> [m Doc]
forall (m :: * -> *). Applicative m => [Char] -> [m Doc]
pwords [Char]
"Exact splitting is enabled, but the following" [m Doc] -> [m Doc] -> [m Doc]
forall a. [a] -> [a] -> [a]
++ [ List1 Clause -> m Doc -> m Doc
forall (m :: * -> *) a. (Functor m, Sized a) => a -> m Doc -> m Doc
pluralS List1 Clause
cs m Doc
"clause" ] [m Doc] -> [m Doc] -> [m Doc]
forall a. [a] -> [a] -> [a]
++
            [Char] -> [m Doc]
forall (m :: * -> *). Applicative m => [Char] -> [m Doc]
pwords [Char]
"could not be preserved as definitional equalities in the translation to a case tree:"
           ) m Doc -> NonEmpty (m Doc) -> NonEmpty (m Doc)
forall a. a -> NonEmpty a -> NonEmpty a
<|
      (Clause -> m Doc) -> List1 Clause -> 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 (VerboseLevel -> m Doc -> m Doc
forall (m :: * -> *). Functor m => VerboseLevel -> m Doc -> m Doc
nest VerboseLevel
2 (m Doc -> m Doc) -> (Clause -> m Doc) -> Clause -> m Doc
forall b c a. (b -> c) -> (a -> b) -> a -> c
. NamedClause -> m Doc
forall a (m :: * -> *). (PrettyTCM a, MonadPretty m) => a -> m Doc
forall (m :: * -> *). MonadPretty m => NamedClause -> m Doc
prettyTCM (NamedClause -> m Doc)
-> (Clause -> NamedClause) -> Clause -> m Doc
forall b c a. (b -> c) -> (a -> b) -> a -> c
. QName -> Bool -> Clause -> NamedClause
NamedClause QName
f Bool
True) List1 Clause
cs

    InlineNoExactSplit QName
f Clause
c -> [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
$
          [Char] -> [m Doc]
forall (m :: * -> *). Applicative m => [Char] -> [m Doc]
pwords [Char]
"Exact splitting is enabled, but the following clause" [m Doc] -> [m Doc] -> [m Doc]
forall a. [a] -> [a] -> [a]
++
          [Char] -> [m Doc]
forall (m :: * -> *). Applicative m => [Char] -> [m Doc]
pwords [Char]
"is no longer a definitional equality because it was translated to a copattern match:"
      , VerboseLevel -> m Doc -> m Doc
forall (m :: * -> *). Functor m => VerboseLevel -> m Doc -> m Doc
nest VerboseLevel
2 (m Doc -> m Doc) -> (Clause -> m Doc) -> Clause -> m Doc
forall b c a. (b -> c) -> (a -> b) -> a -> c
. NamedClause -> m Doc
forall a (m :: * -> *). (PrettyTCM a, MonadPretty m) => a -> m Doc
forall (m :: * -> *). MonadPretty m => NamedClause -> m Doc
prettyTCM (NamedClause -> m Doc)
-> (Clause -> NamedClause) -> Clause -> m Doc
forall b c a. (b -> c) -> (a -> b) -> a -> c
. QName -> Bool -> Clause -> NamedClause
NamedClause QName
f Bool
True (Clause -> m Doc) -> Clause -> m Doc
forall a b. (a -> b) -> a -> b
$ Clause
c
      ]

    NotStrictlyPositive QName
d Seq OccursWhere
ocs -> [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
d] [m Doc] -> [m Doc] -> [m Doc]
forall a. [a] -> [a] -> [a]
++ [Char] -> [m Doc]
forall (m :: * -> *). Applicative m => [Char] -> [m Doc]
pwords [Char]
"is not strictly positive, because it occurs"
      [m Doc] -> [m Doc] -> [m Doc]
forall a. [a] -> [a] -> [a]
++ [Seq OccursWhere -> m Doc
forall a (m :: * -> *). (PrettyTCM a, MonadPretty m) => a -> m Doc
forall (m :: * -> *). MonadPretty m => Seq OccursWhere -> m Doc
prettyTCM Seq OccursWhere
ocs]

    ConstructorDoesNotFitInData DataOrRecord_
dataOrRecord QName
c Sort
s1 Sort
s2 TCErr
err -> m Doc
msg m Doc -> m Doc -> m Doc
forall (m :: * -> *). Applicative m => m Doc -> m Doc -> m Doc
$$
      case TCErr
err of
        TypeError CallStack
_loc TCState
s Closure TypeError
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
$ Closure TypeError -> (TypeError -> m Doc) -> m Doc
forall (m :: * -> *) c a b.
(MonadTCEnv m, ReadTCState m, LensClosure c a) =>
c -> (a -> m b) -> m b
enterClosure Closure TypeError
e \ TypeError
e ->
          m Doc -> m Doc
forall (m :: * -> *). Functor m => m Doc -> m Doc
parens (m Doc
"Reason:" m Doc -> m Doc -> m Doc
forall (m :: * -> *). Applicative m => m Doc -> m Doc -> m Doc
<+> TypeError -> m Doc
forall a (m :: * -> *). (PrettyTCM a, MonadPretty m) => a -> m Doc
forall (m :: * -> *). MonadPretty m => TypeError -> m Doc
prettyTCM TypeError
e)
        TCErr
_ ->
          TCErr -> m Doc
forall a (m :: * -> *). (PrettyTCM a, MonadPretty m) => a -> m Doc
forall (m :: * -> *). MonadPretty m => TCErr -> m Doc
prettyTCM TCErr
err
      where
        msg :: m Doc
msg = [m Doc] -> m Doc
forall (m :: * -> *) (t :: * -> *).
(Applicative m, Foldable t) =>
t (m Doc) -> m Doc
sep
          [ m Doc
"Constructor" 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
c
          , m Doc
"of inferred 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 Sort
s1
          , (m Doc
"does not fit into" m Doc -> m Doc -> m Doc
forall (m :: * -> *). Applicative m => m Doc -> m Doc -> m Doc
<+> DataOrRecord_ -> m Doc
forall a (m :: * -> *). (PrettyTCM a, MonadPretty m) => a -> m Doc
forall (m :: * -> *). MonadPretty m => DataOrRecord_ -> m Doc
prettyTCM DataOrRecord_
dataOrRecord m Doc -> m Doc -> m Doc
forall (m :: * -> *). Applicative m => m Doc -> m Doc -> m Doc
<+> m Doc
"type of 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 Sort
s2) m Doc -> m Doc -> m Doc
forall a. Semigroup a => a -> a -> a
<> m Doc
"."
          ]

    CoinductiveEtaRecord QName
name -> [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
$ [Char] -> [m Doc]
forall (m :: * -> *). Applicative m => [Char] -> [m Doc]
pwords [Char]
"Not switching on eta-equality for coinductive records."
      , [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
$ [Char] -> [m Doc]
forall (m :: * -> *). Applicative m => [Char] -> [m Doc]
pwords [Char]
"If you must, use pragma" [m Doc] -> [m Doc] -> [m Doc]
forall a. [a] -> [a] -> [a]
++ [ m Doc
"{-# ETA", 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
"#-}" ]
      ]

    UnsupportedIndexedMatch Doc
doc -> [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 ([Char] -> [m Doc]
forall (m :: * -> *). Applicative m => [Char] -> [m Doc]
pwords [Char]
"This clause uses pattern-matching features that are not yet supported by Cubical Agda,"
           [m Doc] -> [m Doc] -> [m Doc]
forall a. [a] -> [a] -> [a]
++ [Char] -> [m Doc]
forall (m :: * -> *). Applicative m => [Char] -> [m Doc]
pwords [Char]
"the function to which it belongs will not compute when applied to transports."
             )
      , m Doc
""
      , m Doc
"Reason:" 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
doc
      , m Doc
""
      ]

    CantGeneralizeOverSorts Set1 MetaId
ms -> do
      rms <- [MetaId] -> (MetaId -> m (Range, MetaId)) -> m [(Range, MetaId)]
forall (t :: * -> *) (m :: * -> *) a b.
(Traversable t, Monad m) =>
t a -> (a -> m b) -> m (t b)
forM (Set1 MetaId -> [MetaId]
forall a. NESet a -> [a]
forall (t :: * -> *) a. Foldable t => t a -> [a]
Fold.toList Set1 MetaId
ms) \ MetaId
x -> (,MetaId
x) (Range -> (Range, MetaId)) -> m Range -> m (Range, MetaId)
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> MetaId -> m Range
forall (m :: * -> *).
(HasCallStack, MonadDebug m, ReadTCState m) =>
MetaId -> m Range
getMetaRange MetaId
x
      vcat
            [ text "Cannot generalize over unsolved sort metas:"
            , nest 2 $ vcat [ prettyTCM x <+> text "at" <+> pretty r | (r,x) <- List.sort rms ]
            , fsep $ pwords "Suggestion: add a `variable Any : Set _` and replace unsolved metas by Any"
            ]

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

    OldBuiltin BuiltinId
old BuiltinId
new -> [Char] -> m Doc
forall (m :: * -> *). Applicative m => [Char] -> m Doc
fwords ([Char] -> m Doc) -> [Char] -> m Doc
forall a b. (a -> b) -> a -> b
$
      [Char]
"Builtin " [Char] -> [Char] -> [Char]
forall a. [a] -> [a] -> [a]
++ BuiltinId -> [Char]
forall a. IsBuiltin a => a -> [Char]
getBuiltinId BuiltinId
old [Char] -> [Char] -> [Char]
forall a. [a] -> [a] -> [a]
++ [Char]
" no longer exists. " [Char] -> [Char] -> [Char]
forall a. [a] -> [a] -> [a]
++
      [Char]
"It is now bound by BUILTIN " [Char] -> [Char] -> [Char]
forall a. [a] -> [a] -> [a]
++ BuiltinId -> [Char]
forall a. IsBuiltin a => a -> [Char]
getBuiltinId BuiltinId
new

    BuiltinDeclaresIdentifier BuiltinId
b -> [Char] -> m Doc
forall (m :: * -> *). Applicative m => [Char] -> m Doc
fwords ([Char] -> m Doc) -> [Char] -> m Doc
forall a b. (a -> b) -> a -> b
$
      [Char]
"BUILTIN " [Char] -> [Char] -> [Char]
forall a. [a] -> [a] -> [a]
++ BuiltinId -> [Char]
forall a. IsBuiltin a => a -> [Char]
getBuiltinId BuiltinId
b [Char] -> [Char] -> [Char]
forall a. [a] -> [a] -> [a]
++ [Char]
" declares an identifier " [Char] -> [Char] -> [Char]
forall a. [a] -> [a] -> [a]
++
      [Char]
"(no longer expects an already defined identifier)"

    Warning
EmptyRewritePragma -> [m Doc] -> m Doc
forall (m :: * -> *) (t :: * -> *).
(Applicative m, Foldable t) =>
t (m Doc) -> m Doc
fsep ([m Doc] -> m Doc) -> ([Char] -> [m Doc]) -> [Char] -> m Doc
forall b c a. (b -> c) -> (a -> b) -> a -> c
. [Char] -> [m Doc]
forall (m :: * -> *). Applicative m => [Char] -> [m Doc]
pwords ([Char] -> m Doc) -> [Char] -> m Doc
forall a b. (a -> b) -> a -> b
$ [Char]
"Empty REWRITE pragma"

    Warning
EmptyWhere         -> [m Doc] -> m Doc
forall (m :: * -> *) (t :: * -> *).
(Applicative m, Foldable t) =>
t (m Doc) -> m Doc
fsep ([m Doc] -> m Doc) -> ([Char] -> [m Doc]) -> [Char] -> m Doc
forall b c a. (b -> c) -> (a -> b) -> a -> c
. [Char] -> [m Doc]
forall (m :: * -> *). Applicative m => [Char] -> [m Doc]
pwords ([Char] -> m Doc) -> [Char] -> m Doc
forall a b. (a -> b) -> a -> b
$ [Char]
"Empty `where' block (ignored)"

    -- TODO: linearity
    -- FixingQuantity s q q' -> fsep $ concat
    --   [ pwords "Replacing illegal quantity", [ pretty q ], pwords s, [ "by", pretty q' ] ]

    FixingRelevance [Char]
s Relevance
r Relevance
r' -> [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
      [ [Char] -> [m Doc]
forall (m :: * -> *). Applicative m => [Char] -> [m Doc]
pwords [Char]
"Replacing illegal relevance", [ Relevance -> m Doc
forall {m :: * -> *} {a}.
(Applicative m, Verbalize a) =>
a -> m Doc
p Relevance
r ]
      , [Char] -> [m Doc]
forall (m :: * -> *). Applicative m => [Char] -> [m Doc]
pwords [Char]
s, [ m Doc
"by", Relevance -> m Doc
forall {m :: * -> *} {a}.
(Applicative m, Verbalize a) =>
a -> m Doc
p Relevance
r' ]
      ]
      where p :: a -> m Doc
p a
r = [Char] -> m Doc
forall (m :: * -> *). Applicative m => [Char] -> m Doc
text ([Char] -> m Doc) -> [Char] -> m Doc
forall a b. (a -> b) -> a -> b
$ [Char]
"`" [Char] -> [Char] -> [Char]
forall a. [a] -> [a] -> [a]
++ a -> [Char]
forall a. Verbalize a => a -> [Char]
verbalize a
r [Char] -> [Char] -> [Char]
forall a. [a] -> [a] -> [a]
++ [Char]
"'"

    FixingCohesion [Char]
s Cohesion
c Cohesion
c' -> [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
      [ [Char] -> [m Doc]
forall (m :: * -> *). Applicative m => [Char] -> [m Doc]
pwords [Char]
"Replacing illegal cohesion", [ Cohesion -> m Doc
forall {m :: * -> *} {a}.
(Applicative m, Verbalize a) =>
a -> m Doc
p Cohesion
c ]
      , [Char] -> [m Doc]
forall (m :: * -> *). Applicative m => [Char] -> [m Doc]
pwords [Char]
s, [ m Doc
"by", Cohesion -> m Doc
forall {m :: * -> *} {a}.
(Applicative m, Verbalize a) =>
a -> m Doc
p Cohesion
c' ]
      ]
      where p :: a -> m Doc
p a
c = [Char] -> m Doc
forall (m :: * -> *). Applicative m => [Char] -> m Doc
text ([Char] -> m Doc) -> [Char] -> m Doc
forall a b. (a -> b) -> a -> b
$ [Char]
"`" [Char] -> [Char] -> [Char]
forall a. [a] -> [a] -> [a]
++ a -> [Char]
forall a. Verbalize a => a -> [Char]
verbalize a
c [Char] -> [Char] -> [Char]
forall a. [a] -> [a] -> [a]
++ [Char]
"'"

    FixingPolarity [Char]
s PolarityModality
q PolarityModality
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]] -> [m Doc]
forall (t :: * -> *) a. Foldable t => t [a] -> [a]
concat
      [ [Char] -> [m Doc]
forall (m :: * -> *). Applicative m => [Char] -> [m Doc]
pwords [Char]
"Replacing illegal polarity", [ PolarityModality -> m Doc
forall {m :: * -> *} {a}.
(Applicative m, Verbalize a) =>
a -> m Doc
p PolarityModality
q ]
      , [Char] -> [m Doc]
forall (m :: * -> *). Applicative m => [Char] -> [m Doc]
pwords [Char]
s, [ m Doc
"by", PolarityModality -> m Doc
forall {m :: * -> *} {a}.
(Applicative m, Verbalize a) =>
a -> m Doc
p PolarityModality
q' ]
      ]
      where p :: a -> m Doc
p a
q = [Char] -> m Doc
forall (m :: * -> *). Applicative m => [Char] -> m Doc
text ([Char] -> m Doc) -> [Char] -> m Doc
forall a b. (a -> b) -> a -> b
$ [Char]
"`" [Char] -> [Char] -> [Char]
forall a. [a] -> [a] -> [a]
++ a -> [Char]
forall a. Verbalize a => a -> [Char]
verbalize a
q [Char] -> [Char] -> [Char]
forall a. [a] -> [a] -> [a]
++ [Char]
"'"

    IllformedAsClause [Char]
s -> [m Doc] -> m Doc
forall (m :: * -> *) (t :: * -> *).
(Applicative m, Foldable t) =>
t (m Doc) -> m Doc
fsep ([m Doc] -> m Doc) -> ([Char] -> [m Doc]) -> [Char] -> m Doc
forall b c a. (b -> c) -> (a -> b) -> a -> c
. [Char] -> [m Doc]
forall (m :: * -> *). Applicative m => [Char] -> [m Doc]
pwords ([Char] -> m Doc) -> [Char] -> m Doc
forall a b. (a -> b) -> a -> b
$
      [Char]
"`as' must be followed by an identifier" [Char] -> [Char] -> [Char]
forall a. [a] -> [a] -> [a]
++ [Char]
s

    ClashesViaRenaming NameOrModule
nm Set1 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
$ [[m Doc]] -> [m Doc]
forall (t :: * -> *) a. Foldable t => t [a] -> [a]
concat ([[m Doc]] -> [m Doc]) -> [[m Doc]] -> [m Doc]
forall a b. (a -> b) -> a -> b
$
      [ [ case NameOrModule
nm of NameOrModule
NameNotModule -> m Doc
"Name"; NameOrModule
ModuleNotName -> m Doc
"Module" ]
      , [Char] -> [m Doc]
forall (m :: * -> *). Applicative m => [Char] -> [m Doc]
pwords [Char]
"clashes introduced by `renaming':"
      , (Name -> m Doc) -> [Name] -> [m Doc]
forall a b. (a -> b) -> [a] -> [b]
map Name -> m Doc
forall a (m :: * -> *). (PrettyTCM a, MonadPretty m) => a -> m Doc
forall (m :: * -> *). MonadPretty m => Name -> m Doc
prettyTCM ([Name] -> [m Doc]) -> [Name] -> [m Doc]
forall a b. (a -> b) -> a -> b
$ Set1 Name -> [Name]
forall a. NESet a -> [a]
forall (t :: * -> *) a. Foldable t => t a -> [a]
Fold.toList Set1 Name
xs
      ]

    UselessPatternDeclarationForRecord [Char]
s -> [Char] -> m Doc
forall (m :: * -> *). Applicative m => [Char] -> m Doc
fwords ([Char] -> m Doc) -> [Char] -> m Doc
forall a b. (a -> b) -> a -> b
$ [[Char]] -> [Char]
unwords
      [ [Char]
"`pattern' attribute ignored for", [Char]
s, [Char]
"record" ]
      -- the @s@ is a qualifier like "eta" or "coinductive"

    UselessPublic UselessPublicReason
reason ->
      case UselessPublicReason
reason of
         UselessPublicReason
UselessPublicLet
           -> [Char] -> m Doc
forall (m :: * -> *). Applicative m => [Char] -> m Doc
fwords ([Char] -> m Doc) -> [Char] -> m Doc
forall a b. (a -> b) -> a -> b
$ [Char]
"Ignoring `public'; useless in let bindings"
         UselessPublicReason
UselessPublicNoOpen
           -> [Char] -> m Doc
forall (m :: * -> *). Applicative m => [Char] -> m Doc
fwords ([Char] -> m Doc) -> [Char] -> m Doc
forall a b. (a -> b) -> a -> b
$ [Char]
"Ignoring `public'; useless without `open' here"
         UselessPublicReason
UselessPublicPreamble
           -> [Char] -> m Doc
forall (m :: * -> *). Applicative m => [Char] -> m Doc
fwords ([Char] -> m Doc) -> [Char] -> m Doc
forall a b. (a -> b) -> a -> b
$ [Char]
"Ignoring `public'; cannot reexport outside of the `module' body"
         UselessPublicReason
UselessPublicAnonymousModule
           -> [Char] -> m Doc
forall (m :: * -> *). Applicative m => [Char] -> m Doc
fwords ([Char] -> m Doc) -> [Char] -> m Doc
forall a b. (a -> b) -> a -> b
$ [Char]
"Ignoring `public'; cannot reexport from unopened anonymous module"

    UselessHiding List1 ImportedName
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
$ [[m Doc]] -> [m Doc]
forall (t :: * -> *) a. Foldable t => t [a] -> [a]
concat
      [ [Char] -> [m Doc]
forall (m :: * -> *). Applicative m => [Char] -> [m Doc]
pwords [Char]
"Ignoring names in `hiding' directive:"
      , 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
      ]

    UselessInline 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
$
      [Char] -> [m Doc]
forall (m :: * -> *). Applicative m => [Char] -> [m Doc]
pwords [Char]
"It is pointless for INLINE'd function" [m Doc] -> [m Doc] -> [m Doc]
forall a. [a] -> [a] -> [a]
++ [QName -> m Doc
forall a (m :: * -> *). (PrettyTCM a, MonadPretty m) => a -> m Doc
forall (m :: * -> *). MonadPretty m => QName -> m Doc
prettyTCM QName
q] [m Doc] -> [m Doc] -> [m Doc]
forall a. [a] -> [a] -> [a]
++
      [Char] -> [m Doc]
forall (m :: * -> *). Applicative m => [Char] -> [m Doc]
pwords [Char]
"to have a separate Haskell definition"

    Warning
UselessTactic -> [Char] -> m Doc
forall (m :: * -> *). Applicative m => [Char] -> m Doc
fwords ([Char] -> m Doc) -> [Char] -> m Doc
forall a b. (a -> b) -> a -> b
$ [Char]
"Ignoring `tactic' attribute for non-hidden (explicit or instance) binder"

    Warning
WrongInstanceDeclaration -> [Char] -> m Doc
forall (m :: * -> *). Applicative m => [Char] -> m Doc
fwords ([Char] -> m Doc) -> [Char] -> m Doc
forall a b. (a -> b) -> a -> b
$
      [Char]
"Instances should be of type {Γ} → C, where C evaluates to a postulated name or the name of " [Char] -> [Char] -> [Char]
forall a. [a] -> [a] -> [a]
++
      [Char]
"a data or record type, so `instance' is ignored here."

    InstanceWithExplicitArg 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
$
      [Char] -> [m Doc]
forall (m :: * -> *). Applicative m => [Char] -> [m Doc]
pwords [Char]
"Instance declarations with explicit arguments are never considered by instance search," [m Doc] -> [m Doc] -> [m Doc]
forall a. [a] -> [a] -> [a]
++
      [Char] -> [m Doc]
forall (m :: * -> *). Applicative m => [Char] -> [m Doc]
pwords [Char]
"so making" [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]
++ [Char] -> [m Doc]
forall (m :: * -> *). Applicative m => [Char] -> [m Doc]
pwords [Char]
"into an instance has no effect."

    InstanceNoOutputTypeName Doc
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
$
      [Char] -> [m Doc]
forall (m :: * -> *). Applicative m => [Char] -> [m Doc]
pwords [Char]
"Instance arguments whose type is not {Γ} → C, where C evaluates to a postulated type, " [m Doc] -> [m Doc] -> [m Doc]
forall a. [a] -> [a] -> [a]
++
      [Char] -> [m Doc]
forall (m :: * -> *). Applicative m => [Char] -> [m Doc]
pwords [Char]
"a parameter type or the name of a data or record type, are never considered by instance search," [m Doc] -> [m Doc] -> [m Doc]
forall a. [a] -> [a] -> [a]
++
      [Char] -> [m Doc]
forall (m :: * -> *). Applicative m => [Char] -> [m Doc]
pwords [Char]
"so having an instance argument" [m Doc] -> [m Doc] -> [m Doc]
forall a. [a] -> [a] -> [a]
++ [Doc -> m Doc
forall a. a -> m a
forall (m :: * -> *) a. Monad m => a -> m a
return Doc
b] [m Doc] -> [m Doc] -> [m Doc]
forall a. [a] -> [a] -> [a]
++ [Char] -> [m Doc]
forall (m :: * -> *). Applicative m => [Char] -> [m Doc]
pwords [Char]
"has no effect."

    InstanceArgWithExplicitArg Doc
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
$
      [Char] -> [m Doc]
forall (m :: * -> *). Applicative m => [Char] -> [m Doc]
pwords [Char]
"Instance arguments with explicit arguments are never considered by instance search," [m Doc] -> [m Doc] -> [m Doc]
forall a. [a] -> [a] -> [a]
++
      [Char] -> [m Doc]
forall (m :: * -> *). Applicative m => [Char] -> [m Doc]
pwords [Char]
"so having an instance argument" [m Doc] -> [m Doc] -> [m Doc]
forall a. [a] -> [a] -> [a]
++ [Doc -> m Doc
forall a. a -> m a
forall (m :: * -> *) a. Monad m => a -> m a
return Doc
b] [m Doc] -> [m Doc] -> [m Doc]
forall a. [a] -> [a] -> [a]
++ [Char] -> [m Doc]
forall (m :: * -> *). Applicative m => [Char] -> [m Doc]
pwords [Char]
"has no effect."

    InversionDepthReached QName
f -> do
      maxDepth <- m VerboseLevel
forall (m :: * -> *). HasOptions m => m VerboseLevel
maxInversionDepth
      fsep $ pwords "Refusing to invert pattern matching of" ++ [prettyTCM f] ++
             pwords ("because the maximum depth (" ++ show maxDepth ++ ") has been reached.") ++
             pwords "Most likely this means you have an unsatisfiable constraint, but it could" ++
             pwords "also mean that you need to increase the maximum depth using the flag" ++
             pwords "--inversion-max-depth=N"

    InvalidCharacterLiteral Char
c -> [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
$
      [Char] -> [m Doc]
forall (m :: * -> *). Applicative m => [Char] -> [m Doc]
pwords [Char]
"Invalid character literal" [m Doc] -> [m Doc] -> [m Doc]
forall a. [a] -> [a] -> [a]
++ [[Char] -> m Doc
forall (m :: * -> *). Applicative m => [Char] -> m Doc
text ([Char] -> m Doc) -> [Char] -> m Doc
forall a b. (a -> b) -> a -> b
$ Char -> [Char]
forall a. Show a => a -> [Char]
show Char
c] [m Doc] -> [m Doc] -> [m Doc]
forall a. [a] -> [a] -> [a]
++
      [Char] -> [m Doc]
forall (m :: * -> *). Applicative m => [Char] -> [m Doc]
pwords [Char]
"(surrogate code points are not supported)"

    UselessPragma Range
_r Doc
d -> Doc -> m Doc
forall a. a -> m a
forall (m :: * -> *) a. Monad m => a -> m a
return Doc
d

    SafeFlagPostulate 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
$
      [Char] -> [m Doc]
forall (m :: * -> *). Applicative m => [Char] -> [m Doc]
pwords [Char]
"Cannot postulate" [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]
++ [Char] -> [m Doc]
forall (m :: * -> *). Applicative m => [Char] -> [m Doc]
pwords [Char]
"with safe flag"

    SafeFlagPragma Set [Char]
sset -> [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 (t :: * -> *) a. Foldable t => t [a] -> [a]
concat
      [ [ [Char] -> m Doc
forall (m :: * -> *). Applicative m => [Char] -> m Doc
fwords ([Char] -> m Doc) -> [Char] -> m Doc
forall a b. (a -> b) -> a -> b
$ [[Char]]
-> ([Char] -> [Char]) -> ([Char] -> [Char]) -> [Char] -> [Char]
forall a c. Sized a => a -> c -> c -> c
singPlural ([Char] -> [[Char]]
words ([Char] -> [[Char]]) -> [[Char]] -> [[Char]]
forall (m :: * -> *) a b. Monad m => (a -> m b) -> m a -> m b
=<< [[Char]]
xs) [Char] -> [Char]
forall a. a -> a
id ([Char] -> [Char] -> [Char]
forall a. [a] -> [a] -> [a]
++ [Char]
"s") [Char]
"The --safe mode does not allow OPTIONS pragma" ]
      , ([Char] -> m Doc) -> [[Char]] -> [m Doc]
forall a b. (a -> b) -> [a] -> [b]
map [Char] -> m Doc
forall (m :: * -> *). Applicative m => [Char] -> m Doc
text [[Char]]
xs
      ]
      where xs :: [[Char]]
xs = Set [Char] -> [[Char]]
forall a. Set a -> [a]
Set.toAscList Set [Char]
sset

    Warning
SafeFlagWithoutKFlagPrimEraseEquality -> [m Doc] -> m Doc
forall (m :: * -> *) (t :: * -> *).
(Applicative m, Foldable t) =>
t (m Doc) -> m Doc
fsep ([Char] -> [m Doc]
forall (m :: * -> *). Applicative m => [Char] -> [m Doc]
pwords [Char]
"Cannot use primEraseEquality with safe and without-K flags.")

    Warning
WithoutKFlagPrimEraseEquality -> [m Doc] -> m Doc
forall (m :: * -> *) (t :: * -> *).
(Applicative m, Foldable t) =>
t (m Doc) -> m Doc
fsep ([Char] -> [m Doc]
forall (m :: * -> *). Applicative m => [Char] -> [m Doc]
pwords [Char]
"Using primEraseEquality with the without-K flag is inconsistent.")

    ConflictingPragmaOptions [Char]
a [Char]
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
$ [Char] -> [m Doc]
forall (m :: * -> *). Applicative m => [Char] -> [m Doc]
pwords ([Char] -> [m Doc]) -> [Char] -> [m Doc]
forall a b. (a -> b) -> a -> b
$ [[Char]] -> [Char]
unwords
      [ [Char]
"Conflicting options", [Char] -> [Char]
yes [Char]
a, [Char]
"and", [Char] -> [Char]
no [Char]
b, [Char]
"(" [Char] -> [Char] -> [Char]
forall a. [a] -> [a] -> [a]
++ [Char] -> [Char]
yes [Char]
a, [Char]
"implies", [Char] -> [Char]
yes [Char]
b [Char] -> [Char] -> [Char]
forall a. [a] -> [a] -> [a]
++ [Char]
")."
      , [Char]
"Ignoring", [Char] -> [Char]
no [Char]
b [Char] -> [Char] -> [Char]
forall a. [a] -> [a] -> [a]
++ [Char]
"." ]
      where
        yes :: [Char] -> [Char]
yes [Char]
s = [Char]
"--" [Char] -> [Char] -> [Char]
forall a. [a] -> [a] -> [a]
++ [Char]
s
        no :: [Char] -> [Char]
no (Char
'n' : Char
'o' : Char
'-' : [Char]
s) = [Char]
"--" [Char] -> [Char] -> [Char]
forall a. [a] -> [a] -> [a]
++ [Char]
s
        no [Char]
s                     = [Char]
"--no-" [Char] -> [Char] -> [Char]
forall a. [a] -> [a] -> [a]
++ [Char]
s

    OptionWarning OptionWarning
ow -> OptionWarning -> m Doc
forall (m :: * -> *) a. (Applicative m, Pretty a) => a -> m Doc
pretty OptionWarning
ow

    ParseWarning ParseWarning
pw -> ParseWarning -> m Doc
forall (m :: * -> *) a. (Applicative m, Pretty a) => a -> m Doc
pretty ParseWarning
pw

    DeprecationWarning [Char]
old [Char]
new [Char]
version -> [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
$
      [[Char] -> m Doc
forall (m :: * -> *). Applicative m => [Char] -> m Doc
text [Char]
old] [m Doc] -> [m Doc] -> [m Doc]
forall a. [a] -> [a] -> [a]
++ [Char] -> [m Doc]
forall (m :: * -> *). Applicative m => [Char] -> [m Doc]
pwords [Char]
"has been deprecated. Use" [m Doc] -> [m Doc] -> [m Doc]
forall a. [a] -> [a] -> [a]
++ [[Char] -> m Doc
forall (m :: * -> *). Applicative m => [Char] -> m Doc
text [Char]
new] [m Doc] -> [m Doc] -> [m Doc]
forall a. [a] -> [a] -> [a]
++ [Char] -> [m Doc]
forall (m :: * -> *). Applicative m => [Char] -> [m Doc]
pwords
      [Char]
"instead. This will be an error in Agda" [m Doc] -> [m Doc] -> [m Doc]
forall a. [a] -> [a] -> [a]
++ [[Char] -> m Doc
forall (m :: * -> *). Applicative m => [Char] -> m Doc
text [Char]
version m Doc -> m Doc -> m Doc
forall a. Semigroup a => a -> a -> a
<> m Doc
"."]

    NicifierIssue DeclarationWarning
w -> DeclarationWarning -> m Doc
forall (m :: * -> *) a. (Applicative m, Pretty a) => a -> m Doc
pretty DeclarationWarning
w

    UserWarning BackendName
str -> [Char] -> m Doc
forall (m :: * -> *). Applicative m => [Char] -> m Doc
text (BackendName -> [Char]
T.unpack BackendName
str)

    ModuleDoesntExport QName
m [Name]
names [Name]
modules List1 ImportedName
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] -> m Doc) -> [m Doc] -> m Doc
forall a b. (a -> b) -> a -> b
$ [Char] -> [m Doc]
forall (m :: * -> *). Applicative m => [Char] -> [m Doc]
pwords [Char]
"The 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]
++ [Char] -> [m Doc]
forall (m :: * -> *). Applicative m => [Char] -> [m Doc]
pwords [Char]
"doesn't export the following:"
      , Bool -> (ImportedName -> m Doc) -> [ImportedName] -> m Doc
forall (m :: * -> *) a.
(MonadPretty m, Pretty a, HasRange a) =>
Bool -> (a -> m Doc) -> [a] -> m Doc
prettyNotInScopeNames Bool
False ([Name] -> ImportedName -> m Doc
forall {m :: * -> *} {b}.
(Null (m Doc), MonadFresh NameId m, MonadInteractionPoints m,
 MonadStConcreteNames m, PureTCM m, IsString (m Doc),
 Semigroup (m Doc), Pretty b) =>
[Name] -> ImportedName' b b -> m Doc
suggestion [Name]
names)   [ImportedName]
ys
      , Bool -> (ImportedName -> m Doc) -> [ImportedName] -> m Doc
forall (m :: * -> *) a.
(MonadPretty m, Pretty a, HasRange a) =>
Bool -> (a -> m Doc) -> [a] -> m Doc
prettyNotInScopeNames Bool
False ([Name] -> ImportedName -> m Doc
forall {m :: * -> *} {b}.
(Null (m Doc), MonadFresh NameId m, MonadInteractionPoints m,
 MonadStConcreteNames m, PureTCM m, IsString (m Doc),
 Semigroup (m Doc), Pretty b) =>
[Name] -> ImportedName' b b -> m Doc
suggestion [Name]
modules) [ImportedName]
ms
      ]
      where
      ys, ms :: [C.ImportedName]
      ys :: [ImportedName]
ys            = (Name -> ImportedName) -> [Name] -> [ImportedName]
forall a b. (a -> b) -> [a] -> [b]
map Name -> ImportedName
forall n m. n -> ImportedName' n m
ImportedName   [Name]
ys0
      ms :: [ImportedName]
ms            = (Name -> ImportedName) -> [Name] -> [ImportedName]
forall a b. (a -> b) -> [a] -> [b]
map Name -> ImportedName
forall n m. m -> ImportedName' n m
ImportedModule [Name]
ms0
      ([Name]
ys0, [Name]
ms0)    = [ImportedName] -> ([Name], [Name])
forall n m. [ImportedName' n m] -> ([n], [m])
partitionImportedNames ([ImportedName] -> ([Name], [Name]))
-> [ImportedName] -> ([Name], [Name])
forall a b. (a -> b) -> a -> b
$ List1 ImportedName -> [Item (List1 ImportedName)]
forall l. IsList l => l -> [Item l]
List1.toList List1 ImportedName
xs
      suggestion :: [Name] -> ImportedName' b b -> m Doc
suggestion [Name]
zs = m Doc -> (m Doc -> m Doc) -> Maybe (m Doc) -> m Doc
forall b a. b -> (a -> b) -> Maybe a -> b
maybe m Doc
forall a. Null a => a
empty m Doc -> m Doc
forall (m :: * -> *). Functor m => m Doc -> m Doc
parens (Maybe (m Doc) -> m Doc)
-> (ImportedName' b b -> Maybe (m Doc))
-> ImportedName' b b
-> m Doc
forall b c a. (b -> c) -> (a -> b) -> a -> c
. [QName]
-> (ImportedName' b b -> b) -> ImportedName' b b -> Maybe (m Doc)
forall (m :: * -> *) a b.
(MonadPretty m, Pretty a, Pretty b) =>
[QName] -> (a -> b) -> a -> Maybe (m Doc)
didYouMean ((Name -> QName) -> [Name] -> [QName]
forall a b. (a -> b) -> [a] -> [b]
map Name -> QName
C.QName [Name]
zs) ImportedName' b b -> b
forall a. ImportedName' a a -> a
fromImportedName

    DuplicateUsing List1 ImportedName
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
$ [Char] -> [m Doc]
forall (m :: * -> *). Applicative m => [Char] -> [m Doc]
pwords [Char]
"Duplicates in `using` directive:" [m Doc] -> [m Doc] -> [m Doc]
forall a. [a] -> [a] -> [a]
++ (ImportedName -> m Doc) -> [ImportedName] -> [m Doc]
forall a b. (a -> b) -> [a] -> [b]
map ImportedName -> m Doc
forall (m :: * -> *) a. (Applicative m, Pretty a) => a -> m Doc
pretty (List1 ImportedName -> [Item (List1 ImportedName)]
forall l. IsList l => l -> [Item l]
List1.toList List1 ImportedName
xs)

    FixityInRenamingModule List1 Range
_rs -> [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
$ [Char] -> [m Doc]
forall (m :: * -> *). Applicative m => [Char] -> [m Doc]
pwords [Char]
"Modules do not have fixity"

    LibraryWarning LibWarning
lw -> LibWarning -> m Doc
forall (m :: * -> *) a. (Applicative m, Pretty a) => a -> m Doc
pretty LibWarning
lw

    InfectiveImport Doc
msg -> Doc -> m Doc
forall a. a -> m a
forall (m :: * -> *) a. Monad m => a -> m a
return Doc
msg

    CoInfectiveImport Doc
msg -> Doc -> m Doc
forall a. a -> m a
forall (m :: * -> *) a. Monad m => a -> m a
return Doc
msg

    NotARewriteRule QName
x IsAmbiguous
amb -> [m Doc] -> m Doc
forall (m :: * -> *) (t :: * -> *).
(Applicative m, Foldable t) =>
t (m Doc) -> m Doc
hsep ([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
        [ [ QName -> m Doc
forall (m :: * -> *) a. (Applicative m, Pretty a) => a -> m Doc
pretty QName
x ]
        , [Char] -> [m Doc]
forall (m :: * -> *). Applicative m => [Char] -> [m Doc]
pwords [Char]
"is not a legal rewrite rule, since the left-hand side is"
        , case IsAmbiguous
amb of
            YesAmbiguous AmbiguousQName
xs -> [ m Doc
"ambiguous:", AmbiguousQName -> m Doc
forall (m :: * -> *) a. (Applicative m, Pretty a) => a -> m Doc
pretty AmbiguousQName
xs ]
            IsAmbiguous
NotAmbiguous -> [Char] -> [m Doc]
forall (m :: * -> *). Applicative m => [Char] -> [m Doc]
pwords [Char]
"neither a defined symbol nor a constructor"
        ]

    IllegalRewriteRule QName
q IllegalRewriteRuleReason
reason -> case IllegalRewriteRuleReason
reason of
      IllegalRewriteRuleReason
LHSNotDefinitionOrConstructor -> [m Doc] -> m Doc
forall (m :: * -> *) (t :: * -> *).
(Applicative m, Foldable t) =>
t (m Doc) -> m Doc
hsep
        [ 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
" is not a legal rewrite rule, since the left-hand side is neither a defined symbol nor a constructor" ]
      VariablesNotBoundByLHS VarSet
xs -> [m Doc] -> m Doc
forall (m :: * -> *) (t :: * -> *).
(Applicative m, Foldable t) =>
t (m Doc) -> m Doc
hsep
        [ 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
" is not a legal rewrite rule, since the following variables are not bound by the left hand side: "
        , [m Doc] -> m Doc
forall (m :: * -> *) (t :: * -> *).
(Applicative m, Semigroup (m Doc), Foldable t) =>
t (m Doc) -> m Doc
prettyList_ ((VerboseLevel -> m Doc) -> [VerboseLevel] -> [m Doc]
forall a b. (a -> b) -> [a] -> [b]
map (Term -> m Doc
forall a (m :: * -> *). (PrettyTCM a, MonadPretty m) => a -> m Doc
forall (m :: * -> *). MonadPretty m => Term -> m Doc
prettyTCM (Term -> m Doc) -> (VerboseLevel -> Term) -> VerboseLevel -> m Doc
forall b c a. (b -> c) -> (a -> b) -> a -> c
. VerboseLevel -> Term
var) ([VerboseLevel] -> [m Doc]) -> [VerboseLevel] -> [m Doc]
forall a b. (a -> b) -> a -> b
$ VarSet -> [VerboseLevel]
VarSet.toAscList VarSet
xs)
        ]
      VariablesBoundMoreThanOnce VarSet
xs -> do
        (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
" is not a legal rewrite rule, since the following parameters are bound more than once on the left hand side: "
          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
hsep (m Doc -> [m Doc] -> [m Doc]
forall a. a -> [a] -> [a]
List.intersperse m Doc
"," ([m Doc] -> [m Doc]) -> [m Doc] -> [m Doc]
forall a b. (a -> b) -> a -> b
$ (VerboseLevel -> m Doc) -> [VerboseLevel] -> [m Doc]
forall a b. (a -> b) -> [a] -> [b]
map (Term -> m Doc
forall a (m :: * -> *). (PrettyTCM a, MonadPretty m) => a -> m Doc
forall (m :: * -> *). MonadPretty m => Term -> m Doc
prettyTCM (Term -> m Doc) -> (VerboseLevel -> Term) -> VerboseLevel -> m Doc
forall b c a. (b -> c) -> (a -> b) -> a -> c
. VerboseLevel -> Term
var) ([VerboseLevel] -> [m Doc]) -> [VerboseLevel] -> [m Doc]
forall a b. (a -> b) -> a -> b
$ VarSet -> [VerboseLevel]
VarSet.toAscList VarSet
xs))
          m Doc -> m Doc -> m Doc
forall a. Semigroup a => a -> a -> a
<> m Doc
". Perhaps you can use a postulate instead of a constructor as the head symbol?"
      LHSReduces Term
v Term
v' -> [m Doc] -> m Doc
forall (m :: * -> *) (t :: * -> *).
(Applicative m, Foldable t) =>
t (m Doc) -> m Doc
fsep
        [ 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
" is not a legal rewrite rule, since the left-hand side "
        , Term -> m Doc
forall a (m :: * -> *). (PrettyTCM a, MonadPretty m) => a -> m Doc
forall (m :: * -> *). MonadPretty m => Term -> m Doc
prettyTCM Term
v m Doc -> m Doc -> m Doc
forall (m :: * -> *). Applicative m => m Doc -> m Doc -> m Doc
<+> m Doc
" reduces to " 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' ]
      HeadSymbolIsProjectionLikeFunction QName
f -> [m Doc] -> m Doc
forall (m :: * -> *) (t :: * -> *).
(Applicative m, Foldable t) =>
t (m Doc) -> m Doc
hsep
        [ 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
" is not a legal rewrite rule, since the head symbol"
        , m Doc
hd , m Doc
"is a projection-like function."
        , m Doc
"You can turn off the projection-like optimization for", m Doc
hd
        , m Doc
"with the pragma {-# NOT_PROJECTION_LIKE", m Doc
hd, m Doc
"#-}"
        , m Doc
"or globally with the flag --no-projection-like"
        ]
        where hd :: m Doc
hd = QName -> m Doc
forall a (m :: * -> *). (PrettyTCM a, MonadPretty m) => a -> m Doc
forall (m :: * -> *). MonadPretty m => QName -> m Doc
prettyTCM QName
f
      HeadSymbolIsTypeConstructor QName
f -> [m Doc] -> m Doc
forall (m :: * -> *) (t :: * -> *).
(Applicative m, Foldable t) =>
t (m Doc) -> m Doc
hsep
        [ 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
" is not a legal rewrite rule, since the head symbol"
        , 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
"is a type constructor."
        ]
      HeadSymbolContainsMetas QName
f -> [m Doc] -> m Doc
forall (m :: * -> *) (t :: * -> *).
(Applicative m, Foldable t) =>
t (m Doc) -> m Doc
hsep
        [ 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
"is not a legal rewrite rule, since the definition of the head symbol"
        , 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
"contains unsolved metavariables and confluence checking is enabled."
        ]
      ConstructorParametersNotGeneral ConHead
c Args
vs -> [m Doc] -> m Doc
forall (m :: * -> *) (t :: * -> *).
(Applicative m, Foldable t) =>
t (m Doc) -> m Doc
vcat
        [ 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
<+> [Char] -> m Doc
forall (m :: * -> *). Applicative m => [Char] -> m Doc
text [Char]
" is not a legal rewrite rule, since the constructor parameters are not fully general:"
        , VerboseLevel -> m Doc -> m Doc
forall (m :: * -> *). Functor m => VerboseLevel -> m Doc -> m Doc
nest VerboseLevel
2 (m Doc -> m Doc) -> m Doc -> m Doc
forall a b. (a -> b) -> a -> b
$ [Char] -> m Doc
forall (m :: * -> *). Applicative m => [Char] -> m Doc
text [Char]
"Constructor: " m Doc -> m Doc -> m Doc
forall (m :: * -> *). Applicative m => m Doc -> m Doc -> m Doc
<+> ConHead -> m Doc
forall a (m :: * -> *). (PrettyTCM a, MonadPretty m) => a -> m Doc
forall (m :: * -> *). MonadPretty m => ConHead -> m Doc
prettyTCM ConHead
c
        , VerboseLevel -> m Doc -> m Doc
forall (m :: * -> *). Functor m => VerboseLevel -> m Doc -> m Doc
nest VerboseLevel
2 (m Doc -> m Doc) -> m Doc -> m Doc
forall a b. (a -> b) -> a -> b
$ [Char] -> m Doc
forall (m :: * -> *). Applicative m => [Char] -> m Doc
text [Char]
"Parameters: " 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
prettyList ((Arg Term -> m Doc) -> Args -> [m Doc]
forall a b. (a -> b) -> [a] -> [b]
map Arg Term -> m Doc
forall a (m :: * -> *). (PrettyTCM a, MonadPretty m) => a -> m Doc
forall (m :: * -> *). MonadPretty m => Arg Term -> m Doc
prettyTCM Args
vs)
        ]
      ContainsUnsolvedMetaVariables Set1 MetaId
ms -> [m Doc] -> m Doc
forall (m :: * -> *) (t :: * -> *).
(Applicative m, Foldable t) =>
t (m Doc) -> m Doc
hsep
        [ 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
" is not a legal rewrite rule, since"
        , m Doc
"it contains the unsolved meta variable(s)", NonEmpty (m Doc) -> m Doc
forall (m :: * -> *) (t :: * -> *).
(Applicative m, Semigroup (m Doc), Foldable t) =>
t (m Doc) -> m Doc
prettyList_ ((MetaId -> m Doc) -> NonEmpty MetaId -> 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 MetaId -> m Doc
forall a (m :: * -> *). (PrettyTCM a, MonadPretty m) => a -> m Doc
forall (m :: * -> *). MonadPretty m => MetaId -> m Doc
prettyTCM (NonEmpty MetaId -> NonEmpty (m Doc))
-> NonEmpty MetaId -> NonEmpty (m Doc)
forall a b. (a -> b) -> a -> b
$ Set1 MetaId -> NonEmpty MetaId
forall a. NESet a -> NonEmpty a
Set1.toList Set1 MetaId
ms)
        ]
      BlockedOnProblems Set1 ProblemId
ps -> [m Doc] -> m Doc
forall (m :: * -> *) (t :: * -> *).
(Applicative m, Foldable t) =>
t (m Doc) -> m Doc
hsep
        [ 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
" is not a legal rewrite rule, since"
        , m Doc
"it is blocked on problem(s)", NonEmpty (m Doc) -> m Doc
forall (m :: * -> *) (t :: * -> *).
(Applicative m, Semigroup (m Doc), Foldable t) =>
t (m Doc) -> m Doc
prettyList_ ((ProblemId -> m Doc) -> NonEmpty ProblemId -> 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 ProblemId -> m Doc
forall a (m :: * -> *). (PrettyTCM a, MonadPretty m) => a -> m Doc
forall (m :: * -> *). MonadPretty m => ProblemId -> m Doc
prettyTCM (NonEmpty ProblemId -> NonEmpty (m Doc))
-> NonEmpty ProblemId -> NonEmpty (m Doc)
forall a b. (a -> b) -> a -> b
$ Set1 ProblemId -> NonEmpty ProblemId
forall a. NESet a -> NonEmpty a
Set1.toList Set1 ProblemId
ps)
        ]
      RequiresDefinitions Set1 QName
qs -> [m Doc] -> m Doc
forall (m :: * -> *) (t :: * -> *).
(Applicative m, Foldable t) =>
t (m Doc) -> m Doc
hsep
        [ 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
" is not a legal rewrite rule, since"
        , m Doc
"it requires the definition(s) of", NonEmpty (m Doc) -> m Doc
forall (m :: * -> *) (t :: * -> *).
(Applicative m, Semigroup (m Doc), Foldable t) =>
t (m Doc) -> m Doc
prettyList_ ((QName -> m Doc) -> NonEmpty QName -> 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 QName -> m Doc
forall a (m :: * -> *). (PrettyTCM a, MonadPretty m) => a -> m Doc
forall (m :: * -> *). MonadPretty m => QName -> m Doc
prettyTCM (NonEmpty QName -> NonEmpty (m Doc))
-> NonEmpty QName -> NonEmpty (m Doc)
forall a b. (a -> b) -> a -> b
$ Set1 QName -> NonEmpty QName
forall a. NESet a -> NonEmpty a
Set1.toList Set1 QName
qs)
        ]
      IllegalRewriteRuleReason
DoesNotTargetRewriteRelation -> [m Doc] -> m Doc
forall (m :: * -> *) (t :: * -> *).
(Applicative m, Foldable t) =>
t (m Doc) -> m Doc
hsep
        [ 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
" does not target rewrite relation" ]
      IllegalRewriteRuleReason
BeforeFunctionDefinition -> [m Doc] -> m Doc
forall (m :: * -> *) (t :: * -> *).
(Applicative m, Foldable t) =>
t (m Doc) -> m Doc
hsep
        [ m Doc
"Rewrite rule from function "
        , 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
" cannot be added before the function definition"
        ]
      BeforeMutualFunctionDefinition QName
r -> [m Doc] -> m Doc
forall (m :: * -> *) (t :: * -> *).
(Applicative m, Foldable t) =>
t (m Doc) -> m Doc
hsep
        [ m Doc
"Rewrite rule from function "
        , 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
" cannot be added before the definition of mutually defined"
        , QName -> m Doc
forall a (m :: * -> *). (PrettyTCM a, MonadPretty m) => a -> m Doc
forall (m :: * -> *). MonadPretty m => QName -> m Doc
prettyTCM QName
r
        ]
      IllegalRewriteRuleReason
DuplicateRewriteRule ->
        m Doc
"Rewrite rule " 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
q m Doc -> m Doc -> m Doc
forall (m :: * -> *). Applicative m => m Doc -> m Doc -> m Doc
<+> m Doc
" has already been added"

    ConfluenceCheckingIncompleteBecauseOfMeta QName
f -> [m Doc] -> m Doc
forall (m :: * -> *) (t :: * -> *).
(Applicative m, Foldable t) =>
t (m Doc) -> m Doc
fsep
      [ m Doc
"Confluence checking incomplete because the definition of"
      , QName -> m Doc
forall a (m :: * -> *). (PrettyTCM a, MonadPretty m) => a -> m Doc
forall (m :: * -> *). MonadPretty m => QName -> m Doc
prettyTCM QName
f
      , [Char] -> m Doc
forall (m :: * -> *). Applicative m => [Char] -> m Doc
text [Char]
"contains unsolved metavariables."
      ]

    Warning
ConfluenceForCubicalNotSupported -> [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
$ [Char] -> [m Doc]
forall (m :: * -> *). Applicative m => [Char] -> [m Doc]
pwords ([Char] -> [m Doc]) -> [Char] -> [m Doc]
forall a b. (a -> b) -> a -> b
$
      [Char]
"Confluence checking for --cubical is not yet supported, confluence checking might be incomplete"

    RewriteNonConfluent Term
lhs Term
rhs1 Term
rhs2 Doc
err -> [m Doc] -> m Doc
forall (m :: * -> *) (t :: * -> *).
(Applicative m, Foldable t) =>
t (m Doc) -> m Doc
fsep
      [ m Doc
"Local confluence check failed:"
      , Term -> m Doc
forall a (m :: * -> *). (PrettyTCM a, MonadPretty m) => a -> m Doc
forall (m :: * -> *). MonadPretty m => Term -> m Doc
prettyTCM Term
lhs , m Doc
"reduces to both"
      , Term -> m Doc
forall a (m :: * -> *). (PrettyTCM a, MonadPretty m) => a -> m Doc
forall (m :: * -> *). MonadPretty m => Term -> m Doc
prettyTCM Term
rhs1 , m Doc
"and" , Term -> m Doc
forall a (m :: * -> *). (PrettyTCM a, MonadPretty m) => a -> m Doc
forall (m :: * -> *). MonadPretty m => Term -> m Doc
prettyTCM Term
rhs2
      , m Doc
"which are not equal because"
      , Doc -> m Doc
forall a. a -> m a
forall (m :: * -> *) a. Monad m => a -> m a
return Doc
err
      ]

    RewriteMaybeNonConfluent Term
lhs1 Term
lhs2 [Doc]
cs -> [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 (t :: * -> *) a. Foldable t => t [a] -> [a]
concat
      [ [ [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
          [ [Char] -> [m Doc]
forall (m :: * -> *). Applicative m => [Char] -> [m Doc]
pwords [Char]
"Couldn't determine overlap between left-hand sides"
          , [ Term -> m Doc
forall a (m :: * -> *). (PrettyTCM a, MonadPretty m) => a -> m Doc
forall (m :: * -> *). MonadPretty m => Term -> m Doc
prettyTCM Term
lhs1 , [Char] -> m Doc
forall (m :: * -> *). Applicative m => [Char] -> m Doc
text [Char]
"and" , Term -> m Doc
forall a (m :: * -> *). (PrettyTCM a, MonadPretty m) => a -> m Doc
forall (m :: * -> *). MonadPretty m => Term -> m Doc
prettyTCM Term
lhs2 ]
          , [Char] -> [m Doc]
forall (m :: * -> *). Applicative m => [Char] -> [m Doc]
pwords [Char]
"because of unsolved constraints:"
          ]
        ]
      , (Doc -> m Doc) -> [Doc] -> [m Doc]
forall a b. (a -> b) -> [a] -> [b]
map (VerboseLevel -> m Doc -> m Doc
forall (m :: * -> *). Functor m => VerboseLevel -> m Doc -> m Doc
nest VerboseLevel
2 (m Doc -> m Doc) -> (Doc -> m Doc) -> Doc -> m Doc
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Doc -> m Doc
forall a. a -> m a
forall (m :: * -> *) a. Monad m => a -> m a
return) [Doc]
cs
      ]

    RewriteAmbiguousRules Term
lhs Term
rhs1 Term
rhs2 -> [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
          [ [Char] -> [m Doc]
forall (m :: * -> *). Applicative m => [Char] -> [m Doc]
pwords [Char]
"Global confluence check failed:" , [Term -> m Doc
forall a (m :: * -> *). (PrettyTCM a, MonadPretty m) => a -> m Doc
forall (m :: * -> *). MonadPretty m => Term -> m Doc
prettyTCM Term
lhs]
          , [Char] -> [m Doc]
forall (m :: * -> *). Applicative m => [Char] -> [m Doc]
pwords [Char]
"can be rewritten to either" , [Term -> m Doc
forall a (m :: * -> *). (PrettyTCM a, MonadPretty m) => a -> m Doc
forall (m :: * -> *). MonadPretty m => Term -> m Doc
prettyTCM Term
rhs1]
          , [Char] -> [m Doc]
forall (m :: * -> *). Applicative m => [Char] -> [m Doc]
pwords [Char]
"or" , [Term -> m Doc
forall a (m :: * -> *). (PrettyTCM a, MonadPretty m) => a -> m Doc
forall (m :: * -> *). MonadPretty m => Term -> m Doc
prettyTCM Term
rhs2 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
        [ [Char] -> [m Doc]
forall (m :: * -> *). Applicative m => [Char] -> [m Doc]
pwords [Char]
"Possible fix: add a rewrite rule with left-hand side"
        , [Term -> m Doc
forall a (m :: * -> *). (PrettyTCM a, MonadPretty m) => a -> m Doc
forall (m :: * -> *). MonadPretty m => Term -> m Doc
prettyTCM Term
lhs] , [Char] -> [m Doc]
forall (m :: * -> *). Applicative m => [Char] -> [m Doc]
pwords [Char]
"to resolve the ambiguity."
        ]
      ]

    RewriteMissingRule Term
u Term
v Term
rhou -> [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
        [ [Char] -> [m Doc]
forall (m :: * -> *). Applicative m => [Char] -> [m Doc]
pwords [Char]
"Global confluence check failed:" , [Term -> m Doc
forall a (m :: * -> *). (PrettyTCM a, MonadPretty m) => a -> m Doc
forall (m :: * -> *). MonadPretty m => Term -> m Doc
prettyTCM Term
u]
        , [Char] -> [m Doc]
forall (m :: * -> *). Applicative m => [Char] -> [m Doc]
pwords [Char]
"unfolds to" , [Term -> m Doc
forall a (m :: * -> *). (PrettyTCM a, MonadPretty m) => a -> m Doc
forall (m :: * -> *). MonadPretty m => Term -> m Doc
prettyTCM Term
v] , [Char] -> [m Doc]
forall (m :: * -> *). Applicative m => [Char] -> [m Doc]
pwords [Char]
"which should further unfold to"
        , [Term -> m Doc
forall a (m :: * -> *). (PrettyTCM a, MonadPretty m) => a -> m Doc
forall (m :: * -> *). MonadPretty m => Term -> m Doc
prettyTCM Term
rhou] , [Char] -> [m Doc]
forall (m :: * -> *). Applicative m => [Char] -> [m Doc]
pwords [Char]
"but it does not."
        ]
      , [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
        [ [Char] -> [m Doc]
forall (m :: * -> *). Applicative m => [Char] -> [m Doc]
pwords [Char]
"Possible fix: add a rule to rewrite"
        , [ 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
"to" , Term -> m Doc
forall a (m :: * -> *). (PrettyTCM a, MonadPretty m) => a -> m Doc
forall (m :: * -> *). MonadPretty m => Term -> m Doc
prettyTCM Term
rhou ]
        ]
      ]

    DuplicateRecordDirective RecordDirective
dir ->
      m Doc
"Ignoring duplicate record directive: " m Doc -> m Doc -> m Doc
forall (m :: * -> *). Applicative m => m Doc -> m Doc -> m Doc
<+> RecordDirective -> m Doc
forall (m :: * -> *) a. (Applicative m, Pretty a) => a -> m Doc
pretty RecordDirective
dir

    PragmaCompileErased BackendName
bn QName
qn -> [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
      [ [Char] -> [m Doc]
forall (m :: * -> *). Applicative m => [Char] -> [m Doc]
pwords [Char]
"The backend"
      , [ BackendName -> m Doc
forall a (m :: * -> *). (PrettyTCM a, MonadPretty m) => a -> m Doc
forall (m :: * -> *). MonadPretty m => BackendName -> m Doc
prettyTCM BackendName
bn
        , m Doc
"erases"
        , QName -> m Doc
forall a (m :: * -> *). (PrettyTCM a, MonadPretty m) => a -> m Doc
forall (m :: * -> *). MonadPretty m => QName -> m Doc
prettyTCM QName
qn
        ]
      , [Char] -> [m Doc]
forall (m :: * -> *). Applicative m => [Char] -> [m Doc]
pwords [Char]
"so the COMPILE pragma will be ignored."
      ]

    Warning
PragmaCompileList -> [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
$ [Char] -> [m Doc]
forall (m :: * -> *). Applicative m => [Char] -> [m Doc]
pwords
      [Char]
"Ignoring GHC pragma for builtin lists; they always compile to Haskell lists."

    Warning
PragmaCompileMaybe -> [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
$ [Char] -> [m Doc]
forall (m :: * -> *). Applicative m => [Char] -> [m Doc]
pwords
      [Char]
"Ignoring GHC pragma for builtin MAYBE; it always compiles to Haskell Maybe."

    PragmaCompileUnparsable [Char]
s -> [Char] -> m Doc
forall (m :: * -> *). Applicative m => [Char] -> m Doc
fwords ([Char] -> m Doc) -> [Char] -> m Doc
forall a b. (a -> b) -> a -> b
$ [Char]
"Ignoring unparsable GHC pragma '" [Char] -> [Char] -> [Char]
forall a. [a] -> [a] -> [a]
++ [Char]
s [Char] -> [Char] -> [Char]
forall a. [a] -> [a] -> [a]
++ [Char]
"'"

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

    PragmaCompileWrongName QName
x IsAmbiguous
amb -> [m Doc] -> m Doc
forall (m :: * -> *) (t :: * -> *).
(Applicative m, Foldable t) =>
t (m Doc) -> m Doc
hsep ([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
      [ [Char] -> [m Doc]
forall (m :: * -> *). Applicative m => [Char] -> [m Doc]
pwords [Char]
"Cannot COMPILE"
      , [ QName -> m Doc
forall (m :: * -> *) a. (Applicative m, Pretty a) => a -> m Doc
pretty QName
x ]
      , [Char] -> [m Doc]
forall (m :: * -> *). Applicative m => [Char] -> [m Doc]
pwords [Char]
"since it is"
      , case IsAmbiguous
amb of
          YesAmbiguous AmbiguousQName
xs -> [ m Doc
"ambiguous:", AmbiguousQName -> m Doc
forall (m :: * -> *) a. (Applicative m, Pretty a) => a -> m Doc
pretty AmbiguousQName
xs ]
          IsAmbiguous
NotAmbiguous -> [Char] -> [m Doc]
forall (m :: * -> *). Applicative m => [Char] -> [m Doc]
pwords [Char]
"neither a defined symbol nor a constructor"
      ]

    PragmaExpectsDefinedSymbol [Char]
pragma QName
_x -> [m Doc] -> m Doc
forall (m :: * -> *) (t :: * -> *).
(Applicative m, Foldable t) =>
t (m Doc) -> m Doc
hsep ([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
      [ [Char] -> [m Doc]
forall (m :: * -> *). Applicative m => [Char] -> [m Doc]
pwords [Char]
"Target of"
      , [ [Char] -> m Doc
forall (m :: * -> *). Applicative m => [Char] -> m Doc
text [Char]
pragma ]
      , [Char] -> [m Doc]
forall (m :: * -> *). Applicative m => [Char] -> [m Doc]
pwords [Char]
"pragma should be a defined symbol"
      ]

    PragmaExpectsUnambiguousConstructorOrFunction [Char]
pragma QName
_x IsAmbiguous
amb -> [m Doc] -> m Doc
forall (m :: * -> *) (t :: * -> *).
(Applicative m, Foldable t) =>
t (m Doc) -> m Doc
hsep ([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
      [ [Char] -> [m Doc]
forall (m :: * -> *). Applicative m => [Char] -> [m Doc]
pwords [Char]
"Target of"
      , [ [Char] -> m Doc
forall (m :: * -> *). Applicative m => [Char] -> m Doc
text [Char]
pragma ]
      , [Char] -> [m Doc]
forall (m :: * -> *). Applicative m => [Char] -> [m Doc]
pwords [Char]
"pragma should be"
      , case IsAmbiguous
amb of
          YesAmbiguous AmbiguousQName
xs -> [Char] -> [m Doc]
forall (m :: * -> *). Applicative m => [Char] -> [m Doc]
pwords [Char]
"unambiguous, but it resolves to:" [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 ]
          IsAmbiguous
NotAmbiguous -> [Char] -> [m Doc]
forall (m :: * -> *). Applicative m => [Char] -> [m Doc]
pwords [Char]
"a function, constructor, or projection"
      ]

    PragmaExpectsUnambiguousProjectionOrFunction [Char]
pragma QName
_x IsAmbiguous
amb -> [m Doc] -> m Doc
forall (m :: * -> *) (t :: * -> *).
(Applicative m, Foldable t) =>
t (m Doc) -> m Doc
hsep ([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
      [ [Char] -> [m Doc]
forall (m :: * -> *). Applicative m => [Char] -> [m Doc]
pwords [Char]
"Target of"
      , [ [Char] -> m Doc
forall (m :: * -> *). Applicative m => [Char] -> m Doc
text [Char]
pragma ]
      , [Char] -> [m Doc]
forall (m :: * -> *). Applicative m => [Char] -> [m Doc]
pwords [Char]
"pragma should be"
      , case IsAmbiguous
amb of
          YesAmbiguous AmbiguousQName
xs -> [Char] -> [m Doc]
forall (m :: * -> *). Applicative m => [Char] -> [m Doc]
pwords [Char]
"unambiguous, but it resolves to:" [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 ]
          IsAmbiguous
NotAmbiguous -> [Char] -> [m Doc]
forall (m :: * -> *). Applicative m => [Char] -> [m Doc]
pwords [Char]
"a function or projection"
      ]

    NoMain TopLevelModuleName
topLevelModule -> [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
$ [Char] -> [m Doc]
forall (m :: * -> *). Applicative m => [Char] -> [m Doc]
pwords [Char]
"No main function defined in" [m Doc] -> [m Doc] -> [m Doc]
forall a. [a] -> [a] -> [a]
++ [TopLevelModuleName -> m Doc
forall a (m :: * -> *). (PrettyTCM a, MonadPretty m) => a -> m Doc
forall (m :: * -> *). MonadPretty m => TopLevelModuleName -> m Doc
prettyTCM TopLevelModuleName
topLevelModule 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
$ [Char] -> [m Doc]
forall (m :: * -> *). Applicative m => [Char] -> [m Doc]
pwords [Char]
"Use option --no-main to suppress this warning."
      ]

    NotInScopeW 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 ([m Doc] -> m Doc) -> [m Doc] -> m Doc
forall a b. (a -> b) -> a -> b
$ [Char] -> [m Doc]
forall (m :: * -> *). Applicative m => [Char] -> [m Doc]
pwords [Char]
"Not in scope:"
      , do
        inscope <- Set QName -> [QName]
forall a. Set a -> [a]
Set.toList (Set QName -> [QName])
-> (ScopeInfo -> Set QName) -> ScopeInfo -> [QName]
forall b c a. (b -> c) -> (a -> b) -> a -> c
. ScopeInfo -> Set QName
concreteNamesInScope (ScopeInfo -> [QName]) -> m ScopeInfo -> m [QName]
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> m ScopeInfo
forall (m :: * -> *). ReadTCState m => m ScopeInfo
getScope
        prettyNotInScopeNames True (suggestion inscope) $ singleton x
      ]
      where
      suggestion :: [QName] -> QName -> m Doc
suggestion [QName]
inscope QName
x = VerboseLevel -> m Doc -> m Doc
forall (m :: * -> *). Functor m => VerboseLevel -> m Doc -> m Doc
nest VerboseLevel
2 (m Doc -> m Doc) -> m Doc -> m Doc
forall a b. (a -> b) -> a -> b
$ [m Doc] -> m Doc
forall {m :: * -> *}.
(Null (m Doc), Applicative m) =>
[m Doc] -> m Doc
par ([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
"did you forget space around the ':'?"  | Char
':' Char -> [Char] -> Bool
forall a. Eq a => a -> [a] -> Bool
forall (t :: * -> *) a. (Foldable t, Eq a) => a -> t a -> Bool
`elem` [Char]
s ]
        , [ m Doc
"did you forget space around the '->'?" | [Char]
"->" [Char] -> [Char] -> Bool
forall a. Eq a => [a] -> [a] -> Bool
`List.isInfixOf` [Char]
s ]
        , Maybe (m Doc) -> [m Doc]
forall a. Maybe a -> [a]
maybeToList (Maybe (m Doc) -> [m Doc]) -> Maybe (m Doc) -> [m Doc]
forall a b. (a -> b) -> a -> b
$ [QName] -> (QName -> Name) -> QName -> Maybe (m Doc)
forall (m :: * -> *) a b.
(MonadPretty m, Pretty a, Pretty b) =>
[QName] -> (a -> b) -> a -> Maybe (m Doc)
didYouMean [QName]
inscope QName -> Name
C.unqualify QName
x
        ]
        where
        par :: [m Doc] -> m Doc
par []  = m Doc
forall a. Null a => a
empty
        par [m Doc
d] = m Doc -> m Doc
forall (m :: * -> *). Functor m => m Doc -> m Doc
parens m Doc
d
        par [m Doc]
ds  = 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
vcat [m Doc]
ds
        s :: [Char]
s = QName -> [Char]
forall a. Pretty a => a -> [Char]
P.prettyShow QName
x

    AsPatternShadowsConstructorOrPatternSynonym ConstructorOrPatternSynonym
patsyn -> [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
      [ [Char] -> [m Doc]
forall (m :: * -> *). Applicative m => [Char] -> [m Doc]
pwords [Char]
"Name bound in @-pattern ignored because it shadows a"
      , [ 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
patsyn ]
      ]

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

    PlentyInHardCompileTimeMode QωOrigin
o -> [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
$
      [Char] -> [m Doc]
forall (m :: * -> *). Applicative m => [Char] -> [m Doc]
pwords [Char]
"Ignored use of" [m Doc] -> [m Doc] -> [m Doc]
forall a. [a] -> [a] -> [a]
++ [QωOrigin -> m Doc
forall (m :: * -> *) a. (Applicative m, Pretty a) => a -> m Doc
pretty QωOrigin
o] [m Doc] -> [m Doc] -> [m Doc]
forall a. [a] -> [a] -> [a]
++
      [Char] -> [m Doc]
forall (m :: * -> *). Applicative m => [Char] -> [m Doc]
pwords [Char]
"in hard compile-time mode"

    RecordFieldWarning RecordFieldWarning
w -> RecordFieldWarning -> m Doc
forall (m :: * -> *). MonadPretty m => RecordFieldWarning -> m Doc
prettyRecordFieldWarning RecordFieldWarning
w

    MissingTypeSignatureForOpaque QName
name IsOpaque
isOpaque -> [m Doc] -> m Doc
forall (m :: * -> *) (t :: * -> *).
(Applicative m, Foldable t) =>
t (m Doc) -> m Doc
vcat
        [ m Doc
"Missing type signature for" m Doc -> m Doc -> m Doc
forall (m :: * -> *). Applicative m => m Doc -> m Doc -> m Doc
<+> [Char] -> m Doc
forall (m :: * -> *). Applicative m => [Char] -> m Doc
text [Char]
what m Doc -> m Doc -> m Doc
forall (m :: * -> *). Applicative m => m Doc -> m Doc -> m Doc
<+> m Doc
"definition" 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 -> 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
$ [Char] -> [m Doc]
forall (m :: * -> *). Applicative m => [Char] -> [m Doc]
pwords ([Char] -> [m Doc]) -> [Char] -> [m Doc]
forall a b. (a -> b) -> a -> b
$
            [Char]
"Types of " [Char] -> [Char] -> [Char]
forall a. [a] -> [a] -> [a]
++ [Char]
what [Char] -> [Char] -> [Char]
forall a. [a] -> [a] -> [a]
++ [Char]
" definitions are never inferred since this would leak " [Char] -> [Char] -> [Char]
forall a. [a] -> [a] -> [a]
++
            [Char]
"information that should be " [Char] -> [Char] -> [Char]
forall a. [a] -> [a] -> [a]
++ [Char]
what [Char] -> [Char] -> [Char]
forall a. [a] -> [a] -> [a]
++ [Char]
"."
        ]
      where
        what :: [Char]
what = case IsOpaque
isOpaque of
          IsOpaque
TransparentDef -> [Char]
"abstract"
          OpaqueDef OpaqueId
_    -> [Char]
"opaque"


    Warning
NotAffectedByOpaque -> [Char] -> m Doc
forall (m :: * -> *). Applicative m => [Char] -> m Doc
fwords [Char]
"Only function definitions can be marked opaque. This definition will be treated as transparent."

    UnfoldingWrongName 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
$
      [Char] -> [m Doc]
forall (m :: * -> *). Applicative m => [Char] -> [m Doc]
pwords [Char]
"Name in unfolding clause should be unambiguous defined name:" [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]

    UnfoldTransparentName QName
qn -> [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
$
      [Char] -> [m Doc]
forall (m :: * -> *). Applicative m => [Char] -> [m Doc]
pwords [Char]
"The name" [m Doc] -> [m Doc] -> [m Doc]
forall a. [a] -> [a] -> [a]
++ [QName -> m Doc
forall a (m :: * -> *). (PrettyTCM a, MonadPretty m) => a -> m Doc
forall (m :: * -> *). MonadPretty m => QName -> m Doc
prettyTCM QName
qn m Doc -> m Doc -> m Doc
forall a. Semigroup a => a -> a -> a
<> m Doc
","] [m Doc] -> [m Doc] -> [m Doc]
forall a. [a] -> [a] -> [a]
++ [Char] -> [m Doc]
forall (m :: * -> *). Applicative m => [Char] -> [m Doc]
pwords [Char]
"mentioned by an unfolding clause, does not belong to an opaque block. This has no effect."

    Warning
AbstractInLetBindings -> [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
$ [Char] -> [m Doc]
forall (m :: * -> *). Applicative m => [Char] -> [m Doc]
pwords [Char]
"Abstract definitions are not allowed in let bindings."
    Warning
MacroInLetBindings    -> [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
$ [Char] -> [m Doc]
forall (m :: * -> *). Applicative m => [Char] -> [m Doc]
pwords [Char]
"Macros can not be defined in let bindings."

    Warning
UselessOpaque -> m Doc
"This `opaque` block has no effect."

    HiddenNotInArgumentPosition 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]
++ [Char] -> [m Doc]
forall (m :: * -> *). Applicative m => [Char] -> [m Doc]
pwords [Char]
"cannot appear by itself. It needs to be the argument to" [m Doc] -> [m Doc] -> [m Doc]
forall a. [a] -> [a] -> [a]
++
      [Char] -> [m Doc]
forall (m :: * -> *). Applicative m => [Char] -> [m Doc]
pwords [Char]
"a function expecting an implicit argument."

    InstanceNotInArgumentPosition 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]
++ [Char] -> [m Doc]
forall (m :: * -> *). Applicative m => [Char] -> [m Doc]
pwords [Char]
"cannot appear by itself. It needs to be the argument to" [m Doc] -> [m Doc] -> [m Doc]
forall a. [a] -> [a] -> [a]
++
      [Char] -> [m Doc]
forall (m :: * -> *). Applicative m => [Char] -> [m Doc]
pwords [Char]
"a function expecting an instance argument."

    InvalidDisplayForm QName
x [Char]
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
$ [[m Doc]] -> [m Doc]
forall (t :: * -> *) a. Foldable t => t [a] -> [a]
concat
        [ [Char] -> [m Doc]
forall (m :: * -> *). Applicative m => [Char] -> [m Doc]
pwords [Char]
"Ignoring invalid display form for"
        , [ QName -> m Doc
forall a (m :: * -> *). (PrettyTCM a, MonadPretty m) => a -> m Doc
forall (m :: * -> *). MonadPretty m => QName -> m Doc
prettyTCM QName
x ]
        , if [Char] -> Bool
forall a. Null a => a -> Bool
null [Char]
reason then [] else m Doc
"because" m Doc -> [m Doc] -> [m Doc]
forall a. a -> [a] -> [a]
: [Char] -> [m Doc]
forall (m :: * -> *). Applicative m => [Char] -> [m Doc]
pwords [Char]
reason
        ]

    UnusedVariablesInDisplayForm List1 Name
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] -> 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
        [ [Char] -> [m Doc]
forall (m :: * -> *). Applicative m => [Char] -> [m Doc]
pwords [Char]
"The following"
        , [Char] -> [m Doc]
forall (m :: * -> *). Applicative m => [Char] -> [m Doc]
pwords ([Char] -> [m Doc]) -> [Char] -> [m Doc]
forall a b. (a -> b) -> a -> b
$ List1 Name -> [Char] -> [Char] -> [Char]
forall a c. Sized a => a -> c -> c -> c
singPlural List1 Name
xs [Char]
"variable is" [Char]
"variables are"
        , [Char] -> [m Doc]
forall (m :: * -> *). Applicative m => [Char] -> [m Doc]
pwords [Char]
"bound on the left hand side but unused on the right hand side of the display form:"
        ]
      , VerboseLevel -> m Doc -> m Doc
forall (m :: * -> *). Functor m => VerboseLevel -> m Doc -> m Doc
nest VerboseLevel
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
fsep (NonEmpty (m Doc) -> m Doc) -> NonEmpty (m Doc) -> m Doc
forall a b. (a -> b) -> a -> b
$ (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
      , [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
"Replace" ]
        , [Char] -> [m Doc]
forall (m :: * -> *). Applicative m => [Char] -> [m Doc]
pwords ([Char] -> [m Doc]) -> [Char] -> [m Doc]
forall a b. (a -> b) -> a -> b
$ List1 Name -> [Char] -> [Char] -> [Char]
forall a c. Sized a => a -> c -> c -> c
singPlural List1 Name
xs [Char]
"it by an underscore" [Char]
"them by underscores"
        , [Char] -> [m Doc]
forall (m :: * -> *). Applicative m => [Char] -> [m Doc]
pwords [Char]
"to pacify this warning"
        ]
      ]

    TooManyArgumentsToSort QName
q List1 (NamedArg Expr)
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
$ [[m Doc]] -> [m Doc]
forall (t :: * -> *) a. Foldable t => t [a] -> [a]
concat
      [ [Char] -> [m Doc]
forall (m :: * -> *). Applicative m => [Char] -> [m Doc]
pwords [Char]
"Too many arguments given to sort"
      , [ QName -> m Doc
forall a (m :: * -> *). (PrettyTCM a, MonadPretty m) => a -> m Doc
forall (m :: * -> *). MonadPretty m => QName -> m Doc
prettyTCM QName
q ]
      ]

    Warning
RewritesNothing -> [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
$ [Char] -> [m Doc]
forall (m :: * -> *). Applicative m => [Char] -> [m Doc]
pwords [Char]
"`rewrite' did not apply"

    WithClauseProjectionFixityMismatch NamedArg Pattern
p0 ProjOrigin
o' NamedArg DeBruijnPattern
q ProjOrigin
o -> [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
        [ [Char] -> [m Doc]
forall (m :: * -> *). Applicative m => [Char] -> [m Doc]
pwords [Char]
"With clause pattern"
        , [ NamedArg Pattern -> m Doc
forall a (m :: * -> *).
(ToConcrete a, Pretty (ConOfAbs a), MonadAbsToCon m) =>
a -> m Doc
prettyA NamedArg Pattern
p0 ]
        , [Char] -> [m Doc]
forall (m :: * -> *). Applicative m => [Char] -> [m Doc]
pwords [Char]
"is not an instance of its parent pattern"
        , [ [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] ]
        , [Char] -> [m Doc]
forall (m :: * -> *). Applicative m => [Char] -> [m Doc]
pwords [Char]
"since the parent pattern is"
        , [Char] -> [m Doc]
forall (m :: * -> *). Applicative m => [Char] -> [m Doc]
pwords ([Char] -> [m Doc]) -> [Char] -> [m Doc]
forall a b. (a -> b) -> a -> b
$ ProjOrigin -> [Char]
forall {a}. IsString a => ProjOrigin -> a
prettyProjOrigin ProjOrigin
o
        , [Char] -> [m Doc]
forall (m :: * -> *). Applicative m => [Char] -> [m Doc]
pwords [Char]
"and the with clause pattern is"
        , [Char] -> [m Doc]
forall (m :: * -> *). Applicative m => [Char] -> [m Doc]
pwords ([Char] -> [m Doc]) -> [Char] -> [m Doc]
forall a b. (a -> b) -> a -> b
$ ProjOrigin -> [Char]
forall {a}. IsString a => ProjOrigin -> a
prettyProjOrigin ProjOrigin
o'
        ]
      where
        prettyProjOrigin :: ProjOrigin -> a
prettyProjOrigin ProjOrigin
ProjPrefix  = a
"a prefix projection"
        prettyProjOrigin ProjOrigin
ProjPostfix = a
"a postfix projection"
        prettyProjOrigin ProjOrigin
ProjSystem  = a
forall a. HasCallStack => a
__IMPOSSIBLE__

    FaceConstraintCannotBeHidden ArgInfo
ai -> [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
$
      [Char] -> [m Doc]
forall (m :: * -> *). Applicative m => [Char] -> [m Doc]
pwords [Char]
"Face constraint patterns cannot be" [m Doc] -> [m Doc] -> [m Doc]
forall a. [a] -> [a] -> [a]
++ [ Hiding -> m Doc
forall (m :: * -> *) a. (Applicative m, Pretty a) => a -> m Doc
pretty (ArgInfo -> Hiding
forall a. LensHiding a => a -> Hiding
getHiding ArgInfo
ai), m Doc
"arguments"]

    FaceConstraintCannotBeNamed NamedName
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
$
      [Char] -> [m Doc]
forall (m :: * -> *). Applicative m => [Char] -> [m Doc]
pwords [Char]
"Ignoring name" [m Doc] -> [m Doc] -> [m Doc]
forall a. [a] -> [a] -> [a]
++ [m Doc
"`" m Doc -> m Doc -> m Doc
forall a. Semigroup a => a -> a -> a
<> NamedName -> m Doc
forall (m :: * -> *) a. (Applicative m, Pretty a) => a -> m Doc
pretty NamedName
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]
++ [Char] -> [m Doc]
forall (m :: * -> *). Applicative m => [Char] -> [m Doc]
pwords [Char]
"given to face constraint pattern"

    CustomBackendWarning [Char]
backend Doc
warn -> ([Char] -> m Doc
forall (m :: * -> *). Applicative m => [Char] -> m Doc
text [Char]
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
warn

    TopLevelPolarity QName
x PolarityModality
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
$
      [m Doc
"Definition", 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
"has explicit polarity annotation", PolarityModality -> m Doc
forall (m :: * -> *) a. (Applicative m, Pretty a) => a -> m Doc
pretty PolarityModality
p, m Doc
"which is currently not supported"]

    TooManyPolarities QName
x PragmaPolarities
occs -> [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
$
      [VerboseLevel -> m Doc
forall a (m :: * -> *). (PrettyTCM a, MonadPretty m) => a -> m Doc
forall (m :: * -> *). MonadPretty m => VerboseLevel -> m Doc
prettyTCM (VerboseLevel -> m Doc) -> VerboseLevel -> m Doc
forall a b. (a -> b) -> a -> b
$ PragmaPolarities -> VerboseLevel
forall a. NonEmpty a -> VerboseLevel
forall (t :: * -> *) a. Foldable t => t a -> VerboseLevel
length PragmaPolarities
occs] [m Doc] -> [m Doc] -> [m Doc]
forall a. [a] -> [a] -> [a]
++
      [Char] -> [m Doc]
forall (m :: * -> *). Applicative m => [Char] -> [m Doc]
pwords [Char]
"too many polarities given in the POLARITY pragma for" [m Doc] -> [m Doc] -> [m Doc]
forall a. [a] -> [a] -> [a]
++
      [QName -> m Doc
forall a (m :: * -> *). (PrettyTCM a, MonadPretty m) => a -> m Doc
forall (m :: * -> *). MonadPretty m => QName -> m Doc
prettyTCM QName
x]

instance PrettyTCM DataOrRecord_ where
  prettyTCM :: forall (m :: * -> *). MonadPretty m => DataOrRecord_ -> m Doc
prettyTCM = \case
    IsData{}   -> m Doc
"data"
    IsRecord{} -> m Doc
"record"


{-# SPECIALIZE prettyRecordFieldWarning :: RecordFieldWarning -> TCM Doc #-}
prettyRecordFieldWarning :: MonadPretty m => RecordFieldWarning -> m Doc
prettyRecordFieldWarning :: forall (m :: * -> *). MonadPretty m => RecordFieldWarning -> m Doc
prettyRecordFieldWarning = \case
  W.DuplicateFields List1 (Name, List1 Range)
xrs    -> List1 Name -> m Doc
forall (m :: * -> *). MonadPretty m => List1 Name -> m Doc
prettyDuplicateFields    (List1 Name -> m Doc) -> List1 Name -> m Doc
forall a b. (a -> b) -> a -> b
$ ((Name, List1 Range) -> Name)
-> List1 (Name, List1 Range) -> List1 Name
forall a b. (a -> b) -> NonEmpty a -> NonEmpty b
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap (Name, List1 Range) -> Name
forall a b. (a, b) -> a
fst List1 (Name, List1 Range)
xrs
  W.TooManyFields QName
q [Name]
ys List1 (Name, Range)
xrs -> QName -> [Name] -> List1 Name -> m Doc
forall (m :: * -> *).
MonadPretty m =>
QName -> [Name] -> List1 Name -> m Doc
prettyTooManyFields QName
q [Name]
ys (List1 Name -> m Doc) -> List1 Name -> m Doc
forall a b. (a -> b) -> a -> b
$ ((Name, Range) -> Name) -> List1 (Name, Range) -> List1 Name
forall a b. (a -> b) -> NonEmpty a -> NonEmpty b
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap (Name, Range) -> Name
forall a b. (a, b) -> a
fst List1 (Name, Range)
xrs

prettyDuplicateFields :: MonadPretty m => List1 C.Name -> m Doc
prettyDuplicateFields :: forall (m :: * -> *). MonadPretty m => List1 Name -> m Doc
prettyDuplicateFields 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
$ [[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
"field" ]
    , 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
forall (m :: * -> *). Applicative m => m Doc
comma ((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)
    , [Char] -> [m Doc]
forall (m :: * -> *). Applicative m => [Char] -> [m Doc]
pwords [Char]
"in record"
    ]

{-# SPECIALIZE prettyTooManyFields :: QName -> [C.Name] -> List1 C.Name -> TCM Doc  #-}
prettyTooManyFields :: MonadPretty m => QName -> [C.Name] -> List1 C.Name -> m Doc
prettyTooManyFields :: forall (m :: * -> *).
MonadPretty m =>
QName -> [Name] -> List1 Name -> m Doc
prettyTooManyFields QName
r [Name]
missing 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
$ [[m Doc]] -> [m Doc]
forall (t :: * -> *) a. Foldable t => t [a] -> [a]
concat
    [ [Char] -> [m Doc]
forall (m :: * -> *). Applicative m => [Char] -> [m Doc]
pwords [Char]
"The record type"
    , [QName -> m Doc
forall a (m :: * -> *). (PrettyTCM a, MonadPretty m) => a -> m Doc
forall (m :: * -> *). MonadPretty m => QName -> m Doc
prettyTCM QName
r]
    , [Char] -> [m Doc]
forall (m :: * -> *). Applicative m => [Char] -> [m Doc]
pwords [Char]
"does not have the"
    , List1 Name -> [m Doc]
forall {m :: * -> *} {a}.
(Functor m, Sized a, IsString (m Doc)) =>
a -> [m Doc]
fields List1 Name
xs
    , 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
forall (m :: * -> *). Applicative m => m Doc
comma ((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)
    , if [Name] -> Bool
forall a. Null a => a -> Bool
null [Name]
missing then [] else [[m Doc]] -> [m Doc]
forall (t :: * -> *) a. Foldable t => t [a] -> [a]
concat
      [ [Char] -> [m Doc]
forall (m :: * -> *). Applicative m => [Char] -> [m Doc]
pwords [Char]
"but it would have the"
      , [Name] -> [m Doc]
forall {m :: * -> *} {a}.
(Functor m, Sized a, IsString (m Doc)) =>
a -> [m Doc]
fields [Name]
missing
      , m Doc -> [m Doc] -> [m Doc]
forall (m :: * -> *) (t :: * -> *).
(Applicative m, Semigroup (m Doc), Foldable t) =>
m Doc -> t (m Doc) -> [m Doc]
punctuate m Doc
forall (m :: * -> *). Applicative m => m Doc
comma ((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]
missing)
      ]
    ]
  where
    fields :: a -> [m Doc]
fields a
ys = [ a -> m Doc -> m Doc
forall (m :: * -> *) a. (Functor m, Sized a) => a -> m Doc -> m Doc
pluralS a
ys m Doc
"field" ]

{-# SPECIALIZE prettyNotInScopeNames :: (Pretty a, HasRange a) => Bool -> (a -> TCM Doc) -> [a] -> TCM Doc #-}
-- | Report a number of names that are not in scope.
prettyNotInScopeNames
  :: (MonadPretty m, Pretty a, HasRange a)
  => Bool          -- ^ Print range?
  -> (a -> m Doc)  -- ^ Correction suggestion generator.
  -> [a]           -- ^ Names that are not in scope.
  -> m Doc
prettyNotInScopeNames :: forall (m :: * -> *) a.
(MonadPretty m, Pretty a, HasRange a) =>
Bool -> (a -> m Doc) -> [a] -> m Doc
prettyNotInScopeNames Bool
printRange a -> m Doc
suggestion [a]
xs = VerboseLevel -> m Doc -> m Doc
forall (m :: * -> *). Functor m => VerboseLevel -> m Doc -> m Doc
nest VerboseLevel
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
$ (a -> m Doc) -> [a] -> [m Doc]
forall a b. (a -> b) -> [a] -> [b]
map a -> m Doc
name [a]
xs
  where
  name :: a -> m Doc
name a
x = [m Doc] -> m Doc
forall (m :: * -> *) (t :: * -> *).
(Applicative m, Foldable t) =>
t (m Doc) -> m Doc
fsep
    [ a -> m Doc
forall (m :: * -> *) a. (Applicative m, Pretty a) => a -> m Doc
pretty a
x
    , if Bool
printRange then 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 (a -> Range
forall a. HasRange a => a -> Range
getRange a
x) else m Doc
forall a. Null a => a
empty
    , a -> m Doc
suggestion a
x
    ]

{-# SPECIALIZE didYouMean :: (Pretty a, Pretty b) => [C.QName] -> (a -> b) -> a -> Maybe (TCM Doc) #-}
-- | Suggest some corrections to a misspelled name.
didYouMean
  :: (MonadPretty m, Pretty a, Pretty b)
  => [C.QName]     -- ^ Names in scope.
  -> (a -> b)      -- ^ Canonization function for similarity search.
  -> a             -- ^ A name which is not in scope.
  -> Maybe (m Doc) -- ^ "did you mean" hint.
didYouMean :: forall (m :: * -> *) a b.
(MonadPretty m, Pretty a, Pretty b) =>
[QName] -> (a -> b) -> a -> Maybe (m Doc)
didYouMean [QName]
inscope a -> b
canon a
x
  | [[Char]] -> Bool
forall a. Null a => a -> Bool
null [[Char]]
ys   = Maybe (m Doc)
forall a. Maybe a
Nothing
  | Bool
otherwise = m Doc -> Maybe (m Doc)
forall a. a -> Maybe a
Just (m Doc -> Maybe (m Doc)) -> m Doc -> Maybe (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
sep
      [ m Doc
"did you mean"
      , VerboseLevel -> m Doc -> m Doc
forall (m :: * -> *). Functor m => VerboseLevel -> m Doc -> m Doc
nest VerboseLevel
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
$ m Doc -> [m Doc] -> [m Doc]
forall (m :: * -> *) (t :: * -> *).
(Applicative m, Semigroup (m Doc), Foldable t) =>
m Doc -> t (m Doc) -> [m Doc]
punctuate m Doc
" or" ([m Doc] -> [m Doc]) -> [m Doc] -> [m Doc]
forall a b. (a -> b) -> a -> b
$
                 ([Char] -> m Doc) -> [[Char]] -> [m Doc]
forall a b. (a -> b) -> [a] -> [b]
map (\ [Char]
y -> [Char] -> m Doc
forall (m :: * -> *). Applicative m => [Char] -> m Doc
text ([Char] -> m Doc) -> [Char] -> m Doc
forall a b. (a -> b) -> a -> b
$ [Char]
"'" [Char] -> [Char] -> [Char]
forall a. [a] -> [a] -> [a]
++ [Char]
y [Char] -> [Char] -> [Char]
forall a. [a] -> [a] -> [a]
++ [Char]
"'") [[Char]]
ys)
        m Doc -> m Doc -> m Doc
forall a. Semigroup a => a -> a -> a
<> m Doc
"?"
      ]
  where
  strip :: Pretty b => b -> String
  strip :: forall a. Pretty a => a -> [Char]
strip        = (Char -> Char) -> [Char] -> [Char]
forall a b. (a -> b) -> [a] -> [b]
map Char -> Char
toLower ([Char] -> [Char]) -> (b -> [Char]) -> b -> [Char]
forall b c a. (b -> c) -> (a -> b) -> a -> c
. (Char -> Bool) -> [Char] -> [Char]
forall a. (a -> Bool) -> [a] -> [a]
filter (Char -> Char -> Bool
forall a. Eq a => a -> a -> Bool
/= Char
'_') ([Char] -> [Char]) -> (b -> [Char]) -> b -> [Char]
forall b c a. (b -> c) -> (a -> b) -> a -> c
. b -> [Char]
forall a. Pretty a => a -> [Char]
prettyShow
  -- dropModule x = fromMaybe x $ List.stripPrefix "module " x
  maxDist :: a -> a
maxDist a
n    = a -> a -> a
forall a. Integral a => a -> a -> a
div a
n a
3
  close :: [a] -> [a] -> Bool
close [a]
a [a]
b    = [a] -> [a] -> VerboseLevel
forall a. Eq a => [a] -> [a] -> VerboseLevel
editDistance [a]
a [a]
b VerboseLevel -> VerboseLevel -> Bool
forall a. Ord a => a -> a -> Bool
<= VerboseLevel -> VerboseLevel
forall {a}. Integral a => a -> a
maxDist ([a] -> VerboseLevel
forall a. [a] -> VerboseLevel
forall (t :: * -> *) a. Foldable t => t a -> VerboseLevel
length [a]
a)
  ys :: [[Char]]
ys           = (QName -> [Char]) -> [QName] -> [[Char]]
forall a b. (a -> b) -> [a] -> [b]
map QName -> [Char]
forall a. Pretty a => a -> [Char]
prettyShow ([QName] -> [[Char]]) -> [QName] -> [[Char]]
forall a b. (a -> b) -> a -> b
$ (QName -> Bool) -> [QName] -> [QName]
forall a. (a -> Bool) -> [a] -> [a]
filter ([Char] -> [Char] -> Bool
forall a. Eq a => [a] -> [a] -> Bool
close (b -> [Char]
forall a. Pretty a => a -> [Char]
strip (b -> [Char]) -> b -> [Char]
forall a b. (a -> b) -> a -> b
$ a -> b
canon a
x) ([Char] -> Bool) -> (QName -> [Char]) -> QName -> Bool
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Name -> [Char]
forall a. Pretty a => a -> [Char]
strip (Name -> [Char]) -> (QName -> Name) -> QName -> [Char]
forall b c a. (b -> c) -> (a -> b) -> a -> c
. QName -> Name
C.unqualify) [QName]
inscope


prettyTCWarnings :: Set TCWarning -> TCM String
prettyTCWarnings :: Set TCWarning -> TCM [Char]
prettyTCWarnings = [Char] -> [[Char]] -> [Char]
forall a. [a] -> [[a]] -> [a]
List.intercalate [Char]
"\n" ([[Char]] -> [Char])
-> (Set TCWarning -> TCMT IO [[Char]])
-> Set TCWarning
-> TCM [Char]
forall (m :: * -> *) b c a.
Functor m =>
(b -> c) -> (a -> m b) -> a -> m c
<.> (Doc -> [Char]) -> [Doc] -> [[Char]]
forall a b. (a -> b) -> [a] -> [b]
map Doc -> [Char]
forall a. Doc a -> [Char]
P.render ([Doc] -> [[Char]])
-> (Set TCWarning -> TCMT IO [Doc])
-> Set TCWarning
-> TCMT IO [[Char]]
forall (m :: * -> *) b c a.
Functor m =>
(b -> c) -> (a -> m b) -> a -> m c
<.> Set TCWarning -> TCMT IO [Doc]
prettyTCWarnings'

prettyTCWarnings' :: Set TCWarning -> TCM [Doc]
prettyTCWarnings' :: Set TCWarning -> TCMT IO [Doc]
prettyTCWarnings' = (TCWarning -> TCMT IO Doc) -> [TCWarning] -> TCMT IO [Doc]
forall (t :: * -> *) (f :: * -> *) a b.
(Traversable t, Applicative f) =>
(a -> f b) -> t a -> f (t b)
forall (f :: * -> *) a b.
Applicative f =>
(a -> f b) -> [a] -> f [b]
traverse TCWarning -> TCMT IO Doc
forall a (m :: * -> *). (PrettyTCM a, MonadPretty m) => a -> m Doc
forall (m :: * -> *). MonadPretty m => TCWarning -> m Doc
prettyTCM ([TCWarning] -> TCMT IO [Doc])
-> (Set TCWarning -> TCMT IO [TCWarning])
-> Set TCWarning
-> TCMT IO [Doc]
forall (m :: * -> *) b c a.
Monad m =>
(b -> m c) -> (a -> m b) -> a -> m c
<=< Set TCWarning -> TCMT IO [TCWarning]
filterTCWarnings

-- | If there are several warnings, remove the unsolved-constraints warning
-- in case there are no interesting constraints to list.
filterTCWarnings :: Set TCWarning -> TCM [TCWarning]
filterTCWarnings :: Set TCWarning -> TCMT IO [TCWarning]
filterTCWarnings Set TCWarning
wset = case Set TCWarning -> [TCWarning]
forall a. Set a -> [a]
Set.toAscList Set TCWarning
wset of
  -- #4065: Always keep the only warning
  [TCWarning
w] -> [TCWarning] -> TCMT IO [TCWarning]
forall a. a -> TCMT IO a
forall (m :: * -> *) a. Monad m => a -> m a
return [TCWarning
w]
  -- Andreas, 2019-09-10, issue #4065:
  -- If there are several warnings, remove the unsolved-constraints warning
  -- in case there are no interesting constraints to list.
  [TCWarning]
ws  -> ((TCWarning -> TCMT IO Bool) -> [TCWarning] -> TCMT IO [TCWarning]
forall (m :: * -> *) a.
Applicative m =>
(a -> m Bool) -> [a] -> m [a]
`filterM` [TCWarning]
ws) ((TCWarning -> TCMT IO Bool) -> TCMT IO [TCWarning])
-> (TCWarning -> TCMT IO Bool) -> TCMT IO [TCWarning]
forall a b. (a -> b) -> a -> b
$ \ TCWarning
w -> case TCWarning -> Warning
tcWarning TCWarning
w of
    UnsolvedConstraints List1 ProblemConstraint
cs -> (ProblemConstraint -> TCMT IO Bool)
-> List1 ProblemConstraint -> TCMT IO Bool
forall (f :: * -> *) (m :: * -> *) a.
(Foldable f, Monad m) =>
(a -> m Bool) -> f a -> m Bool
anyM ProblemConstraint -> TCMT IO Bool
forall (m :: * -> *). MonadPretty m => ProblemConstraint -> m Bool
interestingConstraint List1 ProblemConstraint
cs
    Warning
_ -> Bool -> TCMT IO Bool
forall a. a -> TCMT IO a
forall (f :: * -> *) a. Applicative f => a -> f a
pure Bool
True


-- | Turns warnings, if any, into errors.
tcWarningsToError :: [TCWarning] -> TCM ()
tcWarningsToError :: [TCWarning] -> TCM ()
tcWarningsToError [TCWarning]
mws = case ([TCWarning]
unsolvedHoles, [TCWarning]
otherWarnings) of
   ([], [])                   -> () -> TCM ()
forall a. a -> TCMT IO a
forall (m :: * -> *) a. Monad m => a -> m a
return ()
   (_unsolvedHoles :: [TCWarning]
_unsolvedHoles@(TCWarning
_:[TCWarning]
_), []) -> TypeError -> TCM ()
forall (m :: * -> *) a.
(HasCallStack, MonadTCError m) =>
TypeError -> m a
typeError TypeError
SolvedButOpenHoles
   ([TCWarning]
_ , TCWarning
w : [TCWarning]
ws)               -> TypeError -> TCM ()
forall (m :: * -> *) a.
(HasCallStack, MonadTCError m) =>
TypeError -> m a
typeError (TypeError -> TCM ()) -> TypeError -> TCM ()
forall a b. (a -> b) -> a -> b
$ Set1 TCWarning -> TypeError
NonFatalErrors (Set1 TCWarning -> TypeError) -> Set1 TCWarning -> TypeError
forall a b. (a -> b) -> a -> b
$ NonEmpty TCWarning -> Set1 TCWarning
forall a. Ord a => NonEmpty a -> NESet a
Set1.fromList (TCWarning
w TCWarning -> [TCWarning] -> NonEmpty TCWarning
forall a. a -> [a] -> NonEmpty a
:| [TCWarning]
ws)
   where
   -- filter out unsolved interaction points for imported module so
   -- that we get the right error message (see test case Fail/Issue1296)
   ([TCWarning]
unsolvedHoles, [TCWarning]
otherWarnings) = (TCWarning -> Bool) -> [TCWarning] -> ([TCWarning], [TCWarning])
forall a. (a -> Bool) -> [a] -> ([a], [a])
List.partition (Warning -> Bool
isUnsolvedIM (Warning -> Bool) -> (TCWarning -> Warning) -> TCWarning -> Bool
forall b c a. (b -> c) -> (a -> b) -> a -> c
. TCWarning -> Warning
tcWarning) [TCWarning]
mws
   isUnsolvedIM :: Warning -> Bool
isUnsolvedIM UnsolvedInteractionMetas{} = Bool
True
   isUnsolvedIM Warning
_                          = Bool
False


-- | Depending which flags are set, one may happily ignore some
-- warnings.

applyFlagsToTCWarningsPreserving :: HasOptions m => Set WarningName -> Set TCWarning -> m (Set TCWarning)
applyFlagsToTCWarningsPreserving :: forall (m :: * -> *).
HasOptions m =>
Set WarningName -> Set TCWarning -> m (Set TCWarning)
applyFlagsToTCWarningsPreserving Set WarningName
additionalKeptWarnings Set TCWarning
ws = do
  -- For some reason some SafeFlagPragma seem to be created multiple times.
  -- This is a way to collect all of them and remove duplicates.
  let pragmas :: TCWarning -> ([TCWarning], Set [Char])
pragmas TCWarning
w = case TCWarning -> Warning
tcWarning TCWarning
w of { SafeFlagPragma Set [Char]
ps -> ([TCWarning
w], Set [Char]
ps); Warning
_ -> ([], Set [Char]
forall a. Null a => a
empty) }
  let sfp :: Set TCWarning
sfp = case (TCWarning -> ([TCWarning], Set [Char]))
-> Set TCWarning -> ([TCWarning], Set [Char])
forall m a. Monoid m => (a -> m) -> Set a -> m
forall (t :: * -> *) m a.
(Foldable t, Monoid m) =>
(a -> m) -> t a -> m
foldMap TCWarning -> ([TCWarning], Set [Char])
pragmas Set TCWarning
ws of
              (TCWarning CallStack
loc Range
r Warning
w Doc
doc [Char]
str Bool
b : [TCWarning]
_, Set [Char]
sfp) ->
                 TCWarning -> Set TCWarning
forall el coll. Singleton el coll => el -> coll
singleton (TCWarning -> Set TCWarning) -> TCWarning -> Set TCWarning
forall a b. (a -> b) -> a -> b
$ CallStack -> Range -> Warning -> Doc -> [Char] -> Bool -> TCWarning
TCWarning CallStack
loc Range
r (Set [Char] -> Warning
SafeFlagPragma Set [Char]
sfp) Doc
doc [Char]
str Bool
b
              ([TCWarning], Set [Char])
_ -> Set TCWarning
forall a. Null a => a
empty

  pragmaWarnings <- (WarningMode
-> Lens' WarningMode (Set WarningName) -> Set WarningName
forall o i. o -> Lens' o i -> i
^. (Set WarningName -> f (Set WarningName))
-> WarningMode -> f WarningMode
Lens' WarningMode (Set WarningName)
warningSet) (WarningMode -> Set WarningName)
-> (PragmaOptions -> WarningMode)
-> PragmaOptions
-> Set WarningName
forall b c a. (b -> c) -> (a -> b) -> a -> c
. PragmaOptions -> WarningMode
optWarningMode (PragmaOptions -> Set WarningName)
-> m PragmaOptions -> m (Set WarningName)
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> m PragmaOptions
forall (m :: * -> *). HasOptions m => m PragmaOptions
pragmaOptions
  let warnSet = Set WarningName -> Set WarningName -> Set WarningName
forall a. Ord a => Set a -> Set a -> Set a
Set.union Set WarningName
pragmaWarnings Set WarningName
additionalKeptWarnings

  -- filter out the warnings the flags told us to ignore
  let cleanUp Warning
w = let wName :: WarningName
wName = Warning -> WarningName
warningName Warning
w in
        WarningName
wName WarningName -> WarningName -> Bool
forall a. Eq a => a -> a -> Bool
/= WarningName
SafeFlagPragma_
        Bool -> Bool -> Bool
&& WarningName
wName WarningName -> Set WarningName -> Bool
forall a. Ord a => a -> Set a -> Bool
`Set.member` Set WarningName
warnSet

  return $ Set.union sfp $ Set.filter (cleanUp . tcWarning) ws

applyFlagsToTCWarnings :: HasOptions m => Set TCWarning -> m (Set TCWarning)
applyFlagsToTCWarnings :: forall (m :: * -> *).
HasOptions m =>
Set TCWarning -> m (Set TCWarning)
applyFlagsToTCWarnings = Set WarningName -> Set TCWarning -> m (Set TCWarning)
forall (m :: * -> *).
HasOptions m =>
Set WarningName -> Set TCWarning -> m (Set TCWarning)
applyFlagsToTCWarningsPreserving Set WarningName
forall a. Set a
Set.empty

{-# SPECIALIZE isBoundaryConstraint :: ProblemConstraint -> TCM (Maybe Range) #-}
isBoundaryConstraint :: (ReadTCState m, MonadTCM m) => ProblemConstraint -> m (Maybe Range)
isBoundaryConstraint :: forall (m :: * -> *).
(ReadTCState m, MonadTCM m) =>
ProblemConstraint -> m (Maybe Range)
isBoundaryConstraint ProblemConstraint
c =
  Closure Constraint
-> (Constraint -> m (Maybe Range)) -> m (Maybe Range)
forall (m :: * -> *) c a b.
(MonadTCEnv m, ReadTCState m, LensClosure c a) =>
c -> (a -> m b) -> m b
enterClosure (ProblemConstraint -> Closure Constraint
theConstraint ProblemConstraint
c) ((Constraint -> m (Maybe Range)) -> m (Maybe Range))
-> (Constraint -> m (Maybe Range)) -> m (Maybe Range)
forall a b. (a -> b) -> a -> b
$ \case
    ValueCmp Comparison
_ CompareAs
_ (MetaV MetaId
mid Elims
xs) Term
y | Just Args
xs <- Elims -> Maybe Args
forall a. [Elim' a] -> Maybe [Arg a]
allApplyElims Elims
xs ->
      ((MetaVariable, IntMap Bool, SubstCand, Substitution) -> Range)
-> Maybe (MetaVariable, IntMap Bool, SubstCand, Substitution)
-> Maybe Range
forall a b. (a -> b) -> Maybe a -> Maybe b
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap (MetaVariable, IntMap Bool, SubstCand, Substitution) -> Range
forall {a} {b} {c} {d}. HasRange a => (a, b, c, d) -> Range
g (Maybe (MetaVariable, IntMap Bool, SubstCand, Substitution)
 -> Maybe Range)
-> m (Maybe (MetaVariable, IntMap Bool, SubstCand, Substitution))
-> m (Maybe Range)
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> TCM (Maybe (MetaVariable, IntMap Bool, SubstCand, Substitution))
-> m (Maybe (MetaVariable, IntMap Bool, SubstCand, Substitution))
forall a. TCM a -> m a
forall (tcm :: * -> *) a. MonadTCM tcm => TCM a -> tcm a
liftTCM (MetaId
-> Args
-> TCM (Maybe (MetaVariable, IntMap Bool, SubstCand, Substitution))
isFaceConstraint MetaId
mid Args
xs)
    ValueCmp Comparison
_ CompareAs
_ Term
y (MetaV MetaId
mid Elims
xs) | Just Args
xs <- Elims -> Maybe Args
forall a. [Elim' a] -> Maybe [Arg a]
allApplyElims Elims
xs ->
      ((MetaVariable, IntMap Bool, SubstCand, Substitution) -> Range)
-> Maybe (MetaVariable, IntMap Bool, SubstCand, Substitution)
-> Maybe Range
forall a b. (a -> b) -> Maybe a -> Maybe b
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap (MetaVariable, IntMap Bool, SubstCand, Substitution) -> Range
forall {a} {b} {c} {d}. HasRange a => (a, b, c, d) -> Range
g (Maybe (MetaVariable, IntMap Bool, SubstCand, Substitution)
 -> Maybe Range)
-> m (Maybe (MetaVariable, IntMap Bool, SubstCand, Substitution))
-> m (Maybe Range)
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> TCM (Maybe (MetaVariable, IntMap Bool, SubstCand, Substitution))
-> m (Maybe (MetaVariable, IntMap Bool, SubstCand, Substitution))
forall a. TCM a -> m a
forall (tcm :: * -> *) a. MonadTCM tcm => TCM a -> tcm a
liftTCM (MetaId
-> Args
-> TCM (Maybe (MetaVariable, IntMap Bool, SubstCand, Substitution))
isFaceConstraint MetaId
mid Args
xs)
    Constraint
_ -> Maybe Range -> m (Maybe Range)
forall a. a -> m a
forall (f :: * -> *) a. Applicative f => a -> f a
pure Maybe Range
forall a. Maybe a
Nothing
  where
    g :: (a, b, c, d) -> Range
g (a
a, b
_, c
_, d
_) = a -> Range
forall a. HasRange a => a -> Range
getRange a
a

{-# SPECIALIZE getAllUnsolvedWarnings :: TCM [TCWarning] #-}
getAllUnsolvedWarnings :: (ReadTCState m, MonadWarning m, MonadTCM m) => m [TCWarning]
getAllUnsolvedWarnings :: forall (m :: * -> *).
(ReadTCState m, MonadWarning m, MonadTCM m) =>
m [TCWarning]
getAllUnsolvedWarnings = do
  unsolvedInteractions <- m [Range]
forall (m :: * -> *).
(HasCallStack, MonadDebug m, ReadTCState m) =>
m [Range]
getUnsolvedInteractionMetas

  allCons <- getAllConstraints
  unsolvedConstraints  <- filterM (fmap isNothing . isBoundaryConstraint) allCons
  interactionBoundary  <- catMaybes <$> traverse isBoundaryConstraint allCons

  unsolvedMetas        <- getUnsolvedMetas

  mapM warning_ $ catMaybes
    [ UnsolvedInteractionMetas  . Set1.fromList <$> List1.nonEmpty unsolvedInteractions
    , UnsolvedMetaVariables     . Set1.fromList <$> List1.nonEmpty unsolvedMetas
    , UnsolvedConstraints                       <$> List1.nonEmpty unsolvedConstraints
    , InteractionMetaBoundaries . Set1.fromList <$> List1.nonEmpty interactionBoundary
    ]

-- | Collect all warnings that have accumulated in the state.

{-# SPECIALIZE getAllWarnings :: WhichWarnings -> TCM (Set TCWarning) #-}
getAllWarnings :: (ReadTCState m, MonadWarning m, MonadTCM m) => WhichWarnings -> m (Set TCWarning)
getAllWarnings :: forall (m :: * -> *).
(ReadTCState m, MonadWarning m, MonadTCM m) =>
WhichWarnings -> m (Set TCWarning)
getAllWarnings = Set WarningName -> WhichWarnings -> m (Set TCWarning)
forall (m :: * -> *).
(ReadTCState m, MonadWarning m, MonadTCM m) =>
Set WarningName -> WhichWarnings -> m (Set TCWarning)
getAllWarningsPreserving Set WarningName
forall a. Set a
Set.empty

{-# SPECIALIZE getAllWarningsPreserving :: Set WarningName -> WhichWarnings -> TCM (Set TCWarning) #-}
getAllWarningsPreserving ::
  (ReadTCState m, MonadWarning m, MonadTCM m) => Set WarningName -> WhichWarnings -> m (Set TCWarning)
getAllWarningsPreserving :: forall (m :: * -> *).
(ReadTCState m, MonadWarning m, MonadTCM m) =>
Set WarningName -> WhichWarnings -> m (Set TCWarning)
getAllWarningsPreserving Set WarningName
keptWarnings WhichWarnings
ww = do
  unsolved            <- [TCWarning] -> Set TCWarning
forall a. Ord a => [a] -> Set a
Set.fromList ([TCWarning] -> Set TCWarning)
-> m [TCWarning] -> m (Set TCWarning)
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> m [TCWarning]
forall (m :: * -> *).
(ReadTCState m, MonadWarning m, MonadTCM m) =>
m [TCWarning]
getAllUnsolvedWarnings
  collectedTCWarnings <- useTC stTCWarnings

  -- E.g. the InversionDepthReached warning is only shown when we have unsolved constraints.
  let showWarn
        | Set TCWarning -> Bool
forall a. Null a => a -> Bool
null Set TCWarning
unsolved = \ Warning
w -> Warning -> WhichWarnings
classifyWarning Warning
w WhichWarnings -> WhichWarnings -> Bool
forall a. Ord a => a -> a -> Bool
<= WhichWarnings
ww Bool -> Bool -> Bool
&& Bool -> Bool
not (Warning -> Bool
onlyShowIfUnsolved Warning
w)
        | Bool
otherwise     = \ Warning
w -> Warning -> WhichWarnings
classifyWarning Warning
w WhichWarnings -> WhichWarnings -> Bool
forall a. Ord a => a -> a -> Bool
<= WhichWarnings
ww

  Set.filter (showWarn . tcWarning) <$> do
    applyFlagsToTCWarningsPreserving keptWarnings $
      unsolved `Set.union` collectedTCWarnings

getAllWarningsOfTCErr :: TCErr -> TCM (Set TCWarning)
getAllWarningsOfTCErr :: TCErr -> TCM (Set TCWarning)
getAllWarningsOfTCErr = \case
  TypeError CallStack
_ TCState
tcst Closure TypeError
cls -> case Closure TypeError -> TypeError
forall a. Closure a -> a
clValue Closure TypeError
cls of
    NonFatalErrors{} -> Set TCWarning -> TCM (Set TCWarning)
forall a. a -> TCMT IO a
forall (m :: * -> *) a. Monad m => a -> m a
return Set TCWarning
forall a. Null a => a
empty
    TypeError
_ -> TCM (Set TCWarning) -> TCM (Set TCWarning)
forall a. TCM a -> TCM a
localTCState (TCM (Set TCWarning) -> TCM (Set TCWarning))
-> TCM (Set TCWarning) -> TCM (Set TCWarning)
forall a b. (a -> b) -> a -> b
$ do
      TCState -> TCM ()
forall (m :: * -> *). MonadTCState m => TCState -> m ()
putTC TCState
tcst
      -- We filter out the unsolved(Metas/Constraints) to stay
      -- true to the previous error messages.
      (TCWarning -> Bool) -> Set TCWarning -> Set TCWarning
forall a. (a -> Bool) -> Set a -> Set a
Set.filter (Bool -> Bool
not (Bool -> Bool) -> (TCWarning -> Bool) -> TCWarning -> Bool
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Warning -> Bool
isUnsolvedWarning (Warning -> Bool) -> (TCWarning -> Warning) -> TCWarning -> Bool
forall b c a. (b -> c) -> (a -> b) -> a -> c
. TCWarning -> Warning
tcWarning) (Set TCWarning -> Set TCWarning)
-> TCM (Set TCWarning) -> TCM (Set TCWarning)
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> WhichWarnings -> TCM (Set TCWarning)
forall (m :: * -> *).
(ReadTCState m, MonadWarning m, MonadTCM m) =>
WhichWarnings -> m (Set TCWarning)
getAllWarnings WhichWarnings
AllWarnings
  TCErr
_ -> Set TCWarning -> TCM (Set TCWarning)
forall a. a -> TCMT IO a
forall (m :: * -> *) a. Monad m => a -> m a
return Set TCWarning
forall a. Null a => a
empty