Agda.TypeChecking.Errors

Documentation

renderError :: MonadTCM tcm => TCErr -> tcm String

prettyError :: MonadTCM tcm => TCErr -> tcm Doc

tcErrString :: TCErr -> String

prettyTCWarnings' :: [TCWarning] -> TCM [Doc]

prettyTCWarnings :: [TCWarning] -> TCM String

tcWarningsToError :: [TCWarning] -> TCM ()

Turns warnings, if any, into errors.

applyFlagsToTCWarningsPreserving :: HasOptions m => Set WarningName -> [TCWarning] -> m [TCWarning]

Depending which flags are set, one may happily ignore some warnings.

applyFlagsToTCWarnings :: HasOptions m => [TCWarning] -> m [TCWarning]

getAllUnsolvedWarnings :: (MonadFail m, ReadTCState m, MonadWarning m, MonadTCM m) => m [TCWarning]

getAllWarningsPreserving :: (MonadFail m, ReadTCState m, MonadWarning m, MonadTCM m) => Set WarningName -> WhichWarnings -> m [TCWarning]

getAllWarnings :: (MonadFail m, ReadTCState m, MonadWarning m, MonadTCM m) => WhichWarnings -> m [TCWarning]

Collect all warnings that have accumulated in the state.

getAllWarningsOfTCErr :: TCErr -> TCM [TCWarning]

dropTopLevelModule :: MonadPretty m => QName -> m QName

Drops the filename component of the qualified name.

topLevelModuleDropper :: (MonadDebug m, MonadTCEnv m, ReadTCState m) => m (QName -> QName)

Produces a function which drops the filename component of the qualified name.

stringTCErr :: String -> TCErr

explainWhyInScope :: forall m. MonadPretty m => WhyInScopeData -> m Doc

class Verbalize a where

Methods

verbalize :: a -> String

Instances

Verbalize Cohesion

Defined in Agda.TypeChecking.Errors

Methods

verbalize :: Cohesion -> String

Verbalize Hiding

Defined in Agda.TypeChecking.Errors

Methods

verbalize :: Hiding -> String

Verbalize Modality

Defined in Agda.TypeChecking.Errors

Methods

verbalize :: Modality -> String

Verbalize Quantity

Defined in Agda.TypeChecking.Errors

Methods

verbalize :: Quantity -> String

Verbalize Relevance

Defined in Agda.TypeChecking.Errors

Methods

verbalize :: Relevance -> String

Orphan instances

PrettyTCM NegativeUnification

Methods

prettyTCM :: MonadPretty m => NegativeUnification -> m Doc

PrettyTCM SplitError

Methods

prettyTCM :: MonadPretty m => SplitError -> m Doc

PrettyTCM TCErr

Methods

prettyTCM :: MonadPretty m => TCErr -> m Doc

PrettyTCM TypeError

Methods

prettyTCM :: MonadPretty m => TypeError -> m Doc

PrettyTCM UnificationFailure

Methods

prettyTCM :: MonadPretty m => UnificationFailure -> m Doc