-- | 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
forall a.
(Int -> a -> ShowS) -> (a -> String) -> ([a] -> ShowS) -> Show a
showList :: [RecordFieldWarning] -> ShowS
$cshowList :: [RecordFieldWarning] -> ShowS
show :: RecordFieldWarning -> String
$cshow :: RecordFieldWarning -> String
showsPrec :: Int -> RecordFieldWarning -> ShowS
$cshowsPrec :: Int -> RecordFieldWarning -> ShowS
Show, 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
$cto :: forall x. Rep RecordFieldWarning x -> RecordFieldWarning
$cfrom :: forall x. RecordFieldWarning -> Rep RecordFieldWarning x
Generic)