Data.Type.Coercion

Definition of representational equality (Coercion).

Since: 4.7.0.0

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

Constructors

Coercion ∷ Coercible a b ⇒ Coercion a b

Instances

Category k (Coercion k)

TestCoercion k (Coercion k a)

Typeable (k → k → ★) (Coercion k)

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

Type-safe cast, using representational equality

sym ∷ ∀ a b. 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

TestCoercion k (Coercion k a)

TestCoercion k ((:~:) k a)