base-4.8.2.0: Basic libraries

Data.Type.Coercion

Description

Definition of representational equality (`Coercion`).

Since: 4.7.0.0

Synopsis

# Documentation

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.

Since: 4.7.0.0

Constructors

 Coercion :: Coercible a b => Coercion a b

Instances

 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.

Methods

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

Conditionally prove the representational equality of `a` and `b`.

Instances

 TestCoercion k (Coercion k a) TestCoercion k ((:~:) k a)