| Safe Haskell | None |
|---|---|
| Language | Haskell2010 |
Agda.TypeChecking.Errors
Contents
Synopsis
- renderError :: MonadTCM tcm => TCErr -> tcm String
- prettyError :: MonadTCM tcm => TCErr -> tcm Doc
- prettyShadowedModule :: MonadPretty m => Name -> List1 ModuleName -> m (m Doc, Range)
- tcErrString :: TCErr -> String
- tcErrModuleToSource :: TCErr -> Maybe ModuleToSource
- prettyTCWarnings' :: Set TCWarning -> TCM [Doc]
- prettyTCWarnings :: Set TCWarning -> TCM String
- tcWarningsToError :: TopLevelModuleNameWithSourceFile -> [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
prettyShadowedModule :: MonadPretty m => Name -> List1 ModuleName -> m (m Doc, Range) Source #
Pretty-print error ShadowedModule and return the range of the shadowed module.
tcErrString :: TCErr -> String Source #
tcErrModuleToSource :: TCErr -> Maybe ModuleToSource Source #
If the TCErr carries a TCState, return the ModuleToSource
from there, since that's the ModuleToSource we need for
highlighting the actual error message.
Arguments
| :: TopLevelModuleNameWithSourceFile | The module we have checked (which produced the warnings). |
| -> [TCWarning] | The warnings to turn into errors. |
| -> TCM () |
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 # | |