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


-- | Open type representations and dynamic types
--   
@package open-typerep
@version 0.1


-- | Open type representations and dynamic types
module Data.TypeRep.Internal

-- | <a>Full</a>-indexed type representation
type TR = AST

-- | This class provides reification of type <tt>a</tt> in a universe
--   <tt>t</tt>. <tt><a>Typeable</a> t a</tt> means that <tt>a</tt> is in
--   the type universe represented by <tt>t</tt>.
class Typeable t a
typeRep' :: Typeable t a => TR t (Full a)

-- | Representation of type <tt>a</tt> in a type universe <tt>t</tt>
--   
--   This type can also be seen as a witness that <tt>a</tt> is a member of
--   <tt>t</tt> (i.e. <tt><a>Typeable</a> t a</tt>); see
--   <a>witTypeable</a>.
newtype TypeRep t a
TypeRep :: TR t (Full a) -> TypeRep t a
unTypeRep :: TypeRep t a -> TR t (Full a)

-- | Reification of type <tt>a</tt> in a type universe <tt>t</tt>
typeRep :: Typeable t a => TypeRep t a

-- | Equality on type representations
class TypeEq t u
typeEqSym :: TypeEq t u => (t sig1, Args (AST u) sig1) -> (t sig2, Args (AST u) sig2) -> Maybe (Dict (DenResult sig1 ~ DenResult sig2))

-- | Equality on type representations
typeEq :: TypeEq t t => TypeRep t a -> TypeRep t b -> Maybe (Dict (a ~ b))

-- | Type constructor matching. This function makes it possible to match on
--   type representations without dealing with the underlying <a>AST</a>
--   representation.
--   
--   For example, to check that a <a>TypeRep</a> represents the type <tt>a
--   -&gt; Int</tt> for some <tt>a</tt>:
--   
--   <pre>
--   is_atoi :: (TypeEq t t, IntType :&lt;: t) =&gt; TypeRep t a -&gt; Bool
--   is_atoi t
--       | [E ta, E tb] &lt;- matchCon t
--       , Just _       &lt;- typeEq ta intType = True
--       | otherwise                         = False
--   </pre>
matchCon :: TypeRep t c -> [E (TypeRep t)]

-- | Monadic version of <a>matchCon</a>
--   
--   <pre>
--   matchConM = return . matchCon
--   </pre>
--   
--   <a>matchConM</a> is convenient when matching types in a monad, e.g.:
--   
--   <pre>
--   do ...
--      [E ta, E tb] &lt;- matchConM t
--      Dict         &lt;- typeEq ta tb
--      ...
--   </pre>
matchConM :: Monad m => TypeRep t c -> m [E (TypeRep t)]

-- | Witness a type constraint for a reified type
class Witness p t u
witSym :: Witness p t u => t sig -> Args (AST u) sig -> Dict (p (DenResult sig))

-- | Partially witness a type constraint for a reified type
class PWitness p t u where pwitSym _ _ = Nothing
pwitSym :: PWitness p t u => t sig -> Args (AST u) sig -> Maybe (Dict (p (DenResult sig)))

-- | Default implementation of <a>pwitSym</a> for types that have a
--   <a>Witness</a> instance
pwitSymDefault :: Witness p t u => t sig -> Args (AST u) sig -> Maybe (Dict (p (DenResult sig)))

-- | Witness a type constraint for a reified type
wit :: Witness p t t => Proxy p -> TypeRep t a -> Dict (p a)

-- | Partially witness a type constraint for a reified type
pwit :: PWitness p t t => Proxy p -> TypeRep t a -> Maybe (Dict (p a))

-- | Safe cast (does not use <tt>unsafeCoerce</tt>)
cast :: (Typeable t a, Typeable t b, TypeEq t t) => Proxy t -> a -> Maybe b

-- | Safe generalized cast (does not use <tt>unsafeCoerce</tt>)
gcast :: (Typeable t a, Typeable t b, TypeEq t t) => Proxy t -> c a -> Maybe (c b)

