# Data.Type.Equality

#### Description

Definition of propositional equality `(:~:)`. Pattern-matching on a variable of type `(a :~: b)` produces a proof that `a ~ b`.

Since: 4.7.0.0

## The equality types

data a :~: b where infix 4 Source

Propositional equality. If `a :~: b` is inhabited by some terminating value, then the type `a` is the same as the type `b`. To use this equality in practice, pattern-match on the `a :~: b` to get out the `Refl` constructor; in the body of the pattern-match, the compiler knows that `a ~ b`.

Since: 4.7.0.0

#### Constructors

 Refl :: a :~: a

#### Instances

Category k ((:~:) k)

Since: 4.7.0.0

#### Methods

id :: cat a a Source

(.) :: cat b c -> cat a b -> cat a c Source

TestEquality k ((:~:) k a)

Since: 4.7.0.0

#### Methods

testEquality :: f a -> f b -> Maybe (((k :~: a) :~: a) b) Source

TestCoercion k ((:~:) k a)

Since: 4.7.0.0

#### Methods

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

(~) k a b => Bounded ((:~:) k a b)

Since: 4.7.0.0

#### Methods

minBound :: (k :~: a) b Source

maxBound :: (k :~: a) b Source

(~) k a b => Enum ((:~:) k a b)

Since: 4.7.0.0

#### Methods

succ :: (k :~: a) b -> (k :~: a) b Source

pred :: (k :~: a) b -> (k :~: a) b Source

toEnum :: Int -> (k :~: a) b Source

fromEnum :: (k :~: a) b -> Int Source

enumFrom :: (k :~: a) b -> [(k :~: a) b] Source

enumFromThen :: (k :~: a) b -> (k :~: a) b -> [(k :~: a) b] Source

enumFromTo :: (k :~: a) b -> (k :~: a) b -> [(k :~: a) b] Source

enumFromThenTo :: (k :~: a) b -> (k :~: a) b -> (k :~: a) b -> [(k :~: a) b] Source

Eq ((:~:) k a b)

#### Methods

(==) :: (k :~: a) b -> (k :~: a) b -> Bool Source

(/=) :: (k :~: a) b -> (k :~: a) b -> Bool Source

((~) * a b, Data a) => Data ((:~:) * a b)

Since: 4.7.0.0

#### Methods

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

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

toConstr :: (* :~: a) b -> Constr Source

dataTypeOf :: (* :~: a) b -> DataType Source

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

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

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

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

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

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

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

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

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

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

Ord ((:~:) k a b)

#### Methods

compare :: (k :~: a) b -> (k :~: a) b -> Ordering Source

(<) :: (k :~: a) b -> (k :~: a) b -> Bool Source

(<=) :: (k :~: a) b -> (k :~: a) b -> Bool Source

(>) :: (k :~: a) b -> (k :~: a) b -> Bool Source

(>=) :: (k :~: a) b -> (k :~: a) b -> Bool Source

max :: (k :~: a) b -> (k :~: a) b -> (k :~: a) b Source

min :: (k :~: a) b -> (k :~: a) b -> (k :~: a) b Source

(~) k a b => Read ((:~:) k a b)

Since: 4.7.0.0

#### Methods

Show ((:~:) k a b)

#### Methods

showsPrec :: Int -> (k :~: a) b -> ShowS Source

show :: (k :~: a) b -> String Source

showList :: [(k :~: a) b] -> ShowS Source

