    module Agda.Syntax.Concrete.Definitions.Errors where

    import Control.DeepSeq

    import Data.Data

    import GHC.Generics (Generic)

    import Agda.Syntax.Position
    import Agda.Syntax.Concrete
    import Agda.Syntax.Concrete.Name
    import Agda.Syntax.Concrete.Definitions.Types

    import Agda.Interaction.Options.Warnings

    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.Pretty

    ------------------------------------------------------------------------
    -- 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
      | InvalidName Name
      | DuplicateDefinition Name
      | DuplicateAnonDeclaration Range
      | MissingWithClauses Name LHS
      | WrongDefinition Name DataRecOrFun DataRecOrFun
      | DeclarationPanic String
      | 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 of mutual block.
      | UnquoteDefRequiresSignature (List1 Name)
      | BadMacroDef NiceDeclaration
        deriving (Typeable DeclarationException'
    Typeable DeclarationException'
    -> (forall (c :: * -> *).
        (forall d b. Data d => c (d -> b) -> d -> c b)
        -> (forall g. g -> c g)
        -> DeclarationException'
        -> c DeclarationException')
    -> (forall (c :: * -> *).
        (forall b r. Data b => c (b -> r) -> c r)
        -> (forall r. r -> c r) -> Constr -> c DeclarationException')
    -> (DeclarationException' -> Constr)
    -> (DeclarationException' -> DataType)
    -> (forall (t :: * -> *) (c :: * -> *).
        Typeable t =>
        (forall d. Data d => c (t d)) -> Maybe (c DeclarationException'))
    -> (forall (t :: * -> * -> *) (c :: * -> *).
        Typeable t =>
        (forall d e. (Data d, Data e) => c (t d e))
        -> Maybe (c DeclarationException'))
    -> ((forall b. Data b => b -> b)
        -> DeclarationException' -> DeclarationException')
    -> (forall r r'.
        (r -> r' -> r)
        -> r
        -> (forall d. Data d => d -> r')
        -> DeclarationException'
        -> r)
    -> (forall r r'.
        (r' -> r -> r)
        -> r
        -> (forall d. Data d => d -> r')
        -> DeclarationException'
        -> r)
    -> (forall u.
        (forall d. Data d => d -> u) -> DeclarationException' -> [u])
    -> (forall u.
        Int -> (forall d. Data d => d -> u) -> DeclarationException' -> u)
    -> (forall (m :: * -> *).
        Monad m =>
        (forall d. Data d => d -> m d)
        -> DeclarationException' -> m DeclarationException')
    -> (forall (m :: * -> *).
        MonadPlus m =>
        (forall d. Data d => d -> m d)
        -> DeclarationException' -> m DeclarationException')
    -> (forall (m :: * -> *).
        MonadPlus m =>
        (forall d. Data d => d -> m d)
        -> DeclarationException' -> m DeclarationException')
    -> Data DeclarationException'
    DeclarationException' -> DataType
    DeclarationException' -> Constr
    (forall b. Data b => b -> b)
    -> DeclarationException' -> DeclarationException'
    forall a.
    Typeable a
    -> (forall (c :: * -> *).
        (forall d b. Data d => c (d -> b) -> d -> c b)
        -> (forall g. g -> c g) -> a -> c a)
    -> (forall (c :: * -> *).
        (forall b r. Data b => c (b -> r) -> c r)
        -> (forall r. r -> c r) -> Constr -> c a)
    -> (a -> Constr)
    -> (a -> DataType)
    -> (forall (t :: * -> *) (c :: * -> *).
        Typeable t =>
        (forall d. Data d => c (t d)) -> Maybe (c a))
    -> (forall (t :: * -> * -> *) (c :: * -> *).
        Typeable t =>
        (forall d e. (Data d, Data e) => c (t d e)) -> Maybe (c a))
    -> ((forall b. Data b => b -> b) -> a -> a)
    -> (forall r r'.
        (r -> r' -> r) -> r -> (forall d. Data d => d -> r') -> a -> r)
    -> (forall r r'.
        (r' -> r -> r) -> r -> (forall d. Data d => d -> r') -> a -> r)
    -> (forall u. (forall d. Data d => d -> u) -> a -> [u])
    -> (forall u. Int -> (forall d. Data d => d -> u) -> a -> u)
    -> (forall (m :: * -> *).
        Monad m =>
        (forall d. Data d => d -> m d) -> a -> m a)
    -> (forall (m :: * -> *).
        MonadPlus m =>
        (forall d. Data d => d -> m d) -> a -> m a)
    -> (forall (m :: * -> *).
        MonadPlus m =>
        (forall d. Data d => d -> m d) -> a -> m a)
    -> Data a
    forall u.
    Int -> (forall d. Data d => d -> u) -> DeclarationException' -> u
    forall u.
    (forall d. Data d => d -> u) -> DeclarationException' -> [u]
    forall r r'.
    (r -> r' -> r)
    -> r -> (forall d. Data d => d -> r') -> DeclarationException' -> r
    forall r r'.
    (r' -> r -> r)
    -> r -> (forall d. Data d => d -> r') -> DeclarationException' -> r
    forall (m :: * -> *).
    Monad m =>
    (forall d. Data d => d -> m d)
    -> DeclarationException' -> m DeclarationException'
    forall (m :: * -> *).
    MonadPlus m =>
    (forall d. Data d => d -> m d)
    -> DeclarationException' -> m DeclarationException'
    forall (c :: * -> *).
    (forall b r. Data b => c (b -> r) -> c r)
    -> (forall r. r -> c r) -> Constr -> c DeclarationException'
    forall (c :: * -> *).
    (forall d b. Data d => c (d -> b) -> d -> c b)
    -> (forall g. g -> c g)
    -> DeclarationException'
    -> c DeclarationException'
    forall (t :: * -> *) (c :: * -> *).
    Typeable t =>
    (forall d. Data d => c (t d)) -> Maybe (c DeclarationException')
    forall (t :: * -> * -> *) (c :: * -> *).
    Typeable t =>
    (forall d e. (Data d, Data e) => c (t d e))
    -> Maybe (c DeclarationException')
    gmapMo :: forall (m :: * -> *).
    MonadPlus m =>
    (forall d. Data d => d -> m d)
    -> DeclarationException' -> m DeclarationException'
    $cgmapMo :: forall (m :: * -> *).
    MonadPlus m =>
    (forall d. Data d => d -> m d)
    -> DeclarationException' -> m DeclarationException'
    gmapMp :: forall (m :: * -> *).
    MonadPlus m =>
    (forall d. Data d => d -> m d)
    -> DeclarationException' -> m DeclarationException'
    $cgmapMp :: forall (m :: * -> *).
    MonadPlus m =>
    (forall d. Data d => d -> m d)
    -> DeclarationException' -> m DeclarationException'
    gmapM :: forall (m :: * -> *).
    Monad m =>
    (forall d. Data d => d -> m d)
    -> DeclarationException' -> m DeclarationException'
    $cgmapM :: forall (m :: * -> *).
    Monad m =>
    (forall d. Data d => d -> m d)
    -> DeclarationException' -> m DeclarationException'
    gmapQi :: forall u.
    Int -> (forall d. Data d => d -> u) -> DeclarationException' -> u
    $cgmapQi :: forall u.
    Int -> (forall d. Data d => d -> u) -> DeclarationException' -> u
    gmapQ :: forall u.
    (forall d. Data d => d -> u) -> DeclarationException' -> [u]
    $cgmapQ :: forall u.
    (forall d. Data d => d -> u) -> DeclarationException' -> [u]
    gmapQr :: forall r r'.
    (r' -> r -> r)
    -> r -> (forall d. Data d => d -> r') -> DeclarationException' -> r
    $cgmapQr :: forall r r'.
    (r' -> r -> r)
    -> r -> (forall d. Data d => d -> r') -> DeclarationException' -> r
    gmapQl :: forall r r'.
    (r -> r' -> r)
    -> r -> (forall d. Data d => d -> r') -> DeclarationException' -> r
    $cgmapQl :: forall r r'.
    (r -> r' -> r)
    -> r -> (forall d. Data d => d -> r') -> DeclarationException' -> r
    gmapT :: (forall b. Data b => b -> b)
    -> DeclarationException' -> DeclarationException'
    $cgmapT :: (forall b. Data b => b -> b)
    -> DeclarationException' -> DeclarationException'
    dataCast2 :: forall (t :: * -> * -> *) (c :: * -> *).
    Typeable t =>
    (forall d e. (Data d, Data e) => c (t d e))
    -> Maybe (c DeclarationException')
    $cdataCast2 :: forall (t :: * -> * -> *) (c :: * -> *).
    Typeable t =>
    (forall d e. (Data d, Data e) => c (t d e))
    -> Maybe (c DeclarationException')
    dataCast1 :: forall (t :: * -> *) (c :: * -> *).
    Typeable t =>
    (forall d. Data d => c (t d)) -> Maybe (c DeclarationException')
    $cdataCast1 :: forall (t :: * -> *) (c :: * -> *).
    Typeable t =>
    (forall d. Data d => c (t d)) -> Maybe (c DeclarationException')
    dataTypeOf :: DeclarationException' -> DataType
    $cdataTypeOf :: DeclarationException' -> DataType
    toConstr :: DeclarationException' -> Constr
    $ctoConstr :: DeclarationException' -> Constr
    gunfold :: forall (c :: * -> *).
    (forall b r. Data b => c (b -> r) -> c r)
    -> (forall r. r -> c r) -> Constr -> c DeclarationException'
    $cgunfold :: forall (c :: * -> *).
    (forall b r. Data b => c (b -> r) -> c r)
    -> (forall r. r -> c r) -> Constr -> c DeclarationException'
    gfoldl :: forall (c :: * -> *).
    (forall d b. Data d => c (d -> b) -> d -> c b)
    -> (forall g. g -> c g)
    -> DeclarationException'
    -> c DeclarationException'
    $cgfoldl :: forall (c :: * -> *).
    (forall d b. Data d => c (d -> b) -> d -> c b)
    -> (forall g. g -> c g)
    -> DeclarationException'
    -> c DeclarationException'
    Data, 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
    showList :: [DeclarationException'] -> ShowS
    $cshowList :: [DeclarationException'] -> ShowS
    show :: DeclarationException' -> String
    $cshow :: DeclarationException' -> String
    showsPrec :: Int -> DeclarationException' -> ShowS
    $cshowsPrec :: Int -> DeclarationException' -> ShowS
    Show)

    ------------------------------------------------------------------------
    -- 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
    showList :: [DeclarationWarning] -> ShowS
    $cshowList :: [DeclarationWarning] -> ShowS
    show :: DeclarationWarning -> String
    $cshow :: DeclarationWarning -> String
    showsPrec :: Int -> DeclarationWarning -> ShowS
    $cshowsPrec :: Int -> 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
    $cto :: forall x. Rep DeclarationWarning x -> DeclarationWarning
    $cfrom :: forall x. DeclarationWarning -> Rep DeclarationWarning x
    Generic)

    -- | Non-fatal errors encountered in the Nicifier.
    data DeclarationWarning'
      -- Please keep in alphabetical order.
      = EmptyAbstract Range    -- ^ Empty @abstract@  block.
      | EmptyConstructor Range -- ^ Empty @constructor@ block.
      | EmptyField Range       -- ^ Empty @field@     block.
      | EmptyGeneralize Range  -- ^ Empty @variable@  block.
      | EmptyInstance Range    -- ^ Empty @instance@  block
      | EmptyMacro Range       -- ^ Empty @macro@     block.
      | EmptyMutual Range      -- ^ Empty @mutual@    block.
      | EmptyPostulate Range   -- ^ Empty @postulate@ block.
      | EmptyPrivate Range     -- ^ Empty @private@   block.
      | EmptyPrimitive Range   -- ^ Empty @primitive@ block.
      | InvalidCatchallPragma Range
          -- ^ A {-\# CATCHALL \#-} pragma
          --   that does not precede a function clause.
      | InvalidConstructor Range
          -- ^ Invalid definition in a constructor block
      | 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.
      | InvalidRecordDirective Range
          -- ^ A record directive outside of a record / below existing fields.
      | InvalidTerminationCheckPragma Range
          -- ^ A {-\# TERMINATING \#-} and {-\# NON_TERMINATING \#-} pragma
          --   that does not apply to any function.
      | MissingDeclarations [(Name, Range)]
          -- ^ Definitions (e.g. constructors or functions) without a declaration.
      | MissingDefinitions [(Name, Range)]
          -- ^ Declarations (e.g. type signatures) without a definition.
      | NotAllowedInMutual Range String
      | OpenPublicPrivate Range
          -- ^ @private@ has no effect on @open public@.  (But the user might think so.)
      | OpenPublicAbstract Range
          -- ^ @abstract@ has no effect on @open public@.  (But the user might think so.)
      | PolarityPragmasButNotPostulates [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
      | ShadowingInTelescope (List1 (Name, List2 Range))
      | UnknownFixityInMixfixDecl [Name]
      | UnknownNamesInFixityDecl [Name]
      | UnknownNamesInPolarityPragmas [Name]
      | UselessAbstract Range
          -- ^ @abstract@ block with nothing that can (newly) be made abstract.
      | UselessInstance Range
          -- ^ @instance@ block with nothing that can (newly) become an instance.
      | UselessPrivate Range
          -- ^ @private@ block with nothing that can (newly) be made private.
      deriving (Typeable DeclarationWarning'
    Typeable DeclarationWarning'
    -> (forall (c :: * -> *).
        (forall d b. Data d => c (d -> b) -> d -> c b)
        -> (forall g. g -> c g)
        -> DeclarationWarning'
        -> c DeclarationWarning')
    -> (forall (c :: * -> *).
        (forall b r. Data b => c (b -> r) -> c r)
        -> (forall r. r -> c r) -> Constr -> c DeclarationWarning')
    -> (DeclarationWarning' -> Constr)
    -> (DeclarationWarning' -> DataType)
    -> (forall (t :: * -> *) (c :: * -> *).
        Typeable t =>
        (forall d. Data d => c (t d)) -> Maybe (c DeclarationWarning'))
    -> (forall (t :: * -> * -> *) (c :: * -> *).
        Typeable t =>
        (forall d e. (Data d, Data e) => c (t d e))
        -> Maybe (c DeclarationWarning'))
    -> ((forall b. Data b => b -> b)
        -> DeclarationWarning' -> DeclarationWarning')
    -> (forall r r'.
        (r -> r' -> r)
        -> r -> (forall d. Data d => d -> r') -> DeclarationWarning' -> r)
    -> (forall r r'.
        (r' -> r -> r)
        -> r -> (forall d. Data d => d -> r') -> DeclarationWarning' -> r)
    -> (forall u.
        (forall d. Data d => d -> u) -> DeclarationWarning' -> [u])
    -> (forall u.
        Int -> (forall d. Data d => d -> u) -> DeclarationWarning' -> u)
    -> (forall (m :: * -> *).
        Monad m =>
        (forall d. Data d => d -> m d)
        -> DeclarationWarning' -> m DeclarationWarning')
    -> (forall (m :: * -> *).
        MonadPlus m =>
        (forall d. Data d => d -> m d)
        -> DeclarationWarning' -> m DeclarationWarning')
    -> (forall (m :: * -> *).
        MonadPlus m =>
        (forall d. Data d => d -> m d)
        -> DeclarationWarning' -> m DeclarationWarning')
    -> Data DeclarationWarning'
    DeclarationWarning' -> DataType
    DeclarationWarning' -> Constr
    (forall b. Data b => b -> b)
    -> DeclarationWarning' -> DeclarationWarning'
    forall a.
    Typeable a
    -> (forall (c :: * -> *).
        (forall d b. Data d => c (d -> b) -> d -> c b)
        -> (forall g. g -> c g) -> a -> c a)
    -> (forall (c :: * -> *).
        (forall b r. Data b => c (b -> r) -> c r)
        -> (forall r. r -> c r) -> Constr -> c a)
    -> (a -> Constr)
    -> (a -> DataType)
    -> (forall (t :: * -> *) (c :: * -> *).
        Typeable t =>
        (forall d. Data d => c (t d)) -> Maybe (c a))
    -> (forall (t :: * -> * -> *) (c :: * -> *).
        Typeable t =>
        (forall d e. (Data d, Data e) => c (t d e)) -> Maybe (c a))
    -> ((forall b. Data b => b -> b) -> a -> a)
    -> (forall r r'.
        (r -> r' -> r) -> r -> (forall d. Data d => d -> r') -> a -> r)
    -> (forall r r'.
        (r' -> r -> r) -> r -> (forall d. Data d => d -> r') -> a -> r)
    -> (forall u. (forall d. Data d => d -> u) -> a -> [u])
    -> (forall u. Int -> (forall d. Data d => d -> u) -> a -> u)
    -> (forall (m :: * -> *).
        Monad m =>
        (forall d. Data d => d -> m d) -> a -> m a)
    -> (forall (m :: * -> *).
        MonadPlus m =>
        (forall d. Data d => d -> m d) -> a -> m a)
    -> (forall (m :: * -> *).
        MonadPlus m =>
        (forall d. Data d => d -> m d) -> a -> m a)
    -> Data a
    forall u.
    Int -> (forall d. Data d => d -> u) -> DeclarationWarning' -> u
    forall u.
    (forall d. Data d => d -> u) -> DeclarationWarning' -> [u]
    forall r r'.
    (r -> r' -> r)
    -> r -> (forall d. Data d => d -> r') -> DeclarationWarning' -> r
    forall r r'.
    (r' -> r -> r)
    -> r -> (forall d. Data d => d -> r') -> DeclarationWarning' -> r
    forall (m :: * -> *).
    Monad m =>
    (forall d. Data d => d -> m d)
    -> DeclarationWarning' -> m DeclarationWarning'
    forall (m :: * -> *).
    MonadPlus m =>
    (forall d. Data d => d -> m d)
    -> DeclarationWarning' -> m DeclarationWarning'
    forall (c :: * -> *).
    (forall b r. Data b => c (b -> r) -> c r)
    -> (forall r. r -> c r) -> Constr -> c DeclarationWarning'
    forall (c :: * -> *).
    (forall d b. Data d => c (d -> b) -> d -> c b)
    -> (forall g. g -> c g)
    -> DeclarationWarning'
    -> c DeclarationWarning'
    forall (t :: * -> *) (c :: * -> *).
    Typeable t =>
    (forall d. Data d => c (t d)) -> Maybe (c DeclarationWarning')
    forall (t :: * -> * -> *) (c :: * -> *).
    Typeable t =>
    (forall d e. (Data d, Data e) => c (t d e))
    -> Maybe (c DeclarationWarning')
    gmapMo :: forall (m :: * -> *).
    MonadPlus m =>
    (forall d. Data d => d -> m d)
    -> DeclarationWarning' -> m DeclarationWarning'
    $cgmapMo :: forall (m :: * -> *).
    MonadPlus m =>
    (forall d. Data d => d -> m d)
    -> DeclarationWarning' -> m DeclarationWarning'
    gmapMp :: forall (m :: * -> *).
    MonadPlus m =>
    (forall d. Data d => d -> m d)
    -> DeclarationWarning' -> m DeclarationWarning'
    $cgmapMp :: forall (m :: * -> *).
    MonadPlus m =>
    (forall d. Data d => d -> m d)
    -> DeclarationWarning' -> m DeclarationWarning'
    gmapM :: forall (m :: * -> *).
    Monad m =>
    (forall d. Data d => d -> m d)
    -> DeclarationWarning' -> m DeclarationWarning'
    $cgmapM :: forall (m :: * -> *).
    Monad m =>
    (forall d. Data d => d -> m d)
    -> DeclarationWarning' -> m DeclarationWarning'
    gmapQi :: forall u.
    Int -> (forall d. Data d => d -> u) -> DeclarationWarning' -> u
    $cgmapQi :: forall u.
    Int -> (forall d. Data d => d -> u) -> DeclarationWarning' -> u
    gmapQ :: forall u.
    (forall d. Data d => d -> u) -> DeclarationWarning' -> [u]
    $cgmapQ :: forall u.
    (forall d. Data d => d -> u) -> DeclarationWarning' -> [u]
    gmapQr :: forall r r'.
    (r' -> r -> r)
    -> r -> (forall d. Data d => d -> r') -> DeclarationWarning' -> r
    $cgmapQr :: forall r r'.
    (r' -> r -> r)
    -> r -> (forall d. Data d => d -> r') -> DeclarationWarning' -> r
    gmapQl :: forall r r'.
    (r -> r' -> r)
    -> r -> (forall d. Data d => d -> r') -> DeclarationWarning' -> r
    $cgmapQl :: forall r r'.
    (r -> r' -> r)
    -> r -> (forall d. Data d => d -> r') -> DeclarationWarning' -> r
    gmapT :: (forall b. Data b => b -> b)
    -> DeclarationWarning' -> DeclarationWarning'
    $cgmapT :: (forall b. Data b => b -> b)
    -> DeclarationWarning' -> DeclarationWarning'
    dataCast2 :: forall (t :: * -> * -> *) (c :: * -> *).
    Typeable t =>
    (forall d e. (Data d, Data e) => c (t d e))
    -> Maybe (c DeclarationWarning')
    $cdataCast2 :: forall (t :: * -> * -> *) (c :: * -> *).
    Typeable t =>
    (forall d e. (Data d, Data e) => c (t d e))
    -> Maybe (c DeclarationWarning')
    dataCast1 :: forall (t :: * -> *) (c :: * -> *).
    Typeable t =>
    (forall d. Data d => c (t d)) -> Maybe (c DeclarationWarning')
    $cdataCast1 :: forall (t :: * -> *) (c :: * -> *).
    Typeable t =>
    (forall d. Data d => c (t d)) -> Maybe (c DeclarationWarning')
    dataTypeOf :: DeclarationWarning' -> DataType
    $cdataTypeOf :: DeclarationWarning' -> DataType
    toConstr :: DeclarationWarning' -> Constr
    $ctoConstr :: DeclarationWarning' -> Constr
    gunfold :: forall (c :: * -> *).
    (forall b r. Data b => c (b -> r) -> c r)
    -> (forall r. r -> c r) -> Constr -> c DeclarationWarning'
    $cgunfold :: forall (c :: * -> *).
    (forall b r. Data b => c (b -> r) -> c r)
    -> (forall r. r -> c r) -> Constr -> c DeclarationWarning'
    gfoldl :: forall (c :: * -> *).
    (forall d b. Data d => c (d -> b) -> d -> c b)
    -> (forall g. g -> c g)
    -> DeclarationWarning'
    -> c DeclarationWarning'
    $cgfoldl :: forall (c :: * -> *).
    (forall d b. Data d => c (d -> b) -> d -> c b)
    -> (forall g. g -> c g)
    -> DeclarationWarning'
    -> c DeclarationWarning'
    Data, 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
    showList :: [DeclarationWarning'] -> ShowS
    $cshowList :: [DeclarationWarning'] -> ShowS
    show :: DeclarationWarning' -> String
    $cshow :: DeclarationWarning' -> String
    showsPrec :: Int -> DeclarationWarning' -> ShowS
    $cshowsPrec :: Int -> 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
    $cto :: forall x. Rep DeclarationWarning' x -> DeclarationWarning'
    $cfrom :: forall x. DeclarationWarning' -> Rep DeclarationWarning' x
    Generic)

    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_
      InvalidCatchallPragma{}           -> WarningName
    InvalidCatchallPragma_
      InvalidConstructor{}              -> WarningName
    InvalidConstructor_
      InvalidConstructorBlock{}         -> WarningName
    InvalidConstructorBlock_
      InvalidNoPositivityCheckPragma{}  -> WarningName
    InvalidNoPositivityCheckPragma_
      InvalidNoUniverseCheckPragma{}    -> WarningName
    InvalidNoUniverseCheckPragma_
      InvalidRecordDirective{}          -> WarningName
    InvalidRecordDirective_
      InvalidTerminationCheckPragma{}   -> WarningName
    InvalidTerminationCheckPragma_
      InvalidCoverageCheckPragma{}      -> WarningName
    InvalidCoverageCheckPragma_
      MissingDeclarations{}             -> WarningName
    MissingDeclarations_
      MissingDefinitions{}              -> WarningName
    MissingDefinitions_
      NotAllowedInMutual{}              -> WarningName
    NotAllowedInMutual_
      OpenPublicPrivate{}               -> WarningName
    OpenPublicPrivate_
      OpenPublicAbstract{}              -> WarningName
    OpenPublicAbstract_
      PolarityPragmasButNotPostulates{} -> WarningName
    PolarityPragmasButNotPostulates_
      PragmaNoTerminationCheck{}        -> WarningName
    PragmaNoTerminationCheck_
      PragmaCompiled{}                  -> WarningName
    PragmaCompiled_
      ShadowingInTelescope{}            -> WarningName
    ShadowingInTelescope_
      UnknownFixityInMixfixDecl{}       -> WarningName
    UnknownFixityInMixfixDecl_
      UnknownNamesInFixityDecl{}        -> WarningName
    UnknownNamesInFixityDecl_
      UnknownNamesInPolarityPragmas{}   -> WarningName
    UnknownNamesInPolarityPragmas_
      UselessAbstract{}                 -> WarningName
    UselessAbstract_
      UselessInstance{}                 -> WarningName
    UselessInstance_
      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
      InvalidCatchallPragma{}           -> Bool
    False
      InvalidConstructor{}              -> Bool
    False
      InvalidConstructorBlock{}         -> Bool
    False
      InvalidNoPositivityCheckPragma{}  -> Bool
    False
      InvalidNoUniverseCheckPragma{}    -> Bool
    False
      InvalidRecordDirective{}          -> Bool
    False
      InvalidTerminationCheckPragma{}   -> Bool
    False
      InvalidCoverageCheckPragma{}      -> Bool
    False
      MissingDeclarations{}             -> Bool
    True  -- not safe
      MissingDefinitions{}              -> Bool
    True  -- not safe
      NotAllowedInMutual{}              -> Bool
    False -- really safe?
      OpenPublicPrivate{}               -> Bool
    False
      OpenPublicAbstract{}              -> Bool
    False
      PolarityPragmasButNotPostulates{} -> Bool
    False
      PragmaNoTerminationCheck{}        -> Bool
    True  -- not safe
      PragmaCompiled{}                  -> Bool
    True  -- not safe
      ShadowingInTelescope{}            -> Bool
    False
      UnknownFixityInMixfixDecl{}       -> Bool
    False
      UnknownNamesInFixityDecl{}        -> Bool
    False
      UnknownNamesInPolarityPragmas{}   -> Bool
    False
      UselessAbstract{}                 -> Bool
    False
      UselessInstance{}                 -> Bool
    False
      UselessPrivate{}                  -> Bool
    False

    ------------------------------------------------------------------------
    -- 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 (InvalidName Name
    x)                      = Name -> Range
    forall a. HasRange a => a -> Range
    getRange Name
    x
      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 (DeclarationPanic String
    _)                 = Range
    forall a. Range' a
    noRange
      getRange (WrongContentBlock KindOfBlock
    _ Range
    r)              = Range
    r
      getRange (InvalidMeasureMutual Range
    r)             = Range
    r
      getRange (UnquoteDefRequiresSignature List1 Name
    x)      = List1 Name -> Range
    forall a. HasRange a => a -> Range
    getRange List1 Name
    x
      getRange (BadMacroDef NiceDeclaration
    d)                      = NiceDeclaration -> Range
    forall a. HasRange a => a -> Range
    getRange NiceDeclaration
    d

    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 (UnknownNamesInFixityDecl [Name]
    xs)        = [Name] -> Range
    forall a. HasRange a => a -> Range
    getRange [Name]
    xs
      getRange (UnknownFixityInMixfixDecl [Name]
    xs)       = [Name] -> Range
    forall a. HasRange a => a -> Range
    getRange [Name]
    xs
      getRange (UnknownNamesInPolarityPragmas [Name]
    xs)   = [Name] -> Range
    forall a. HasRange a => a -> Range
    getRange [Name]
    xs
      getRange (PolarityPragmasButNotPostulates [Name]
    xs) = [Name] -> Range
    forall a. HasRange a => a -> Range
    getRange [Name]
    xs
      getRange (MissingDeclarations [(Name, Range)]
    xs)             = [(Name, Range)] -> Range
    forall a. HasRange a => a -> Range
    getRange [(Name, Range)]
    xs
      getRange (MissingDefinitions [(Name, Range)]
    xs)              = [(Name, Range)] -> Range
    forall a. HasRange a => a -> Range
    getRange [(Name, Range)]
    xs
      getRange (UselessPrivate Range
    r)                   = Range
    r
      getRange (NotAllowedInMutual Range
    r String
    x)             = Range
    r
      getRange (UselessAbstract Range
    r)                  = Range
    r
      getRange (UselessInstance Range
    r)                  = Range
    r
      getRange (EmptyConstructor Range
    r)                 = Range
    r
      getRange (EmptyMutual Range
    r)                      = Range
    r
      getRange (EmptyAbstract Range
    r)                    = Range
    r
      getRange (EmptyPrivate Range
    r)                     = Range
    r
      getRange (EmptyInstance Range
    r)                    = Range
    r
      getRange (EmptyMacro Range
    r)                       = Range
    r
      getRange (EmptyPostulate Range
    r)                   = Range
    r
      getRange (EmptyGeneralize Range
    r)                  = Range
    r
      getRange (EmptyPrimitive Range
    r)                   = Range
    r
      getRange (EmptyField Range
    r)                       = Range
    r
      getRange (InvalidTerminationCheckPragma Range
    r)    = Range
    r
      getRange (InvalidCoverageCheckPragma Range
    r)       = Range
    r
      getRange (InvalidNoPositivityCheckPragma Range
    r)   = Range
    r
      getRange (InvalidCatchallPragma Range
    r)            = Range
    r
      getRange (InvalidConstructor Range
    r)               = Range
    r
      getRange (InvalidConstructorBlock Range
    r)          = Range
    r
      getRange (InvalidNoUniverseCheckPragma Range
    r)     = Range
    r
      getRange (InvalidRecordDirective Range
    r)           = Range
    r
      getRange (PragmaNoTerminationCheck Range
    r)         = Range
    r
      getRange (PragmaCompiled Range
    r)                   = Range
    r
      getRange (OpenPublicAbstract Range
    r)               = Range
    r
      getRange (OpenPublicPrivate Range
    r)                = Range
    r
      getRange (ShadowingInTelescope List1 (Name, List2 Range)
    ns)            = List1 (Name, List2 Range) -> Range
    forall a. HasRange a => a -> Range
    getRange List1 (Name, List2 Range)
    ns

    -- 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 (InvalidName 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
    "Invalid name:" [Doc] -> [Doc] -> [Doc]
    forall a. [a] -> [a] -> [a]
    ++ [Name -> Doc
    forall a. Pretty a => a -> Doc
    pretty Name
    x]
      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:"
        , NonEmpty Doc -> Doc
    forall (t :: * -> *). Foldable t => t Doc -> Doc
    vcat (NonEmpty Doc -> Doc) -> NonEmpty Doc -> Doc
    forall a b. (a -> b) -> a -> b
    $ (Name -> Doc) -> List1 Name -> NonEmpty Doc
    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 (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 keyword instance"
          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 -> [Name]
    forall a. NonEmpty a -> [a]
    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
    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 (DeclarationPanic String
    s) = String -> Doc
    text String
    s

    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 (UnknownNamesInFixityDecl [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 -> [Doc] -> [Doc]
    forall (t :: * -> *). Foldable t => Doc -> t Doc -> [Doc]
    punctuate Doc
    comma ((Name -> Doc) -> [Name] -> [Doc]
    forall a b. (a -> b) -> [a] -> [b]
    map Name -> Doc
    forall a. Pretty a => a -> Doc
    pretty [Name]
    xs)
      pretty (UnknownFixityInMixfixDecl [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 -> [Doc] -> [Doc]
    forall (t :: * -> *). Foldable t => Doc -> t Doc -> [Doc]
    punctuate Doc
    comma ((Name -> Doc) -> [Name] -> [Doc]
    forall a b. (a -> b) -> [a] -> [b]
    map Name -> Doc
    forall a. Pretty a => a -> Doc
    pretty [Name]
    xs)
      pretty (UnknownNamesInPolarityPragmas [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 -> [Doc] -> [Doc]
    forall (t :: * -> *). Foldable t => Doc -> t Doc -> [Doc]
    punctuate Doc
    comma  ((Name -> Doc) -> [Name] -> [Doc]
    forall a b. (a -> b) -> [a] -> [b]
    map Name -> Doc
    forall a. Pretty a => a -> Doc
    pretty [Name]
    xs)
      pretty (MissingDeclarations [(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 defined but not accompanied by a declaration:"
       [Doc] -> [Doc] -> [Doc]
    forall a. [a] -> [a] -> [a]
    ++ Doc -> [Doc] -> [Doc]
    forall (t :: * -> *). Foldable t => Doc -> t Doc -> [Doc]
    punctuate Doc
    comma (((Name, Range) -> Doc) -> [(Name, Range)] -> [Doc]
    forall a b. (a -> b) -> [a] -> [b]
    map (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) [(Name, Range)]
    xs)
      pretty (MissingDefinitions [(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 -> [Doc] -> [Doc]
    forall (t :: * -> *). Foldable t => Doc -> t Doc -> [Doc]
    punctuate Doc
    comma (((Name, Range) -> Doc) -> [(Name, Range)] -> [Doc]
    forall a b. (a -> b) -> [a] -> [b]
    map (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) [(Name, Range)]
    xs)
      pretty (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
    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"
      pretty (PolarityPragmasButNotPostulates [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 -> [Doc] -> [Doc]
    forall (t :: * -> *). Foldable t => Doc -> t Doc -> [Doc]
    punctuate Doc
    comma ((Name -> Doc) -> [Name] -> [Doc]
    forall a b. (a -> b) -> [a] -> [b]
    map Name -> Doc
    forall a. Pretty a => a -> Doc
    pretty [Name]
    xs)
      pretty (UselessPrivate 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
    "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."
      pretty (UselessAbstract 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
    "Using abstract here has no effect. Abstract applies to only definitions like data definitions, record type definitions and function clauses."
      pretty (UselessInstance 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
    "Using instance here has no effect. Instance applies only to declarations that introduce new identifiers into the module, like type signatures and axioms."
      pretty (EmptyMutual    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
    "Empty mutual block."
      pretty 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."
      pretty (EmptyAbstract  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
    "Empty abstract block."
      pretty (EmptyPrivate   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
    "Empty private block."
      pretty (EmptyInstance  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
    "Empty instance block."
      pretty (EmptyMacro     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
    "Empty macro block."
      pretty (EmptyPostulate 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
    "Empty postulate block."
      pretty (EmptyGeneralize 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
    "Empty variable block."
      pretty (EmptyPrimitive 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
    "Empty primitive block."
      pretty (EmptyField 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
    "Empty field block."
      pretty InvalidRecordDirective{} = [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
    "Record directives can only be used inside record definitions and before field declarations."
      pretty (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)."
      pretty InvalidConstructor{} = [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
    "`constructor' blocks may only contain type signatures for constructors."
      pretty 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 `constructor' blocks outside of `interleaved mutual' blocks."
      pretty (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)."
      pretty (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)."
      pretty (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."
      pretty (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."
      pretty (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 #-}."
      pretty (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."
      pretty (OpenPublicAbstract 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
    "public does not have any effect in an abstract block."
      pretty (OpenPublicPrivate 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
    "public does not have any effect in a private block."
      pretty (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 -> NonEmpty Doc -> [Doc]
    forall (t :: * -> *). Foldable t => Doc -> t Doc -> [Doc]
    punctuate Doc
    comma (((Name, List2 Range) -> Doc)
    -> List1 (Name, List2 Range) -> NonEmpty Doc
    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)

    instance NFData DeclarationWarning
    instance NFData DeclarationWarning'