-- Code from Section 12.3

module Dynamic where
import PhantomTypes
import Monad

data Dynamic = forall t . Dyn (Type t) t

data Type t =              RInt  (Int     :=: t)
            |              RChar (Char    :=: t)
            | forall a   . RList ([a]     :=: t) (Type a)
            | forall a b . RPair ((a,b)   :=: t) (Type a) (Type b)
            |              RDyn  (Dynamic :=: t)

rInt :: Type Int
rInt = RInt refl

rChar :: Type Char
rChar = RChar refl

rList :: forall a . Type a -> Type [a]
rList t = RList refl t

rPair :: forall a b . Type a -> Type b -> Type (a,b)
rPair t1 t2 = RPair refl t1 t2

rString :: Type String
rString = rList rChar

tequal :: forall t s . Type t -> Type s -> Maybe (t->s)
tequal (RInt p1) (RInt p2) = return (from p2 . id . to p1)
tequal (RChar p1) (RChar p2) = return (from p2 . id . to p1)
tequal (RList p1 ra1) (RList p2 ra2) 
 = liftM (\f -> from p2 . map f . to p1) (tequal ra1 ra2)
tequal (RPair p1 ra1 rb1) (RPair p2 ra2 rb2)
 = liftM2 (\f1 f2 -> from p2 . pair f1 f2 . to p1) 
          (tequal ra1 ra2) 
          (tequal rb1 rb2)
        where pair f1 f2 (a,b) = (f1 a,f2 b)
tequal (RDyn p1) (RDyn p2) = return (from p2 . id . to p1)
tequal _ _ = Nothing

cast :: forall t . Dynamic -> Type t -> Maybe t
cast (Dyn ra a) rt = fmap (\f -> f a) (tequal ra rt)