base-4.13.0.0: Basic libraries

Data.Type.Coercion

Description

Definition of representational equality (Coercion).

Since: base-4.7.0.0

Synopsis

# Documentation

data Coercion a b where #

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: base-4.7.0.0

Constructors

 Coercion :: Coercible a b => Coercion a b

#### Instances

Instances details

coerceWith :: Coercion a b -> a -> b #

Type-safe cast, using representational equality

gcoerceWith :: Coercion a b -> (Coercible a b => r) -> r #

Generalized form of type-safe cast using representational equality

Since: base-4.10.0.0

sym :: Coercion a b -> Coercion b a #

Symmetry of representational equality

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

Transitivity of representational equality

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

Convert propositional (nominal) equality to representational equality

class TestCoercion f where #

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

Conditionally prove the representational equality of a and b.

#### Instances

Instances details
 TestCoercion (Coercion a :: k -> Type) # Since: base-4.7.0.0 Instance detailsDefined in Data.Type.Coercion MethodstestCoercion :: forall (a0 :: k0) (b :: k0). Coercion a a0 -> Coercion a b -> Maybe (Coercion a0 b) # TestCoercion ((:~:) a :: k -> Type) # Since: base-4.7.0.0 Instance detailsDefined in Data.Type.Coercion MethodstestCoercion :: forall (a0 :: k0) (b :: k0). (a :~: a0) -> (a :~: b) -> Maybe (Coercion a0 b) # TestCoercion ((:~~:) a :: k -> Type) # Since: base-4.10.0.0 Instance detailsDefined in Data.Type.Coercion MethodstestCoercion :: forall (a0 :: k0) (b :: k0). (a :~~: a0) -> (a :~~: b) -> Maybe (Coercion a0 b) #