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


-- | Open type representations and dynamic types
--   
--   This package uses Data Types à la Carte to provide open type
--   representations and dynamic types/coercions for open type universes.
--   
--   Example 1 (dynamic types):
--   
--   <pre>
--   type MyUniverse = IntType :+: BoolType
--   
--   hlist :: [Dynamic MyUniverse]
--   hlist = [toDyn True, toDyn (1 :: Int)]
--   </pre>
--   
--   <pre>
--   *Main&gt; hlist
--   [True,1]
--   </pre>
--   
--   Note that if we were using <a>Data.Dynamic</a>, it would just print
--   
--   <pre>
--   [&lt;&lt;Bool&gt;&gt;,&lt;&lt;Int&gt;&gt;]
--   </pre>
--   
--   Example 2 (dynamically typed addition):
--   
--   <pre>
--   addDyn :: (TypeEq ts ts, PWitness Num ts ts) =&gt; Dynamic ts -&gt; Dynamic ts -&gt; Maybe (Dynamic ts)
--   addDyn (Dyn ta a) (Dyn tb b) = do
--       Dict &lt;- typeEq ta tb
--       Dict &lt;- pwit pNum ta
--       return (Dyn ta (a+b))
--   </pre>
--   
--   <a>Data.Dynamic</a> could only do this monomorphically, for one
--   <a>Num</a> type at a time.
@package open-typerep
@version 0.3.3


-- | 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)

