Safe Haskell  Trustworthy 

Types and combinators for storing and manipulating type equality evidence.
This module is kindpolymorphic if PolyKinds
are available (GHC 7.6+).
Notable combinators missing from this module include applyEq
, constructorEq
, and sameOuterEq
.
See also Type.Eq.Higher
and Type.Eq.Poly
.
 data a :~: b where
 withEq :: (a ~ b => r) > (a :~: b) > r
 idEq :: a :~: a
 composeEq :: (b :~: c) > (a :~: b) > a :~: c
 flipEq :: (a :~: b) > b :~: a
 argumentEq :: (f a :~: g b) > a :~: b
 cast, (>) :: a > (a :~: b) > b
 data OuterEq f a where
 data InnerEq i a where
 withOuterEq :: (forall i. f i ~ a => r) > OuterEq f a > r
 withInnerEq :: (forall f. f i ~ a => r) > InnerEq i a > r
 outerEq :: (f i :~: a) > OuterEq f a
 innerEq :: (f i :~: a) > InnerEq i a
 assembleEq :: OuterEq f a > InnerEq i a > f i :~: a
 sameInnerEq :: InnerEq i a > InnerEq j a > i :~: j
 dynamicEq :: (Typeable a, Typeable b) => Maybe (a :~: b)
 class TypeEq t where
Full equality
Evidence that type a
is the same as type b
.
The
, Functor
, and Applicative
instances of Monad
Maybe
are extremely useful for working with values of type Maybe (a :~: b)
.
withEq :: (a ~ b => r) > (a :~: b) > rSource
Unpack equality evidence and use it.
This function compiles with GHC 6.10, but doesn't work. Beware!
argumentEq :: (f a :~: g b) > a :~: bSource
Type constructors are injective
Partial equality
Evidence that f
is the outermost type constructor of a
Evidence that i
is the argument type of the outermost type constructor of a
withOuterEq :: (forall i. f i ~ a => r) > OuterEq f a > rSource
Unpack partial equality evidence and use it.
This function compiles with GHC 6.10, but doesn't work. Beware!
withInnerEq :: (forall f. f i ~ a => r) > InnerEq i a > rSource
Unpack partial equality evidence and use it.
This function compiles with GHC 6.10, but doesn't work. Beware!
assembleEq :: OuterEq f a > InnerEq i a > f i :~: aSource
sameInnerEq :: InnerEq i a > InnerEq j a > i :~: jSource
Testing for equality
dynamicEq :: (Typeable a, Typeable b) => Maybe (a :~: b)Source
Runtime type equality evidence from Typeable
Can be implemented by types storing evidence of type equalities, i.e. GADTs.
A return value of Nothing
can mean any of definite inequality, impossible arguments, or insufficient information.
Minimal complete definition: maybeEq
or (~~)
, plus either:

piecewiseMaybeEq
, or  both
maybeOuterEq
andmaybeInnerEq
. or 
(<~>)
, or  both
(~>)
and(<~)
.
maybeEq, (~~) :: t a > t b > Maybe (a :~: b)Source
maybeOuterEq, (~>) :: t (f i) > t a > Maybe (OuterEq f a)Source
maybeInnerEq, (<~) :: t (f i) > t a > Maybe (InnerEq i a)Source
piecewiseMaybeEq, (<~>) :: t (f i) > t a > (Maybe (OuterEq f a), Maybe (InnerEq i a))Source
uncurry (liftA2 assembleEq) (a <~> b) = a ~~ b