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


-- | Typed type representations and equality proofs
--   
--   Typed type representations and equality proofs
--   
--   Project wiki page: <a>http://haskell.org/haskellwiki/ty</a>
--   
--   Copyright 2009-2012 Conal Elliott; BSD3 license.
@package ty
@version 0.1.7


-- | Type equality proofs
module Data.Proof.EQ

-- | Type equality proof
data (:=:) :: * -> * -> *
[Refl] :: a :=: a

-- | Lift proof through a unary type constructor
liftEq :: a :=: a' -> f a :=: f a'

-- | Lift proof through a binary type constructor (including '(,)')
liftEq2 :: a :=: a' -> b :=: b' -> f a b :=: f a' b'

-- | Lift proof through a ternary type constructor (including '(,,)')
liftEq3 :: a :=: a' -> b :=: b' -> c :=: c' -> f a b c :=: f a' b' c'

-- | Lift proof through a quaternary type constructor (including '(,,,)')
liftEq4 :: a :=: a' -> b :=: b' -> c :=: c' -> d :=: d' -> f a b c d :=: f a' b' c' d'

-- | Commutativity
commEq :: a :=: a' -> a' :=: a

-- | Transitivity
transEq :: a :=: a' -> a' :=: a'' -> a :=: a''


-- | Type class for typed type representations
module Data.IsTy

-- | Type class for typed type representations
class IsTy f where type IsTyConstraint f z :: Constraint type IsTyConstraint f z = Yes f z where {
    type family IsTyConstraint f z :: Constraint;
    type IsTyConstraint f z = Yes f z;
}
tyEq :: (IsTy f, IsTyConstraint f a, IsTyConstraint f b) => f a -> f b -> Maybe (a :=: b)

-- | Type class for typed type representations
class IsTy2 f where type IsTy2Constraint f u v :: Constraint type IsTy2Constraint f u v = Yes2 f u v where {
    type family IsTy2Constraint f u v :: Constraint;
    type IsTy2Constraint f u v = Yes2 f u v;
}
tyEq2 :: (IsTy2 f, IsTy2Constraint f a b, IsTy2Constraint f c d) => f a b -> f c d -> Maybe ((a, b) :=: (c, d))
class Yes (f :: * -> *) a
class Yes2 (f :: * -> * -> *) a b
instance Data.IsTy.Yes f a
instance Data.IsTy.Yes2 f a b


-- | Typed typerefs
module Data.Ty

-- | The class <a>Typeable</a> allows a concrete representation of a type
--   to be calculated.
class Typeable k (a :: k)

-- | Phantom type wrapper around a <a>TypeRep</a>
data Ty a
tyRep :: Ty a -> TypeRep
ty :: Typeable a => Ty a

-- | The <a>Ty</a> of a value
tyOf :: Typeable a => a -> Ty a

-- | The <a>Ty</a> of a value from a constructor application
tyOf1 :: forall f a. Typeable a => f a -> Ty a

-- | The <a>Ty</a> of a value from a nested constructor application
tyOf2 :: forall g f a. Typeable a => g (f a) -> Ty a

-- | Equality of typed values. <tt><a>Just</a> <a>Refl</a></tt> means the
--   the types match and the values match.
(=:=) :: forall a b. (Typeable a, Typeable b, Eq a) => a -> b -> Maybe (a :=: b)
data AsPairTy :: * -> *
[PairTy] :: Ty a -> Ty b -> AsPairTy (a, b)
asPairTy :: Ty t -> Maybe (AsPairTy t)
instance GHC.Classes.Eq (Data.Ty.Ty a)
instance GHC.Show.Show (Data.Ty.Ty a)
instance Data.IsTy.IsTy Data.Ty.Ty