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

data Coercion a b where
- Coercion :: Coercible a b => Coercion a b
coerceWith :: Coercion a b -> a -> b
gcoerceWith :: Coercion a b -> (Coercible a b => r) -> r
sym :: Coercion a b -> Coercion b a
trans :: Coercion a b -> Coercion b c -> Coercion a c
repr :: (a :~: b) -> Coercion a b
class TestCoercion f where

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

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

Type-safe cast, using representational equality

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

Generalized form of type-safe cast using representational equality

Since: 4.10.0.0

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 (Coercion a :: k -> *) #	Since: 4.7.0.0
Instance details Methods testCoercion :: Coercion a a0 -> Coercion a b -> Maybe (Coercion a0 b) Source #
TestCoercion ((:~:) a :: k -> *) #	Since: 4.7.0.0
Instance details Methods testCoercion :: (a :~: a0) -> (a :~: b) -> Maybe (Coercion a0 b) Source #
TestCoercion ((:~~:) a :: k -> *) #	Since: 4.10.0.0
Instance details Methods testCoercion :: (a :~~: a0) -> (a :~~: b) -> Maybe (Coercion a0 b) Source #