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.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
  | 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
  | UnfoldingOutsideOpaque Range
    -- ^ An unfolding declaration was not the first declaration
    -- contained in an opaque block.
  | OpaqueInMutual Range
      -- ^ @opaque@ block nested in a @mutual@ block. This can never
      -- happen, even with reordering.
  | DisallowedInterleavedMutual Range 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

------------------------------------------------------------------------
-- 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 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.
  | 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.
  | 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.
  | 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 [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 (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)

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_
  HiddenGeneralize{}                -> WarningName
HiddenGeneralize_
  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_
  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_
  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
  HiddenGeneralize{}                -> 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
  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
  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
    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
  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 (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
  getRange (UnfoldingOutsideOpaque Range
r)           = Range
r
  getRange (OpaqueInMutual Range
r)                   = Range
r
  getRange (DisallowedInterleavedMutual Range
r String
_ List1 Name
_)  = Range
r

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

-- 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:"
    , 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 (DeclarationPanic String
s) = String -> Doc
forall a. String -> Doc a
text String
s
  pretty (UnfoldingOutsideOpaque 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
$
    String
"Unfolding declarations can only appear as the first declaration immediately contained in an opaque block."
  pretty (OpaqueInMutual 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
"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 Range
_ 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 [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)

    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)

    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)

    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)

    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)

    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 [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)

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

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

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

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

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

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

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

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

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

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

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

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

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

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

    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)."

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

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

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

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

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

    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 NFData DeclarationWarning
instance NFData DeclarationWarning'