This class indicates that the error type to can always represent the error type from.

This is useful in implementing generic procedures that may throw errors. For example, we support symbolic division and modulo operations. These operations should throw an error when the divisor is zero, and we use the standard error type ArithException for this purpose. However, the user may use other type to represent errors, so we need this type class to transform the ArithException to the user-defined types.

Another example of these generic procedures is the symAssert and symAssume functions. They can be used with any error types that are compatible with the AssertionError and VerificationConditions types, respectively.

Used within a monadic multi path computation for exception processing.

Terminate the current execution path with the specified error if the condition does not hold. Compatible error can be transformed.

>>> let assert = symAssertTransformableError AssertionError
>>> assert "a" :: ExceptT AssertionError UnionM ()
ExceptT {If (! a) (Left AssertionError) (Right ())}

Used within a monadic multi path computation to begin exception processing.

Terminate the current execution path with the specified error. Compatible errors can be transformed.

>>> symThrowTransformableError Overflow :: ExceptT AssertionError UnionM ()
ExceptT {Left AssertionError}