Agda.TypeChecking.Warnings

Documentation

class (MonadPretty m, MonadError TCErr m) => MonadWarning m where

Methods

addWarning :: TCWarning -> m ()

Render the warning

Instances

MonadWarning TCM

Defined in Agda.TypeChecking.Warnings

Methods

addWarning :: TCWarning -> TCM ()

(MonadReduce m, MonadAddContext m, HasConstInfo m, HasBuiltins m) => MonadWarning (PureConversionT m)

Defined in Agda.TypeChecking.Conversion.Pure

Methods

addWarning :: TCWarning -> PureConversionT m ()

MonadWarning m => MonadWarning (StateT s m)

Defined in Agda.TypeChecking.Warnings

Methods

addWarning :: TCWarning -> StateT s m ()

MonadWarning m => MonadWarning (ReaderT r m)

Defined in Agda.TypeChecking.Warnings

Methods

addWarning :: TCWarning -> ReaderT r m ()

genericWarning :: MonadWarning m => Doc -> m ()

genericNonFatalError :: MonadWarning m => Doc -> m ()

warning_ :: MonadWarning m => Warning -> m TCWarning

warning :: MonadWarning m => Warning -> m ()

warnings :: MonadWarning m => [Warning] -> m ()

isUnsolvedWarning :: Warning -> Bool

isMetaWarning :: Warning -> Bool

isMetaTCWarning :: TCWarning -> Bool

onlyShowIfUnsolved :: Warning -> Bool

data WhichWarnings

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

Defined in Agda.TypeChecking.Warnings

Methods

(==) :: WhichWarnings -> WhichWarnings -> Bool

(/=) :: WhichWarnings -> WhichWarnings -> Bool

Ord WhichWarnings

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

classifyWarning :: Warning -> WhichWarnings

data WarningsAndNonFatalErrors

Assorted warnings and errors to be displayed to the user

tcWarnings :: WarningsAndNonFatalErrors -> [TCWarning]

nonFatalErrors :: WarningsAndNonFatalErrors -> [TCWarning]

emptyWarningsAndNonFatalErrors :: WarningsAndNonFatalErrors

The only way to construct a empty WarningsAndNonFatalErrors

classifyWarnings :: [TCWarning] -> WarningsAndNonFatalErrors

runPM :: PM a -> TCM a

running the Parse monad

Orphan instances

Semigroup (TCM Doc)

Methods

(<>) :: TCM Doc -> TCM Doc -> TCM Doc

sconcat :: NonEmpty (TCM Doc) -> TCM Doc

stimes :: Integral b => b -> TCM Doc -> TCM Doc

Monad m => Semigroup (StateT s m Doc)

Methods

(<>) :: StateT s m Doc -> StateT s m Doc -> StateT s m Doc

sconcat :: NonEmpty (StateT s m Doc) -> StateT s m Doc

stimes :: Integral b => b -> StateT s m Doc -> StateT s m Doc

Applicative m => Semigroup (ReaderT s m Doc)

Methods

(<>) :: ReaderT s m Doc -> ReaderT s m Doc -> ReaderT s m Doc

sconcat :: NonEmpty (ReaderT s m Doc) -> ReaderT s m Doc

stimes :: Integral b => b -> ReaderT s m Doc -> ReaderT s m Doc