Agda-2.6.20240714: A dependently typed functional programming language and proof assistant
Safe HaskellNone
LanguageHaskell2010

Agda.Syntax.Concrete.Definitions.Errors

Synopsis

Documentation

data DeclarationException Source #

Exception with internal source code callstack

data DeclarationException' Source #

The exception type.

Constructors

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 the one of the offending pragma or the mutual block.

UnquoteDefRequiresSignature (List1 Name) 
BadMacroDef NiceDeclaration 
UnfoldingOutsideOpaque KwRange

An unfolding declaration was not the first declaration contained in an opaque block.

OpaqueInMutual KwRange

opaque block nested in a mutual block. This can never happen, even with reordering. The KwRange is the one of the opaque keyword.

DisallowedInterleavedMutual KwRange String (List1 Name)

A declaration that breaks an implicit mutual block (named by the String argument) was present while the given lone type signatures were still without their definitions.

data DeclarationWarning Source #

Instances

Instances details
Pretty DeclarationWarning Source # 
Instance details

Defined in Agda.Syntax.Concrete.Definitions.Errors

HasRange DeclarationWarning Source # 
Instance details

Defined in Agda.Syntax.Concrete.Definitions.Errors

EmbPrj DeclarationWarning Source # 
Instance details

Defined in Agda.TypeChecking.Serialise.Instances.Errors

NFData DeclarationWarning Source # 
Instance details

Defined in Agda.Syntax.Concrete.Definitions.Errors

Methods

rnf :: DeclarationWarning -> ()

Generic DeclarationWarning Source # 
Instance details

Defined in Agda.Syntax.Concrete.Definitions.Errors

Associated Types

type Rep DeclarationWarning 
Instance details

Defined in Agda.Syntax.Concrete.Definitions.Errors

