-- | Types related to warnings raised by Agda.

module Agda.TypeChecking.Monad.Base.Warning where

import           GHC.Generics               (Generic)

import           Agda.Syntax.Abstract.Name
import           Agda.Syntax.Position       (Range)
import qualified Agda.Syntax.Concrete.Name  as C

data RecordFieldWarning
  = DuplicateFields [(C.Name, Range)]
      -- ^ Each redundant field comes with a range of associated dead code.
  | TooManyFields QName [C.Name] [(C.Name, Range)]
      -- ^ Record type, fields not supplied by user, non-fields but supplied.
      --   The redundant fields come with a range of associated dead code.
  deriving (Int -> RecordFieldWarning -> ShowS
[RecordFieldWarning] -> ShowS
RecordFieldWarning -> String
(Int -> RecordFieldWarning -> ShowS)
-> (RecordFieldWarning -> String)
-> ([RecordFieldWarning] -> ShowS)
-> Show RecordFieldWarning
forall a.
(Int -> a -> ShowS) -> (a -> String) -> ([a] -> ShowS) -> Show a
$cshowsPrec :: Int -> RecordFieldWarning -> ShowS
showsPrec :: Int -> RecordFieldWarning -> ShowS
$cshow :: RecordFieldWarning -> String
show :: RecordFieldWarning -> String
$cshowList :: [RecordFieldWarning] -> ShowS
showList :: [RecordFieldWarning] -> ShowS
Show, (forall x. RecordFieldWarning -> Rep RecordFieldWarning x)
-> (forall x. Rep RecordFieldWarning x -> RecordFieldWarning)
-> Generic RecordFieldWarning
forall x. Rep RecordFieldWarning x -> RecordFieldWarning
forall x. RecordFieldWarning -> Rep RecordFieldWarning x
forall a.
(forall x. a -> Rep a x) -> (forall x. Rep a x -> a) -> Generic a
$cfrom :: forall x. RecordFieldWarning -> Rep RecordFieldWarning x
from :: forall x. RecordFieldWarning -> Rep RecordFieldWarning x
$cto :: forall x. Rep RecordFieldWarning x -> RecordFieldWarning
to :: forall x. Rep RecordFieldWarning x -> RecordFieldWarning
Generic)