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


-- | Type equality evidence you can carry around
--   
@package type-eq
@version 0.5


-- | This module is kind-polymorphic if <tt>PolyKinds</tt> are available
--   (GHC 7.6+).
module Type.Eq.Unsafe

-- | Very unsafe! The same rules apply as for <a>unsafeCoerce</a>.
unsafeCoercion :: a :~: b

-- | Very unsafe!
unsafeOuterEq :: OuterEq f a

-- | Very unsafe!
unsafeInnerEq :: InnerEq i a

module Type.Eq.Higher.Unsafe

-- | Very unsafe! The same rules apply as for <a>unsafeCoerce</a>.
unsafeCoercion1 :: f ::~:: g

-- | Very unsafe! The same rules apply as for <a>unsafeCoerce</a>.
unsafeCoercion2 :: m :::~::: n

-- | Very unsafe!
unsafeOuterEq1 :: OuterEq1 m f

-- | Very unsafe!
unsafeInnerEq1 :: InnerEq1 a f


-- | Types and functions for storing and manipulating type equality
--   evidence.
--   
--   This module is kind-polymorphic if <tt>PolyKinds</tt> are available
--   (GHC 7.6+).
--   
--   Notable functions missing from this module include <tt>applyEq</tt>,
--   <tt>constructorEq</tt>, and <tt>sameOuterEq</tt>.
--   
--   See also <tt><a>Type.Eq.Higher</a></tt> and
--   <tt><a>Type.Eq.Poly</a></tt>.
module Type.Eq

-- | Evidence that <tt>a</tt> is the same type as <tt>b</tt>.
--   
--   The <tt><a>Functor</a></tt>, <tt><a>Applicative</a></tt>, and
--   <tt><a>Monad</a></tt> instances of <tt>Maybe</tt> are very useful for
--   working with values of type <tt>Maybe (a :~: b)</tt>.
data (:~:) a b
Eq :: a :~: b

-- | Unpack equality evidence and use it.
--   
--   This function compiles with GHC 6.10, but doesn't work.
withEq :: (a ~ b => r) -> (a :~: b) -> r

-- | Reflexivity
idEq :: a :~: a

-- | Transitivity
composeEq :: (b :~: c) -> (a :~: b) -> (a :~: c)

-- | Symmetry
flipEq :: (a :~: b) -> (b :~: a)

-- | Type constructors are injective
argumentEq :: (f a :~: g b) -> (a :~: b)

-- | Use equality evidence to cast between types
cast :: a -> (a :~: b) -> b

-- | Use equality evidence to cast between types
(|>) :: a -> (a :~: b) -> b

-- | Evidence that <tt>f</tt> is the outermost type constructor of
--   <tt>a</tt>
data OuterEq f a
OuterEq :: OuterEq f a

-- | Evidence that <tt>i</tt> is the argument type of the outermost type
--   constructor of <tt>a</tt>
data InnerEq i a
InnerEq :: InnerEq i a

-- | Unpack partial equality evidence and use it.
--   
--   This function compiles with GHC 6.10, but doesn't work.
withOuterEq :: (forall i. f i ~ a => r) -> OuterEq f a -> r

-- | Unpack partial equality evidence and use it.
--   
--   This function compiles with GHC 6.10, but doesn't work.
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)

-- | Can be implemented by types storing evidence of type equalities, i.e.
--   GADTs.
--   
--   A return value of <tt>Nothing</tt> can mean any of definite
--   inequality, impossible arguments, or insufficient information.
--   
--   Minimal complete definition: <tt>maybeEq</tt> or <tt>(~~)</tt>, plus
--   either:
--   
--   <ul>
--   <li><tt>piecewiseMaybeEq</tt>, or</li>
--   <li>both <tt>maybeOuterEq</tt> and <tt>maybeInnerEq</tt>. or</li>
--   <li><tt>(&lt;~&gt;)</tt>, or</li>
--   <li>both <tt>(~&gt;)</tt> and <tt>(&lt;~)</tt>.</li>
--   </ul>
--   
--   Due to <a>http://hackage.haskell.org/trac/ghc/ticket/5591</a> you may
--   have to use <a>unsafeOuterEq</a> and/or <a>unsafeInnerEq</a> to define
--   some of these.
class TypeCompare t where maybeEq = (~~) (~~) = maybeEq maybeOuterEq a b = fst (a <~> b) maybeInnerEq a b = snd (a <~> b) piecewiseMaybeEq a b = (a ~> b, a <~ b) (~>) = maybeOuterEq (<~) = maybeInnerEq (<~>) = piecewiseMaybeEq
maybeEq, ~~ :: TypeCompare t => t a -> t b -> Maybe (a :~: b)
maybeOuterEq, ~> :: TypeCompare t => t (f i) -> t a -> Maybe (OuterEq f a)
maybeInnerEq, <~ :: TypeCompare t => t (f i) -> t a -> Maybe (InnerEq i a)
piecewiseMaybeEq, <~> :: TypeCompare t => t (f i) -> t a -> (Maybe (OuterEq f a), Maybe (InnerEq i a))
instance Typeable InnerEq
instance Typeable OuterEq
instance Typeable (:~:)
instance Typeable TypeCompare
instance TypeCompare (OuterEq f)
instance TypeCompare (InnerEq i)
instance TypeCompare ((:~:) a)
instance Category (:~:)


-- | Types and functions for storing and manipulating evidence of equality
--   between types of higher kind.
--   
--   Available up to <tt>* -&gt; * -&gt; *</tt>. Yell if you need more.
module Type.Eq.Higher

