module Data.OpenWitness.Typeable where
{
import Data.Kind;
import Data.OpenWitness.TypeRep;
import Data.OpenWitness;
import Data.Witness;
;
class Typeable (a :: k) where
{
typeRep :: TypeRep a;
};
instance (Typeable (f :: k1 -> k2),Typeable (a :: k1)) => Typeable (f a) where
{
typeRep = ApplyTypeRep typeRep typeRep;
};
instance Typeable Type where
{
typeRep = SimpleTypeRep $(iowitness [t|Type|]);
};
type Fun = (->);
instance Typeable (->) where
{
typeRep = SimpleTypeRep $(iowitness [t|Fun|]);
};
instance Typeable Constraint where
{
typeRep = SimpleTypeRep $(iowitness [t|Constraint|]);
};
instance Typeable TypeRep where
{
typeRep = SimpleTypeRep $(iowitness [t|TypeRep|]);
};
instance Typeable Typeable where
{
typeRep = SimpleTypeRep $(iowitness [t|Typeable|]);
};
instance Typeable () where
{
typeRep = SimpleTypeRep $(iowitness [t|()|]);
};
instance Typeable (,) where
{
typeRep = SimpleTypeRep $(iowitness [t|(,)|]);
};
instance Typeable Either where
{
typeRep = SimpleTypeRep $(iowitness [t|Either|]);
};
instance Typeable Maybe where
{
typeRep = SimpleTypeRep $(iowitness [t|Maybe|]);
};
instance Typeable [] where
{
typeRep = SimpleTypeRep $(iowitness [t|[]|]);
};
instance Typeable Bool where
{
typeRep = SimpleTypeRep $(iowitness [t|Bool|]);
};
instance Typeable Char where
{
typeRep = SimpleTypeRep $(iowitness [t|Char|]);
};
instance Typeable Int where
{
typeRep = SimpleTypeRep $(iowitness [t|Int|]);
};
cast :: forall (a :: *) (b :: *). (Typeable a,Typeable b) => a -> Maybe b;
cast a = do
{
Refl :: a :~: b <- testEquality typeRep typeRep;
return a;
};
gcast :: forall (k :: *) (a :: k) (b :: k) (c :: k -> *). (Typeable a,Typeable b) => c a -> Maybe (c b);
gcast ca = do
{
Refl :: a :~: b <- testEquality typeRep typeRep;
return ca;
};
;
mkFunTy :: TypeRep a -> TypeRep b -> TypeRep (a -> b);
mkFunTy ta tb = ApplyTypeRep (ApplyTypeRep (typeRep :: TypeRep (->)) ta) tb;
;
funResultTy :: TypeRep (a -> b) -> TypeRep a -> Maybe (TypeRep b);
funResultTy (ApplyTypeRep (ApplyTypeRep repFn' ta') tb') ta = do
{
Refl <- testEquality repFn' (typeRep :: TypeRep (->));
Refl <- testEquality ta' ta;
return tb';
};
funResultTy _ _ = Nothing;
mkAppTy :: forall (k1 :: *) (k2 :: *) (f :: k1 -> k2) (a :: k1). TypeRep f -> TypeRep a -> TypeRep (f a);
mkAppTy = ApplyTypeRep;
}