| Safe Haskell | None |
|---|---|
| Language | Haskell2010 |
Agda.TypeChecking.Warnings
Synopsis
- class (MonadPretty m, MonadError TCErr m) => MonadWarning (m :: Type -> Type) where
- addWarning :: TCWarning -> m ()
- warning'_ :: MonadWarning m => CallStack -> Warning -> m TCWarning
- warning_ :: (HasCallStack, MonadWarning m) => Warning -> m TCWarning
- warning' :: MonadWarning m => CallStack -> Warning -> m ()
- warning :: (HasCallStack, MonadWarning m) => Warning -> m ()
- warnings :: (HasCallStack, MonadWarning m) => [Warning] -> m ()
- raiseWarningsOnUsage :: (MonadWarning m, ReadTCState m) => QName -> m ()
- isUnsolvedWarning :: Warning -> Bool
- isMetaWarning :: Warning -> Bool
- isMetaTCWarning :: TCWarning -> Bool
- onlyShowIfUnsolved :: Warning -> Bool
- data WhichWarnings
- classifyWarning :: Warning -> WhichWarnings
- data WarningsAndNonFatalErrors
- tcWarnings :: WarningsAndNonFatalErrors -> [TCWarning]
- nonFatalErrors :: WarningsAndNonFatalErrors -> [TCWarning]
- emptyWarningsAndNonFatalErrors :: WarningsAndNonFatalErrors
- classifyWarnings :: [TCWarning] -> WarningsAndNonFatalErrors
- runPM :: PM a -> TCM a
Documentation
class (MonadPretty m, MonadError TCErr m) => MonadWarning (m :: Type -> Type) where Source #
Minimal complete definition
Nothing
Methods
addWarning :: TCWarning -> m () Source #
Store a warning and generate highlighting from it.
default addWarning :: forall (n :: Type -> Type) (t :: (Type -> Type) -> Type -> Type). (MonadWarning n, MonadTrans t, t n ~ m) => TCWarning -> m () Source #
Instances
| MonadWarning TCM Source # | |
Defined in Agda.TypeChecking.Warnings Methods addWarning :: TCWarning -> TCM () Source # | |
| (PureTCM m, MonadBlock m) => MonadWarning (PureConversionT m) Source # | |
Defined in Agda.TypeChecking.Conversion.Pure Methods addWarning :: TCWarning -> PureConversionT m () Source # | |
| MonadWarning m => MonadWarning (ReaderT r m) Source # | |
Defined in Agda.TypeChecking.Warnings Methods addWarning :: TCWarning -> ReaderT r m () Source # | |
| MonadWarning m => MonadWarning (StateT s m) Source # | |
Defined in Agda.TypeChecking.Warnings Methods addWarning :: TCWarning -> StateT s m () Source # | |
warning_ :: (HasCallStack, MonadWarning m) => Warning -> m TCWarning Source #
warning :: (HasCallStack, MonadWarning m) => Warning -> m () Source #
warnings :: (HasCallStack, MonadWarning m) => [Warning] -> m () Source #
raiseWarningsOnUsage :: (MonadWarning m, ReadTCState m) => QName -> m () Source #
Raise every WARNING_ON_USAGE connected to a name.
isUnsolvedWarning :: Warning -> Bool Source #
isMetaWarning :: Warning -> Bool Source #
isMetaTCWarning :: TCWarning -> Bool Source #
onlyShowIfUnsolved :: Warning -> Bool Source #
data WhichWarnings Source #
Classifying warnings: some are benign, others are (non-fatal) errors
Constructors
| 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 |
Instances
| Eq WhichWarnings Source # | |
Defined in Agda.TypeChecking.Warnings | |
| Ord WhichWarnings Source # | |
Defined in Agda.TypeChecking.Warnings Methods compare :: WhichWarnings -> WhichWarnings -> Ordering (<) :: WhichWarnings -> WhichWarnings -> Bool (<=) :: WhichWarnings -> WhichWarnings -> Bool (>) :: WhichWarnings -> WhichWarnings -> Bool (>=) :: WhichWarnings -> WhichWarnings -> Bool max :: WhichWarnings -> WhichWarnings -> WhichWarnings min :: WhichWarnings -> WhichWarnings -> WhichWarnings | |
data WarningsAndNonFatalErrors Source #
Assorted warnings and errors to be displayed to the user
emptyWarningsAndNonFatalErrors :: WarningsAndNonFatalErrors Source #
The only way to construct a empty WarningsAndNonFatalErrors