    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 Data.IntSet (IntSet)
    import qualified Data.IntSet as IntSet
    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 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 IntSet
    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
    $ IntSet -> [VerboseLevel]
    IntSet.toList IntSet
    xs)
            ]
          VariablesBoundMoreThanOnce IntSet
    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
    $ IntSet -> [VerboseLevel]
    IntSet.toList IntSet
    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, 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, 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
      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