ModuleAgda-2.8.0.2Haskell2010

Agda.TypeChecking.Warnings

Synopsis

classclass (MonadPretty m, MonadError TCErr m) => MonadWarning (m :: Type -> Type) where

addWarning :: Bool -> TCWarning -> m ()
Store a warning and generate highlighting from it.

Instances6MonadWarning

MonadWarning TCMDefined in Agda-2.8.0.2 · Agda.TypeChecking.Warnings
PureTCM m => MonadWarning (PureConversionT m)Defined in Agda-2.8.0.2 · Agda.TypeChecking.Conversion.Pure
MonadWarning m => MonadWarning (MaybeT m)Defined in Agda-2.8.0.2 · Agda.TypeChecking.Warnings
MonadWarning m => MonadWarning (ReaderT r m)Defined in Agda-2.8.0.2 · Agda.TypeChecking.Warnings
MonadWarning m => MonadWarning (StateT s m)Defined in Agda-2.8.0.2 · Agda.TypeChecking.Warnings
(MonadWarning m, Monoid w) => MonadWarning (WriterT w m)Defined in Agda-2.8.0.2 · Agda.TypeChecking.Warnings

valuewarning'_ :: MonadWarning m => CallStack -> Warning -> m TCWarning

valuewarning_ :: (HasCallStack, MonadWarning m) => Warning -> m TCWarning

valuewarning' :: MonadWarning m => CallStack -> Warning -> m ()

valuewarning :: (HasCallStack, MonadWarning m) => Warning -> m ()

valuewarnings :: (HasCallStack, MonadWarning m) => List1 Warning -> m ()

valueraiseWarningsOnUsage :: (MonadWarning m, ReadTCState m) => QName -> m ()

Raise every WARNING_ON_USAGE connected to a name.

valueisUnsolvedWarning :: Warning -> Bool

valueisMetaWarning :: Warning -> Bool

valueisMetaTCWarning :: TCWarning -> Bool

valueonlyShowIfUnsolved :: Warning -> Bool

datadata WhichWarnings

Classifying warnings: some are benign, others are (non-fatal) errors

ErrorWarnings
warnings that will be turned into errors
AllWarnings
all warnings, including errors and benign ones Note: order of constructors is important for the derived Ord instance

Instances2Eq, Ord

valueclassifyWarning :: Warning -> WhichWarnings

datadata WarningsAndNonFatalErrors

Assorted warnings and errors to be displayed to the user

Instances3Null, EncodeTCM

Null WarningsAndNonFatalErrorsDefined in Agda-2.8.0.2 · Agda.TypeChecking.Monad.Base
EncodeTCM DisplayInfoDefined in Agda-2.8.0.2 · Agda.Interaction.JSONTop · orphan
EncodeTCM ResponseDefined in Agda-2.8.0.2 · Agda.Interaction.JSONTop · orphan

valuetcWarnings :: WarningsAndNonFatalErrors -> Set TCWarning

valuenonFatalErrors :: WarningsAndNonFatalErrors -> Set TCWarning

valueclassifyWarnings :: [TCWarning] -> WarningsAndNonFatalErrors