Data.Dynamic without typeclasses or unsafeCoerce

{-# LANGUAGE RankNTypes, GADTs #-}

data DYN t where
 BOOL :: DYN Bool
 INT :: DYN Integer
 (:->:) :: DYN a -> DYN b -> DYN (a -> b)

data DYNAMIC where UnDYNAMIC :: DYN t -> t -> DYNAMIC
data Equal a b where REFL :: Equal x x

mkDyn :: DYN t -> t -> DYNAMIC
mkDyn code obj = UnDYNAMIC code obj

decide :: DYN t -> DYN u -> Maybe (Equal t u)
decide BOOL BOOL = Just REFL
decide INT INT = Just REFL
decide (u :->: v) (p :->: q) = do REFL <- decide u p; REFL <- decide v q; return REFL
decide _ _ = Nothing

unbox :: DYNAMIC -> DYN t -> Maybe t
unbox (UnDYNAMIC t e) u = do REFL <- decide t u; return e

list = [ mkDyn BOOL True, mkDyn INT 34, mkDyn (BOOL :->: INT) (\x -> if x then 32 else 56) ]

-- > unbox (list !! 0) BOOL
-- Just True
-- > unbox (list !! 1) BOOL
-- Nothing
-- > unbox (list !! 2) BOOL
-- Nothing
--
-- > unbox (list !! 0) INT
-- Nothing
-- > unbox (list !! 1) INT
-- Just 34
-- > unbox (list !! 2) INT
-- Nothing
--
-- > fmap ($ True) (unbox (list !! 2) (BOOL:->:INT))
-- Just 32
-- > fmap ($ False) (unbox (list !! 2) (BOOL:->:INT))
-- Just 56
-- > fmap ($ True) (unbox (list !! 1) (BOOL:->:INT))
-- Nothing