-- | Type constructors are generative
constructorEq :: f a :~: g b -> f ::~:: g
sameOuterEq :: OuterEq f a -> OuterEq g a -> f ::~:: g
data (::~::) (f :: * -> *) (g :: * -> *)
Eq1 :: f ::~:: g
withEq1 :: (f ~ g => r) -> (f ::~:: g) -> r

-- | Reflexivity
idEq1 :: f ::~:: f

-- | Transitivity
composeEq1 :: (g ::~:: h) -> (f ::~:: g) -> (f ::~:: h)

-- | Transitivity
(|.|) :: (g ::~:: h) -> (f ::~:: g) -> (f ::~:: h)

-- | Symmetry
flipEq1 :: (f ::~:: g) -> (g ::~:: f)

-- | Congruence?
applyEq1 :: f ::~:: g -> a :~: b -> f a :~: g b

-- | Congruence?
(|$|) :: f ::~:: g -> a :~: b -> f a :~: g b

-- | Type constructors are generative
constructorEq1 :: m a ::~:: n b -> m :::~::: n

-- | Type constructors are injective
argumentEq1 :: m a ::~:: n b -> a :~: b

-- | Runtime type equality evidence from <tt>Typeable1</tt>
dynamicEq1 :: (Typeable1 f, Typeable1 g) => Maybe (f ::~:: g)
data OuterEq1 (m :: * -> * -> *) (f :: * -> *)
OuterEq1 :: OuterEq1 m f
data InnerEq1 (a :: *) (f :: * -> *)
InnerEq1 :: InnerEq1 a f
withOuterEq1 :: (forall a. m a ~ f => r) -> OuterEq1 m f -> r
withInnerEq1 :: (forall m. m a ~ f => r) -> InnerEq1 a f -> r
outerEq1 :: m a ::~:: f -> OuterEq1 m f
innerEq1 :: m a ::~:: f -> InnerEq1 a f
assembleEq1 :: OuterEq1 m f -> InnerEq1 a f -> m a ::~:: f
sameOuterEq1 :: OuterEq1 m f -> OuterEq1 n f -> m :::~::: n
sameInnerEq1 :: InnerEq1 a f -> InnerEq1 b f -> a :~: b
data (:::~:::) (m :: * -> * -> *) (n :: * -> * -> *)
Eq2 :: m :::~::: n
withEq2 :: (m ~ n => r) -> (m :::~::: n) -> r

-- | Reflexivity
idEq2 :: m :::~::: m

-- | Transitivity
composeEq2 :: (n :::~::: o) -> (m :::~::: n) -> (m :::~::: o)

-- | Transitivity
(||.||) :: (n :::~::: o) -> (m :::~::: n) -> (m :::~::: o)

-- | Symmetry
flipEq2 :: (m :::~::: n) -> (n :::~::: m)

-- | Congruence?
applyEq2 :: m :::~::: n -> a :~: b -> m a ::~:: n b

-- | Congruence?
(||$||) :: m :::~::: n -> a :~: b -> m a ::~:: n b

-- | Runtime type equality evidence from <tt>Typeable2</tt>
dynamicEq2 :: (Typeable2 n, Typeable2 m) => Maybe (n :::~::: m)


-- | Kind-polymorphic functions for manipulating type equality evidence.
--   
--   This module is available only if <tt>PolyKinds</tt> are available (GHC
--   7.6+).
module Type.Eq.Poly

-- | Synonym for <tt><a>composeEq</a></tt>. Kind-polymorphic, unlike
--   <tt>(<a>.</a>)</tt>.
(|.|) :: b :~: c -> a :~: b -> a :~: c

-- | Congruence?
applyEq :: f :~: g -> a :~: b -> f a :~: g b

-- | Congruence?
(|$|) :: f :~: g -> a :~: b -> f a :~: g b

-- | Type constructors are generative
constructorEq :: f a :~: g b -> f :~: g

-- | Runtime type equality evidence from <tt>Typeable1</tt>
dynamicEq1 :: (Typeable1 f, Typeable1 g) => Maybe (f :~: g)

-- | Runtime type equality evidence from <tt>Typeable2</tt>
dynamicEq2 :: (Typeable2 n, Typeable2 m) => Maybe (n :~: m)

-- | Runtime type equality evidence from <tt>Typeable3</tt>
dynamicEq3 :: (Typeable3 x, Typeable3 y) => Maybe (x :~: y)

-- | Runtime type equality evidence from <tt>Typeable4</tt>
dynamicEq4 :: (Typeable4 x, Typeable4 y) => Maybe (x :~: y)

-- | Runtime type equality evidence from <tt>Typeable5</tt>
dynamicEq5 :: (Typeable5 x, Typeable5 y) => Maybe (x :~: y)

-- | Runtime type equality evidence from <tt>Typeable6</tt>
dynamicEq6 :: (Typeable6 x, Typeable6 y) => Maybe (x :~: y)

-- | Runtime type equality evidence from <tt>Typeable7</tt>
dynamicEq7 :: (Typeable7 x, Typeable7 y) => Maybe (x :~: y)
sameOuterEq :: OuterEq f a -> OuterEq g a -> f :~: g
fromEq1 :: f ::~:: g -> f :~: g
toEq1 :: f :~: g -> f ::~:: g
fromEq2 :: n :::~::: m -> n :~: m
toEq2 :: n :~: m -> n :::~::: m
fromOuterEq1 :: OuterEq1 m f -> OuterEq m f
toOuterEq1 :: OuterEq m f -> OuterEq1 m f
fromInnerEq1 :: InnerEq1 a f -> InnerEq a f
toInnerEq1 :: InnerEq a f -> InnerEq1 a f