-- 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.4


-- | 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 family IsTyConstraint f z :: Constraint type instance 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 family IsTy2Constraint f u v :: Constraint type instance 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))
instance Yes2 f a b
instance Yes f a


-- | Typed typerefs
module Data.Ty

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

-- | 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 :: Typeable a => f a -> Ty a

-- | The <a>Ty</a> of a value from a nested constructor application
tyOf2 :: 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.
(=:=) :: (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 Eq (Ty a)
instance IsTy Ty
instance Show (Ty a)