Safe Haskell | Safe |
---|---|
Language | Haskell2010 |
This module provides a set of runtime assertions about types that
propogates information back to the type system, using Typeable
and :~:
.
These are intended to be used in a test suite (and exclusively in a test
suite) to create monomorphic implementations of polymorphic functions.
Specifically, this is intended to be used with a package like
test-fixture to stub out
polymorphic typeclass methods with monomorphic implementations.
For example, consider the following typeclass:
class Monad m => MonadDB m where get :: DBRecord r => Id r -> m [r] ...
The get
method might be used in another function to retrieve a record of a
specific type, such as a User
. In a test, it might be useful to stub out
the get
method to provide a well-known user:
let fixture = def { _get = \_ -> User { ... } }
However, this will not typecheck, since the type of record should be chosen
by the caller of get
. We might know that the type is guaranteed to be
User
in this particular case, but GHC cannot prove that, and it will reject
attempts to write a stubbed implementation.
To work around this issue, we can effectively defer the type error to runtime
by using the functions in this module. For example, we can use
withAssertEqT
to assert that the types are the same:
{-# LANGUAGE ScopedTypeVariables, TypeApplications #-} let fixture = def { _get = \(_ :: Id r) -> withAssertEqT @r @User $ User { ... } }
This will properly convince GHC that the User
value will only be returned
when the argument is actually an Id User
. If it isn’t, withAssertEqT
will
throw.
- assertHasT :: forall b a. (HasCallStack, Show a, Typeable a, Typeable b) => a -> a :~: b
- withAssertHasT :: forall b a c. (HasCallStack, Show a, Typeable a, Typeable b) => a -> (a ~ b => c) -> c
- assertEqT :: forall a b. (HasCallStack, Typeable a, Typeable b) => a :~: b
- withAssertEqT :: forall a b c. (HasCallStack, Typeable a, Typeable b) => (a ~ b => c) -> c
- data (k :~: a) b :: forall k. k -> k -> * where
Documentation
assertHasT :: forall b a. (HasCallStack, Show a, Typeable a, Typeable b) => a -> a :~: b Source #
Asserts that a value has a particular type, and raises an exception if it does not.
>>>
assertHasT @Bool True
Refl>>>
assertHasT @Bool "hello"
*** Exception: expected value of type ‘Bool’, but got ‘"hello"’, which is of type ‘[Char]’
withAssertHasT :: forall b a c. (HasCallStack, Show a, Typeable a, Typeable b) => a -> (a ~ b => c) -> c Source #
Like assertHasT
, but instead of returning a witness upon success,
withAssertHasT
returns its second argument. The second argument can be an
expression that typechecks under the assumption that a ~ b
.
foo :: (Show a, Typeable a) => a -> a foo x = withAssertHasT @String x $ map toUpper x
>>>
foo "hello"
"HELLO">>>
foo True
*** Exception: expected value of type ‘[Char]’, but got ‘True’, which is of type ‘Bool’ CallStack (from HasCallStack): withAssertHasT, called at <interactive>:17:13 in interactive:Ghci1
assertEqT :: forall a b. (HasCallStack, Typeable a, Typeable b) => a :~: b Source #
Like assertHasT
, but asserts that two types are the same instead of
asserting that a value has a type. Generally, prefer assertHasT
when
possible, since it will produce better error messages, but assertEqT
can be
necessary when the type does not have a runtime representation (such as if it
is phantom).
>>>
assertEqT @Bool @Bool
Refl>>>
assertEqT @Bool @Int
*** Exception: expected type ‘Int’, but got type ‘Bool’
withAssertEqT :: forall a b c. (HasCallStack, Typeable a, Typeable b) => (a ~ b => c) -> c Source #
Like assertEqT
but with the type propogation behavior of
withAssertHasT
. Generally, prefer withAssertHasT
when possible, since it
will produce better error messages, but withAssertEqT
can be necessary when
the type does not have a runtime representation (such as if it is phantom).
foo :: forall a proxy. (Show a, Typeable a) => proxy a -> a foo _ = withAssertEqT @Bool @a True
>>>
foo (Proxy @Bool)
True>>>
foo (Proxy @Int)
*** Exception: expected type ‘Int’, but got type ‘Bool’
data (k :~: a) b :: forall k. k -> k -> * where infix 4 #
Propositional equality. If a :~: b
is inhabited by some terminating
value, then the type a
is the same as the type b
. To use this equality
in practice, pattern-match on the a :~: b
to get out the Refl
constructor;
in the body of the pattern-match, the compiler knows that a ~ b
.
Since: 4.7.0.0