-- | Dynamic type parameterized on a type universe
data Dynamic t
Dyn :: TypeRep t a -> a -> Dynamic t
toDyn :: Typeable t a => a -> Dynamic t
fromDyn :: (Typeable t a, TypeEq t t) => Dynamic t -> Maybe a

-- | The universal class
class Any a

-- | Witness a <a>Typeable</a> constraint for a reified type
witTypeable :: Witness (Typeable t) t t => TypeRep t a -> Dict (Typeable t a)

-- | Partially witness a <a>Typeable</a> constraint for a reified type
pwitTypeable :: PWitness (Typeable t) t t => TypeRep t a -> Maybe (Dict (Typeable t a))
pAny :: Proxy Any
pEq :: Proxy Eq
pOrd :: Proxy Ord
pShow :: Proxy Show
pNum :: Proxy Num
pIntegral :: Proxy Integral
data BoolType a
BoolType :: BoolType (Full Bool)
data CharType a
CharType :: CharType (Full Char)
data IntType a
IntType :: IntType (Full Int)
data FloatType a
FloatType :: FloatType (Full Float)
data ListType a
ListType :: ListType (a :-> Full [a])
data FunType a
FunType :: FunType (a :-> (b :-> Full (a -> b)))
boolType :: (Syntactic a, BoolType :<: Domain a, Internal a ~ Bool) => a
charType :: (Syntactic a, CharType :<: Domain a, Internal a ~ Char) => a
intType :: (Syntactic a, IntType :<: Domain a, Internal a ~ Int) => a
floatType :: (Syntactic a, FloatType :<: Domain a, Internal a ~ Float) => a
listType :: (Syntactic list, Syntactic elem, Domain list ~ Domain elem, ListType :<: Domain list, Internal list ~ [Internal elem], elem ~ c e, list ~ c l) => elem -> list
funType :: (Syntactic fun, Syntactic a, Syntactic b, Domain fun ~ Domain a, Domain fun ~ Domain b, FunType :<: Domain fun, Internal fun ~ (Internal a -> Internal b), a ~ c x, b ~ c y, fun ~ c z) => a -> b -> fun
dynToInteger :: PWitness Integral t t => Dynamic t -> Maybe Integer
instance PWitness Integral FunType t
instance PWitness Integral ListType t
instance PWitness Integral FloatType t
instance PWitness Integral IntType t
instance PWitness Integral CharType t
instance PWitness Integral BoolType t
instance Witness Integral IntType t
instance PWitness Num FunType t
instance PWitness Num ListType t
instance PWitness Num FloatType t
instance PWitness Num IntType t
instance PWitness Num CharType t
instance PWitness Num BoolType t
instance Witness Num FloatType t
instance Witness Num IntType t
instance PWitness Show FunType t
instance PWitness Show t t => PWitness Show ListType t
instance PWitness Show FloatType t
instance PWitness Show IntType t
instance PWitness Show CharType t
instance PWitness Show BoolType t
instance Witness Show t t => Witness Show ListType t
instance Witness Show FloatType t
instance Witness Show IntType t
instance Witness Show CharType t
instance Witness Show BoolType t
instance PWitness Ord FunType t
instance PWitness Ord t t => PWitness Ord ListType t
instance PWitness Ord FloatType t
instance PWitness Ord IntType t
instance PWitness Ord CharType t
instance PWitness Ord BoolType t
instance Witness Ord t t => Witness Ord ListType t
instance Witness Ord FloatType t
instance Witness Ord IntType t
instance Witness Ord CharType t
instance Witness Ord BoolType t
instance PWitness Eq FunType t
instance PWitness Eq t t => PWitness Eq ListType t
instance PWitness Eq FloatType t
instance PWitness Eq IntType t
instance PWitness Eq CharType t
instance PWitness Eq BoolType t
instance Witness Eq t t => Witness Eq ListType t
instance Witness Eq FloatType t
instance Witness Eq IntType t
instance Witness Eq CharType t
instance Witness Eq BoolType t
instance PWitness Any FunType t
instance PWitness Any ListType t
instance PWitness Any FloatType t
instance PWitness Any IntType t
instance PWitness Any CharType t
instance PWitness Any BoolType t
instance Witness Any FunType t
instance Witness Any ListType t
instance Witness Any FloatType t
instance Witness Any IntType t
instance Witness Any CharType t
instance Witness Any BoolType t
instance (FunType :<: t, PWitness (Typeable t) t t) => PWitness (Typeable t) FunType t
instance (ListType :<: t, PWitness (Typeable t) t t) => PWitness (Typeable t) ListType t
instance FloatType :<: t => PWitness (Typeable t) FloatType t
instance IntType :<: t => PWitness (Typeable t) IntType t
instance CharType :<: t => PWitness (Typeable t) CharType t
instance BoolType :<: t => PWitness (Typeable t) BoolType t
instance (FunType :<: t, Witness (Typeable t) t t) => Witness (Typeable t) FunType t
instance (ListType :<: t, Witness (Typeable t) t t) => Witness (Typeable t) ListType t
instance FloatType :<: t => Witness (Typeable t) FloatType t
instance IntType :<: t => Witness (Typeable t) IntType t
instance CharType :<: t => Witness (Typeable t) CharType t
instance BoolType :<: t => Witness (Typeable t) BoolType t
instance TypeEq t t => TypeEq FunType t
instance TypeEq t t => TypeEq ListType t
instance TypeEq FloatType t
instance TypeEq IntType t
instance TypeEq CharType t
instance TypeEq BoolType t
instance (FunType :<: t, Typeable t a, Typeable t b) => Typeable t (a -> b)
instance (ListType :<: t, Typeable t a) => Typeable t [a]
instance FloatType :<: t => Typeable t Float
instance IntType :<: t => Typeable t Int
instance CharType :<: t => Typeable t Char
instance BoolType :<: t => Typeable t Bool
instance Render FunType
instance Render ListType
instance Render FloatType
instance Render IntType
instance Render CharType
instance Render BoolType
instance Any a
instance Witness Show t t => Show (Dynamic t)
instance (TypeEq t t, Witness Eq t t) => Eq (Dynamic t)
instance PWitness p t t => PWitness p (AST t) t
instance (PWitness p t1 t, PWitness p t2 t) => PWitness p (t1 :+: t2) t
instance Witness p t t => Witness p (AST t) t
instance (Witness p t1 t, Witness p t2 t) => Witness p (t1 :+: t2) t
instance TypeEq Empty t
instance TypeEq t t => TypeEq (AST t) t
instance (TypeEq t1 t, TypeEq t2 t) => TypeEq (t1 :+: t2) t
instance Syntactic (TypeRep t a)
instance Render t => Show (TypeRep t a)


