/Haskell 7


License BSD-style (see the LICENSE file in the distribution)
Maintainer [email protected]
Stability experimental
Portability not portable
Safe Haskell None
Language Haskell2010


Definition of representational equality (Coercion).


data Coercion a b where Source

Representational equality. If Coercion a b is inhabited by some terminating value, then the type a has the same underlying representation as the type b.

To use this equality in practice, pattern-match on the Coercion a b to get out the Coercible a b instance, and then use coerce to apply it.



Coercion :: Coercible a b => Coercion a b


Category k (Coercion k)
TestCoercion k (Coercion k a)
Coercible k a b => Bounded (Coercion k a b)
Coercible k a b => Enum (Coercion k a b)
Eq (Coercion k a b)
(Coercible * a b, Data a, Data b) => Data (Coercion * a b)
Ord (Coercion k a b)
Coercible k a b => Read (Coercion k a b)
Show (Coercion k a b)

coerceWith :: Coercion a b -> a -> b Source

Type-safe cast, using representational equality

sym :: forall a b. Coercion a b -> Coercion b a Source

Symmetry of representational equality

trans :: Coercion a b -> Coercion b c -> Coercion a c Source

Transitivity of representational equality

repr :: (a :~: b) -> Coercion a b Source

Convert propositional (nominal) equality to representational equality

class TestCoercion f where Source

This class contains types where you can learn the equality of two types from information contained in terms. Typically, only singleton types should inhabit this class.


testCoercion :: f a -> f b -> Maybe (Coercion a b) Source

Conditionally prove the representational equality of a and b.


© The University of Glasgow and others
Licensed under a BSD-style license (see top of the page).