-- Hoogle documentation, generated by Haddock
-- See Hoogle, http://www.haskell.org/hoogle/


-- | Type equality, coercion/cast and other operations.
--   
--   In the presence of GADTs, sometimes a proof is needed that two types
--   are equal. This package contains an equality type for this purpose,
--   plus its properties (reflexive, symmetric, transitive) and some useful
--   operations (substitution, congruence, coercion/cast). It also contains
--   a type class for producing equality proofs, providing some form of
--   decidable equality on types.
@package type-equality
@version 0.1.2


-- | Type equality, coercion/cast and other operations.
module Data.Type.Equality

-- | Type equality. A value of <tt>a :=: b</tt> is a proof that types
--   <tt>a</tt> and <tt>b</tt> are equal. By pattern matching on
--   <tt>Refl</tt> this fact is introduced to the type checker.
data (:=:) a b
Refl :: a :=: a

-- | Equality is symmetric.
sym :: a :=: b -> b :=: a

-- | Equality is transitive. This is the same as (&gt;&gt;&gt;) from the
--   <a>Category</a> instance, but also works in GHC 6.8.
trans :: a :=: b -> b :=: c -> a :=: c

-- | Equality is substitutive. This is defined directly, but can also be
--   defined as <a>coerce</a> <a>.</a> <a>cong</a>.
subst :: a :=: b -> f a -> f b

-- | Substitution inside nested type constructors. This is equivalent to
--   <a>coerce</a> <a>.</a> <a>cong</a> <a>.</a> <a>cong</a>.
subst2 :: a :=: b -> f (g a) -> f (g b)

-- | Equality is congruential.
cong :: a :=: b -> f a :=: f b

-- | Congruence for type constructors with two parameters.
cong2 :: a :=: b -> c :=: d -> f a c :=: f b d

-- | Congruence for type constructors with three parameters.
cong3 :: a :=: a' -> b :=: b' -> c :=: c' -> f a b c :=: f a' b' c'

-- | Coerce a type to another using an equality proof.
coerce :: a :=: b -> a -> b

-- | A type class for constructing equality proofs. This is as close as we
--   can get to decidable equality on types. Note that <tt>f</tt> must be a
--   GADT to be able to define <a>eqT</a>.
class EqT f
eqT :: EqT f => f a -> f b -> Maybe (a :=: b)

-- | A type class for constructing equality proofs for type constructor
--   with two parameters. Can be useful when representing relations between
--   types.
class EqT2 f
eqT2 :: EqT2 f => f a b -> f c d -> (Maybe (a :=: c), Maybe (b :=: d))

-- | A type class for constructing equality proofs for type constructor
--   with three parameters. If you find a use for this, let me know.
class EqT3 f
eqT3 :: EqT3 f => f a b c -> f a' b' c' -> (Maybe (a :=: a'), Maybe (b :=: b'), Maybe (c :=: c'))
instance EqT k (k :=: a)
instance Category ((:=:) *)
instance Read ((:=:) k a a)
instance Show ((:=:) k a b)