-- | Open type representations and dynamic types
module Data.TypeRep

-- | This class provides reification of type <tt>a</tt> in a universe
--   <tt>t</tt>. <tt><a>Typeable</a> t a</tt> means that <tt>a</tt> is in
--   the type universe represented by <tt>t</tt>.
class Typeable t a

-- | Representation of type <tt>a</tt> in a type universe <tt>t</tt>
--   
--   This type can also be seen as a witness that <tt>a</tt> is a member of
--   <tt>t</tt> (i.e. <tt><a>Typeable</a> t a</tt>); see
--   <a>witTypeable</a>.
data TypeRep t a

-- | Equality on type representations
class TypeEq t u

-- | Equality on type representations
typeEq :: TypeEq t t => TypeRep t a -> TypeRep t b -> Maybe (Dict (a ~ b))

-- | Type constructor matching. This function makes it possible to match on
--   type representations without dealing with the underlying <a>AST</a>
--   representation.
--   
--   For example, to check that a <a>TypeRep</a> represents the type <tt>a
--   -&gt; Int</tt> for some <tt>a</tt>:
--   
--   <pre>
--   is_atoi :: (TypeEq t t, IntType :&lt;: t) =&gt; TypeRep t a -&gt; Bool
--   is_atoi t
--       | [E ta, E tb] &lt;- matchCon t
--       , Just _       &lt;- typeEq ta intType = True
--       | otherwise                         = False
--   </pre>
matchCon :: TypeRep t c -> [E (TypeRep t)]

