| Safe Haskell | None |
|---|---|
| Language | Haskell2010 |
Mikan.TypeChecking.Errors.Deferred
Description
This module implements utilities for implementing generic error recovery strategies in the elaborator around noncooperative functions (like the conversion checker). Using these functions should be thought of as a fallback strategy wherever the type theory prevents us from doing better; wherever possible, a domain-specific solution to reconstructing a partial program where we can do more checking is preferred.
In summary, the generic error recovery strategies work by catching
(through handleRecoverableError) whatever TypeErrors are marked
"recoverable", which at the moment are those thrown in an environment
where envHardErrors is False (which is the default).
Non-recoverable errors bubble through these handlers as-is, and note
that the handler is not on the stack in its own recovery
continuation.
Some (dynamic) contexts require that thrown errors are not deferred through a generic strategy, even though such a handler would be present on the stack when the error is thrown. For example, while we can ignore a conversion-checking error if the stack looks like
checkRHS ⟩ checkExpr ⟩ ... ⟩ conversionError
we should not ignore the error if the stack instead looks like
solveConstraints ⟩ findInstance ⟩ checkExpr ⟩ ... ⟩ conversionError
because (in this case) the actual result of findInstance depends on
the checkExpr throwing an error but, if generic recovery is
allowed, checkExpr would instead succeed (producing a metavariable)
with a warning. These contexts should be marked with a function like
withHardErrors.
Synopsis
- handleRecoverableError :: MonadError TCErr m => (DeferredError -> m a) -> m a -> m a
- withHardErrors :: MonadTCEnv m => m a -> m a
- withFencedErrors :: (MonadTCEnv m, MonadError TCErr m, MonadDebug m) => m a -> m a
- withBatchedErrors :: (MonadTrace m, MonadTCState m, MonadError TCErr m, MonadDebug m) => m a -> m a
- data DeferredError
- errClosure :: Lens' DeferredError (Closure SomeDiagnostic)
- errLoc :: Lens' DeferredError CallStack
- errState :: Lens' DeferredError TCState
- suspendErrors :: (MonadTCM m, MonadError TCErr m) => TCM a -> m a
- hardTypeError :: (HasCallStack, MonadTCM m, Diagnostic e) => e -> m a
- softTypeError :: (HasCallStack, ReadTCState m, MonadError TCErr m, MonadTCEnv m, Diagnostic e) => e -> m a
- deferredErrorTerm :: Comparison -> Type -> DeferredError -> TCM Term
- sequenceErrors :: Traversable f => f (TCM a) -> TCM (f a)
- sequenceErrors_ :: Traversable f => f (TCM a) -> TCM ()
Errors as control flow
handleRecoverableError :: MonadError TCErr m => (DeferredError -> m a) -> m a -> m a Source #
Handle any recoverable errors thrown by the continuation with the given function.
The dynamic behaviour of this function can be thought of as obeying the equations
handleRecoverableErrorh (softTypeErrore) = h ehandleRecoverableErrorh (hardTypeErrore) =hardTypeErrore
withHardErrors :: MonadTCEnv m => m a -> m a Source #
Run a type-checking computation marking all of its thrown type
errors unrecoverable. This can be used to skip
handleRecoverableError handlers that appear below withHardErrors
in the call stack.
Letting E[_] stand for an arbitrary evaluation context built from
the functions in this module, the dynamic behaviour of this function
can be thought of as obeying the equation
withHardErrorsE[typeErrorerr ] =hardTypeErrorerr
In particular, any handleRecoverableErrors installed during
execution of the continuation are skipped:
withHardErrors(handleRecoverableError_ (typeErrore)) =hardTypeErrore
withFencedErrors :: (MonadTCEnv m, MonadError TCErr m, MonadDebug m) => m a -> m a Source #
Run a type-checking computation under withHardErrors, but mark
any escaping errors with the ambient recovery flag.
Letting E[_] stand for an arbitrary evaluation context built from
the functions in this module, the dynamic behaviour of this function
can be thought of as obeying the equations
withFencedErrorsE[softTypeErrorerr ] =typeErrorerrwithFencedErrorsE[hardTypeErrorerr ] =typeErrorerr
In particular, if withFencedErrors is placed in a context where
errors are recoverable, any unrecoverable errors thrown by the
continuation will be made recoverable when re-thrown by
withFencedErrors (if the context does not otherwise demand errors
are made unrecoverable).
withBatchedErrors :: (MonadTrace m, MonadTCState m, MonadError TCErr m, MonadDebug m) => m a -> m a Source #
Group any errors deferred during execution of the continuation into
a single NonFatalErrors, raised with the ambient error recovery
flag.
This includes any errors deferred by a generic strategy within the continuation.
data DeferredError Source #
Instances
errClosure :: Lens' DeferredError (Closure SomeDiagnostic) Source #
The actual diagnostic behind a deferred error, in its lexical
context; see tcErrClosErr.
errLoc :: Lens' DeferredError CallStack Source #
The original location where the deferred error was thrown; see
tcErrLocation.
errState :: Lens' DeferredError TCState Source #
The TCSTate where the deferred error was thrown; see
tcErrState.
Layered error handling
One pattern for locally making use of errors as control flow is using
a transformer like ExceptT TCErr TCMTCMcatchError @TCM
The functions suspendErrors, softTypeError and hardTypeError
mediate this interaction. Importantly, they can all be used directly
at TCM
suspendErrors :: (MonadTCM m, MonadError TCErr m) => TCM a -> m a Source #
Catch any errors thrown during execution of the continuation and
re-raise them in the monad m instead.
This applies equally to recoverable and unrecoverable errors.
hardTypeError :: (HasCallStack, MonadTCM m, Diagnostic e) => e -> m a Source #
Throw an unrecoverable error.
Regardless of whether m is a monad implementing its own error
handling, the error is thrown in the TCM.
softTypeError :: (HasCallStack, ReadTCState m, MonadError TCErr m, MonadTCEnv m, Diagnostic e) => e -> m a Source #
Throw a recoverable error, regardless of any surrounding
withHardErrors.
If m is a monad supporting its own error handling, the error is
thrown there, instead of in the TCM.
Canned recovery strategies
Arguments
| :: Comparison | How to check the result type. |
| -> Type | The expected type. |
| -> DeferredError | |
| -> TCM Term |
Recover from type-checking errors in a computation by recording the diagnostic as a warning and returning a new metavariable.
sequenceErrors :: Traversable f => f (TCM a) -> TCM (f a) Source #
Execute a Traversable container of TCM actions, allowing each
action to succeed or fail individually, but succeeding only if
every computation succeeds.
Here, "failure" is as per withBatchedErrors: recoverable errors in
each continuation are turned into warnings, and the overall
computation fails if it contributes any DiagErrors to the warning
state.
sequenceErrors_ :: Traversable f => f (TCM a) -> TCM () Source #
As sequenceErrors, but discarding the result.