-- | Show the name of a type class
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 Language.Syntactic.Interpretation.Render t => GHC.Show.Show (Data.TypeRep.Internal.TypeRep t a)
instance Language.Syntactic.Sugar.Syntactic (Data.TypeRep.Internal.TypeRep t a)
instance (Data.TypeRep.Internal.TypeEq t1 t, Data.TypeRep.Internal.TypeEq t2 t) => Data.TypeRep.Internal.TypeEq (t1 Language.Syntactic.Syntax.:+: t2) t
instance Data.TypeRep.Internal.TypeEq Language.Syntactic.Syntax.Empty t
instance (Data.TypeRep.Internal.Witness p t1 t, Data.TypeRep.Internal.Witness p t2 t) => Data.TypeRep.Internal.Witness p (t1 Language.Syntactic.Syntax.:+: t2) t
instance Data.TypeRep.Internal.Witness p t t => Data.TypeRep.Internal.Witness p (Language.Syntactic.Syntax.AST t) t
instance (Data.TypeRep.Internal.PWitness p t1 t, Data.TypeRep.Internal.PWitness p t2 t) => Data.TypeRep.Internal.PWitness p (t1 Language.Syntactic.Syntax.:+: t2) t
instance (Data.TypeRep.Internal.TypeEq t t, Data.TypeRep.Internal.Witness GHC.Classes.Eq t t) => GHC.Classes.Eq (Data.TypeRep.Internal.Dynamic t)
instance Data.TypeRep.Internal.Witness GHC.Show.Show t t => GHC.Show.Show (Data.TypeRep.Internal.Dynamic t)
instance Data.TypeRep.Internal.Any a
instance Data.TypeRep.Internal.ShowClass Data.TypeRep.Internal.Any
instance Data.TypeRep.Internal.ShowClass GHC.Classes.Eq
instance Data.TypeRep.Internal.ShowClass GHC.Classes.Ord
instance Data.TypeRep.Internal.ShowClass GHC.Show.Show
instance Data.TypeRep.Internal.ShowClass GHC.Num.Num
instance Data.TypeRep.Internal.ShowClass GHC.Real.Integral
instance Data.TypeRep.Internal.ShowClass (Data.TypeRep.Internal.Typeable t)
instance Language.Syntactic.Interpretation.Render Data.TypeRep.Internal.BoolType
instance Language.Syntactic.Interpretation.Render Data.TypeRep.Internal.CharType
instance Language.Syntactic.Interpretation.Render Data.TypeRep.Internal.IntType
instance Language.Syntactic.Interpretation.Render Data.TypeRep.Internal.FloatType
instance Language.Syntactic.Interpretation.Render Data.TypeRep.Internal.ListType
instance Language.Syntactic.Interpretation.Render Data.TypeRep.Internal.FunType
instance (Data.TypeRep.Internal.BoolType Language.Syntactic.Syntax.:<: t) => Data.TypeRep.Internal.Typeable t GHC.Types.Bool
instance (Data.TypeRep.Internal.CharType Language.Syntactic.Syntax.:<: t) => Data.TypeRep.Internal.Typeable t GHC.Types.Char
instance (Data.TypeRep.Internal.IntType Language.Syntactic.Syntax.:<: t) => Data.TypeRep.Internal.Typeable t GHC.Types.Int
instance (Data.TypeRep.Internal.FloatType Language.Syntactic.Syntax.:<: t) => Data.TypeRep.Internal.Typeable t GHC.Types.Float
instance (Data.TypeRep.Internal.ListType Language.Syntactic.Syntax.:<: t, Data.TypeRep.Internal.Typeable t a) => Data.TypeRep.Internal.Typeable t [a]
instance (Data.TypeRep.Internal.FunType Language.Syntactic.Syntax.:<: t, Data.TypeRep.Internal.Typeable t a, Data.TypeRep.Internal.Typeable t b) => Data.TypeRep.Internal.Typeable t (a -> b)
instance Data.TypeRep.Internal.TypeEq Data.TypeRep.Internal.BoolType t
instance Data.TypeRep.Internal.TypeEq Data.TypeRep.Internal.CharType t
instance Data.TypeRep.Internal.TypeEq Data.TypeRep.Internal.IntType t
instance Data.TypeRep.Internal.TypeEq Data.TypeRep.Internal.FloatType t
instance Data.TypeRep.Internal.TypeEq t t => Data.TypeRep.Internal.TypeEq Data.TypeRep.Internal.ListType t
instance Data.TypeRep.Internal.TypeEq t t => Data.TypeRep.Internal.TypeEq Data.TypeRep.Internal.FunType t
instance (Data.TypeRep.Internal.BoolType Language.Syntactic.Syntax.:<: t) => Data.TypeRep.Internal.Witness (Data.TypeRep.Internal.Typeable t) Data.TypeRep.Internal.BoolType t
instance (Data.TypeRep.Internal.CharType Language.Syntactic.Syntax.:<: t) => Data.TypeRep.Internal.Witness (Data.TypeRep.Internal.Typeable t) Data.TypeRep.Internal.CharType t
instance (Data.TypeRep.Internal.IntType Language.Syntactic.Syntax.:<: t) => Data.TypeRep.Internal.Witness (Data.TypeRep.Internal.Typeable t) Data.TypeRep.Internal.IntType t
instance (Data.TypeRep.Internal.FloatType Language.Syntactic.Syntax.:<: t) => Data.TypeRep.Internal.Witness (Data.TypeRep.Internal.Typeable t) Data.TypeRep.Internal.FloatType t
instance (Data.TypeRep.Internal.ListType Language.Syntactic.Syntax.:<: t, Data.TypeRep.Internal.Witness (Data.TypeRep.Internal.Typeable t) t t) => Data.TypeRep.Internal.Witness (Data.TypeRep.Internal.Typeable t) Data.TypeRep.Internal.ListType t
instance (Data.TypeRep.Internal.FunType Language.Syntactic.Syntax.:<: t, Data.TypeRep.Internal.Witness (Data.TypeRep.Internal.Typeable t) t t) => Data.TypeRep.Internal.Witness (Data.TypeRep.Internal.Typeable t) Data.TypeRep.Internal.FunType t
instance (Data.TypeRep.Internal.BoolType Language.Syntactic.Syntax.:<: t) => Data.TypeRep.Internal.PWitness (Data.TypeRep.Internal.Typeable t) Data.TypeRep.Internal.BoolType t
instance (Data.TypeRep.Internal.CharType Language.Syntactic.Syntax.:<: t) => Data.TypeRep.Internal.PWitness (Data.TypeRep.Internal.Typeable t) Data.TypeRep.Internal.CharType t
instance (Data.TypeRep.Internal.IntType Language.Syntactic.Syntax.:<: t) => Data.TypeRep.Internal.PWitness (Data.TypeRep.Internal.Typeable t) Data.TypeRep.Internal.IntType t
instance (Data.TypeRep.Internal.FloatType Language.Syntactic.Syntax.:<: t) => Data.TypeRep.Internal.PWitness (Data.TypeRep.Internal.Typeable t) Data.TypeRep.Internal.FloatType t
instance (Data.TypeRep.Internal.ListType Language.Syntactic.Syntax.:<: t, Data.TypeRep.Internal.PWitness (Data.TypeRep.Internal.Typeable t) t t) => Data.TypeRep.Internal.PWitness (Data.TypeRep.Internal.Typeable t) Data.TypeRep.Internal.ListType t
instance (Data.TypeRep.Internal.FunType Language.Syntactic.Syntax.:<: t, Data.TypeRep.Internal.PWitness (Data.TypeRep.Internal.Typeable t) t t) => Data.TypeRep.Internal.PWitness (Data.TypeRep.Internal.Typeable t) Data.TypeRep.Internal.FunType t
instance Data.TypeRep.Internal.Witness Data.TypeRep.Internal.Any Data.TypeRep.Internal.BoolType t
instance Data.TypeRep.Internal.Witness Data.TypeRep.Internal.Any Data.TypeRep.Internal.CharType t
instance Data.TypeRep.Internal.Witness Data.TypeRep.Internal.Any Data.TypeRep.Internal.IntType t
instance Data.TypeRep.Internal.Witness Data.TypeRep.Internal.Any Data.TypeRep.Internal.FloatType t
instance Data.TypeRep.Internal.Witness Data.TypeRep.Internal.Any Data.TypeRep.Internal.ListType t
instance Data.TypeRep.Internal.Witness Data.TypeRep.Internal.Any Data.TypeRep.Internal.FunType t
instance Data.TypeRep.Internal.PWitness Data.TypeRep.Internal.Any Data.TypeRep.Internal.BoolType t
instance Data.TypeRep.Internal.PWitness Data.TypeRep.Internal.Any Data.TypeRep.Internal.CharType t
instance Data.TypeRep.Internal.PWitness Data.TypeRep.Internal.Any Data.TypeRep.Internal.IntType t
instance Data.TypeRep.Internal.PWitness Data.TypeRep.Internal.Any Data.TypeRep.Internal.FloatType t
instance Data.TypeRep.Internal.PWitness Data.TypeRep.Internal.Any Data.TypeRep.Internal.ListType t
instance Data.TypeRep.Internal.PWitness Data.TypeRep.Internal.Any Data.TypeRep.Internal.FunType t
instance Data.TypeRep.Internal.Witness GHC.Classes.Eq Data.TypeRep.Internal.BoolType t
instance Data.TypeRep.Internal.Witness GHC.Classes.Eq Data.TypeRep.Internal.CharType t
instance Data.TypeRep.Internal.Witness GHC.Classes.Eq Data.TypeRep.Internal.IntType t
instance Data.TypeRep.Internal.Witness GHC.Classes.Eq Data.TypeRep.Internal.FloatType t
instance Data.TypeRep.Internal.Witness GHC.Classes.Eq t t => Data.TypeRep.Internal.Witness GHC.Classes.Eq Data.TypeRep.Internal.ListType t
instance Data.TypeRep.Internal.PWitness GHC.Classes.Eq Data.TypeRep.Internal.BoolType t
instance Data.TypeRep.Internal.PWitness GHC.Classes.Eq Data.TypeRep.Internal.CharType t
instance Data.TypeRep.Internal.PWitness GHC.Classes.Eq Data.TypeRep.Internal.IntType t
instance Data.TypeRep.Internal.PWitness GHC.Classes.Eq Data.TypeRep.Internal.FloatType t
instance Data.TypeRep.Internal.PWitness GHC.Classes.Eq t t => Data.TypeRep.Internal.PWitness GHC.Classes.Eq Data.TypeRep.Internal.ListType t
instance Data.TypeRep.Internal.PWitness GHC.Classes.Eq Data.TypeRep.Internal.FunType t
instance Data.TypeRep.Internal.Witness GHC.Classes.Ord Data.TypeRep.Internal.BoolType t
instance Data.TypeRep.Internal.Witness GHC.Classes.Ord Data.TypeRep.Internal.CharType t
instance Data.TypeRep.Internal.Witness GHC.Classes.Ord Data.TypeRep.Internal.IntType t
instance Data.TypeRep.Internal.Witness GHC.Classes.Ord Data.TypeRep.Internal.FloatType t
instance Data.TypeRep.Internal.Witness GHC.Classes.Ord t t => Data.TypeRep.Internal.Witness GHC.Classes.Ord Data.TypeRep.Internal.ListType t
instance Data.TypeRep.Internal.PWitness GHC.Classes.Ord Data.TypeRep.Internal.BoolType t
instance Data.TypeRep.Internal.PWitness GHC.Classes.Ord Data.TypeRep.Internal.CharType t
instance Data.TypeRep.Internal.PWitness GHC.Classes.Ord Data.TypeRep.Internal.IntType t
instance Data.TypeRep.Internal.PWitness GHC.Classes.Ord Data.TypeRep.Internal.FloatType t
instance Data.TypeRep.Internal.PWitness GHC.Classes.Ord t t => Data.TypeRep.Internal.PWitness GHC.Classes.Ord Data.TypeRep.Internal.ListType t
instance Data.TypeRep.Internal.PWitness GHC.Classes.Ord Data.TypeRep.Internal.FunType t
instance Data.TypeRep.Internal.Witness GHC.Show.Show Data.TypeRep.Internal.BoolType t
instance Data.TypeRep.Internal.Witness GHC.Show.Show Data.TypeRep.Internal.CharType t
instance Data.TypeRep.Internal.Witness GHC.Show.Show Data.TypeRep.Internal.IntType t
instance Data.TypeRep.Internal.Witness GHC.Show.Show Data.TypeRep.Internal.FloatType t
instance Data.TypeRep.Internal.Witness GHC.Show.Show t t => Data.TypeRep.Internal.Witness GHC.Show.Show Data.TypeRep.Internal.ListType t
instance Data.TypeRep.Internal.PWitness GHC.Show.Show Data.TypeRep.Internal.BoolType t
instance Data.TypeRep.Internal.PWitness GHC.Show.Show Data.TypeRep.Internal.CharType t
instance Data.TypeRep.Internal.PWitness GHC.Show.Show Data.TypeRep.Internal.IntType t
instance Data.TypeRep.Internal.PWitness GHC.Show.Show Data.TypeRep.Internal.FloatType t
instance Data.TypeRep.Internal.PWitness GHC.Show.Show t t => Data.TypeRep.Internal.PWitness GHC.Show.Show Data.TypeRep.Internal.ListType t
instance Data.TypeRep.Internal.PWitness GHC.Show.Show Data.TypeRep.Internal.FunType t
instance Data.TypeRep.Internal.Witness GHC.Num.Num Data.TypeRep.Internal.IntType t
instance Data.TypeRep.Internal.Witness GHC.Num.Num Data.TypeRep.Internal.FloatType t
instance Data.TypeRep.Internal.PWitness GHC.Num.Num Data.TypeRep.Internal.BoolType t
instance Data.TypeRep.Internal.PWitness GHC.Num.Num Data.TypeRep.Internal.CharType t
instance Data.TypeRep.Internal.PWitness GHC.Num.Num Data.TypeRep.Internal.IntType t
instance Data.TypeRep.Internal.PWitness GHC.Num.Num Data.TypeRep.Internal.FloatType t
instance Data.TypeRep.Internal.PWitness GHC.Num.Num Data.TypeRep.Internal.ListType t
instance Data.TypeRep.Internal.PWitness GHC.Num.Num Data.TypeRep.Internal.FunType t
instance Data.TypeRep.Internal.Witness GHC.Real.Integral Data.TypeRep.Internal.IntType t
instance Data.TypeRep.Internal.PWitness GHC.Real.Integral Data.TypeRep.Internal.BoolType t
instance Data.TypeRep.Internal.PWitness GHC.Real.Integral Data.TypeRep.Internal.CharType t
instance Data.TypeRep.Internal.PWitness GHC.Real.Integral Data.TypeRep.Internal.IntType t
instance Data.TypeRep.Internal.PWitness GHC.Real.Integral Data.TypeRep.Internal.FloatType t
instance Data.TypeRep.Internal.PWitness GHC.Real.Integral Data.TypeRep.Internal.ListType t
instance Data.TypeRep.Internal.PWitness GHC.Real.Integral Data.TypeRep.Internal.FunType t


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

-- | Cast a type representation to a larger universe
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 (Data.TypeRep.VarArg.VarArg t1, Data.TypeRep.VarArg.VarArg t2) => Data.TypeRep.VarArg.VarArg (t1 Language.Syntactic.Syntax.:+: t2)
instance Data.TypeRep.VarArg.VarArg Data.TypeRep.Internal.BoolType
instance Data.TypeRep.VarArg.VarArg Data.TypeRep.Internal.CharType
instance Data.TypeRep.VarArg.VarArg Data.TypeRep.Internal.IntType
instance Data.TypeRep.VarArg.VarArg Data.TypeRep.Internal.FloatType
instance Data.TypeRep.VarArg.VarArg Data.TypeRep.Internal.ListType
instance Data.TypeRep.VarArg.VarArg Data.TypeRep.Internal.FunType