    module Agda.Syntax.Concrete.Definitions.Errors where

    import Control.DeepSeq

    import GHC.Generics (Generic)

    import Agda.Syntax.Position
    import Agda.Syntax.Common
    import Agda.Syntax.Common.Pretty
    import Agda.Syntax.Concrete
    import Agda.Syntax.Concrete.Definitions.Types

    import Agda.Interaction.Options.Warnings

    import Agda.Utils.Null ( empty )
    import Agda.Utils.CallStack ( CallStack )
    import Agda.Utils.List1 (List1, pattern (:|))
    import Agda.Utils.List2 (List2, pattern List2)
    import qualified Agda.Utils.List1 as List1
    import Agda.Utils.Set1 (Set1)
    import qualified Agda.Utils.Set1 as Set1
    import Agda.Utils.Singleton

    ------------------------------------------------------------------------
    -- Errors

    -- | Exception with internal source code callstack
    data DeclarationException = DeclarationException
      { DeclarationException -> CallStack
    deLocation  :: CallStack
      , DeclarationException -> DeclarationException'
    deException :: DeclarationException'
      }

    -- | The exception type.
    data DeclarationException'
      = MultipleEllipses Pattern
      | DuplicateDefinition Name
      | DuplicateAnonDeclaration Range
      | MissingWithClauses Name LHS
      | WrongDefinition Name DataRecOrFun DataRecOrFun
      | WrongContentBlock KindOfBlock Range
      | AmbiguousFunClauses LHS (List1 Name)
          -- ^ In a mutual block, a clause could belong to any of the ≥2 type signatures ('Name').
      | AmbiguousConstructor Range Name [Name]
          -- ^ In an interleaved mutual block, a constructor could belong to any of the data signatures ('Name')
      | InvalidMeasureMutual Range
          -- ^ In a mutual block, all or none need a MEASURE pragma.
          --   'Range' is the one of the offending pragma or the mutual block.
      | UnquoteDefRequiresSignature (List1 Name)
      | BadMacroDef NiceDeclaration
      | UnfoldingOutsideOpaque KwRange
        -- ^ An unfolding declaration was not the first declaration
        -- contained in an opaque block.
      | OpaqueInMutual KwRange
          -- ^ @opaque@ block nested in a @mutual@ block.
          -- This can never happen, even with reordering.
          -- The 'KwRange' is the one of the @opaque@ keyword.
      | DisallowedInterleavedMutual KwRange String (List1 Name)
          -- ^ A declaration that breaks an implicit mutual block (named by
          -- the String argument) was present while the given lone type
          -- signatures were still without their definitions.
        deriving (Int -> DeclarationException' -> ShowS
    [DeclarationException'] -> ShowS
    DeclarationException' -> String
    (Int -> DeclarationException' -> ShowS)
    -> (DeclarationException' -> String)
    -> ([DeclarationException'] -> ShowS)
    -> Show DeclarationException'
    forall a.
    (Int -> a -> ShowS) -> (a -> String) -> ([a] -> ShowS) -> Show a
    $cshowsPrec :: Int -> DeclarationException' -> ShowS
    showsPrec :: Int -> DeclarationException' -> ShowS
    $cshow :: DeclarationException' -> String
    show :: DeclarationException' -> String
    $cshowList :: [DeclarationException'] -> ShowS
    showList :: [DeclarationException'] -> ShowS
    Show, (forall x. DeclarationException' -> Rep DeclarationException' x)
    -> (forall x. Rep DeclarationException' x -> DeclarationException')
    -> Generic DeclarationException'
    forall x. Rep DeclarationException' x -> DeclarationException'
    forall x. DeclarationException' -> Rep DeclarationException' x
    forall a.
    (forall x. a -> Rep a x) -> (forall x. Rep a x -> a) -> Generic a
    $cfrom :: forall x. DeclarationException' -> Rep DeclarationException' x
    from :: forall x. DeclarationException' -> Rep DeclarationException' x
    $cto :: forall x. Rep DeclarationException' x -> DeclarationException'
    to :: forall x. Rep DeclarationException' x -> DeclarationException'
    Generic)

    -- | The name of the error.
    declarationExceptionString :: DeclarationException' -> String
    declarationExceptionString :: DeclarationException' -> String
    declarationExceptionString = \case
      MultipleEllipses            {} -> String
    "MultipleEllipses"
      DuplicateDefinition         {} -> String
    "DuplicateDefinition"
      DuplicateAnonDeclaration    {} -> String
    "DuplicateAnonDeclaration"
      MissingWithClauses          {} -> String
    "MissingWithClauses"
      WrongDefinition             {} -> String
    "WrongDefinition"
      WrongContentBlock           {} -> String
    "WrongContentBlock"
      AmbiguousFunClauses         {} -> String
    "AmbiguousFunClauses"
      AmbiguousConstructor        {} -> String
    "AmbiguousConstructor"
      InvalidMeasureMutual        {} -> String
    "InvalidMeasureMutual"
      UnquoteDefRequiresSignature {} -> String
    "UnquoteDefRequiresSignature"
      BadMacroDef                 {} -> String
    "BadMacroDef"
      UnfoldingOutsideOpaque      {} -> String
    "UnfoldingOutsideOpaque"
      OpaqueInMutual              {} -> String
    "OpaqueInMutual"
      DisallowedInterleavedMutual {} -> String
    "DisallowedInterleavedMutual"

    ------------------------------------------------------------------------
    -- Warnings

    data DeclarationWarning = DeclarationWarning
      { DeclarationWarning -> CallStack
    dwLocation :: CallStack
      , DeclarationWarning -> DeclarationWarning'
    dwWarning  :: DeclarationWarning'
      } deriving (Int -> DeclarationWarning -> ShowS
    [DeclarationWarning] -> ShowS
    DeclarationWarning -> String
    (Int -> DeclarationWarning -> ShowS)
    -> (DeclarationWarning -> String)
    -> ([DeclarationWarning] -> ShowS)
    -> Show DeclarationWarning
    forall a.
    (Int -> a -> ShowS) -> (a -> String) -> ([a] -> ShowS) -> Show a
    $cshowsPrec :: Int -> DeclarationWarning -> ShowS
    showsPrec :: Int -> DeclarationWarning -> ShowS
    $cshow :: DeclarationWarning -> String
    show :: DeclarationWarning -> String
    $cshowList :: [DeclarationWarning] -> ShowS
    showList :: [DeclarationWarning] -> ShowS
    Show, (forall x. DeclarationWarning -> Rep DeclarationWarning x)
    -> (forall x. Rep DeclarationWarning x -> DeclarationWarning)
    -> Generic DeclarationWarning
    forall x. Rep DeclarationWarning x -> DeclarationWarning
    forall x. DeclarationWarning -> Rep DeclarationWarning x
    forall a.
    (forall x. a -> Rep a x) -> (forall x. Rep a x -> a) -> Generic a
    $cfrom :: forall x. DeclarationWarning -> Rep DeclarationWarning x
    from :: forall x. DeclarationWarning -> Rep DeclarationWarning x
    $cto :: forall x. Rep DeclarationWarning x -> DeclarationWarning
    to :: forall x. Rep DeclarationWarning x -> DeclarationWarning
    Generic)

    -- | Non-fatal errors encountered in the Nicifier.
    data DeclarationWarning'
      -- Please keep in (mostly) alphabetical order.
      = EmptyAbstract    KwRange  -- ^ Empty @abstract@     block.
      | EmptyConstructor KwRange  -- ^ Empty @data _ where@ block.
      | EmptyField       KwRange  -- ^ Empty @field@        block.
      | EmptyGeneralize  KwRange  -- ^ Empty @variable@     block.
      | EmptyInstance    KwRange  -- ^ Empty @instance@     block
      | EmptyMacro       KwRange  -- ^ Empty @macro@        block.
      | EmptyMutual      KwRange  -- ^ Empty @mutual@       block.
      | EmptyPostulate   KwRange  -- ^ Empty @postulate@    block.
      | EmptyPrivate     KwRange  -- ^ Empty @private@      block.
      | EmptyPrimitive   KwRange  -- ^ Empty @primitive@    block.
      | EmptyPolarityPragma Range
          -- ^ POLARITY pragma without any polarities.
      | HiddenGeneralize Range
          -- ^ A 'Hidden' identifier in a @variable@ declaration.
          --   Hiding has no effect there as generalized variables are always hidden
          --   (or instance variables).
      | InvalidCatchallPragma Range
          -- ^ A {-\# CATCHALL \#-} pragma
          --   that does not precede a function clause.
      | InvalidConstructorBlock Range
          -- ^ Invalid constructor block (not inside an interleaved mutual block)
      | InvalidCoverageCheckPragma Range
          -- ^ A {-\# NON_COVERING \#-} pragma that does not apply to any function.
      | InvalidNoPositivityCheckPragma Range
          -- ^ A {-\# NO_POSITIVITY_CHECK \#-} pragma
          --   that does not apply to any data or record type.
      | InvalidNoUniverseCheckPragma Range
          -- ^ A {-\# NO_UNIVERSE_CHECK \#-} pragma
          --   that does not apply to a data or record type.
      | InvalidTerminationCheckPragma Range
          -- ^ A {-\# TERMINATING \#-} and {-\# NON_TERMINATING \#-} pragma
          --   that does not apply to any function.
      | MissingDataDeclaration Name
          -- ^ A @data@ definition without a @data@ signature.
      | MissingDefinitions (List1 (Name, Range))
          -- ^ Declarations (e.g. type signatures) without a definition.
      | NotAllowedInMutual Range String
      | OpenImportPrivate Range KwRange KwRange OpenOrImport
          -- ^ @private@ has no effect on @open (import) public@.  (But the user might think so.)
          --   'Range' is the range of the @open public@ or @open import public@ declaration.
          --   The first 'KwRange' is the range of the @public@ keyword.
          --   The second 'KwRange' is the range of the @private@ keyword.
      | OpenImportAbstract Range KwRange OpenOrImport
          -- ^ @abstract@ has no effect on @open@ or @import@.  (But the user might think so.)
          --   'Range' is the range of the @open@ or @import@ declaration.
          --   'KwRange' is the range of the @abstract@ keyword.
      | PolarityPragmasButNotPostulates (Set1 Name)
      | PragmaNoTerminationCheck Range
          -- ^ Pragma @{-\# NO_TERMINATION_CHECK \#-}@ has been replaced
          --   by @{-\# TERMINATING \#-}@ and @{-\# NON_TERMINATING \#-}@.
      | PragmaCompiled Range
          -- ^ @COMPILE@ pragmas are not allowed in safe mode.
      | SafeFlagEta               Range -- ^ @ETA@                 pragma is unsafe.
      | SafeFlagInjective         Range -- ^ @INJECTIVE@           pragma is unsafe.
      | SafeFlagNoCoverageCheck   Range -- ^ @NON_COVERING@        pragma is unsafe.
      | SafeFlagNoPositivityCheck Range -- ^ @NO_POSITIVITY_CHECK@ pragma is unsafe.
      | SafeFlagNoUniverseCheck   Range -- ^ @NO_UNIVERSE_CHECK@   pragma is unsafe.
      | SafeFlagNonTerminating    Range -- ^ @NON_TERMINATING@     pragma is unsafe.
      | SafeFlagPolarity          Range -- ^ @POLARITY@            pragma is unsafe.
      | SafeFlagTerminating       Range -- ^ @TERMINATING@         pragma is unsafe.
      | ShadowingInTelescope (List1 (Name, List2 Range))
      | UnknownFixityInMixfixDecl (Set1 Name)
          -- ^ Public mixfix identifiers without a fixity declaration.
      | UnknownNamesInFixityDecl (Set1 Name)
      | UnknownNamesInPolarityPragmas (Set1 Name)
      | UselessAbstract KwRange
          -- ^ @abstract@ block with nothing that can (newly) be made abstract.
      | UselessInstance KwRange
          -- ^ @instance@ block with nothing that can (newly) become an instance.
      | UselessMacro KwRange
          -- ^ @macro@ block with nothing that can (newly) be made macro.
      | UselessPrivate KwRange
          -- ^ @private@ block with nothing that can (newly) be made private.
      deriving (Int -> DeclarationWarning' -> ShowS
    [DeclarationWarning'] -> ShowS
    DeclarationWarning' -> String
    (Int -> DeclarationWarning' -> ShowS)
    -> (DeclarationWarning' -> String)
    -> ([DeclarationWarning'] -> ShowS)
    -> Show DeclarationWarning'
    forall a.
    (Int -> a -> ShowS) -> (a -> String) -> ([a] -> ShowS) -> Show a
    $cshowsPrec :: Int -> DeclarationWarning' -> ShowS
    showsPrec :: Int -> DeclarationWarning' -> ShowS
    $cshow :: DeclarationWarning' -> String
    show :: DeclarationWarning' -> String
    $cshowList :: [DeclarationWarning'] -> ShowS
    showList :: [DeclarationWarning'] -> ShowS
    Show, (forall x. DeclarationWarning' -> Rep DeclarationWarning' x)
    -> (forall x. Rep DeclarationWarning' x -> DeclarationWarning')
    -> Generic DeclarationWarning'
    forall x. Rep DeclarationWarning' x -> DeclarationWarning'
    forall x. DeclarationWarning' -> Rep DeclarationWarning' x
    forall a.
    (forall x. a -> Rep a x) -> (forall x. Rep a x -> a) -> Generic a
    $cfrom :: forall x. DeclarationWarning' -> Rep DeclarationWarning' x
    from :: forall x. DeclarationWarning' -> Rep DeclarationWarning' x
    $cto :: forall x. Rep DeclarationWarning' x -> DeclarationWarning'
    to :: forall x. Rep DeclarationWarning' x -> DeclarationWarning'
    Generic)

    -- | @open@ or @import@
    data OpenOrImport
      = OpenNotImport  -- ^ @open@.
      | ImportMayOpen  -- ^ @import@ or @open import@.
      deriving (Int -> OpenOrImport -> ShowS
    [OpenOrImport] -> ShowS
    OpenOrImport -> String
    (Int -> OpenOrImport -> ShowS)
    -> (OpenOrImport -> String)
    -> ([OpenOrImport] -> ShowS)
    -> Show OpenOrImport
    forall a.
    (Int -> a -> ShowS) -> (a -> String) -> ([a] -> ShowS) -> Show a
    $cshowsPrec :: Int -> OpenOrImport -> ShowS
    showsPrec :: Int -> OpenOrImport -> ShowS
    $cshow :: OpenOrImport -> String
    show :: OpenOrImport -> String
    $cshowList :: [OpenOrImport] -> ShowS
    showList :: [OpenOrImport] -> ShowS
    Show, (forall x. OpenOrImport -> Rep OpenOrImport x)
    -> (forall x. Rep OpenOrImport x -> OpenOrImport)
    -> Generic OpenOrImport
    forall x. Rep OpenOrImport x -> OpenOrImport
    forall x. OpenOrImport -> Rep OpenOrImport x
    forall a.
    (forall x. a -> Rep a x) -> (forall x. Rep a x -> a) -> Generic a
    $cfrom :: forall x. OpenOrImport -> Rep OpenOrImport x
    from :: forall x. OpenOrImport -> Rep OpenOrImport x
    $cto :: forall x. Rep OpenOrImport x -> OpenOrImport
    to :: forall x. Rep OpenOrImport x -> OpenOrImport
    Generic, Int -> OpenOrImport
    OpenOrImport -> Int
    OpenOrImport -> [OpenOrImport]
    OpenOrImport -> OpenOrImport
    OpenOrImport -> OpenOrImport -> [OpenOrImport]
    OpenOrImport -> OpenOrImport -> OpenOrImport -> [OpenOrImport]
    (OpenOrImport -> OpenOrImport)
    -> (OpenOrImport -> OpenOrImport)
    -> (Int -> OpenOrImport)
    -> (OpenOrImport -> Int)
    -> (OpenOrImport -> [OpenOrImport])
    -> (OpenOrImport -> OpenOrImport -> [OpenOrImport])
    -> (OpenOrImport -> OpenOrImport -> [OpenOrImport])
    -> (OpenOrImport -> OpenOrImport -> OpenOrImport -> [OpenOrImport])
    -> Enum OpenOrImport
    forall a.
    (a -> a)
    -> (a -> a)
    -> (Int -> a)
    -> (a -> Int)
    -> (a -> [a])
    -> (a -> a -> [a])
    -> (a -> a -> [a])
    -> (a -> a -> a -> [a])
    -> Enum a
    $csucc :: OpenOrImport -> OpenOrImport
    succ :: OpenOrImport -> OpenOrImport
    $cpred :: OpenOrImport -> OpenOrImport
    pred :: OpenOrImport -> OpenOrImport
    $ctoEnum :: Int -> OpenOrImport
    toEnum :: Int -> OpenOrImport
    $cfromEnum :: OpenOrImport -> Int
    fromEnum :: OpenOrImport -> Int
    $cenumFrom :: OpenOrImport -> [OpenOrImport]
    enumFrom :: OpenOrImport -> [OpenOrImport]
    $cenumFromThen :: OpenOrImport -> OpenOrImport -> [OpenOrImport]
    enumFromThen :: OpenOrImport -> OpenOrImport -> [OpenOrImport]
    $cenumFromTo :: OpenOrImport -> OpenOrImport -> [OpenOrImport]
    enumFromTo :: OpenOrImport -> OpenOrImport -> [OpenOrImport]
    $cenumFromThenTo :: OpenOrImport -> OpenOrImport -> OpenOrImport -> [OpenOrImport]
    enumFromThenTo :: OpenOrImport -> OpenOrImport -> OpenOrImport -> [OpenOrImport]
    Enum, OpenOrImport
    OpenOrImport -> OpenOrImport -> Bounded OpenOrImport
    forall a. a -> a -> Bounded a
    $cminBound :: OpenOrImport
    minBound :: OpenOrImport
    $cmaxBound :: OpenOrImport
    maxBound :: OpenOrImport
    Bounded)

    declarationWarningName :: DeclarationWarning -> WarningName
    declarationWarningName :: DeclarationWarning -> WarningName
    declarationWarningName = DeclarationWarning' -> WarningName
    declarationWarningName' (DeclarationWarning' -> WarningName)
    -> (DeclarationWarning -> DeclarationWarning')
    -> DeclarationWarning
    -> WarningName
    forall b c a. (b -> c) -> (a -> b) -> a -> c
    . DeclarationWarning -> DeclarationWarning'
    dwWarning

    declarationWarningName' :: DeclarationWarning' -> WarningName
    declarationWarningName' :: DeclarationWarning' -> WarningName
    declarationWarningName' = \case
      -- Please keep in alphabetical order.
      EmptyAbstract{}                   -> WarningName
    EmptyAbstract_
      EmptyConstructor{}                -> WarningName
    EmptyConstructor_
      EmptyField{}                      -> WarningName
    EmptyField_
      EmptyGeneralize{}                 -> WarningName
    EmptyGeneralize_
      EmptyInstance{}                   -> WarningName
    EmptyInstance_
      EmptyMacro{}                      -> WarningName
    EmptyMacro_
      EmptyMutual{}                     -> WarningName
    EmptyMutual_
      EmptyPrivate{}                    -> WarningName
    EmptyPrivate_
      EmptyPostulate{}                  -> WarningName
    EmptyPostulate_
      EmptyPrimitive{}                  -> WarningName
    EmptyPrimitive_
      EmptyPolarityPragma{}             -> WarningName
    EmptyPolarityPragma_
      HiddenGeneralize{}                -> WarningName
    HiddenGeneralize_
      InvalidCatchallPragma{}           -> WarningName
    InvalidCatchallPragma_
      InvalidConstructorBlock{}         -> WarningName
    InvalidConstructorBlock_
      InvalidNoPositivityCheckPragma{}  -> WarningName
    InvalidNoPositivityCheckPragma_
      InvalidNoUniverseCheckPragma{}    -> WarningName
    InvalidNoUniverseCheckPragma_
      InvalidTerminationCheckPragma{}   -> WarningName
    InvalidTerminationCheckPragma_
      InvalidCoverageCheckPragma{}      -> WarningName
    InvalidCoverageCheckPragma_
      MissingDataDeclaration{}          -> WarningName
    MissingDataDeclaration_
      MissingDefinitions{}              -> WarningName
    MissingDefinitions_
      NotAllowedInMutual{}              -> WarningName
    NotAllowedInMutual_
      OpenImportPrivate{}               -> WarningName
    OpenImportPrivate_
      OpenImportAbstract{}              -> WarningName
    OpenImportAbstract_
      PolarityPragmasButNotPostulates{} -> WarningName
    PolarityPragmasButNotPostulates_
      PragmaNoTerminationCheck{}        -> WarningName
    PragmaNoTerminationCheck_
      PragmaCompiled{}                  -> WarningName
    PragmaCompiled_
      SafeFlagEta                    {} -> WarningName
    SafeFlagEta_
      SafeFlagInjective              {} -> WarningName
    SafeFlagInjective_
      SafeFlagNoCoverageCheck        {} -> WarningName
    SafeFlagNoCoverageCheck_
      SafeFlagNoPositivityCheck      {} -> WarningName
    SafeFlagNoPositivityCheck_
      SafeFlagNoUniverseCheck        {} -> WarningName
    SafeFlagNoUniverseCheck_
      SafeFlagNonTerminating         {} -> WarningName
    SafeFlagNonTerminating_
      SafeFlagPolarity               {} -> WarningName
    SafeFlagPolarity_
      SafeFlagTerminating            {} -> WarningName
    SafeFlagTerminating_
      ShadowingInTelescope{}            -> WarningName
    ShadowingInTelescope_
      UnknownFixityInMixfixDecl{}       -> WarningName
    UnknownFixityInMixfixDecl_
      UnknownNamesInFixityDecl{}        -> WarningName
    UnknownNamesInFixityDecl_
      UnknownNamesInPolarityPragmas{}   -> WarningName
    UnknownNamesInPolarityPragmas_
      UselessAbstract{}                 -> WarningName
    UselessAbstract_
      UselessInstance{}                 -> WarningName
    UselessInstance_
      UselessMacro{}                    -> WarningName
    UselessMacro_
      UselessPrivate{}                  -> WarningName
    UselessPrivate_

    -- | Nicifier warnings turned into errors in @--safe@ mode.
    unsafeDeclarationWarning :: DeclarationWarning -> Bool
    unsafeDeclarationWarning :: DeclarationWarning -> Bool
    unsafeDeclarationWarning = DeclarationWarning' -> Bool
    unsafeDeclarationWarning' (DeclarationWarning' -> Bool)
    -> (DeclarationWarning -> DeclarationWarning')
    -> DeclarationWarning
    -> Bool
    forall b c a. (b -> c) -> (a -> b) -> a -> c
    . DeclarationWarning -> DeclarationWarning'
    dwWarning

    unsafeDeclarationWarning' :: DeclarationWarning' -> Bool
    unsafeDeclarationWarning' :: DeclarationWarning' -> Bool
    unsafeDeclarationWarning' = \case
      -- Please keep in alphabetical order.
      EmptyAbstract{}                   -> Bool
    False
      EmptyConstructor{}                -> Bool
    False
      EmptyField{}                      -> Bool
    False
      EmptyGeneralize{}                 -> Bool
    False
      EmptyInstance{}                   -> Bool
    False
      EmptyMacro{}                      -> Bool
    False
      EmptyMutual{}                     -> Bool
    False
      EmptyPrivate{}                    -> Bool
    False
      EmptyPostulate{}                  -> Bool
    False
      EmptyPrimitive{}                  -> Bool
    False
      EmptyPolarityPragma{}             -> Bool
    False
      HiddenGeneralize{}                -> Bool
    False
      InvalidCatchallPragma{}           -> Bool
    False
      InvalidConstructorBlock{}         -> Bool
    False
      InvalidNoPositivityCheckPragma{}  -> Bool
    False
      InvalidNoUniverseCheckPragma{}    -> Bool
    False
      InvalidTerminationCheckPragma{}   -> Bool
    False
      InvalidCoverageCheckPragma{}      -> Bool
    False
      MissingDataDeclaration{}          -> Bool
    True  -- not safe
      MissingDefinitions{}              -> Bool
    False -- not safe but deferred until after typechecking
      NotAllowedInMutual{}              -> Bool
    False -- really safe?
      OpenImportPrivate{}               -> Bool
    False
      OpenImportAbstract{}              -> Bool
    False
      PolarityPragmasButNotPostulates{} -> Bool
    False
      PragmaNoTerminationCheck{}        -> Bool
    True  -- not safe
      PragmaCompiled{}                  -> Bool
    True  -- not safe
      SafeFlagEta                    {} -> Bool
    True
      SafeFlagInjective              {} -> Bool
    True
      SafeFlagNoCoverageCheck        {} -> Bool
    True
      SafeFlagNoPositivityCheck      {} -> Bool
    True
      SafeFlagNoUniverseCheck        {} -> Bool
    True
      SafeFlagNonTerminating         {} -> Bool
    True
      SafeFlagPolarity               {} -> Bool
    True
      SafeFlagTerminating            {} -> Bool
    True
      ShadowingInTelescope{}            -> Bool
    False
      UnknownFixityInMixfixDecl{}       -> Bool
    False
      UnknownNamesInFixityDecl{}        -> Bool
    False
      UnknownNamesInPolarityPragmas{}   -> Bool
    False
      UselessAbstract{}                 -> Bool
    False
      UselessInstance{}                 -> Bool
    False
      UselessMacro{}                    -> Bool
    False
      UselessPrivate{}                  -> Bool
    False

    -- | Pragmas not allowed in @--safe@ mode produce an 'unsafeDeclarationWarning'.
    --
    unsafePragma :: CMaybe DeclarationWarning' m => Pragma -> m
    unsafePragma :: forall m. CMaybe DeclarationWarning' m => Pragma -> m
    unsafePragma Pragma
    p =
      case Pragma
    p of
        BuiltinPragma{}            -> m
    forall a. Null a => a
    empty
        CatchallPragma{}           -> m
    forall a. Null a => a
    empty
        CompilePragma{}            -> DeclarationWarning' -> m
    forall el coll. Singleton el coll => el -> coll
    singleton (DeclarationWarning' -> m) -> DeclarationWarning' -> m
    forall a b. (a -> b) -> a -> b
    $ Range -> DeclarationWarning'
    PragmaCompiled Range
    r
        DisplayPragma{}            -> m
    forall a. Null a => a
    empty
        EtaPragma{}                -> DeclarationWarning' -> m
    forall el coll. Singleton el coll => el -> coll
    singleton (DeclarationWarning' -> m) -> DeclarationWarning' -> m
    forall a b. (a -> b) -> a -> b
    $ Range -> DeclarationWarning'
    SafeFlagEta Range
    r
        ForeignPragma{}            -> m
    forall a. Null a => a
    empty
        ImpossiblePragma{}         -> m
    forall a. Null a => a
    empty
        InjectivePragma{}          -> DeclarationWarning' -> m
    forall el coll. Singleton el coll => el -> coll
    singleton (DeclarationWarning' -> m) -> DeclarationWarning' -> m
    forall a b. (a -> b) -> a -> b
    $ Range -> DeclarationWarning'
    SafeFlagInjective Range
    r
        InjectiveForInferencePragma{} -> m
    forall a. Null a => a
    empty
        InlinePragma{}             -> m
    forall a. Null a => a
    empty
        NoCoverageCheckPragma{}    -> DeclarationWarning' -> m
    forall el coll. Singleton el coll => el -> coll
    singleton (DeclarationWarning' -> m) -> DeclarationWarning' -> m
    forall a b. (a -> b) -> a -> b
    $ Range -> DeclarationWarning'
    SafeFlagNoCoverageCheck Range
    r
        NoPositivityCheckPragma{}  -> DeclarationWarning' -> m
    forall el coll. Singleton el coll => el -> coll
    singleton (DeclarationWarning' -> m) -> DeclarationWarning' -> m
    forall a b. (a -> b) -> a -> b
    $ Range -> DeclarationWarning'
    SafeFlagNoPositivityCheck Range
    r
        NoUniverseCheckPragma{}    -> DeclarationWarning' -> m
    forall el coll. Singleton el coll => el -> coll
    singleton (DeclarationWarning' -> m) -> DeclarationWarning' -> m
    forall a b. (a -> b) -> a -> b
    $ Range -> DeclarationWarning'
    SafeFlagNoUniverseCheck Range
    r
        NotProjectionLikePragma{}  -> m
    forall a. Null a => a
    empty
        OptionsPragma{}            -> m
    forall a. Null a => a
    empty
        PolarityPragma{}           -> DeclarationWarning' -> m
    forall el coll. Singleton el coll => el -> coll
    singleton (DeclarationWarning' -> m) -> DeclarationWarning' -> m
    forall a b. (a -> b) -> a -> b
    $ Range -> DeclarationWarning'
    SafeFlagPolarity Range
    r
        RewritePragma{}            -> m
    forall a. Null a => a
    empty
          -- @RewritePragma@ already requires --rewriting which is incompatible with --safe
        StaticPragma{}             -> m
    forall a. Null a => a
    empty
        TerminationCheckPragma Range
    _ TerminationCheck Name
    m ->
          case TerminationCheck Name
    m of
            TerminationCheck Name
    NonTerminating         -> DeclarationWarning' -> m
    forall el coll. Singleton el coll => el -> coll
    singleton (DeclarationWarning' -> m) -> DeclarationWarning' -> m
    forall a b. (a -> b) -> a -> b
    $ Range -> DeclarationWarning'
    SafeFlagNonTerminating Range
    r
            TerminationCheck Name
    Terminating            -> DeclarationWarning' -> m
    forall el coll. Singleton el coll => el -> coll
    singleton (DeclarationWarning' -> m) -> DeclarationWarning' -> m
    forall a b. (a -> b) -> a -> b
    $ Range -> DeclarationWarning'
    SafeFlagTerminating Range
    r
            TerminationCheck Name
    TerminationCheck       -> m
    forall a. Null a => a
    empty
            TerminationMeasure{}   -> m
    forall a. Null a => a
    empty
            -- @NO_TERMINATION_CHECK@ pragma was removed, but still parses. See Issue #1763.
            -- There is the unsafe @'PragmaNoTerminationCheck'@ warning thrown already,
            -- so we need not throw anything here.
            TerminationCheck Name
    NoTerminationCheck     -> m
    forall a. Null a => a
    empty
        WarningOnImport{}          -> m
    forall a. Null a => a
    empty
        WarningOnUsage{}           -> m
    forall a. Null a => a
    empty
        OverlapPragma{}            -> m
    forall a. Null a => a
    empty
      where
        r :: Range
    r = Pragma -> Range
    forall a. HasRange a => a -> Range
    getRange Pragma
    p

    ------------------------------------------------------------------------
    -- Instances

    instance HasRange DeclarationException where
      getRange :: DeclarationException -> Range
    getRange (DeclarationException CallStack
    _ DeclarationException'
    err) = DeclarationException' -> Range
    forall a. HasRange a => a -> Range
    getRange DeclarationException'
    err

    instance HasRange DeclarationException' where
      getRange :: DeclarationException' -> Range
    getRange (MultipleEllipses Pattern
    d)                 = Pattern -> Range
    forall a. HasRange a => a -> Range
    getRange Pattern
    d
      getRange (DuplicateDefinition Name
    x)              = Name -> Range
    forall a. HasRange a => a -> Range
    getRange Name
    x
      getRange (DuplicateAnonDeclaration Range
    r)         = Range
    r
      getRange (MissingWithClauses Name
    x LHS
    lhs)           = LHS -> Range
    forall a. HasRange a => a -> Range
    getRange LHS
    lhs
      getRange (WrongDefinition Name
    x DataRecOrFun
    k DataRecOrFun
    k')             = Name -> Range
    forall a. HasRange a => a -> Range
    getRange Name
    x
      getRange (AmbiguousFunClauses LHS
    lhs List1 Name
    xs)         = LHS -> Range
    forall a. HasRange a => a -> Range
    getRange LHS
    lhs
      getRange (AmbiguousConstructor Range
    r Name
    _ [Name]
    _)         = Range
    r
      getRange (WrongContentBlock KindOfBlock
    _ Range
    r)              = Range
    r
      getRange (InvalidMeasureMutual Range
    r)             = Range
    r
      getRange (UnquoteDefRequiresSignature List1 Name
    xs)     = List1 Name -> Range
    forall a. HasRange a => a -> Range
    getRange List1 Name
    xs
      getRange (BadMacroDef NiceDeclaration
    d)                      = NiceDeclaration -> Range
    forall a. HasRange a => a -> Range
    getRange NiceDeclaration
    d
      getRange (UnfoldingOutsideOpaque KwRange
    kwr)         = KwRange -> Range
    forall a. HasRange a => a -> Range
    getRange KwRange
    kwr
      getRange (OpaqueInMutual KwRange
    kwr)                 = KwRange -> Range
    forall a. HasRange a => a -> Range
    getRange KwRange
    kwr
      getRange (DisallowedInterleavedMutual KwRange
    kwr String
    _ List1 Name
    _)= KwRange -> Range
    forall a. HasRange a => a -> Range
    getRange KwRange
    kwr

    instance HasRange DeclarationWarning where
      getRange :: DeclarationWarning -> Range
    getRange (DeclarationWarning CallStack
    _ DeclarationWarning'
    w) = DeclarationWarning' -> Range
    forall a. HasRange a => a -> Range
    getRange DeclarationWarning'
    w

    instance HasRange DeclarationWarning' where
      getRange :: DeclarationWarning' -> Range
    getRange = \case
        EmptyAbstract KwRange
    kwr                  -> KwRange -> Range
    forall a. HasRange a => a -> Range
    getRange KwRange
    kwr
        EmptyConstructor KwRange
    kwr               -> KwRange -> Range
    forall a. HasRange a => a -> Range
    getRange KwRange
    kwr
        EmptyField KwRange
    kwr                     -> KwRange -> Range
    forall a. HasRange a => a -> Range
    getRange KwRange
    kwr
        EmptyGeneralize KwRange
    kwr                -> KwRange -> Range
    forall a. HasRange a => a -> Range
    getRange KwRange
    kwr
        EmptyInstance KwRange
    kwr                  -> KwRange -> Range
    forall a. HasRange a => a -> Range
    getRange KwRange
    kwr
        EmptyMacro KwRange
    kwr                     -> KwRange -> Range
    forall a. HasRange a => a -> Range
    getRange KwRange
    kwr
        EmptyMutual KwRange
    kwr                    -> KwRange -> Range
    forall a. HasRange a => a -> Range
    getRange KwRange
    kwr
        EmptyPostulate KwRange
    kwr                 -> KwRange -> Range
    forall a. HasRange a => a -> Range
    getRange KwRange
    kwr
        EmptyPrimitive KwRange
    kwr                 -> KwRange -> Range
    forall a. HasRange a => a -> Range
    getRange KwRange
    kwr
        EmptyPrivate KwRange
    kwr                   -> KwRange -> Range
    forall a. HasRange a => a -> Range
    getRange KwRange
    kwr
        EmptyPolarityPragma Range
    r              -> Range
    r
        HiddenGeneralize Range
    r                 -> Range
    r
        InvalidCatchallPragma Range
    r            -> Range
    r
        InvalidConstructorBlock Range
    r          -> Range
    r
        InvalidCoverageCheckPragma Range
    r       -> Range
    r
        InvalidNoPositivityCheckPragma Range
    r   -> Range
    r
        InvalidNoUniverseCheckPragma Range
    r     -> Range
    r
        InvalidTerminationCheckPragma Range
    r    -> Range
    r
        MissingDataDeclaration Name
    x           -> Name -> Range
    forall a. HasRange a => a -> Range
    getRange Name
    x
        MissingDefinitions List1 (Name, Range)
    xs              -> List1 (Name, Range) -> Range
    forall a. HasRange a => a -> Range
    getRange List1 (Name, Range)
    xs
        NotAllowedInMutual Range
    r String
    x             -> Range
    r
        OpenImportAbstract Range
    r KwRange
    _kwr OpenOrImport
    _        -> Range -> Range
    forall a. HasRange a => a -> Range
    getRange Range
    r
        OpenImportPrivate  Range
    _r KwRange
    kwr KwRange
    _kwr OpenOrImport
    _   -> KwRange -> Range
    forall a. HasRange a => a -> Range
    getRange KwRange
    kwr
        PolarityPragmasButNotPostulates Set1 Name
    xs -> Set1 Name -> Range
    forall a. HasRange a => a -> Range
    getRange Set1 Name
    xs
        PragmaCompiled Range
    r                   -> Range
    r
        PragmaNoTerminationCheck Range
    r         -> Range
    r
        SafeFlagEta Range
    r                      -> Range
    r
        SafeFlagInjective Range
    r                -> Range
    r
        SafeFlagNoCoverageCheck Range
    r          -> Range
    r
        SafeFlagNoPositivityCheck Range
    r        -> Range
    r
        SafeFlagNoUniverseCheck Range
    r          -> Range
    r
        SafeFlagNonTerminating Range
    r           -> Range
    r
        SafeFlagPolarity Range
    r                 -> Range
    r
        SafeFlagTerminating Range
    r              -> Range
    r
        ShadowingInTelescope List1 (Name, List2 Range)
    ns            -> List1 (Name, List2 Range) -> Range
    forall a. HasRange a => a -> Range
    getRange List1 (Name, List2 Range)
    ns
        UnknownFixityInMixfixDecl Set1 Name
    xs       -> Set1 Name -> Range
    forall a. HasRange a => a -> Range
    getRange Set1 Name
    xs
        UnknownNamesInFixityDecl Set1 Name
    xs        -> Set1 Name -> Range
    forall a. HasRange a => a -> Range
    getRange Set1 Name
    xs
        UnknownNamesInPolarityPragmas Set1 Name
    xs   -> Set1 Name -> Range
    forall a. HasRange a => a -> Range
    getRange Set1 Name
    xs
        UselessAbstract KwRange
    kwr                -> KwRange -> Range
    forall a. HasRange a => a -> Range
    getRange KwRange
    kwr
        UselessInstance KwRange
    kwr                -> KwRange -> Range
    forall a. HasRange a => a -> Range
    getRange KwRange
    kwr
        UselessMacro KwRange
    kwr                   -> KwRange -> Range
    forall a. HasRange a => a -> Range
    getRange KwRange
    kwr
        UselessPrivate KwRange
    kwr                 -> KwRange -> Range
    forall a. HasRange a => a -> Range
    getRange KwRange
    kwr

    -- These error messages can (should) be terminated by a dot ".",
    -- there is no error context printed after them.
    instance Pretty DeclarationException' where
      pretty :: DeclarationException' -> Doc
    pretty (MultipleEllipses Pattern
    p) = [Doc] -> Doc
    forall (t :: * -> *). Foldable t => t Doc -> Doc
    fsep ([Doc] -> Doc) -> [Doc] -> Doc
    forall a b. (a -> b) -> a -> b
    $
        String -> [Doc]
    pwords String
    "Multiple ellipses in left-hand side" [Doc] -> [Doc] -> [Doc]
    forall a. [a] -> [a] -> [a]
    ++ [Pattern -> Doc
    forall a. Pretty a => a -> Doc
    pretty Pattern
    p]
      pretty (DuplicateDefinition Name
    x) = [Doc] -> Doc
    forall (t :: * -> *). Foldable t => t Doc -> Doc
    fsep ([Doc] -> Doc) -> [Doc] -> Doc
    forall a b. (a -> b) -> a -> b
    $
        String -> [Doc]
    pwords String
    "Duplicate definition of" [Doc] -> [Doc] -> [Doc]
    forall a. [a] -> [a] -> [a]
    ++ [Name -> Doc
    forall a. Pretty a => a -> Doc
    pretty Name
    x]
      pretty (DuplicateAnonDeclaration Range
    _) = [Doc] -> Doc
    forall (t :: * -> *). Foldable t => t Doc -> Doc
    fsep ([Doc] -> Doc) -> [Doc] -> Doc
    forall a b. (a -> b) -> a -> b
    $
        String -> [Doc]
    pwords String
    "Duplicate declaration of _"
      pretty (MissingWithClauses Name
    x LHS
    lhs) = [Doc] -> Doc
    forall (t :: * -> *). Foldable t => t Doc -> Doc
    fsep ([Doc] -> Doc) -> [Doc] -> Doc
    forall a b. (a -> b) -> a -> b
    $
        String -> [Doc]
    pwords String
    "Missing with-clauses for function" [Doc] -> [Doc] -> [Doc]
    forall a. [a] -> [a] -> [a]
    ++ [Name -> Doc
    forall a. Pretty a => a -> Doc
    pretty Name
    x]

      pretty (WrongDefinition Name
    x DataRecOrFun
    k DataRecOrFun
    k') = [Doc] -> Doc
    forall (t :: * -> *). Foldable t => t Doc -> Doc
    fsep ([Doc] -> Doc) -> [Doc] -> Doc
    forall a b. (a -> b) -> a -> b
    $ Name -> Doc
    forall a. Pretty a => a -> Doc
    pretty Name
    x Doc -> [Doc] -> [Doc]
    forall a. a -> [a] -> [a]
    :
        String -> [Doc]
    pwords (String
    "has been declared as a " String -> ShowS
    forall a. [a] -> [a] -> [a]
    ++ DataRecOrFun -> String
    forall a. Pretty a => a -> String
    prettyShow DataRecOrFun
    k String -> ShowS
    forall a. [a] -> [a] -> [a]
    ++
          String
    ", but is being defined as a " String -> ShowS
    forall a. [a] -> [a] -> [a]
    ++ DataRecOrFun -> String
    forall a. Pretty a => a -> String
    prettyShow DataRecOrFun
    k')
      pretty (AmbiguousFunClauses LHS
    lhs List1 Name
    xs) = [Doc] -> Doc
    forall (t :: * -> *). Foldable t => t Doc -> Doc
    sep
        [ [Doc] -> Doc
    forall (t :: * -> *). Foldable t => t Doc -> Doc
    fsep ([Doc] -> Doc) -> [Doc] -> Doc
    forall a b. (a -> b) -> a -> b
    $
            String -> [Doc]
    pwords String
    "More than one matching type signature for left hand side " [Doc] -> [Doc] -> [Doc]
    forall a. [a] -> [a] -> [a]
    ++ [LHS -> Doc
    forall a. Pretty a => a -> Doc
    pretty LHS
    lhs] [Doc] -> [Doc] -> [Doc]
    forall a. [a] -> [a] -> [a]
    ++
            String -> [Doc]
    pwords String
    "it could belong to any of:"
        , List1 Doc -> Doc
    forall (t :: * -> *). Foldable t => t Doc -> Doc
    vcat (List1 Doc -> Doc) -> List1 Doc -> Doc
    forall a b. (a -> b) -> a -> b
    $ (Name -> Doc) -> List1 Name -> List1 Doc
    forall a b. (a -> b) -> NonEmpty a -> NonEmpty b
    forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
    fmap (PrintRange Name -> Doc
    forall a. Pretty a => a -> Doc
    pretty (PrintRange Name -> Doc)
    -> (Name -> PrintRange Name) -> Name -> Doc
    forall b c a. (b -> c) -> (a -> b) -> a -> c
    . Name -> PrintRange Name
    forall a. a -> PrintRange a
    PrintRange) List1 Name
    xs
        ]
      pretty (AmbiguousConstructor Range
    _ Name
    n [Name]
    ns) = [Doc] -> Doc
    forall (t :: * -> *). Foldable t => t Doc -> Doc
    sep
        [ [Doc] -> Doc
    forall (t :: * -> *). Foldable t => t Doc -> Doc
    fsep (String -> [Doc]
    pwords String
    "Could not find a matching data signature for constructor " [Doc] -> [Doc] -> [Doc]
    forall a. [a] -> [a] -> [a]
    ++ [Name -> Doc
    forall a. Pretty a => a -> Doc
    pretty Name
    n])
        , [Doc] -> Doc
    forall (t :: * -> *). Foldable t => t Doc -> Doc
    vcat (case [Name]
    ns of
                  [] -> [[Doc] -> Doc
    forall (t :: * -> *). Foldable t => t Doc -> Doc
    fsep ([Doc] -> Doc) -> [Doc] -> Doc
    forall a b. (a -> b) -> a -> b
    $ String -> [Doc]
    pwords String
    "There was no candidate."]
                  [Name]
    _  -> [Doc] -> Doc
    forall (t :: * -> *). Foldable t => t Doc -> Doc
    fsep (String -> [Doc]
    pwords String
    "It could be any of:") Doc -> [Doc] -> [Doc]
    forall a. a -> [a] -> [a]
    : (Name -> Doc) -> [Name] -> [Doc]
    forall a b. (a -> b) -> [a] -> [b]
    forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
    fmap (PrintRange Name -> Doc
    forall a. Pretty a => a -> Doc
    pretty (PrintRange Name -> Doc)
    -> (Name -> PrintRange Name) -> Name -> Doc
    forall b c a. (b -> c) -> (a -> b) -> a -> c
    . Name -> PrintRange Name
    forall a. a -> PrintRange a
    PrintRange) [Name]
    ns
               )
        ]
      pretty (WrongContentBlock KindOfBlock
    b Range
    _)      = [Doc] -> Doc
    forall (t :: * -> *). Foldable t => t Doc -> Doc
    fsep ([Doc] -> Doc) -> (String -> [Doc]) -> String -> Doc
    forall b c a. (b -> c) -> (a -> b) -> a -> c
    . String -> [Doc]
    pwords (String -> Doc) -> String -> Doc
    forall a b. (a -> b) -> a -> b
    $
        case KindOfBlock
    b of
          KindOfBlock
    PostulateBlock -> String
    "A `postulate` block can only contain type signatures, possibly under keywords `instance` and `private`"
          KindOfBlock
    DataBlock -> String
    "A data definition can only contain type signatures, possibly under keyword instance"
          KindOfBlock
    _ -> String
    "Unexpected declaration"
      pretty (InvalidMeasureMutual Range
    _) = [Doc] -> Doc
    forall (t :: * -> *). Foldable t => t Doc -> Doc
    fsep ([Doc] -> Doc) -> [Doc] -> Doc
    forall a b. (a -> b) -> a -> b
    $
        String -> [Doc]
    pwords String
    "In a mutual block, either all functions must have the same (or no) termination checking pragma."
      pretty (UnquoteDefRequiresSignature List1 Name
    xs) = [Doc] -> Doc
    forall (t :: * -> *). Foldable t => t Doc -> Doc
    fsep ([Doc] -> Doc) -> [Doc] -> Doc
    forall a b. (a -> b) -> a -> b
    $
        String -> [Doc]
    pwords String
    "Missing type signatures for unquoteDef" [Doc] -> [Doc] -> [Doc]
    forall a. [a] -> [a] -> [a]
    ++ (Name -> Doc) -> [Name] -> [Doc]
    forall a b. (a -> b) -> [a] -> [b]
    map Name -> Doc
    forall a. Pretty a => a -> Doc
    pretty (List1 Name -> [Item (List1 Name)]
    forall l. IsList l => l -> [Item l]
    List1.toList List1 Name
    xs)
      pretty (BadMacroDef NiceDeclaration
    nd) = [Doc] -> Doc
    forall (t :: * -> *). Foldable t => t Doc -> Doc
    fsep ([Doc] -> Doc) -> [Doc] -> Doc
    forall a b. (a -> b) -> a -> b
    $
        String -> Doc
    forall a. String -> Doc a
    text (NiceDeclaration -> String
    declName NiceDeclaration
    nd) Doc -> [Doc] -> [Doc]
    forall a. a -> [a] -> [a]
    : String -> [Doc]
    pwords String
    "are not allowed in macro blocks"
      pretty (UnfoldingOutsideOpaque KwRange
    _) = [Doc] -> Doc
    forall (t :: * -> *). Foldable t => t Doc -> Doc
    fsep ([Doc] -> Doc) -> (String -> [Doc]) -> String -> Doc
    forall b c a. (b -> c) -> (a -> b) -> a -> c
    . String -> [Doc]
    pwords (String -> Doc) -> String -> Doc
    forall a b. (a -> b) -> a -> b
    $
        String
    "Unfolding declarations can only appear as the first declaration immediately contained in an opaque block."
      pretty (OpaqueInMutual KwRange
    _) = [Doc] -> Doc
    forall (t :: * -> *). Foldable t => t Doc -> Doc
    fsep ([Doc] -> Doc) -> [Doc] -> Doc
    forall a b. (a -> b) -> a -> b
    $
        String -> [Doc]
    pwords String
    "Opaque blocks can not participate in mutual recursion. If the opaque definitions are to be mutually recursive, move the `mutual` block inside the `opaque` block."
      pretty (DisallowedInterleavedMutual KwRange
    _ String
    what List1 Name
    xs) = [Doc] -> Doc
    forall (t :: * -> *). Foldable t => t Doc -> Doc
    vcat ([Doc] -> Doc) -> [Doc] -> Doc
    forall a b. (a -> b) -> a -> b
    $ [List1 Doc] -> [Doc]
    forall a. [List1 a] -> [a]
    List1.concat
        [ Doc -> List1 Doc
    forall el coll. Singleton el coll => el -> coll
    singleton (Doc -> List1 Doc) -> Doc -> List1 Doc
    forall a b. (a -> b) -> a -> b
    $ [Doc] -> Doc
    forall (t :: * -> *). Foldable t => t Doc -> Doc
    fsep ([Doc] -> Doc) -> [Doc] -> Doc
    forall a b. (a -> b) -> a -> b
    $ String -> [Doc]
    pwords String
    "The following names are declared, but not accompanied by a definition:"
          -- Andreas, 2023-09-07, issue #6823: print also the range.
          -- Print a bullet list; thus, the plural version of this error message is sufficient.
        , (Name -> Doc) -> List1 Name -> List1 Doc
    forall a b. (a -> b) -> NonEmpty a -> NonEmpty b
    forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
    fmap ((Doc
    "-" Doc -> Doc -> Doc
    forall a. Doc a -> Doc a -> Doc a
    <+>) (Doc -> Doc) -> (Name -> Doc) -> Name -> Doc
    forall b c a. (b -> c) -> (a -> b) -> a -> c
    . PrintRange Name -> Doc
    forall a. Pretty a => a -> Doc
    pretty (PrintRange Name -> Doc)
    -> (Name -> PrintRange Name) -> Name -> Doc
    forall b c a. (b -> c) -> (a -> b) -> a -> c
    . Name -> PrintRange Name
    forall a. a -> PrintRange a
    PrintRange) List1 Name
    xs
        , Doc -> List1 Doc
    forall el coll. Singleton el coll => el -> coll
    singleton (Doc -> List1 Doc) -> Doc -> List1 Doc
    forall a b. (a -> b) -> a -> b
    $ String -> Doc
    fwords (String -> Doc) -> String -> Doc
    forall a b. (a -> b) -> a -> b
    $ String
    "Since " String -> ShowS
    forall a. [a] -> [a] -> [a]
    ++ String
    what String -> ShowS
    forall a. [a] -> [a] -> [a]
    ++ String
    " can not participate in mutual recursion, their definition must be given before this point."
        ]

    instance Pretty DeclarationWarning where
      pretty :: DeclarationWarning -> Doc
    pretty (DeclarationWarning CallStack
    _ DeclarationWarning'
    w) = DeclarationWarning' -> Doc
    forall a. Pretty a => a -> Doc
    pretty DeclarationWarning'
    w

    instance Pretty DeclarationWarning' where
      pretty :: DeclarationWarning' -> Doc
    pretty = \case

        UnknownNamesInFixityDecl Set1 Name
    xs -> [Doc] -> Doc
    forall (t :: * -> *). Foldable t => t Doc -> Doc
    fsep ([Doc] -> Doc) -> [Doc] -> Doc
    forall a b. (a -> b) -> a -> b
    $
          String -> [Doc]
    pwords String
    "The following names are not declared in the same scope as their syntax or fixity declaration (i.e., either not in scope at all, imported from another module, or declared in a super module):"
          [Doc] -> [Doc] -> [Doc]
    forall a. [a] -> [a] -> [a]
    ++ Doc -> List1 Doc -> [Doc]
    forall (t :: * -> *). Foldable t => Doc -> t Doc -> [Doc]
    punctuate Doc
    comma ((Name -> Doc) -> List1 Name -> List1 Doc
    forall a b. (a -> b) -> NonEmpty a -> NonEmpty b
    forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
    fmap Name -> Doc
    forall a. Pretty a => a -> Doc
    pretty (List1 Name -> List1 Doc) -> List1 Name -> List1 Doc
    forall a b. (a -> b) -> a -> b
    $ Set1 Name -> List1 Name
    forall a. NESet a -> NonEmpty a
    Set1.toList Set1 Name
    xs)

        UnknownFixityInMixfixDecl Set1 Name
    xs -> [Doc] -> Doc
    forall (t :: * -> *). Foldable t => t Doc -> Doc
    fsep ([Doc] -> Doc) -> [Doc] -> Doc
    forall a b. (a -> b) -> a -> b
    $
          String -> [Doc]
    pwords String
    "The following mixfix names do not have an associated fixity declaration:"
          [Doc] -> [Doc] -> [Doc]
    forall a. [a] -> [a] -> [a]
    ++ Doc -> List1 Doc -> [Doc]
    forall (t :: * -> *). Foldable t => Doc -> t Doc -> [Doc]
    punctuate Doc
    comma ((Name -> Doc) -> List1 Name -> List1 Doc
    forall a b. (a -> b) -> NonEmpty a -> NonEmpty b
    forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
    fmap Name -> Doc
    forall a. Pretty a => a -> Doc
    pretty (List1 Name -> List1 Doc) -> List1 Name -> List1 Doc
    forall a b. (a -> b) -> a -> b
    $ Set1 Name -> List1 Name
    forall a. NESet a -> NonEmpty a
    Set1.toList Set1 Name
    xs)

        UnknownNamesInPolarityPragmas Set1 Name
    xs -> [Doc] -> Doc
    forall (t :: * -> *). Foldable t => t Doc -> Doc
    fsep ([Doc] -> Doc) -> [Doc] -> Doc
    forall a b. (a -> b) -> a -> b
    $
          String -> [Doc]
    pwords String
    "The following names are not declared in the same scope as their polarity pragmas (they could for instance be out of scope, imported from another module, or declared in a super module):"
          [Doc] -> [Doc] -> [Doc]
    forall a. [a] -> [a] -> [a]
    ++ Doc -> List1 Doc -> [Doc]
    forall (t :: * -> *). Foldable t => Doc -> t Doc -> [Doc]
    punctuate Doc
    comma ((Name -> Doc) -> List1 Name -> List1 Doc
    forall a b. (a -> b) -> NonEmpty a -> NonEmpty b
    forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
    fmap Name -> Doc
    forall a. Pretty a => a -> Doc
    pretty (List1 Name -> List1 Doc) -> List1 Name -> List1 Doc
    forall a b. (a -> b) -> a -> b
    $ Set1 Name -> List1 Name
    forall a. NESet a -> NonEmpty a
    Set1.toList Set1 Name
    xs)

        MissingDataDeclaration Name
    x -> [Doc] -> Doc
    forall (t :: * -> *). Foldable t => t Doc -> Doc
    fsep ([Doc] -> Doc) -> [Doc] -> Doc
    forall a b. (a -> b) -> a -> b
    $ [[Doc]] -> [Doc]
    forall (t :: * -> *) a. Foldable t => t [a] -> [a]
    concat
          [ String -> [Doc]
    pwords String
    "Data definition"
          , [ Name -> Doc
    forall a. Pretty a => a -> Doc
    pretty Name
    x ]
          , String -> [Doc]
    pwords String
    "misses a data declaration"
          ]

        MissingDefinitions List1 (Name, Range)
    xs -> [Doc] -> Doc
    forall (t :: * -> *). Foldable t => t Doc -> Doc
    fsep ([Doc] -> Doc) -> [Doc] -> Doc
    forall a b. (a -> b) -> a -> b
    $
         String -> [Doc]
    pwords String
    "The following names are declared but not accompanied by a definition:"
         [Doc] -> [Doc] -> [Doc]
    forall a. [a] -> [a] -> [a]
    ++ Doc -> List1 Doc -> [Doc]
    forall (t :: * -> *). Foldable t => Doc -> t Doc -> [Doc]
    punctuate Doc
    comma (((Name, Range) -> Doc) -> List1 (Name, Range) -> List1 Doc
    forall a b. (a -> b) -> NonEmpty a -> NonEmpty b
    forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
    fmap (Name -> Doc
    forall a. Pretty a => a -> Doc
    pretty (Name -> Doc) -> ((Name, Range) -> Name) -> (Name, Range) -> Doc
    forall b c a. (b -> c) -> (a -> b) -> a -> c
    . (Name, Range) -> Name
    forall a b. (a, b) -> a
    fst) List1 (Name, Range)
    xs)

        NotAllowedInMutual Range
    r String
    nd -> [Doc] -> Doc
    forall (t :: * -> *). Foldable t => t Doc -> Doc
    fsep ([Doc] -> Doc) -> [Doc] -> Doc
    forall a b. (a -> b) -> a -> b
    $
          String -> Doc
    forall a. String -> Doc a
    text String
    nd Doc -> [Doc] -> [Doc]
    forall a. a -> [a] -> [a]
    : String -> [Doc]
    pwords String
    "in mutual blocks are not supported.  Suggestion: get rid of the mutual block by manually ordering declarations"

        PolarityPragmasButNotPostulates Set1 Name
    xs -> [Doc] -> Doc
    forall (t :: * -> *). Foldable t => t Doc -> Doc
    fsep ([Doc] -> Doc) -> [Doc] -> Doc
    forall a b. (a -> b) -> a -> b
    $
          String -> [Doc]
    pwords String
    "Polarity pragmas have been given for the following identifiers which are not postulates:"
          [Doc] -> [Doc] -> [Doc]
    forall a. [a] -> [a] -> [a]
    ++ Doc -> List1 Doc -> [Doc]
    forall (t :: * -> *). Foldable t => Doc -> t Doc -> [Doc]
    punctuate Doc
    comma ((Name -> Doc) -> List1 Name -> List1 Doc
    forall a b. (a -> b) -> NonEmpty a -> NonEmpty b
    forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
    fmap Name -> Doc
    forall a. Pretty a => a -> Doc
    pretty (List1 Name -> List1 Doc) -> List1 Name -> List1 Doc
    forall a b. (a -> b) -> a -> b
    $ Set1 Name -> List1 Name
    forall a. NESet a -> NonEmpty a
    Set1.toList Set1 Name
    xs)

        UselessPrivate KwRange
    _ -> [Doc] -> Doc
    forall (t :: * -> *). Foldable t => t Doc -> Doc
    fsep ([Doc] -> Doc) -> [Doc] -> Doc
    forall a b. (a -> b) -> a -> b
    $
          String -> [Doc]
    pwords String
    "Using private here has no effect. Private applies only to declarations that introduce new identifiers into the module, like type signatures and data, record, and module declarations."

        UselessAbstract KwRange
    _ -> [Doc] -> Doc
    forall (t :: * -> *). Foldable t => t Doc -> Doc
    fsep ([Doc] -> Doc) -> [Doc] -> Doc
    forall a b. (a -> b) -> a -> b
    $
          String -> [Doc]
    pwords String
    "Using abstract here has no effect. Abstract applies to only definitions like data definitions, record type definitions and function clauses."

        UselessInstance KwRange
    _ -> [Doc] -> Doc
    forall (t :: * -> *). Foldable t => t Doc -> Doc
    fsep ([Doc] -> Doc) -> [Doc] -> Doc
    forall a b. (a -> b) -> a -> b
    $
          String -> [Doc]
    pwords String
    "Using instance here has no effect. Instance applies only to declarations that introduce new identifiers into the module, like type signatures and axioms."

        UselessMacro KwRange
    _ -> [Doc] -> Doc
    forall (t :: * -> *). Foldable t => t Doc -> Doc
    fsep ([Doc] -> Doc) -> [Doc] -> Doc
    forall a b. (a -> b) -> a -> b
    $
          String -> [Doc]
    pwords String
    "Using a macro block here has no effect. `macro' applies only to function definitions."

        EmptyMutual    KwRange
    _ -> [Doc] -> Doc
    forall (t :: * -> *). Foldable t => t Doc -> Doc
    fsep ([Doc] -> Doc) -> [Doc] -> Doc
    forall a b. (a -> b) -> a -> b
    $ String -> [Doc]
    pwords String
    "Empty mutual block."

        EmptyConstructor{}  -> [Doc] -> Doc
    forall (t :: * -> *). Foldable t => t Doc -> Doc
    fsep ([Doc] -> Doc) -> [Doc] -> Doc
    forall a b. (a -> b) -> a -> b
    $ String -> [Doc]
    pwords String
    "Empty constructor block."

        EmptyAbstract  KwRange
    _ -> [Doc] -> Doc
    forall (t :: * -> *). Foldable t => t Doc -> Doc
    fsep ([Doc] -> Doc) -> [Doc] -> Doc
    forall a b. (a -> b) -> a -> b
    $ String -> [Doc]
    pwords String
    "Empty abstract block."

        EmptyPrivate   KwRange
    _ -> [Doc] -> Doc
    forall (t :: * -> *). Foldable t => t Doc -> Doc
    fsep ([Doc] -> Doc) -> [Doc] -> Doc
    forall a b. (a -> b) -> a -> b
    $ String -> [Doc]
    pwords String
    "Empty private block."

        EmptyInstance  KwRange
    _ -> [Doc] -> Doc
    forall (t :: * -> *). Foldable t => t Doc -> Doc
    fsep ([Doc] -> Doc) -> [Doc] -> Doc
    forall a b. (a -> b) -> a -> b
    $ String -> [Doc]
    pwords String
    "Empty instance block."

        EmptyMacro     KwRange
    _ -> [Doc] -> Doc
    forall (t :: * -> *). Foldable t => t Doc -> Doc
    fsep ([Doc] -> Doc) -> [Doc] -> Doc
    forall a b. (a -> b) -> a -> b
    $ String -> [Doc]
    pwords String
    "Empty macro block."

        EmptyPostulate KwRange
    _ -> [Doc] -> Doc
    forall (t :: * -> *). Foldable t => t Doc -> Doc
    fsep ([Doc] -> Doc) -> [Doc] -> Doc
    forall a b. (a -> b) -> a -> b
    $ String -> [Doc]
    pwords String
    "Empty postulate block."

        EmptyGeneralize KwRange
    _ -> [Doc] -> Doc
    forall (t :: * -> *). Foldable t => t Doc -> Doc
    fsep ([Doc] -> Doc) -> [Doc] -> Doc
    forall a b. (a -> b) -> a -> b
    $ String -> [Doc]
    pwords String
    "Empty variable block."

        EmptyPrimitive KwRange
    _ -> [Doc] -> Doc
    forall (t :: * -> *). Foldable t => t Doc -> Doc
    fsep ([Doc] -> Doc) -> [Doc] -> Doc
    forall a b. (a -> b) -> a -> b
    $ String -> [Doc]
    pwords String
    "Empty primitive block."

        EmptyField KwRange
    _ -> [Doc] -> Doc
    forall (t :: * -> *). Foldable t => t Doc -> Doc
    fsep ([Doc] -> Doc) -> [Doc] -> Doc
    forall a b. (a -> b) -> a -> b
    $ String -> [Doc]
    pwords String
    "Empty field block."

        EmptyPolarityPragma Range
    _ -> [Doc] -> Doc
    forall (t :: * -> *). Foldable t => t Doc -> Doc
    fsep ([Doc] -> Doc) -> [Doc] -> Doc
    forall a b. (a -> b) -> a -> b
    $ String -> [Doc]
    pwords String
    "POLARITY pragma without polarities (ignored)."

        HiddenGeneralize Range
    _ -> [Doc] -> Doc
    forall (t :: * -> *). Foldable t => t Doc -> Doc
    fsep ([Doc] -> Doc) -> [Doc] -> Doc
    forall a b. (a -> b) -> a -> b
    $ String -> [Doc]
    pwords String
    "Declaring a variable as hidden has no effect in a variable block. Generalization never introduces visible arguments."

        InvalidTerminationCheckPragma Range
    _ -> [Doc] -> Doc
    forall (t :: * -> *). Foldable t => t Doc -> Doc
    fsep ([Doc] -> Doc) -> [Doc] -> Doc
    forall a b. (a -> b) -> a -> b
    $
          String -> [Doc]
    pwords String
    "Termination checking pragmas can only precede a function definition or a mutual block (that contains a function definition)."

        InvalidConstructorBlock{} -> [Doc] -> Doc
    forall (t :: * -> *). Foldable t => t Doc -> Doc
    fsep ([Doc] -> Doc) -> [Doc] -> Doc
    forall a b. (a -> b) -> a -> b
    $
          String -> [Doc]
    pwords String
    "No `data _ where' blocks outside of `interleaved mutual' blocks."

        InvalidCoverageCheckPragma Range
    _ -> [Doc] -> Doc
    forall (t :: * -> *). Foldable t => t Doc -> Doc
    fsep ([Doc] -> Doc) -> [Doc] -> Doc
    forall a b. (a -> b) -> a -> b
    $
          String -> [Doc]
    pwords String
    "Coverage checking pragmas can only precede a function definition or a mutual block (that contains a function definition)."

        InvalidNoPositivityCheckPragma Range
    _ -> [Doc] -> Doc
    forall (t :: * -> *). Foldable t => t Doc -> Doc
    fsep ([Doc] -> Doc) -> [Doc] -> Doc
    forall a b. (a -> b) -> a -> b
    $
          String -> [Doc]
    pwords String
    "NO_POSITIVITY_CHECKING pragmas can only precede a data/record definition or a mutual block (that contains a data/record definition)."

        InvalidCatchallPragma Range
    _ -> [Doc] -> Doc
    forall (t :: * -> *). Foldable t => t Doc -> Doc
    fsep ([Doc] -> Doc) -> [Doc] -> Doc
    forall a b. (a -> b) -> a -> b
    $
          String -> [Doc]
    pwords String
    "The CATCHALL pragma can only precede a function clause."

        InvalidNoUniverseCheckPragma Range
    _ -> [Doc] -> Doc
    forall (t :: * -> *). Foldable t => t Doc -> Doc
    fsep ([Doc] -> Doc) -> [Doc] -> Doc
    forall a b. (a -> b) -> a -> b
    $
          String -> [Doc]
    pwords String
    "NO_UNIVERSE_CHECKING pragmas can only precede a data/record definition."

        PragmaNoTerminationCheck Range
    _ -> [Doc] -> Doc
    forall (t :: * -> *). Foldable t => t Doc -> Doc
    fsep ([Doc] -> Doc) -> [Doc] -> Doc
    forall a b. (a -> b) -> a -> b
    $
          String -> [Doc]
    pwords String
    "Pragma {-# NO_TERMINATION_CHECK #-} has been removed.  To skip the termination check, label your definitions either as {-# TERMINATING #-} or {-# NON_TERMINATING #-}."

        PragmaCompiled Range
    _ -> [Doc] -> Doc
    forall (t :: * -> *). Foldable t => t Doc -> Doc
    fsep ([Doc] -> Doc) -> [Doc] -> Doc
    forall a b. (a -> b) -> a -> b
    $
          String -> [Doc]
    pwords String
    "COMPILE pragma not allowed in safe mode."

        OpenImportAbstract Range
    _ KwRange
    _ OpenOrImport
    openOrImport -> [Doc] -> Doc
    forall (t :: * -> *). Foldable t => t Doc -> Doc
    fsep ([Doc] -> Doc) -> [Doc] -> Doc
    forall a b. (a -> b) -> a -> b
    $ [[Doc]] -> [Doc]
    forall (t :: * -> *) a. Foldable t => t [a] -> [a]
    concat
          [ String -> [Doc]
    pwords String
    "`abstract' does not have any effect on"
          , [ OpenOrImport -> Doc
    forall a. Pretty a => a -> Doc
    pretty OpenOrImport
    openOrImport ]
          , String -> [Doc]
    pwords String
    "so better place this statement outside of the abstract block"
          ]

        OpenImportPrivate Range
    _ KwRange
    _ KwRange
    _ OpenOrImport
    _openOrImport -> [Doc] -> Doc
    forall (t :: * -> *). Foldable t => t Doc -> Doc
    fsep ([Doc] -> Doc) -> [Doc] -> Doc
    forall a b. (a -> b) -> a -> b
    $ [[Doc]] -> [Doc]
    forall (t :: * -> *) a. Foldable t => t [a] -> [a]
    concat
          [ String -> [Doc]
    pwords String
    "`private' does not have any effect on"
          , String -> [Doc]
    pwords String
    "`open public'"
          , String -> [Doc]
    pwords String
    "so better place this statement outside of the private block"
          ]

        ShadowingInTelescope List1 (Name, List2 Range)
    nrs -> [Doc] -> Doc
    forall (t :: * -> *). Foldable t => t Doc -> Doc
    fsep ([Doc] -> Doc) -> [Doc] -> Doc
    forall a b. (a -> b) -> a -> b
    $
          String -> [Doc]
    pwords String
    "Shadowing in telescope, repeated variable names:"
          [Doc] -> [Doc] -> [Doc]
    forall a. [a] -> [a] -> [a]
    ++ Doc -> List1 Doc -> [Doc]
    forall (t :: * -> *). Foldable t => Doc -> t Doc -> [Doc]
    punctuate Doc
    comma (((Name, List2 Range) -> Doc)
    -> List1 (Name, List2 Range) -> List1 Doc
    forall a b. (a -> b) -> NonEmpty a -> NonEmpty b
    forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
    fmap (Name -> Doc
    forall a. Pretty a => a -> Doc
    pretty (Name -> Doc)
    -> ((Name, List2 Range) -> Name) -> (Name, List2 Range) -> Doc
    forall b c a. (b -> c) -> (a -> b) -> a -> c
    . (Name, List2 Range) -> Name
    forall a b. (a, b) -> a
    fst) List1 (Name, List2 Range)
    nrs)

        SafeFlagEta               Range
    _ -> Doc -> Doc
    unsafePragma Doc
    "ETA"
        SafeFlagInjective         Range
    _ -> Doc -> Doc
    unsafePragma Doc
    "INJECTIVE"
        SafeFlagNoCoverageCheck   Range
    _ -> Doc -> Doc
    unsafePragma Doc
    "NON_COVERING"
        SafeFlagNoPositivityCheck Range
    _ -> Doc -> Doc
    unsafePragma Doc
    "NO_POSITIVITY_CHECK"
        SafeFlagNoUniverseCheck   Range
    _ -> Doc -> Doc
    unsafePragma Doc
    "NO_UNIVERSE_CHECK"
        SafeFlagNonTerminating    Range
    _ -> Doc -> Doc
    unsafePragma Doc
    "NON_TERMINATING"
        SafeFlagPolarity          Range
    _ -> Doc -> Doc
    unsafePragma Doc
    "POLARITY"
        SafeFlagTerminating       Range
    _ -> Doc -> Doc
    unsafePragma Doc
    "TERMINATING"

        where
          unsafePragma :: Doc -> Doc
    unsafePragma Doc
    s = [Doc] -> Doc
    forall (t :: * -> *). Foldable t => t Doc -> Doc
    fsep ([Doc] -> Doc) -> [Doc] -> Doc
    forall a b. (a -> b) -> a -> b
    $ [Doc
    "Cannot", Doc
    "use", Doc
    s] [Doc] -> [Doc] -> [Doc]
    forall a. [a] -> [a] -> [a]
    ++ String -> [Doc]
    pwords String
    "pragma with safe flag."

    instance Pretty OpenOrImport where
      pretty :: OpenOrImport -> Doc
    pretty = \case
        OpenOrImport
    OpenNotImport -> Doc
    "`open'"
        OpenOrImport
    ImportMayOpen -> Doc
    "`import'"

    instance NFData DeclarationException'
    instance NFData DeclarationWarning
    instance NFData DeclarationWarning'
    instance NFData OpenOrImport