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.

`>>>`

Refl`assertHasT @Bool True`

`>>>`

*** Exception: expected value of type ‘Bool’, but got ‘"hello"’, which is of type ‘[Char]’`assertHasT @Bool "hello"`

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

`>>>`

"HELLO"`foo "hello"`

`>>>`

*** 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`foo True`

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).

`>>>`

Refl`assertEqT @Bool @Bool`

`>>>`

*** Exception: expected type ‘Int’, but got type ‘Bool’`assertEqT @Bool @Int`

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

`>>>`

True`foo (Proxy @Bool)`

`>>>`

*** Exception: expected type ‘Int’, but got type ‘Bool’`foo (Proxy @Int)`

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*