-- | Monadic version of <a>matchCon</a>
--   
--   <pre>
--   matchConM = return . matchCon
--   </pre>
--   
--   <a>matchConM</a> is convenient when matching types in a monad, e.g.:
--   
--   <pre>
--   do ...
--      [E ta, E tb] &lt;- matchConM t
--      Dict         &lt;- typeEq ta tb
--      ...
--   </pre>
matchConM :: Monad m => TypeRep t c -> m [E (TypeRep t)]

-- | Witness a type constraint for a reified type
class Witness p t u

-- | Partially witness a type constraint for a reified type
class PWitness p t u where pwitSym _ _ = Nothing

-- | Witness a type constraint for a reified type
wit :: Witness p t t => Proxy p -> TypeRep t a -> Dict (p a)

-- | Partially witness a type constraint for a reified type
pwit :: PWitness p t t => Proxy p -> TypeRep t a -> Maybe (Dict (p a))

-- | Safe cast (does not use <tt>unsafeCoerce</tt>)
cast :: (Typeable t a, Typeable t b, TypeEq t t) => Proxy t -> a -> Maybe b

-- | Safe generalized cast (does not use <tt>unsafeCoerce</tt>)
gcast :: (Typeable t a, Typeable t b, TypeEq t t) => Proxy t -> c a -> Maybe (c b)

-- | Dynamic type parameterized on a type universe
data Dynamic t
Dyn :: TypeRep t a -> a -> Dynamic t
toDyn :: Typeable t a => a -> Dynamic t
fromDyn :: (Typeable t a, TypeEq t t) => Dynamic t -> Maybe a
dynToInteger :: PWitness Integral t t => Dynamic t -> Maybe Integer

-- | The universal class
class Any a

-- | Witness a <a>Typeable</a> constraint for a reified type
witTypeable :: Witness (Typeable t) t t => TypeRep t a -> Dict (Typeable t a)

-- | Partially witness a <a>Typeable</a> constraint for a reified type
pwitTypeable :: PWitness (Typeable t) t t => TypeRep t a -> Maybe (Dict (Typeable t a))
pAny :: Proxy Any
pEq :: Proxy Eq
pOrd :: Proxy Ord
pShow :: Proxy Show
pNum :: Proxy Num
pIntegral :: Proxy Integral
data BoolType a
data CharType a
data IntType a
data FloatType a
data ListType a
data FunType a
boolType :: (Syntactic a, BoolType :<: Domain a, Internal a ~ Bool) => a
charType :: (Syntactic a, CharType :<: Domain a, Internal a ~ Char) => a
intType :: (Syntactic a, IntType :<: Domain a, Internal a ~ Int) => a
floatType :: (Syntactic a, FloatType :<: Domain a, Internal a ~ Float) => a
listType :: (Syntactic list, Syntactic elem, Domain list ~ Domain elem, ListType :<: Domain list, Internal list ~ [Internal elem], elem ~ c e, list ~ c l) => elem -> list
funType :: (Syntactic fun, Syntactic a, Syntactic b, Domain fun ~ Domain a, Domain fun ~ Domain b, FunType :<: Domain fun, Internal fun ~ (Internal a -> Internal b), a ~ c x, b ~ c y, fun ~ c z) => a -> b -> fun

-- | Sub-universe relation
--   
--   In general, a universe <tt>t</tt> is a sub-universe of <tt>u</tt> if
--   <tt>u</tt> has the form
--   
--   <pre>
--   t1 :+: t2 :+: ... :+: t
--   </pre>
class SubUniverse sub sup
weakenUniverse :: SubUniverse sub sup => TypeRep sub a -> TypeRep sup a