module Data.OpenWitness.Typeable.Rep where
{
import Data.Witness;
import Data.OpenWitness;
import Data.Maybe;
data Rep2 p where
{
SimpleRep2 :: IOWitness (p () ()) -> Rep2 p;
};
matchRep2 :: Rep2 a -> Rep2 b -> Maybe (EqualType (a () ()) (b () ()));
matchRep2 (SimpleRep2 wa) (SimpleRep2 wb) = matchWitness wa wb;
data Rep1 p where
{
SimpleRep1 :: IOWitness (p ()) -> Rep1 p;
ApplyRep1 :: Rep2 p -> Rep a -> Rep1 (p a);
};
matchRep1 :: Rep1 a -> Rep1 b -> Maybe (EqualType (a ()) (b ()));
matchRep1 (SimpleRep1 wa) (SimpleRep1 wb) = matchWitness wa wb;
matchRep1 (ApplyRep1 tfa ta) (ApplyRep1 tfb tb) = do
{
MkEqualType <- matchRep2 tfa tfb;
MkEqualType <- matchWitness ta tb;
return MkEqualType;
};
matchRep1 _ _ = Nothing;
data Rep a where
{
SimpleRep :: IOWitness a -> Rep a;
ApplyRep :: Rep1 p -> Rep a -> Rep (p a);
};
instance SimpleWitness Rep where
{
matchWitness (SimpleRep wa) (SimpleRep wb) = matchWitness wa wb;
matchWitness (ApplyRep tfa ta) (ApplyRep tfb tb) = do
{
MkEqualType <- matchRep1 tfa tfb;
MkEqualType <- matchWitness ta tb;
return MkEqualType;
};
matchWitness _ _ = Nothing;
};
instance Eq1 Rep where
{
equals1 r1 r2 = isJust (matchWitness r1 r2);
};
}