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


-- | Open type representations and dynamic types
--   
@package open-typerep
@version 0.3.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 Render t => TypeEq t u
typeEqSym :: TypeEq t u => (t sig1, Args (AST u) sig1) -> (t sig2, Args (AST u) sig2) -> Either String (Dict (DenResult sig1 ~ DenResult sig2))

-- | Equality on type representations
typeEq :: (TypeEq t t, MonadError String m) => TypeRep t a -> TypeRep t b -> m (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)]

-- | Show the name of type classes
class ShowClass (p :: * -> Constraint)
showClass :: ShowClass p => Proxy p -> String

-- | 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 (ShowClass p, Render t) => PWitness p t u where pwitSym _ _ = throwError ""
pwitSym :: PWitness p t u => t sig -> Args (AST u) sig -> Either String (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 -> Either String (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, MonadError String m) => Proxy p -> TypeRep t a -> m (Dict (p a))

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

-- | Safe generalized cast (does not use <tt>unsafeCoerce</tt>)
gcast :: (Typeable t a, Typeable t b, TypeEq t t) => Proxy t -> c a -> Either String (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 -> Either String 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 -> Either String (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 -> Either String 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 ShowClass (Typeable t)
instance ShowClass Integral
instance ShowClass Num
instance ShowClass Show
instance ShowClass Ord
instance ShowClass Eq
instance ShowClass Any
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 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 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

-- | 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 Render t => TypeEq t u

-- | Equality on type representations
typeEq :: (TypeEq t t, MonadError String m) => TypeRep t a -> TypeRep t b -> m (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 (ShowClass p, Render t) => PWitness p t u where pwitSym _ _ = throwError ""

-- | 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, MonadError String m) => Proxy p -> TypeRep t a -> m (Dict (p a))

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

-- | Safe generalized cast (does not use <tt>unsafeCoerce</tt>)
gcast :: (Typeable t a, Typeable t b, TypeEq t t) => Proxy t -> c a -> Either String (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 -> Either String a
dynToInteger :: PWitness Integral t t => Dynamic t -> Either String 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 -> Either String (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


-- | Utilities for polyvariadic functions
module Data.TypeRep.VarArg

-- | Newtype marking the result of a N-ary function
newtype Res a
Res :: a -> Res a

-- | Put a <a>Res</a> marker at the result type of a function
--   
--   <pre>
--   ToRes (a -&gt; b -&gt; ... -&gt; x) = a -&gt; b -&gt; ... -&gt; Res x
--   </pre>

-- | Remove the <a>Res</a> marker at the result type of a function
--   
--   <pre>
--   FromRes (a -&gt; b -&gt; ... -&gt; Res x) = a -&gt; b -&gt; ... -&gt; x
--   </pre>

-- | Witness of the arity of a function. <a>Arity</a> will normally be
--   indexed by <tt>(<a>ToRes</a> a)</tt>.
data Arity a
FunRes :: Arity (Res a)
FunArg :: Arity b -> Arity (a -> b)
class VarArg t
aritySym :: (VarArg t, VarArg u) => t sig -> Args (AST u) sig -> Arity (ToRes (DenResult sig))
fromResInvSym :: (VarArg t, VarArg u, a ~ DenResult sig) => t sig -> Args (AST u) sig -> Dict (FromRes (ToRes a) ~ a)

-- | Get the <a>Arity</a> of a type. The purpose is to be able to
--   distinguish between functions and non-functions without having to
--   handle all cases of a <a>TypeRep</a>.
arity :: VarArg t => TypeRep t a -> Arity (ToRes a)

-- | Prove that <a>FromRes</a> is the inverse of <a>ToRes</a>
fromResInv :: VarArg t => TypeRep t a -> Dict (FromRes (ToRes a) ~ a)
type NonFunction a = ToRes a ~ Res a

-- | Attempt to prove that a type is not a function type
nonFunction :: (VarArg t, MonadError String m) => TypeRep t a -> m (Dict (NonFunction a))

-- | Give a function a monadic result type. <tt>(<a>FunM</a> m)</tt> will
--   normally be indexed by <tt>(<a>ToRes</a> a)</tt>.
--   
--   <pre>
--   FunM m (a -&gt; b -&gt; ... -&gt; Res x) = a -&gt; b -&gt; ... -&gt; m x
--   </pre>

-- | Lift a function to a similar function with monadic result type
--   
--   <pre>
--   liftMonadic _ _ f = \a b ... x -&gt; return (f a b ... x)
--   </pre>
liftMonadic :: (VarArg t, Monad m) => Proxy m -> TypeRep t a -> a -> FunM m (ToRes a)

-- | Run the result of a monadic function
--   
--   <pre>
--   runMonadic run _ f = \a b ... x -&gt; run (f a b ... x)
--   </pre>
runMonadic :: VarArg t => (forall a. m a -> a) -> TypeRep t a -> FunM m (ToRes a) -> a

-- | Compose a function with an N-ary monadic function
--   
--   <pre>
--   compMonadic f _ g = \a b ... x -&gt; f (g a b ... x)
--   </pre>
compMonadic :: VarArg t => (forall a. m1 a -> m2 a) -> TypeRep t a -> FunM m1 (ToRes a) -> FunM m2 (ToRes a)

-- | Give a function monadic arguments and result type. <tt>(<a>FunM2</a>
--   m)</tt> will normally be indexed by <tt>(<a>ToRes</a> a)</tt>.
--   
--   <pre>
--   FunM m (a -&gt; b -&gt; ... -&gt; Res x) = m a -&gt; m b -&gt; ... -&gt; m x
--   </pre>

-- | Lift a function to a similar function with monadic arguments and
--   result
--   
--   <pre>
--   liftMonadic f = \ma mb ... mx -&gt; do
--       a &lt;- ma
--       b &lt;- mb
--       ...
--       x &lt;- mx
--       return (f a b ... x)
--   </pre>
liftMonadic2 :: (VarArg t, Monad m) => Proxy m -> TypeRep t a -> a -> FunM2 m (ToRes a)
instance VarArg FunType
instance VarArg ListType
instance VarArg FloatType
instance VarArg IntType
instance VarArg CharType
instance VarArg BoolType
instance (VarArg t1, VarArg t2) => VarArg (t1 :+: t2)