class (~#) k0 k1 a b => (k0 ~~ k1) (a :: k0) (b :: k1) Source

Lifted, heterogeneous equality. By lifted, we mean that it can be bogus (deferred type error). By heterogeneous, the two types `a` and `b` might have different kinds. Because `~~` can appear unexpectedly in error messages to users who do not care about the difference between heterogeneous equality `~~` and homogeneous equality `~`, this is printed as `~` unless `-fprint-equality-relations` is set.

data (a :: k1) :~~: (b :: k2) where infix 4 Source

Kind heterogeneous propositional equality. Like '(:~:)', `a :~~: b` is inhabited by a terminating value if and only if `a` is the same type as `b`.

Since: 4.10.0.0

#### Constructors

 HRefl :: a :~~: a

#### Instances

Category k ((:~~:) k k)

Since: 4.10.0.0

#### Methods

id :: cat a a Source

(.) :: cat b c -> cat a b -> cat a c Source

TestEquality k ((:~~:) k1 k a)

Since: 4.10.0.0

#### Methods

testEquality :: f a -> f b -> Maybe (((k1 :~~: k) a :~: a) b) Source

TestCoercion k ((:~~:) k1 k a)

Since: 4.10.0.0

#### Methods

testCoercion :: f a -> f b -> Maybe (Coercion ((k1 :~~: k) a) a b) Source

(~~) k1 k2 a b => Bounded ((:~~:) k1 k2 a b)

Since: 4.10.0.0

#### Methods

minBound :: (k1 :~~: k2) a b Source

maxBound :: (k1 :~~: k2) a b Source

(~~) k1 k2 a b => Enum ((:~~:) k1 k2 a b)

Since: 4.10.0.0

#### Methods

succ :: (k1 :~~: k2) a b -> (k1 :~~: k2) a b Source

pred :: (k1 :~~: k2) a b -> (k1 :~~: k2) a b Source

toEnum :: Int -> (k1 :~~: k2) a b Source

fromEnum :: (k1 :~~: k2) a b -> Int Source

enumFrom :: (k1 :~~: k2) a b -> [(k1 :~~: k2) a b] Source

enumFromThen :: (k1 :~~: k2) a b -> (k1 :~~: k2) a b -> [(k1 :~~: k2) a b] Source

enumFromTo :: (k1 :~~: k2) a b -> (k1 :~~: k2) a b -> [(k1 :~~: k2) a b] Source

enumFromThenTo :: (k1 :~~: k2) a b -> (k1 :~~: k2) a b -> (k1 :~~: k2) a b -> [(k1 :~~: k2) a b] Source

Eq ((:~~:) k1 k2 a b)

Since: 4.10.0.0

#### Methods

(==) :: (k1 :~~: k2) a b -> (k1 :~~: k2) a b -> Bool Source

(/=) :: (k1 :~~: k2) a b -> (k1 :~~: k2) a b -> Bool Source

(Typeable * i2, Typeable * j2, Typeable i2 a, Typeable j2 b, (~~) i2 j2 a b) => Data ((:~~:) i2 j2 a b)

Since: 4.10.0.0

#### Methods

gfoldl :: (forall d c. Data d => c (d -> c) -> d -> c c) -> (forall g. g -> c g) -> (i2 :~~: j2) a b -> c ((i2 :~~: j2) a b) Source

gunfold :: (forall c r. Data c => c (c -> r) -> c r) -> (forall r. r -> c r) -> Constr -> c ((i2 :~~: j2) a b) Source

toConstr :: (i2 :~~: j2) a b -> Constr Source

dataTypeOf :: (i2 :~~: j2) a b -> DataType Source

dataCast1 :: Typeable (* -> *) t => (forall d. Data d => c (t d)) -> Maybe (c ((i2 :~~: j2) a b)) Source

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

gmapT :: (forall c. Data c => c -> c) -> (i2 :~~: j2) a b -> (i2 :~~: j2) a b Source

gmapQl :: (r -> r' -> r) -> r -> (forall d. Data d => d -> r') -> (i2 :~~: j2) a b -> r Source

gmapQr :: (r' -> r -> r) -> r -> (forall d. Data d => d -> r') -> (i2 :~~: j2) a b -> r Source

gmapQ :: (forall d. Data d => d -> u) -> (i2 :~~: j2) a b -> [u] Source

gmapQi :: Int -> (forall d. Data d => d -> u) -> (i2 :~~: j2) a b -> u Source

gmapM :: Monad m => (forall d. Data d => d -> m d) -> (i2 :~~: j2) a b -> m ((i2 :~~: j2) a b) Source

gmapMp :: MonadPlus m => (forall d. Data d => d -> m d) -> (i2 :~~: j2) a b -> m ((i2 :~~: j2) a b) Source

gmapMo :: MonadPlus m => (forall d. Data d => d -> m d) -> (i2 :~~: j2) a b -> m ((i2 :~~: j2) a b) Source

Ord ((:~~:) k1 k2 a b)

Since: 4.10.0.0

#### Methods

compare :: (k1 :~~: k2) a b -> (k1 :~~: k2) a b -> Ordering Source

(<) :: (k1 :~~: k2) a b -> (k1 :~~: k2) a b -> Bool Source

(<=) :: (k1 :~~: k2) a b -> (k1 :~~: k2) a b -> Bool Source

(>) :: (k1 :~~: k2) a b -> (k1 :~~: k2) a b -> Bool Source

(>=) :: (k1 :~~: k2) a b -> (k1 :~~: k2) a b -> Bool Source

max :: (k1 :~~: k2) a b -> (k1 :~~: k2) a b -> (k1 :~~: k2) a b Source

min :: (k1 :~~: k2) a b -> (k1 :~~: k2) a b -> (k1 :~~: k2) a b Source

(~~) k1 k2 a b => Read ((:~~:) k1 k2 a b)

Since: 4.10.0.0

#### Methods

Show ((:~~:) k1 k2 a b)

Since: 4.10.0.0

#### Methods

showsPrec :: Int -> (k1 :~~: k2) a b -> ShowS Source

show :: (k1 :~~: k2) a b -> String Source

showList :: [(k1 :~~: k2) a b] -> ShowS Source

## Working with equality

sym :: (a :~: b) -> b :~: a Source

Symmetry of equality

trans :: (a :~: b) -> (b :~: c) -> a :~: c Source

Transitivity of equality

castWith :: (a :~: b) -> a -> b Source

Type-safe cast, using propositional equality

gcastWith :: (a :~: b) -> (a ~ b => r) -> r Source

Generalized form of type-safe cast using propositional equality

apply :: (f :~: g) -> (a :~: b) -> f a :~: g b Source

Apply one equality to another, respectively

inner :: (f a :~: g b) -> a :~: b Source

Extract equality of the arguments from an equality of applied types

outer :: (f a :~: g b) -> f :~: g Source

Extract equality of type constructors from an equality of applied types

## Inferring equality from other types

class TestEquality 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.

testEquality

#### Methods

testEquality :: f a -> f b -> Maybe (a :~: b) Source

Conditionally prove the equality of `a` and `b`.

#### Instances

TestEquality k (TypeRep k)

#### Methods

testEquality :: f a -> f b -> Maybe ((TypeRep k :~: a) b) Source

TestEquality k ((:~:) k a)

Since: 4.7.0.0

#### Methods

testEquality :: f a -> f b -> Maybe (((k :~: a) :~: a) b) Source

TestEquality k ((:~~:) k1 k a)

Since: 4.10.0.0

#### Methods

testEquality :: f a -> f b -> Maybe (((k1 :~~: k) a :~: a) b) Source

## Boolean type-level equality

type family (a :: k) == (b :: k) :: Bool infix 4 Source

A type family to compute Boolean equality. Instances are provided only for open kinds, such as `*` and function kinds. Instances are also provided for datatypes exported from base. A poly-kinded instance is not provided, as a recursive definition for algebraic kinds is generally more useful.

#### Instances

 type (==) Bool a b type (==) Bool a b type (==) Ordering a b type (==) Ordering a b type (==) * a b type (==) * a b type (==) Nat a b type (==) Nat a b type (==) Symbol a b type (==) Symbol a b type (==) () a b type (==) () a b type (==) [k] a b type (==) [k] a b type (==) (Maybe k) a b type (==) (Maybe k) a b type (==) (k1 -> k2) a b type (==) (k1 -> k2) a b type (==) (Either k1 k2) a b type (==) (Either k1 k2) a b type (==) (k1, k2) a b type (==) (k1, k2) a b type (==) (k1, k2, k3) a b type (==) (k1, k2, k3) a b type (==) (k1, k2, k3, k4) a b type (==) (k1, k2, k3, k4) a b type (==) (k1, k2, k3, k4, k5) a b type (==) (k1, k2, k3, k4, k5) a b type (==) (k1, k2, k3, k4, k5, k6) a b type (==) (k1, k2, k3, k4, k5, k6) a b type (==) (k1, k2, k3, k4, k5, k6, k7) a b type (==) (k1, k2, k3, k4, k5, k6, k7) a b type (==) (k1, k2, k3, k4, k5, k6, k7, k8) a b type (==) (k1, k2, k3, k4, k5, k6, k7, k8) a b type (==) (k1, k2, k3, k4, k5, k6, k7, k8, k9) a b type (==) (k1, k2, k3, k4, k5, k6, k7, k8, k9) a b type (==) (k1, k2, k3, k4, k5, k6, k7, k8, k9, k10) a b type (==) (k1, k2, k3, k4, k5, k6, k7, k8, k9, k10) a b type (==) (k1, k2, k3, k4, k5, k6, k7, k8, k9, k10, k11) a b type (==) (k1, k2, k3, k4, k5, k6, k7, k8, k9, k10, k11) a b type (==) (k1, k2, k3, k4, k5, k6, k7, k8, k9, k10, k11, k12) a b type (==) (k1, k2, k3, k4, k5, k6, k7, k8, k9, k10, k11, k12) a b type (==) (k1, k2, k3, k4, k5, k6, k7, k8, k9, k10, k11, k12, k13) a b type (==) (k1, k2, k3, k4, k5, k6, k7, k8, k9, k10, k11, k12, k13) a b type (==) (k1, k2, k3, k4, k5, k6, k7, k8, k9, k10, k11, k12, k13, k14) a b type (==) (k1, k2, k3, k4, k5, k6, k7, k8, k9, k10, k11, k12, k13, k14) a b type (==) (k1, k2, k3, k4, k5, k6, k7, k8, k9, k10, k11, k12, k13, k14, k15) a b type (==) (k1, k2, k3, k4, k5, k6, k7, k8, k9, k10, k11, k12, k13, k14, k15) a b

© The University of Glasgow and others