License	BSD-style (see the LICENSE file in the distribution)
Maintainer	libraries@haskell.org
Stability	experimental
Portability	not portable
Safe Haskell	None
Language	Haskell2010

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)
Methods id :: cat a a Source (.) :: cat b c -> cat a b -> cat a c Source
TestCoercion k (Coercion k a)
Methods testCoercion :: f a -> f b -> Maybe (Coercion (Coercion k a) a b) Source
Coercible k a b => Bounded (Coercion k a b)
Methods minBound :: Coercion k a b Source maxBound :: Coercion k a b Source
Coercible k a b => Enum (Coercion k a b)
Methods succ :: Coercion k a b -> Coercion k a b Source pred :: Coercion k a b -> Coercion k a b Source toEnum :: Int -> Coercion k a b Source fromEnum :: Coercion k a b -> Int Source enumFrom :: Coercion k a b -> [Coercion k a b] Source enumFromThen :: Coercion k a b -> Coercion k a b -> [Coercion k a b] Source enumFromTo :: Coercion k a b -> Coercion k a b -> [Coercion k a b] Source enumFromThenTo :: Coercion k a b -> Coercion k a b -> Coercion k a b -> [Coercion k a b] Source
Eq (Coercion k a b)
Methods (==) :: Coercion k a b -> Coercion k a b -> Bool Source (/=) :: Coercion k a b -> Coercion k a b -> Bool Source
(Coercible (TYPE Lifted) a b, Data a, Data b) => Data (Coercion (TYPE Lifted) a b)
Methods gfoldl :: (forall d c. Data d => c (d -> c) -> d -> c c) -> (forall g. g -> c g) -> Coercion (TYPE Lifted) a b -> c (Coercion (TYPE Lifted) a b) Source gunfold :: (forall c r. Data c => c (c -> r) -> c r) -> (forall r. r -> c r) -> Constr -> c (Coercion (TYPE Lifted) a b) Source toConstr :: Coercion (TYPE Lifted) a b -> Constr Source dataTypeOf :: Coercion (TYPE Lifted) a b -> DataType Source dataCast1 :: Typeable (TYPE Lifted -> TYPE Lifted) t => (forall d. Data d => c (t d)) -> Maybe (c (Coercion (TYPE Lifted) a b)) Source dataCast2 :: Typeable (TYPE Lifted -> TYPE Lifted -> TYPE Lifted) t => (forall d e. (Data d, Data e) => c (t d e)) -> Maybe (c (Coercion (TYPE Lifted) a b)) Source gmapT :: (forall c. Data c => c -> c) -> Coercion (TYPE Lifted) a b -> Coercion (TYPE Lifted) a b Source gmapQl :: (r -> r' -> r) -> r -> (forall d. Data d => d -> r') -> Coercion (TYPE Lifted) a b -> r Source gmapQr :: (r' -> r -> r) -> r -> (forall d. Data d => d -> r') -> Coercion (TYPE Lifted) a b -> r Source gmapQ :: (forall d. Data d => d -> u) -> Coercion (TYPE Lifted) a b -> [u] Source gmapQi :: Int -> (forall d. Data d => d -> u) -> Coercion (TYPE Lifted) a b -> u Source gmapM :: Monad m => (forall d. Data d => d -> m d) -> Coercion (TYPE Lifted) a b -> m (Coercion (TYPE Lifted) a b) Source gmapMp :: MonadPlus m => (forall d. Data d => d -> m d) -> Coercion (TYPE Lifted) a b -> m (Coercion (TYPE Lifted) a b) Source gmapMo :: MonadPlus m => (forall d. Data d => d -> m d) -> Coercion (TYPE Lifted) a b -> m (Coercion (TYPE Lifted) a b) Source
Ord (Coercion k a b)
Methods compare :: Coercion k a b -> Coercion k a b -> Ordering Source (<) :: Coercion k a b -> Coercion k a b -> Bool Source (<=) :: Coercion k a b -> Coercion k a b -> Bool Source (>) :: Coercion k a b -> Coercion k a b -> Bool Source (>=) :: Coercion k a b -> Coercion k a b -> Bool Source max :: Coercion k a b -> Coercion k a b -> Coercion k a b Source min :: Coercion k a b -> Coercion k a b -> Coercion k a b Source
Coercible k a b => Read (Coercion k a b)
Methods readsPrec :: Int -> ReadS (Coercion k a b) Source readList :: ReadS [Coercion k a b] Source readPrec :: ReadPrec (Coercion k a b) Source readListPrec :: ReadPrec [Coercion k a b] Source
Show (Coercion k a b)
Methods showsPrec :: Int -> Coercion k a b -> ShowS Source show :: Coercion k a b -> String Source showList :: [Coercion k a b] -> ShowS Source

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

Type-safe cast, using representational equality

sym :: 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.

Minimal complete definition

testCoercion

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)
Methods testCoercion :: f a -> f b -> Maybe (Coercion (Coercion k a) a b) Source
TestCoercion k ((:~:) k a)
Methods testCoercion :: f a -> f b -> Maybe (Coercion (k :~: a) a b) Source