Agda.TypeChecking.Monad.Base.Warning

Types related to warnings raised by Agda.

Documentation

data RecordFieldWarning

Constructors

DuplicateFields [(Name, Range)]

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

TooManyFields QName [Name] [(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

EmbPrj RecordFieldWarning

Defined in Agda.TypeChecking.Serialise.Instances.Errors

Methods

icode :: RecordFieldWarning -> S Int32

icod_ :: RecordFieldWarning -> S Int32

value :: Int32 -> R RecordFieldWarning

Generic RecordFieldWarning

Defined in Agda.TypeChecking.Monad.Base.Warning

Associated Types

type Rep RecordFieldWarning :: Type -> Type

Methods

from :: RecordFieldWarning -> Rep RecordFieldWarning x

to :: Rep RecordFieldWarning x -> RecordFieldWarning

Show RecordFieldWarning

Defined in Agda.TypeChecking.Monad.Base.Warning

Methods

showsPrec :: Int -> RecordFieldWarning -> ShowS

show :: RecordFieldWarning -> String

showList :: [RecordFieldWarning] -> ShowS

NFData RecordFieldWarning

Defined in Agda.TypeChecking.Monad.Base

Methods

rnf :: RecordFieldWarning -> ()

type Rep RecordFieldWarning

Defined in Agda.TypeChecking.Monad.Base.Warning

type Rep RecordFieldWarning = D1 ('MetaData "RecordFieldWarning" "Agda.TypeChecking.Monad.Base.Warning" "Agda-2.6.3.20230914-inplace" 'False) (C1 ('MetaCons "DuplicateFields" 'PrefixI 'False) (S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 [(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 [(Name, Range)]))))