| Safe Haskell | None |
|---|---|
| Language | Haskell2010 |
Mikan.TypeChecking.Monad.Diagnostic
Synopsis
- data DiagnosticReason
- = DiagError
- | DiagWarning { }
- class (NFData a, Show a, PrettyTCM a, Typeable a) => Diagnostic a where
- diagnosticReason :: a -> DiagnosticReason
- diagnosticString :: a -> String
- toSomeDiagnostic :: a -> SomeDiagnostic
- fromSomeDiagnostic :: SomeDiagnostic -> Maybe a
- data SomeDiagnostic
- data EncodedDiagnostic = EncodedDiagnostic {
- _edReason :: !DiagnosticReason
- _edString :: !String
- internalErrorDiagnostic :: String -> SomeDiagnostic
- type MonadTCError (m :: Type -> Type) = (MonadTCEnv m, ReadTCState m, MonadError TCErr m)
- typeError :: (HasCallStack, MonadTCError m, Diagnostic e) => e -> m a
- typeError' :: (MonadTCError m, Diagnostic e) => CallStack -> e -> m a
- locatedTypeError :: (MonadTCError m, Diagnostic e) => (a -> e) -> HasCallStack => a -> m b
- typeError_ :: (HasCallStack, MonadTCEnv m, ReadTCState m, Diagnostic e) => e -> m TCErr
- typeError'_ :: (MonadTCEnv m, ReadTCState m, Diagnostic e) => CallStack -> e -> m TCErr
- syntaxError :: (HasCallStack, MonadTCError m) => String -> m a
- internalError :: (HasCallStack, MonadTCError m) => String -> m a
The Diagnostic class
data DiagnosticReason Source #
The reason for raising a diagnostic.
Constructors
| DiagError | The diagnostic is always an error. |
| DiagWarning | The diagnostic is a warning with the given name. This |
Fields | |
Instances
class (NFData a, Show a, PrettyTCM a, Typeable a) => Diagnostic a where Source #
A Diagnostic is a value that can be thrown to abort elaboration
(see typeError and variants), or logged to the set of warnings (see
warning and variants).
New instances of Diagnostic (new type errors, new warnings) should
be added in a support module adjacent to the component that raises
them. For example, errors related to execution of metaprograms
(implemented in Mikan.TypeChecking.Unquote) are defined in the
module Mikan.TypeChecking.Unquote.Errors.
Minimal complete definition
Methods
diagnosticReason :: a -> DiagnosticReason Source #
The reason, or "intrinsic severity", of a diagnostic.
This is the base for computing the actual severity of the diagnostic after flags are applied.
diagnosticString :: a -> String Source #
Return a string that identifies the diagnostic. It is generally, but not necessarily, the name of the constructor for that value as a string. These strings are shown to the user in brackets after the diagnostic's severity.
TODO: This should be replaced with something that statically guarantees a unique numeric identifier for each diagnostic constructor.
toSomeDiagnostic :: a -> SomeDiagnostic Source #
Wrap the Diagnostic into a SomeDiagnostic.
NOTE: This method should not be implemented manually. It only
exists to avoid repeated boxing of SomeDiagnostics.
fromSomeDiagnostic :: SomeDiagnostic -> Maybe a Source #
Attempt to recover the Diagnostic from a SomeDiagnostic.
NOTE: This method should not be implemented manually. It only
exists to avoid repeated boxing of SomeDiagnostics.
Instances
| Diagnostic InteractionError Source # | |
Defined in Mikan.Interaction.Errors | |
| Diagnostic DeclarationException' Source # | |
Defined in Mikan.TypeChecking.Monad.Diagnostic | |
| Diagnostic DeclarationWarning Source # | |
Defined in Mikan.TypeChecking.Warnings | |
| Diagnostic IgnoredRecordDeclaration Source # | |
Defined in Mikan.Syntax.Scope.Errors | |
| Diagnostic PatternSynonymError Source # | |
Defined in Mikan.Syntax.Scope.Errors | |
| Diagnostic NoConstraintsError Source # | |
Defined in Mikan.TypeChecking.Constraints | |
| Diagnostic ConversionError Source # | |
Defined in Mikan.TypeChecking.Conversion.Errors | |
| Diagnostic SplitError Source # | |
Defined in Mikan.TypeChecking.Coverage.Errors Methods diagnosticReason :: SplitError -> DiagnosticReason Source # diagnosticString :: SplitError -> String Source # toSomeDiagnostic :: SplitError -> SomeDiagnostic Source # fromSomeDiagnostic :: SomeDiagnostic -> Maybe SplitError Source # | |
| Diagnostic DeferredError Source # | |
Defined in Mikan.TypeChecking.Errors.Deferred | |
| Diagnostic InstanceSearchError Source # | |
Defined in Mikan.TypeChecking.InstanceArguments.Errors | |
| Diagnostic TypeError Source # | |
Defined in Mikan.TypeChecking.Monad.Diagnostic Methods diagnosticReason :: TypeError -> DiagnosticReason Source # diagnosticString :: TypeError -> String Source # toSomeDiagnostic :: TypeError -> SomeDiagnostic Source # fromSomeDiagnostic :: SomeDiagnostic -> Maybe TypeError Source # | |
| Diagnostic UnsolvedWarning Source # | |
Defined in Mikan.TypeChecking.Warnings | |
| Diagnostic Warning Source # | |
Defined in Mikan.TypeChecking.Warnings Methods diagnosticReason :: Warning -> DiagnosticReason Source # diagnosticString :: Warning -> String Source # toSomeDiagnostic :: Warning -> SomeDiagnostic Source # fromSomeDiagnostic :: SomeDiagnostic -> Maybe Warning Source # | |
| Diagnostic EncodedDiagnostic Source # | |
Defined in Mikan.TypeChecking.Monad.Diagnostic | |
| Diagnostic SomeDiagnostic Source # | |
Defined in Mikan.TypeChecking.Monad.Diagnostic | |
| Diagnostic UnboundParameters Source # | |
Defined in Mikan.TypeChecking.Rules.Data | |
| Diagnostic ExecError Source # | |
Defined in Mikan.TypeChecking.Unquote.Errors Methods diagnosticReason :: ExecError -> DiagnosticReason Source # diagnosticString :: ExecError -> String Source # toSomeDiagnostic :: ExecError -> SomeDiagnostic Source # fromSomeDiagnostic :: SomeDiagnostic -> Maybe ExecError Source # | |
| Diagnostic UnquoteError Source # | |
Defined in Mikan.TypeChecking.Unquote.Errors | |
Wrappers for ferrying diagnostic values
The TCM needs to store Diagnostic values in two forms: for
control flow, in TCErr; and for warning reporting, in TCWarning.
TCErrs only exist during execution, and are sometimes matched on,
while non-fatal TCWarnings can persist into interface files.
These two needs are served by the wrapper types SomeDiagnostic and
EncodedDiagnostic respectively.
data SomeDiagnostic Source #
A package precisely wrapping a Diagnostic value.
The Diagnostic methods toSomeDiagnostic and fromSomeDiagnostic
can be used to up- and down-cast between SomeDiagnostic and a
concrete Diagnostic type.
Instances
| EncodeTCM DisplayInfo Source # | |
Defined in Mikan.Interaction.JSONTop | |
| EncodeTCM Info_Error Source # | |
Defined in Mikan.Interaction.JSONTop | |
| EncodeTCM Response Source # | |
| EncodeTCM TCWarning Source # | |
| Diagnostic SomeDiagnostic Source # | |
Defined in Mikan.TypeChecking.Monad.Diagnostic | |
| PrettyTCM SomeDiagnostic Source # | |
Defined in Mikan.TypeChecking.Monad.Diagnostic Methods prettyTCM :: MonadPretty m => SomeDiagnostic -> m Doc Source # | |
| NFData SomeDiagnostic Source # | |
Defined in Mikan.TypeChecking.Monad.Diagnostic Methods rnf :: SomeDiagnostic -> () # | |
| Show SomeDiagnostic Source # | |
Defined in Mikan.TypeChecking.Monad.Diagnostic Methods showsPrec :: Int -> SomeDiagnostic -> ShowS # show :: SomeDiagnostic -> String # showList :: [SomeDiagnostic] -> ShowS # | |
data EncodedDiagnostic Source #
The serialised form of a Diagnostic, recording only the
identifying string and the intrinsic DiagnosticReason.
Can not be downcast back to the Diagnostic it was originally
encoded from.
Constructors
| EncodedDiagnostic | |
Fields
| |
Instances
| Diagnostic EncodedDiagnostic Source # | |||||
Defined in Mikan.TypeChecking.Monad.Diagnostic | |||||
| PrettyTCM EncodedDiagnostic Source # | |||||
Defined in Mikan.TypeChecking.Monad.Diagnostic Methods prettyTCM :: MonadPretty m => EncodedDiagnostic -> m Doc Source # | |||||
| EmbPrj EncodedDiagnostic Source # | |||||
| NFData EncodedDiagnostic Source # | |||||
Defined in Mikan.TypeChecking.Monad.Diagnostic Methods rnf :: EncodedDiagnostic -> () # | |||||
| Generic EncodedDiagnostic Source # | |||||
Defined in Mikan.TypeChecking.Monad.Diagnostic Associated Types
Methods from :: EncodedDiagnostic -> Rep EncodedDiagnostic x # to :: Rep EncodedDiagnostic x -> EncodedDiagnostic # | |||||
| Show EncodedDiagnostic Source # | |||||
Defined in Mikan.TypeChecking.Monad.Diagnostic Methods showsPrec :: Int -> EncodedDiagnostic -> ShowS # show :: EncodedDiagnostic -> String # showList :: [EncodedDiagnostic] -> ShowS # | |||||
| type Rep EncodedDiagnostic Source # | |||||
Defined in Mikan.TypeChecking.Monad.Diagnostic type Rep EncodedDiagnostic = D1 ('MetaData "EncodedDiagnostic" "Mikan.TypeChecking.Monad.Diagnostic" "Mikan-2.9.0-CZbYRMbHmng2A9zjJ31VFu" 'False) (C1 ('MetaCons "EncodedDiagnostic" 'PrefixI 'True) (S1 ('MetaSel ('Just "_edReason") 'NoSourceUnpackedness 'SourceStrict 'DecidedStrict) (Rec0 DiagnosticReason) :*: S1 ('MetaSel ('Just "_edString") 'NoSourceUnpackedness 'SourceStrict 'DecidedStrict) (Rec0 String))) | |||||
internalErrorDiagnostic :: String -> SomeDiagnostic Source #
The SomeDiagnostic associated to an internal error.
NOTE: This is needed to break an import cycle:
Mikan.Interaction.Monad.Base needs a SomeDiagnostic which can be
thrown for the MonadError TCErrTCM, but it can
not import the Diagnostic class since that depends on PrettyTCM.
Monads which can throw and catch diagnostics
type MonadTCError (m :: Type -> Type) = (MonadTCEnv m, ReadTCState m, MonadError TCErr m) Source #
The constraints needed for typeError and similar.
typeError :: (HasCallStack, MonadTCError m, Diagnostic e) => e -> m a Source #
Throw a Diagnostic in a MonadTCError, associating the error
with the source position from HasCallStack.
typeError' :: (MonadTCError m, Diagnostic e) => CallStack -> e -> m a Source #
Throw a Diagnostic in a MonadTCError with an explicit CallStack.
locatedTypeError :: (MonadTCError m, Diagnostic e) => (a -> e) -> HasCallStack => a -> m b Source #
Utility function for 1-arg constructed Diagnostics.
Note that the HasCallStack constraint is on the *resulting* function.
typeError_ :: (HasCallStack, MonadTCEnv m, ReadTCState m, Diagnostic e) => e -> m TCErr Source #
Construct a TCErr value wrapping the given Diagnostic,
associating it with the source position from HasCallStack.
typeError'_ :: (MonadTCEnv m, ReadTCState m, Diagnostic e) => CallStack -> e -> m TCErr Source #
Construct a TCErr value wrapping the given Diagnostic, associating it with the explicit CallStack.
syntaxError :: (HasCallStack, MonadTCError m) => String -> m a Source #
Raise a SyntaxError.
internalError :: (HasCallStack, MonadTCError m) => String -> m a Source #
Orphan instances
| PrettyTCM DeclarationException' Source # | |
Methods prettyTCM :: MonadPretty m => DeclarationException' -> m Doc Source # | |