| Safe Haskell | None |
|---|---|
| Language | Haskell2010 |
Agda.TypeChecking.Errors
Contents
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
Documentation
tcErrString :: TCErr -> 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.
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 #
Instances
| Verbalize Cohesion Source # | |
| Verbalize Hiding Source # | |
| Verbalize ModalPolarity Source # | |
Defined in Agda.TypeChecking.Errors Methods verbalize :: ModalPolarity -> String Source # | |
| Verbalize Modality Source # | |
| Verbalize PolarityModality Source # | |
Defined in Agda.TypeChecking.Errors Methods verbalize :: PolarityModality -> String Source # | |
| Verbalize Quantity Source # | |
| Verbalize Relevance Source # | |
Orphan instances
| PrettyTCM ExecError Source # | |
| PrettyTCM GHCBackendError Source # | |
Methods prettyTCM :: MonadPretty m => GHCBackendError -> m Doc Source # | |
| PrettyTCM InteractionError Source # | |
Methods prettyTCM :: MonadPretty m => InteractionError -> m Doc Source # | |
| PrettyTCM JSBackendError Source # | |
Methods prettyTCM :: MonadPretty m => JSBackendError -> m Doc Source # | |
| PrettyTCM MissingTypeSignatureInfo Source # | |
Methods prettyTCM :: MonadPretty m => MissingTypeSignatureInfo -> m Doc Source # | |
| PrettyTCM NegativeUnification Source # | |
Methods prettyTCM :: MonadPretty m => NegativeUnification -> m Doc Source # | |
| PrettyTCM SplitError Source # | |
Methods prettyTCM :: MonadPretty m => SplitError -> m Doc Source # | |
| PrettyTCM TCErr Source # | |
| PrettyTCM TypeError Source # | |
| PrettyTCM UnificationFailure Source # | |
Methods prettyTCM :: MonadPretty m => UnificationFailure -> m Doc Source # | |
| PrettyTCM UnquoteError Source # | |
Methods prettyTCM :: MonadPretty m => UnquoteError -> m Doc Source # | |