Agda-2.6.2.1.20220327: A dependently typed functional programming language and proof assistant
Safe HaskellSafe-Inferred
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 of mutual block.

UnquoteDefRequiresSignature (List1 Name) 
BadMacroDef NiceDeclaration 

Instances

Instances details
HasRange DeclarationException' Source # 
Instance details

Defined in Agda.Syntax.Concrete.Definitions.Errors

Pretty DeclarationException' Source # 
Instance details

Defined in Agda.Syntax.Concrete.Definitions.Errors

Data DeclarationException' Source # 
Instance details

Defined in Agda.Syntax.Concrete.Definitions.Errors

Methods

gfoldl :: (forall d b. Data d => c (d -> b) -> d -> c b) -> (forall g. g -> c g) -> DeclarationException' -> c DeclarationException' #

gunfold :: (forall b r. Data b => c (b -> r) -> c r) -> (forall r. r -> c r) -> Constr -> c DeclarationException' #

toConstr :: DeclarationException' -> Constr #

dataTypeOf :: DeclarationException' -> DataType #

dataCast1 :: Typeable t => (forall d. Data d => c (t d)) -> Maybe (c DeclarationException') #

dataCast2 :: Typeable t => (forall d e. (Data d, Data e) => c (t d e)) -> Maybe (c DeclarationException') #

gmapT :: (forall b. Data b => b -> b) -> DeclarationException' -> DeclarationException' #

gmapQl :: (r -> r' -> r) -> r -> (forall d. Data d => d -> r') -> DeclarationException' -> r #

gmapQr :: forall r r'. (r' -> r -> r) -> r -> (forall d. Data d => d -> r') -> DeclarationException' -> r #

gmapQ :: (forall d. Data d => d -> u) -> DeclarationException' -> [u] #

gmapQi :: Int -> (forall d. Data d => d -> u) -> DeclarationException' -> u #

gmapM :: Monad m => (forall d. Data d => d -> m d) -> DeclarationException' -> m DeclarationException' #

gmapMp :: MonadPlus m => (forall d. Data d => d -> m d) -> DeclarationException' -> m DeclarationException' #

gmapMo :: MonadPlus m => (forall d. Data d => d -> m d) -> DeclarationException' -> m DeclarationException' #

Show DeclarationException' Source # 
Instance details

Defined in Agda.Syntax.Concrete.Definitions.Errors

data DeclarationWarning Source #

Instances

Instances details
HasRange DeclarationWarning Source # 
Instance details

Defined in Agda.Syntax.Concrete.Definitions.Errors

EmbPrj DeclarationWarning Source # 
Instance details

Defined in Agda.TypeChecking.Serialise.Instances.Errors

Pretty DeclarationWarning Source # 
Instance details

Defined in Agda.Syntax.Concrete.Definitions.Errors

Generic DeclarationWarning Source # 
Instance details

Defined in Agda.Syntax.Concrete.Definitions.Errors

Associated Types

type Rep DeclarationWarning :: Type -> Type #

Show DeclarationWarning Source # 
Instance details

Defined in Agda.Syntax.Concrete.Definitions.Errors

NFData DeclarationWarning Source # 
Instance details

Defined in Agda.Syntax.Concrete.Definitions.Errors

Methods

rnf :: DeclarationWarning -> () #

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

Instances

Instances details
HasRange DeclarationWarning' Source # 
Instance details

Defined in Agda.Syntax.Concrete.Definitions.Errors

EmbPrj DeclarationWarning' Source # 
Instance details

Defined in Agda.TypeChecking.Serialise.Instances.Errors

Pretty DeclarationWarning' Source # 
Instance details

Defined in Agda.Syntax.Concrete.Definitions.Errors

Data DeclarationWarning' Source # 
Instance details

Defined in Agda.Syntax.Concrete.Definitions.Errors

Methods

gfoldl :: (forall d b. Data d => c (d -> b) -> d -> c b) -> (forall g. g -> c g) -> DeclarationWarning' -> c DeclarationWarning' #

gunfold :: (forall b r. Data b => c (b -> r) -> c r) -> (forall r. r -> c r) -> Constr -> c DeclarationWarning' #

toConstr :: DeclarationWarning' -> Constr #

dataTypeOf :: DeclarationWarning' -> DataType #

dataCast1 :: Typeable t => (forall d. Data d => c (t d)) -> Maybe (c DeclarationWarning') #

dataCast2 :: Typeable t => (forall d e. (Data d, Data e) => c (t d e)) -> Maybe (c DeclarationWarning') #

gmapT :: (forall b. Data b => b -> b) -> DeclarationWarning' -> DeclarationWarning' #

gmapQl :: (r -> r' -> r) -> r -> (forall d. Data d => d -> r') -> DeclarationWarning' -> r #

gmapQr :: forall r r'. (r' -> r -> r) -> r -> (forall d. Data d => d -> r') -> DeclarationWarning' -> r #

gmapQ :: (forall d. Data d => d -> u) -> DeclarationWarning' -> [u] #

gmapQi :: Int -> (forall d. Data d => d -> u) -> DeclarationWarning' -> u #

gmapM :: Monad m => (forall d. Data d => d -> m d) -> DeclarationWarning' -> m DeclarationWarning' #

gmapMp :: MonadPlus m => (forall d. Data d => d -> m d) -> DeclarationWarning' -> m DeclarationWarning' #

gmapMo :: MonadPlus m => (forall d. Data d => d -> m d) -> DeclarationWarning' -> m DeclarationWarning' #

Generic DeclarationWarning' Source # 
Instance details

Defined in Agda.Syntax.Concrete.Definitions.Errors

Associated Types

type Rep DeclarationWarning' :: Type -> Type #

Show DeclarationWarning' Source # 
Instance details

Defined in Agda.Syntax.Concrete.Definitions.Errors

NFData DeclarationWarning' Source # 
Instance details

Defined in Agda.Syntax.Concrete.Definitions.Errors

Methods

rnf :: DeclarationWarning' -> () #

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.2.1.20220327-inplace" 'False) (((((C1 ('MetaCons "EmptyAbstract" 'PrefixI 'False) (S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 Range)) :+: C1 ('MetaCons "EmptyConstructor" 'PrefixI 'False) (S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 Range))) :+: (C1 ('MetaCons "EmptyField" 'PrefixI 'False) (S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 Range)) :+: C1 ('MetaCons "EmptyGeneralize" 'PrefixI 'False) (S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 Range)))) :+: ((C1 ('MetaCons "EmptyInstance" 'PrefixI 'False) (S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 Range)) :+: C1 ('MetaCons "EmptyMacro" 'PrefixI 'False) (S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 Range))) :+: (C1 ('MetaCons "EmptyMutual" 'PrefixI 'False) (S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 Range)) :+: C1 ('MetaCons "EmptyPostulate" 'PrefixI 'False) (S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 Range))))) :+: (((C1 ('MetaCons "EmptyPrivate" 'PrefixI 'False) (S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 Range)) :+: C1 ('MetaCons "EmptyPrimitive" '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 "InvalidRecordDirective" '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 Range))) :+: (C1 ('MetaCons "OpenPublicAbstract" 'PrefixI 'False) (S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 Range)) :+: 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 "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 Range)) :+: (C1 ('MetaCons "UselessInstance" 'PrefixI 'False) (S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 Range)) :+: C1 ('MetaCons "UselessPrivate" 'PrefixI 'False) (S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 Range))))))))

unsafeDeclarationWarning :: DeclarationWarning -> Bool Source #

Nicifier warnings turned into errors in --safe mode.