Data.Type.Equality

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 type

data a :~: b where infix 4

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)

Methods

id :: (:~:) k a a

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

TestEquality k ((:~:) k a)

Methods

testEquality :: (:~:) k a b -> (:~:) k a c -> Maybe ((:~:) k b c)

TestCoercion k ((:~:) k a)

Methods

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

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

Methods

minBound :: (:~:) k a b

maxBound :: (:~:) k a b

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

Methods

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

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

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

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

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

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

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

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

Eq ((:~:) k a b)

Methods

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

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

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

Methods

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

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

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

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

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

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

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

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

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

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

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

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

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

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

Ord ((:~:) k a b)

Methods

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

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

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

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

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

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

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

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

Methods

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

readList :: ReadS [(:~:) k a b]

readPrec :: ReadPrec ((:~:) k a b)

readListPrec :: ReadPrec [(:~:) k a b]

Show ((:~:) k a b)

Methods

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

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

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

Working with equality

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

Symmetry of equality

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

Transitivity of equality

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

Type-safe cast, using propositional equality

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

Generalized form of type-safe cast using propositional equality

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

Apply one equality to another, respectively

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

Extract equality of the arguments from an equality of a applied types

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

Extract equality of type constructors from an equality of applied types

Inferring equality from other types

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

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

Conditionally prove the equality of a and b.

Instances

TestEquality k ((:~:) k a)

Methods

testEquality :: (:~:) k a b -> (:~:) k a c -> Maybe ((:~:) k b c)

Boolean type-level equality

type family a == b :: Bool infix 4

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 (==) Ordering a b

type (==) * a b

type (==) Nat a b

type (==) Symbol a b

type (==) () a b

type (==) [k] a b

type (==) (Maybe k) a b

type (==) (k -> k1) a b

type (==) (Either k k1) a b

type (==) ((,) k k1) a b

type (==) ((,,) k k1 k2) a b

type (==) ((,,,) k k1 k2 k3) a b

type (==) ((,,,,) k k1 k2 k3 k4) a b

type (==) ((,,,,,) k k1 k2 k3 k4 k5) a b

type (==) ((,,,,,,) k k1 k2 k3 k4 k5 k6) a b

type (==) ((,,,,,,,) k k1 k2 k3 k4 k5 k6 k7) a b

type (==) ((,,,,,,,,) k k1 k2 k3 k4 k5 k6 k7 k8) a b

type (==) ((,,,,,,,,,) k k1 k2 k3 k4 k5 k6 k7 k8 k9) a b

type (==) ((,,,,,,,,,,) k k1 k2 k3 k4 k5 k6 k7 k8 k9 k10) a b

type (==) ((,,,,,,,,,,,) k k1 k2 k3 k4 k5 k6 k7 k8 k9 k10 k11) a b

type (==) ((,,,,,,,,,,,,) k k1 k2 k3 k4 k5 k6 k7 k8 k9 k10 k11 k12) a b

type (==) ((,,,,,,,,,,,,,) k k1 k2 k3 k4 k5 k6 k7 k8 k9 k10 k11 k12 k13) a b

type (==) ((,,,,,,,,,,,,,,) k k1 k2 k3 k4 k5 k6 k7 k8 k9 k10 k11 k12 k13 k14) a b