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

Agda.TypeChecking.Monad.Base.Warning

Description

Types related to warnings raised by Agda.

Documentation

data RecordFieldWarning Source #

Constructors

DuplicateFields (List1 (Name, Range))

Each redundant field comes with a range of associated dead code.

TooManyFields QName [Name] (List1 (Name, Range))

Record type, fields not supplied by user, non-fields but supplied. The redundant fields come with a range of associated dead code.

Instances

Instances details
EmbPrj RecordFieldWarning Source # 
Instance details

Defined in Agda.TypeChecking.Serialise.Instances.Errors

Generic RecordFieldWarning Source # 
Instance details

Defined in Agda.TypeChecking.Monad.Base.Warning

Associated Types

type Rep RecordFieldWarning 
Instance details

Defined in Agda.TypeChecking.Monad.Base.Warning

type Rep RecordFieldWarning = D1 ('MetaData "RecordFieldWarning" "Agda.TypeChecking.Monad.Base.Warning" "Agda-2.8.0-ES80446w7YfI1YRCZGcXTm" 'False) (C1 ('MetaCons "DuplicateFields" 'PrefixI 'False) (S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 (List1 (Name, Range)))) :+: C1 ('MetaCons "TooManyFields" 'PrefixI 'False) (S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 QName) :*: (S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 [Name]) :*: S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 (List1 (Name, Range))))))
Show RecordFieldWarning Source # 
Instance details

Defined in Agda.TypeChecking.Monad.Base.Warning

NFData RecordFieldWarning 
Instance details

Defined in Agda.TypeChecking.Monad.Base

Methods

rnf :: RecordFieldWarning -> ()

type Rep RecordFieldWarning Source # 
Instance details

Defined in Agda.TypeChecking.Monad.Base.Warning

type Rep RecordFieldWarning = D1 ('MetaData "RecordFieldWarning" "Agda.TypeChecking.Monad.Base.Warning" "Agda-2.8.0-ES80446w7YfI1YRCZGcXTm" 'False) (C1 ('MetaCons "DuplicateFields" 'PrefixI 'False) (S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 (List1 (Name, Range)))) :+: C1 ('MetaCons "TooManyFields" 'PrefixI 'False) (S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 QName) :*: (S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 [Name]) :*: S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 (List1 (Name, Range))))))

data UselessPublicReason Source #

Instances

Instances details
EmbPrj UselessPublicReason Source # 
Instance details

Defined in Agda.TypeChecking.Serialise.Instances.Errors

Bounded UselessPublicReason Source # 
Instance details

Defined in Agda.TypeChecking.Monad.Base.Warning

Enum UselessPublicReason Source # 
Instance details

Defined in Agda.TypeChecking.Monad.Base.Warning

Generic UselessPublicReason Source # 
Instance details

Defined in Agda.TypeChecking.Monad.Base.Warning

Associated Types

type Rep UselessPublicReason 
Instance details

Defined in Agda.TypeChecking.Monad.Base.Warning

type Rep UselessPublicReason = D1 ('MetaData "UselessPublicReason" "Agda.TypeChecking.Monad.Base.Warning" "Agda-2.8.0-ES80446w7YfI1YRCZGcXTm" 'False) ((C1 ('MetaCons "UselessPublicPreamble" 'PrefixI 'False) (U1 :: Type -> Type) :+: C1 ('MetaCons "UselessPublicLet" 'PrefixI 'False) (U1 :: Type -> Type)) :+: (C1 ('MetaCons "UselessPublicNoOpen" 'PrefixI 'False) (U1 :: Type -> Type) :+: C1 ('MetaCons "UselessPublicAnonymousModule" 'PrefixI 'False) (U1 :: Type -> Type)))
Show UselessPublicReason Source # 
Instance details

Defined in Agda.TypeChecking.Monad.Base.Warning

NFData UselessPublicReason Source # 
Instance details

Defined in Agda.TypeChecking.Monad.Base.Warning

Methods

rnf :: UselessPublicReason -> ()

type Rep UselessPublicReason Source # 
Instance details

Defined in Agda.TypeChecking.Monad.Base.Warning

type Rep UselessPublicReason = D1 ('MetaData "UselessPublicReason" "Agda.TypeChecking.Monad.Base.Warning" "Agda-2.8.0-ES80446w7YfI1YRCZGcXTm" 'False) ((C1 ('MetaCons "UselessPublicPreamble" 'PrefixI 'False) (U1 :: Type -> Type) :+: C1 ('MetaCons "UselessPublicLet" 'PrefixI 'False) (U1 :: Type -> Type)) :+: (C1 ('MetaCons "UselessPublicNoOpen" 'PrefixI 'False) (U1 :: Type -> Type) :+: C1 ('MetaCons "UselessPublicAnonymousModule" 'PrefixI 'False) (U1 :: Type -> Type)))