-- 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 Conal Elliott; BSD3 license.
@package ty
@version 0.0.2


-- | 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 ty
tyEq :: IsTy ty => ty a -> ty b -> Maybe (a :=: b)


-- | Typed typerefs
module Data.Ty

-- | 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 class <a>Typeable</a> allows a concrete representation of a type
--   to be calculated.
class Typeable a
instance IsTy Ty
instance Show (Ty a)