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)

Methods

id :: Coercion k a a

(.) :: Coercion k b c -> Coercion k a b -> Coercion k a c

TestCoercion k (Coercion k a)

Methods

testCoercion :: Coercion k a b -> Coercion k a c -> Maybe (Coercion k b c)

Coercible k a b => Bounded (Coercion k a b)

Methods

minBound :: Coercion k a b

maxBound :: Coercion k a b

Coercible k a b => Enum (Coercion k a b)

Methods

succ :: Coercion k a b -> Coercion k a b

pred :: Coercion k a b -> Coercion k a b

toEnum :: Int -> Coercion k a b

fromEnum :: Coercion k a b -> Int

enumFrom :: Coercion k a b -> [Coercion k a b]

enumFromThen :: Coercion k a b -> Coercion k a b -> [Coercion k a b]

enumFromTo :: Coercion k a b -> Coercion k a b -> [Coercion k a b]

enumFromThenTo :: Coercion k a b -> Coercion k a b -> Coercion k a b -> [Coercion k a b]

Eq (Coercion k a b)

Methods

(==) :: Coercion k a b -> Coercion k a b -> Bool

(/=) :: Coercion k a b -> Coercion k a b -> Bool

(Coercible * a b, Data a, Data b) => Data (Coercion * a b)

Methods

gfoldl :: (forall d e. Data d => c (d -> e) -> d -> c e) -> (forall g. g -> c g) -> Coercion * a b -> c (Coercion * a b)

gunfold :: (forall d r. Data d => c (d -> r) -> c r) -> (forall r. r -> c r) -> Constr -> c (Coercion * a b)

toConstr :: Coercion * a b -> Constr

dataTypeOf :: Coercion * a b -> DataType

dataCast1 :: Typeable (* -> *) t => (forall d. Data d => c (t d)) -> Maybe (c (Coercion * a b))

dataCast2 :: Typeable (* -> * -> *) t => (forall d e. (Data d, Data e) => c (t d e)) -> Maybe (c (Coercion * a b))

gmapT :: (forall c. Data c => c -> c) -> Coercion * a b -> Coercion * a b

gmapQl :: (r -> r' -> r) -> r -> (forall d. Data d => d -> r') -> Coercion * a b -> r

gmapQr :: (r' -> r -> r) -> r -> (forall d. Data d => d -> r') -> Coercion * a b -> r

gmapQ :: (forall d. Data d => d -> u) -> Coercion * a b -> [u]

gmapQi :: Int -> (forall d. Data d => d -> u) -> Coercion * a b -> u

gmapM :: Monad m => (forall d. Data d => d -> m d) -> Coercion * a b -> m (Coercion * a b)

gmapMp :: MonadPlus m => (forall d. Data d => d -> m d) -> Coercion * a b -> m (Coercion * a b)

gmapMo :: MonadPlus m => (forall d. Data d => d -> m d) -> Coercion * a b -> m (Coercion * a b)

Ord (Coercion k a b)

Methods

compare :: Coercion k a b -> Coercion k a b -> Ordering

(<) :: Coercion k a b -> Coercion k a b -> Bool

(<=) :: Coercion k a b -> Coercion k a b -> Bool

(>) :: Coercion k a b -> Coercion k a b -> Bool

(>=) :: Coercion k a b -> Coercion k a b -> Bool

max :: Coercion k a b -> Coercion k a b -> Coercion k a b

min :: Coercion k a b -> Coercion k a b -> Coercion k a b

Coercible k a b => Read (Coercion k a b)

Methods

readsPrec :: Int -> ReadS (Coercion k a b)

readList :: ReadS [Coercion k a b]

readPrec :: ReadPrec (Coercion k a b)

readListPrec :: ReadPrec [Coercion k a b]

Show (Coercion k a b)

Methods

showsPrec :: Int -> Coercion k a b -> ShowS

show :: Coercion k a b -> String

showList :: [Coercion k a b] -> ShowS

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

Type-safe cast, using representational equality

sym :: forall 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)

Methods

testCoercion :: Coercion k a b -> Coercion k a c -> Maybe (Coercion k b c)

TestCoercion k ((:~:) k a)

Methods

testCoercion :: (k :~: a) b -> (k :~: a) c -> Maybe (Coercion k b c)