| Safe Haskell | None |
|---|---|
| Language | Haskell2010 |
Agda.Unused.Monad.Error
Contents
Description
An error monad for determining unused code.
Synopsis
- data Error where
- ErrorAmbiguous :: !Range -> !QName -> Error
- ErrorCyclic :: !Range -> !QName -> Error
- ErrorDeclaration :: !DeclarationException -> Error
- ErrorFile :: !FilePath -> Error
- ErrorFind :: !Range -> !QName -> !FindError -> Error
- ErrorFixity :: !(Maybe Range) -> Error
- ErrorGlobal :: !Range -> Error
- ErrorInclude :: Error
- ErrorInternal :: !InternalError -> Error
- ErrorOpen :: !Range -> !QName -> Error
- ErrorParse :: !ParseError -> Error
- ErrorPolarity :: !(Maybe Range) -> Error
- ErrorRoot :: !QName -> !QName -> Error
- ErrorUnsupported :: !UnsupportedError -> !Range -> Error
- data InternalError where
- ErrorConstructor :: !Range -> InternalError
- ErrorMacro :: !Range -> InternalError
- ErrorModuleName :: !FilePath -> InternalError
- ErrorName :: !Range -> InternalError
- ErrorRenaming :: !Range -> InternalError
- ErrorUnexpected :: !UnexpectedError -> !Range -> InternalError
- data UnexpectedError where
- UnexpectedAbsurd :: UnexpectedError
- UnexpectedAs :: UnexpectedError
- UnexpectedDontCare :: UnexpectedError
- UnexpectedETel :: UnexpectedError
- UnexpectedEllipsis :: UnexpectedError
- UnexpectedEqual :: UnexpectedError
- UnexpectedField :: UnexpectedError
- UnexpectedNiceFunClause :: UnexpectedError
- UnexpectedOpApp :: UnexpectedError
- UnexpectedOpAppP :: UnexpectedError
- data UnsupportedError where
- liftLookup :: MonadError Error m => Range -> QName -> Either LookupError a -> m a
Definitions
An error encountered while checking for unused code.
Constructors
| ErrorAmbiguous :: !Range -> !QName -> Error | Ambiguous lookup. |
| ErrorCyclic :: !Range -> !QName -> Error | Cyclic module dependency. |
| ErrorDeclaration :: !DeclarationException -> Error | Agda declaration exception. |
| ErrorFile :: !FilePath -> Error | File not found. |
| ErrorFind :: !Range -> !QName -> !FindError -> Error | Agda find error. |
| ErrorFixity :: !(Maybe Range) -> Error | Agda fixity exception. |
| ErrorGlobal :: !Range -> Error | Illegal declaration in main module of global check. |
| ErrorInclude :: Error | Error in computing include paths. |
| ErrorInternal :: !InternalError -> Error | Internal error; should be reported. |
| ErrorOpen :: !Range -> !QName -> Error | Module not found in open statement. |
| ErrorParse :: !ParseError -> Error | Agda parse error. |
| ErrorPolarity :: !(Maybe Range) -> Error | Agda polarity error. |
| ErrorRoot :: !QName -> !QName -> Error | Root not found. |
| ErrorUnsupported :: !UnsupportedError -> !Range -> Error | Unsupported language feature. |
data InternalError where Source #
An internal error, indicating a bug in our code. This type of error should be reported by filing an issue.
Constructors
| ErrorConstructor :: !Range -> InternalError | Unexpected declaration type for constructor. |
| ErrorMacro :: !Range -> InternalError | Unexpected arguments to SectionApp constructor. |
| ErrorModuleName :: !FilePath -> InternalError | Unexpected empty top level module name. |
| ErrorName :: !Range -> InternalError | Unexpected underscore as name. |
| ErrorRenaming :: !Range -> InternalError | Unexpected name-module mismatch in renaming statement. |
| ErrorUnexpected :: !UnexpectedError -> !Range -> InternalError | Unexpected data type constructor. |
Instances
| Show InternalError Source # | |
Defined in Agda.Unused.Monad.Error Methods showsPrec :: Int -> InternalError -> ShowS # show :: InternalError -> String # showList :: [InternalError] -> ShowS # | |
data UnexpectedError where Source #
An error indicating that a constructor for a data type is used where it should not be used.
Constructors
Instances
| Show UnexpectedError Source # | |
Defined in Agda.Unused.Monad.Error Methods showsPrec :: Int -> UnexpectedError -> ShowS # show :: UnexpectedError -> String # showList :: [UnexpectedError] -> ShowS # | |
data UnsupportedError where Source #
An error indicating that an unsupported language was found.
Constructors
| UnsupportedMacro :: UnsupportedError | Record module instance applications. |
| UnsupportedUnquote :: UnsupportedError | Unquoting primitives. |
Instances
| Show UnsupportedError Source # | |
Defined in Agda.Unused.Monad.Error Methods showsPrec :: Int -> UnsupportedError -> ShowS # show :: UnsupportedError -> String # showList :: [UnsupportedError] -> ShowS # | |
Lift
liftLookup :: MonadError Error m => Range -> QName -> Either LookupError a -> m a Source #
Lift a lookup result to our error monad.
Orphan instances
| (Monad m, MonadError Error m) => MonadFixityError m Source # | |
Methods throwMultipleFixityDecls :: [(Name, [Fixity'])] -> m a # throwMultiplePolarityPragmas :: [Name] -> m a # warnUnknownNamesInFixityDecl :: [Name] -> m () # warnUnknownNamesInPolarityPragmas :: [Name] -> m () # warnUnknownFixityInMixfixDecl :: [Name] -> m () # warnPolarityPragmasButNotPostulates :: [Name] -> m () # | |