Agda-2.8.0: A dependently typed functional programming language and proof assistant

Safe Haskell | None
Language | Haskell2010

Agda.TypeChecking.Errors

Contents

- Orphan instances

Synopsis

- renderError :: MonadTCM tcm => TCErr -> tcm String
- prettyError :: MonadTCM tcm => TCErr -> tcm Doc
- tcErrString :: TCErr -> String
- prettyTCWarnings' :: Set TCWarning -> TCM [Doc]
- prettyTCWarnings :: Set TCWarning -> TCM String
- tcWarningsToError :: [TCWarning] -> TCM ()
- applyFlagsToTCWarningsPreserving :: HasOptions m => Set WarningName -> Set TCWarning -> m (Set TCWarning)
- applyFlagsToTCWarnings :: HasOptions m => Set TCWarning -> m (Set TCWarning)
- getAllUnsolvedWarnings :: (ReadTCState m, MonadWarning m, MonadTCM m) => m [TCWarning]
- getAllWarningsPreserving :: (ReadTCState m, MonadWarning m, MonadTCM m) => Set WarningName -> WhichWarnings -> m (Set TCWarning)
- getAllWarnings :: (ReadTCState m, MonadWarning m, MonadTCM m) => WhichWarnings -> m (Set TCWarning)
- getAllWarningsOfTCErr :: TCErr -> TCM (Set TCWarning)
- dropTopLevelModule :: MonadPretty m => QName -> m QName
- topLevelModuleDropper :: (MonadDebug m, MonadTCEnv m, ReadTCState m) => m (QName -> QName)
- explainWhyInScope :: MonadPretty m => WhyInScopeData -> m Doc
- class Verbalize a where
  - verbalize :: a -> String

# Documentation

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

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

tcErrString :: TCErr -> String Source #

prettyTCWarnings' :: Set TCWarning -> TCM [Doc] Source #

prettyTCWarnings :: Set TCWarning -> TCM String Source #

tcWarningsToError :: [TCWarning] -> TCM () Source #

Turns warnings, if any, into errors.

applyFlagsToTCWarningsPreserving :: HasOptions m => Set WarningName -> Set TCWarning -> m (Set TCWarning) Source #

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

applyFlagsToTCWarnings :: HasOptions m => Set TCWarning -> m (Set TCWarning) Source #

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

getAllWarningsPreserving :: (ReadTCState m, MonadWarning m, MonadTCM m) => Set WarningName -> WhichWarnings -> m (Set TCWarning) Source #

getAllWarnings :: (ReadTCState m, MonadWarning m, MonadTCM m) => WhichWarnings -> m (Set TCWarning) Source #

Collect all warnings that have accumulated in the state.

getAllWarningsOfTCErr :: TCErr -> TCM (Set TCWarning) Source #

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

Drops the filename component of the qualified name.

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

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

explainWhyInScope :: MonadPretty m => WhyInScopeData -> m Doc Source #

class Verbalize a where Source #

Methods

verbalize :: a -> String Source #

#### Instances

Instances details

Verbalize Cohesion Source # |
Instance details Defined in Agda.TypeChecking.Errors Methods verbalize :: Cohesion -> String Source #
Verbalize Hiding Source # |
Instance details Defined in Agda.TypeChecking.Errors Methods verbalize :: Hiding -> String Source #
Verbalize ModalPolarity Source # |
Instance details Defined in Agda.TypeChecking.Errors Methods verbalize :: ModalPolarity -> String Source #
Verbalize Modality Source # |
Instance details Defined in Agda.TypeChecking.Errors Methods verbalize :: Modality -> String Source #
Verbalize PolarityModality Source # |
Instance details Defined in Agda.TypeChecking.Errors Methods verbalize :: PolarityModality -> String Source #
Verbalize Quantity Source # |
Instance details Defined in Agda.TypeChecking.Errors Methods verbalize :: Quantity -> String Source #
Verbalize Relevance Source # |
Instance details Defined in Agda.TypeChecking.Errors Methods verbalize :: Relevance -> String Source #

# Orphan instances

PrettyTCM ExecError Source # |
Instance details Methods prettyTCM :: MonadPretty m => ExecError -> m Doc Source #
PrettyTCM GHCBackendError Source # |
Instance details Methods prettyTCM :: MonadPretty m => GHCBackendError -> m Doc Source #
PrettyTCM InteractionError Source # |
Instance details Methods prettyTCM :: MonadPretty m => InteractionError -> m Doc Source #
PrettyTCM JSBackendError Source # |
Instance details Methods prettyTCM :: MonadPretty m => JSBackendError -> m Doc Source #
PrettyTCM MissingTypeSignatureInfo Source # |
Instance details Methods prettyTCM :: MonadPretty m => MissingTypeSignatureInfo -> m Doc Source #
PrettyTCM NegativeUnification Source # |
Instance details Methods prettyTCM :: MonadPretty m => NegativeUnification -> m Doc Source #
PrettyTCM SplitError Source # |
Instance details Methods prettyTCM :: MonadPretty m => SplitError -> m Doc Source #
PrettyTCM TCErr Source # |
Instance details Methods prettyTCM :: MonadPretty m => TCErr -> m Doc Source #
PrettyTCM TypeError Source # |
Instance details Methods prettyTCM :: MonadPretty m => TypeError -> m Doc Source #
PrettyTCM UnificationFailure Source # |
Instance details Methods prettyTCM :: MonadPretty m => UnificationFailure -> m Doc Source #
PrettyTCM UnquoteError Source # |
Instance details Methods prettyTCM :: MonadPretty m => UnquoteError -> m Doc Source #