| Safe Haskell | Safe |
|---|---|
| Language | Haskell2010 |
Test.TypeAssertions
Description
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 #
Asserts that a value has a particular type, and raises an exception if it does not.
>>>assertHasT @Bool TrueRefl>>>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 #
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 #
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 @BoolRefl>>>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 #
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