base-4.19.0.0: Basic libraries

Data.Type.Coercion

Description

Definition of representational equality (Coercion).

Since: base-4.7.0.0

Synopsis

# Documentation

data Coercion (a :: k) (b :: k) 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: base-4.7.0.0

Constructors

 Coercion :: forall {k} (a :: k) (b :: k). Coercible a b => Coercion a b

#### Instances

Instances details
 Category (Coercion :: k -> k -> Type) Source # Since: base-4.7.0.0 Instance detailsDefined in Control.Category Methodsid :: forall (a :: k). Coercion a a Source #(.) :: forall (b :: k) (c :: k) (a :: k). Coercion b c -> Coercion a b -> Coercion a c Source # TestCoercion (Coercion a :: k -> Type) Source # Since: base-4.7.0.0 Instance detailsDefined in Data.Type.Coercion MethodstestCoercion :: forall (a0 :: k) (b :: k). Coercion a a0 -> Coercion a b -> Maybe (Coercion a0 b) Source # (Coercible a b, Data a, Data b) => Data (Coercion a b) Source # Since: base-4.7.0.0 Instance detailsDefined in Data.Data Methodsgfoldl :: (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 #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 :: forall r r'. (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 # Coercible a b => Bounded (Coercion a b) Source # Since: base-4.7.0.0 Instance detailsDefined in Data.Type.Coercion Methods Coercible a b => Enum (Coercion a b) Source # Since: base-4.7.0.0 Instance detailsDefined in Data.Type.Coercion Methodssucc :: 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 # Coercible a b => Read (Coercion a b) Source # Since: base-4.7.0.0 Instance detailsDefined in Data.Type.Coercion MethodsreadsPrec :: Int -> ReadS (Coercion a b) Source #readList :: ReadS [Coercion a b] Source # Show (Coercion a b) Source # Since: base-4.7.0.0 Instance detailsDefined in Data.Type.Coercion MethodsshowsPrec :: Int -> Coercion a b -> ShowS Source #show :: Coercion a b -> String Source #showList :: [Coercion a b] -> ShowS Source # Eq (Coercion a b) Source # Since: base-4.7.0.0 Instance detailsDefined in Data.Type.Coercion Methods(==) :: Coercion a b -> Coercion a b -> Bool Source #(/=) :: Coercion a b -> Coercion a b -> Bool Source # Ord (Coercion a b) Source # Since: base-4.7.0.0 Instance detailsDefined in Data.Type.Coercion Methodscompare :: 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 #

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

Type-safe cast, using representational equality

gcoerceWith :: forall {k} (a :: k) (b :: k) r. Coercion a b -> (Coercible a b => r) -> r Source #

Generalized form of type-safe cast using representational equality

Since: base-4.10.0.0

sym :: forall {k} (a :: k) (b :: k). Coercion a b -> Coercion b a Source #

Symmetry of representational equality

trans :: forall {k} (a :: k) (b :: k) (c :: k). Coercion a b -> Coercion b c -> Coercion a c Source #

Transitivity of representational equality

repr :: forall {k} (a :: k) (b :: k). (a :~: b) -> Coercion a b Source #

Convert propositional (nominal) equality to representational equality

class TestCoercion (f :: k -> Type) 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.

Methods

testCoercion :: forall (a :: k) (b :: k). f a -> f b -> Maybe (Coercion a b) Source #

Conditionally prove the representational equality of a and b.

#### Instances

Instances details
 Source # Since: base-4.18.0.0 Instance detailsDefined in GHC.TypeNats MethodstestCoercion :: forall (a :: Nat) (b :: Nat). SNat a -> SNat b -> Maybe (Coercion a b) Source # Source # Since: base-4.18.0.0 Instance detailsDefined in GHC.TypeLits MethodstestCoercion :: forall (a :: Char) (b :: Char). SChar a -> SChar b -> Maybe (Coercion a b) Source # Source # Since: base-4.18.0.0 Instance detailsDefined in GHC.TypeLits MethodstestCoercion :: forall (a :: Symbol) (b :: Symbol). SSymbol a -> SSymbol b -> Maybe (Coercion a b) Source # TestCoercion (Coercion a :: k -> Type) Source # Since: base-4.7.0.0 Instance detailsDefined in Data.Type.Coercion MethodstestCoercion :: forall (a0 :: k) (b :: k). Coercion a a0 -> Coercion a b -> Maybe (Coercion a0 b) Source # TestCoercion ((:~:) a :: k -> Type) Source # Since: base-4.7.0.0 Instance detailsDefined in Data.Type.Coercion MethodstestCoercion :: forall (a0 :: k) (b :: k). (a :~: a0) -> (a :~: b) -> Maybe (Coercion a0 b) Source # TestCoercion ((:~~:) a :: k -> Type) Source # Since: base-4.10.0.0 Instance detailsDefined in Data.Type.Coercion MethodstestCoercion :: forall (a0 :: k) (b :: k). (a :~~: a0) -> (a :~~: b) -> Maybe (Coercion a0 b) Source #