type Rep DeclarationWarning = D1 ('MetaData "DeclarationWarning" "Agda.Syntax.Concrete.Definitions.Errors" "Agda-2.6.20240714-inplace" 'False) (C1 ('MetaCons "DeclarationWarning" 'PrefixI 'True) (S1 ('MetaSel ('Just "dwLocation") 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 CallStack) :*: S1 ('MetaSel ('Just "dwWarning") 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 DeclarationWarning')))
Show DeclarationWarning Source # 
Instance details

Defined in Agda.Syntax.Concrete.Definitions.Errors

Methods

showsPrec :: Int -> DeclarationWarning -> ShowS

show :: DeclarationWarning -> String

showList :: [DeclarationWarning] -> ShowS

type Rep DeclarationWarning Source # 
Instance details

Defined in Agda.Syntax.Concrete.Definitions.Errors

type Rep DeclarationWarning = D1 ('MetaData "DeclarationWarning" "Agda.Syntax.Concrete.Definitions.Errors" "Agda-2.6.20240714-inplace" 'False) (C1 ('MetaCons "DeclarationWarning" 'PrefixI 'True) (S1 ('MetaSel ('Just "dwLocation") 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 CallStack) :*: S1 ('MetaSel ('Just "dwWarning") 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 DeclarationWarning')))

data DeclarationWarning' Source #

Non-fatal errors encountered in the Nicifier.

Constructors

EmptyAbstract KwRange

Empty abstract block.

EmptyConstructor KwRange

Empty data _ where block.

EmptyField KwRange

Empty field block.

EmptyGeneralize KwRange

Empty variable block.

EmptyInstance KwRange

Empty instance block

EmptyMacro KwRange

Empty macro block.

EmptyMutual KwRange

Empty mutual block.

EmptyPostulate KwRange

Empty postulate block.

EmptyPrivate KwRange

Empty private block.

EmptyPrimitive KwRange

Empty primitive block.

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.

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 KwRange

private has no effect on open public. (But the user might think so.) KwRange is the range of the public keyword.

OpenPublicAbstract KwRange

abstract has no effect on open public. (But the user might think so.) KwRange is the range of the public keyword.

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 KwRange

abstract block with nothing that can (newly) be made abstract.

UselessInstance KwRange

instance block with nothing that can (newly) become an instance.

UselessMacro KwRange

macro block with nothing that can (newly) be made macro.

UselessPrivate KwRange

private block with nothing that can (newly) be made private.

Instances

Instances details
Pretty DeclarationWarning' Source # 
Instance details

Defined in Agda.Syntax.Concrete.Definitions.Errors

HasRange DeclarationWarning' Source # 
Instance details

Defined in Agda.Syntax.Concrete.Definitions.Errors

EmbPrj DeclarationWarning' Source # 
Instance details

Defined in Agda.TypeChecking.Serialise.Instances.Errors

NFData DeclarationWarning' Source # 
Instance details

Defined in Agda.Syntax.Concrete.Definitions.Errors

Methods

rnf :: DeclarationWarning' -> ()

Generic DeclarationWarning' Source # 
Instance details

Defined in Agda.Syntax.Concrete.Definitions.Errors

Associated Types

type Rep DeclarationWarning' 
Instance details

Defined in Agda.Syntax.Concrete.Definitions.Errors

type Rep DeclarationWarning' = D1 ('MetaData "DeclarationWarning'" "Agda.Syntax.Concrete.Definitions.Errors" "Agda-2.6.20240714-inplace" 'False) (((((C1 ('MetaCons "EmptyAbstract" 'PrefixI 'False) (S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 KwRange)) :+: C1 ('MetaCons "EmptyConstructor" 'PrefixI 'False) (S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 KwRange))) :+: (C1 ('MetaCons "EmptyField" 'PrefixI 'False) (S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 KwRange)) :+: (C1 ('MetaCons "EmptyGeneralize" 'PrefixI 'False) (S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 KwRange)) :+: C1 ('MetaCons "EmptyInstance" 'PrefixI 'False) (S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 KwRange))))) :+: ((C1 ('MetaCons "EmptyMacro" 'PrefixI 'False) (S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 KwRange)) :+: C1 ('MetaCons "EmptyMutual" 'PrefixI 'False) (S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 KwRange))) :+: (C1 ('MetaCons "EmptyPostulate" 'PrefixI 'False) (S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 KwRange)) :+: (C1 ('MetaCons "EmptyPrivate" 'PrefixI 'False) (S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 KwRange)) :+: C1 ('MetaCons "EmptyPrimitive" 'PrefixI 'False) (S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 KwRange)))))) :+: (((C1 ('MetaCons "HiddenGeneralize" 'PrefixI 'False) (S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 Range)) :+: C1 ('MetaCons "InvalidCatchallPragma" 'PrefixI 'False) (S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 Range))) :+: (C1 ('MetaCons "InvalidConstructor" 'PrefixI 'False) (S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 Range)) :+: (C1 ('MetaCons "InvalidConstructorBlock" 'PrefixI 'False) (S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 Range)) :+: C1 ('MetaCons "InvalidCoverageCheckPragma" 'PrefixI 'False) (S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 Range))))) :+: ((C1 ('MetaCons "InvalidNoPositivityCheckPragma" 'PrefixI 'False) (S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 Range)) :+: (C1 ('MetaCons "InvalidNoUniverseCheckPragma" 'PrefixI 'False) (S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 Range)) :+: C1 ('MetaCons "InvalidTerminationCheckPragma" 'PrefixI 'False) (S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 Range)))) :+: (C1 ('MetaCons "MissingDeclarations" 'PrefixI 'False) (S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 [(Name, Range)])) :+: (C1 ('MetaCons "MissingDefinitions" 'PrefixI 'False) (S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 [(Name, Range)])) :+: C1 ('MetaCons "NotAllowedInMutual" 'PrefixI 'False) (S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 Range) :*: S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 String))))))) :+: ((((C1 ('MetaCons "OpenPublicPrivate" 'PrefixI 'False) (S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 KwRange)) :+: C1 ('MetaCons "OpenPublicAbstract" 'PrefixI 'False) (S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 KwRange))) :+: (C1 ('MetaCons "PolarityPragmasButNotPostulates" 'PrefixI 'False) (S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 [Name])) :+: (C1 ('MetaCons "PragmaNoTerminationCheck" 'PrefixI 'False) (S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 Range)) :+: C1 ('MetaCons "PragmaCompiled" 'PrefixI 'False) (S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 Range))))) :+: ((C1 ('MetaCons "SafeFlagEta" 'PrefixI 'False) (S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 Range)) :+: C1 ('MetaCons "SafeFlagInjective" 'PrefixI 'False) (S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 Range))) :+: (C1 ('MetaCons "SafeFlagNoCoverageCheck" 'PrefixI 'False) (S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 Range)) :+: (C1 ('MetaCons "SafeFlagNoPositivityCheck" 'PrefixI 'False) (S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 Range)) :+: C1 ('MetaCons "SafeFlagNoUniverseCheck" 'PrefixI 'False) (S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 Range)))))) :+: (((C1 ('MetaCons "SafeFlagNonTerminating" 'PrefixI 'False) (S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 Range)) :+: C1 ('MetaCons "SafeFlagPolarity" 'PrefixI 'False) (S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 Range))) :+: (C1 ('MetaCons "SafeFlagTerminating" 'PrefixI 'False) (S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 Range)) :+: (C1 ('MetaCons "ShadowingInTelescope" 'PrefixI 'False) (S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 (List1 (Name, List2 Range)))) :+: C1 ('MetaCons "UnknownFixityInMixfixDecl" 'PrefixI 'False) (S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 [Name]))))) :+: ((C1 ('MetaCons "UnknownNamesInFixityDecl" 'PrefixI 'False) (S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 [Name])) :+: (C1 ('MetaCons "UnknownNamesInPolarityPragmas" 'PrefixI 'False) (S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 [Name])) :+: C1 ('MetaCons "UselessAbstract" 'PrefixI 'False) (S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 KwRange)))) :+: (C1 ('MetaCons "UselessInstance" 'PrefixI 'False) (S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 KwRange)) :+: (C1 ('MetaCons "UselessMacro" 'PrefixI 'False) (S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 KwRange)) :+: C1 ('MetaCons "UselessPrivate" 'PrefixI 'False) (S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 KwRange))))))))
Show DeclarationWarning' Source # 
Instance details

Defined in Agda.Syntax.Concrete.Definitions.Errors

Methods

showsPrec :: Int -> DeclarationWarning' -> ShowS

show :: DeclarationWarning' -> String

showList :: [DeclarationWarning'] -> ShowS

type Rep DeclarationWarning' Source # 
Instance details

Defined in Agda.Syntax.Concrete.Definitions.Errors

type Rep DeclarationWarning' = D1 ('MetaData "DeclarationWarning'" "Agda.Syntax.Concrete.Definitions.Errors" "Agda-2.6.20240714-inplace" 'False) (((((C1 ('MetaCons "EmptyAbstract" 'PrefixI 'False) (S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 KwRange)) :+: C1 ('MetaCons "EmptyConstructor" 'PrefixI 'False) (S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 KwRange))) :+: (C1 ('MetaCons "EmptyField" 'PrefixI 'False) (S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 KwRange)) :+: (C1 ('MetaCons "EmptyGeneralize" 'PrefixI 'False) (S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 KwRange)) :+: C1 ('MetaCons "EmptyInstance" 'PrefixI 'False) (S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 KwRange))))) :+: ((C1 ('MetaCons "EmptyMacro" 'PrefixI 'False) (S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 KwRange)) :+: C1 ('MetaCons "EmptyMutual" 'PrefixI 'False) (S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 KwRange))) :+: (C1 ('MetaCons "EmptyPostulate" 'PrefixI 'False) (S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 KwRange)) :+: (C1 ('MetaCons "EmptyPrivate" 'PrefixI 'False) (S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 KwRange)) :+: C1 ('MetaCons "EmptyPrimitive" 'PrefixI 'False) (S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 KwRange)))))) :+: (((C1 ('MetaCons "HiddenGeneralize" 'PrefixI 'False) (S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 Range)) :+: C1 ('MetaCons "InvalidCatchallPragma" 'PrefixI 'False) (S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 Range))) :+: (C1 ('MetaCons "InvalidConstructor" 'PrefixI 'False) (S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 Range)) :+: (C1 ('MetaCons "InvalidConstructorBlock" 'PrefixI 'False) (S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 Range)) :+: C1 ('MetaCons "InvalidCoverageCheckPragma" 'PrefixI 'False) (S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 Range))))) :+: ((C1 ('MetaCons "InvalidNoPositivityCheckPragma" 'PrefixI 'False) (S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 Range)) :+: (C1 ('MetaCons "InvalidNoUniverseCheckPragma" 'PrefixI 'False) (S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 Range)) :+: C1 ('MetaCons "InvalidTerminationCheckPragma" 'PrefixI 'False) (S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 Range)))) :+: (C1 ('MetaCons "MissingDeclarations" 'PrefixI 'False) (S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 [(Name, Range)])) :+: (C1 ('MetaCons "MissingDefinitions" 'PrefixI 'False) (S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 [(Name, Range)])) :+: C1 ('MetaCons "NotAllowedInMutual" 'PrefixI 'False) (S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 Range) :*: S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 String))))))) :+: ((((C1 ('MetaCons "OpenPublicPrivate" 'PrefixI 'False) (S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 KwRange)) :+: C1 ('MetaCons "OpenPublicAbstract" 'PrefixI 'False) (S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 KwRange))) :+: (C1 ('MetaCons "PolarityPragmasButNotPostulates" 'PrefixI 'False) (S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 [Name])) :+: (C1 ('MetaCons "PragmaNoTerminationCheck" 'PrefixI 'False) (S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 Range)) :+: C1 ('MetaCons "PragmaCompiled" 'PrefixI 'False) (S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 Range))))) :+: ((C1 ('MetaCons "SafeFlagEta" 'PrefixI 'False) (S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 Range)) :+: C1 ('MetaCons "SafeFlagInjective" 'PrefixI 'False) (S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 Range))) :+: (C1 ('MetaCons "SafeFlagNoCoverageCheck" 'PrefixI 'False) (S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 Range)) :+: (C1 ('MetaCons "SafeFlagNoPositivityCheck" 'PrefixI 'False) (S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 Range)) :+: C1 ('MetaCons "SafeFlagNoUniverseCheck" 'PrefixI 'False) (S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 Range)))))) :+: (((C1 ('MetaCons "SafeFlagNonTerminating" 'PrefixI 'False) (S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 Range)) :+: C1 ('MetaCons "SafeFlagPolarity" 'PrefixI 'False) (S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 Range))) :+: (C1 ('MetaCons "SafeFlagTerminating" 'PrefixI 'False) (S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 Range)) :+: (C1 ('MetaCons "ShadowingInTelescope" 'PrefixI 'False) (S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 (List1 (Name, List2 Range)))) :+: C1 ('MetaCons "UnknownFixityInMixfixDecl" 'PrefixI 'False) (S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 [Name]))))) :+: ((C1 ('MetaCons "UnknownNamesInFixityDecl" 'PrefixI 'False) (S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 [Name])) :+: (C1 ('MetaCons "UnknownNamesInPolarityPragmas" 'PrefixI 'False) (S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 [Name])) :+: C1 ('MetaCons "UselessAbstract" 'PrefixI 'False) (S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 KwRange)))) :+: (C1 ('MetaCons "UselessInstance" 'PrefixI 'False) (S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 KwRange)) :+: (C1 ('MetaCons "UselessMacro" 'PrefixI 'False) (S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 KwRange)) :+: C1 ('MetaCons "UselessPrivate" 'PrefixI 'False) (S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 KwRange))))))))

unsafeDeclarationWarning :: DeclarationWarning -> Bool Source #

Nicifier warnings turned into errors in --safe mode.

unsafePragma :: CMaybe DeclarationWarning' m => Pragma -> m Source #

Pragmas not allowed in --safe mode produce an unsafeDeclarationWarning.