| Safe Haskell | Safe-Inferred |
|---|---|
| Language | Haskell2010 |
Agda.TypeChecking.Errors
Contents
Synopsis
- prettyError :: MonadTCM tcm => TCErr -> tcm String
- tcErrString :: TCErr -> String
- prettyTCWarnings' :: [TCWarning] -> TCM [String]
- prettyTCWarnings :: [TCWarning] -> TCM String
- tcWarningsToError :: [TCWarning] -> TCM ()
- applyFlagsToTCWarningsPreserving :: HasOptions m => Set WarningName -> [TCWarning] -> m [TCWarning]
- applyFlagsToTCWarnings :: HasOptions m => [TCWarning] -> m [TCWarning]
- getAllUnsolvedWarnings :: (MonadFail m, ReadTCState m, MonadWarning m) => m [TCWarning]
- getAllWarningsPreserving :: (MonadFail m, ReadTCState m, MonadWarning m) => Set WarningName -> WhichWarnings -> m [TCWarning]
- getAllWarnings :: (MonadFail m, ReadTCState m, MonadWarning m) => WhichWarnings -> m [TCWarning]
- getAllWarningsOfTCErr :: TCErr -> TCM [TCWarning]
- dropTopLevelModule :: QName -> TCM QName
- topLevelModuleDropper :: (MonadDebug m, MonadTCEnv m, ReadTCState m) => m (QName -> QName)
- stringTCErr :: String -> TCErr
Documentation
tcErrString :: TCErr -> String Source #
tcWarningsToError :: [TCWarning] -> TCM () Source #
Turns warnings, if any, into errors.
applyFlagsToTCWarningsPreserving :: HasOptions m => Set WarningName -> [TCWarning] -> m [TCWarning] Source #
Depending which flags are set, one may happily ignore some warnings.
applyFlagsToTCWarnings :: HasOptions m => [TCWarning] -> m [TCWarning] Source #
getAllUnsolvedWarnings :: (MonadFail m, ReadTCState m, MonadWarning m) => m [TCWarning] Source #
getAllWarningsPreserving :: (MonadFail m, ReadTCState m, MonadWarning m) => Set WarningName -> WhichWarnings -> m [TCWarning] Source #
getAllWarnings :: (MonadFail m, ReadTCState m, MonadWarning m) => WhichWarnings -> m [TCWarning] Source #
Collect all warnings that have accumulated in the state.
dropTopLevelModule :: QName -> TCM 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.
stringTCErr :: String -> TCErr Source #
Orphan instances
| 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 # | |