Tomasz Zielonka wrote:

Speaking about casts, I was playing with using GADTs to create a non-extensible version of Data.Typeable and Data.Dynamic. I wonder if it's possible to write such a thing without GADTs (and unsafeCoerce, which is used in Data.Dynamic, IIRC).

Absolutely. Stephanie Weirich did that back in 2000 (actually, earlier: her paper, TypeSafe cast was presented at ICFP'00). The code does not use existentials -- only universals. BTW, if you don't plan to store your dynamics in a data structure (or plan to cast them to the same thing), then no explicit quantification is needed and the code becomes Haskell98. Here's her code for the cast, with slight embellishments. It should be pointed out that we can cast polymorphic lists and polymorphic functions. There is a different way to perform casting within a closed universe, see http://www.mail-archive.com/haskell@haskell.org/msg13089.html {-# OPTIONS -fglasgow-exts #-} module CWeirich where class CF a where cast :: CT b => a -> Maybe b class CT b where cBool :: Bool -> Maybe b cBool = const Nothing cInt :: Int -> Maybe b cInt = const Nothing cList :: CF a => [a] -> Maybe b cList = const Nothing cFun :: (CT b1, CF a2) => (b1->a2) -> Maybe b cFun = const Nothing instance CF Bool where cast = cBool instance CF Int where cast = cInt instance CF a => CF [a] where cast = cList instance (CT b1, CF a2) => CF (b1->a2) where cast = cFun instance CT Bool where cBool = Just instance CT Int where cInt = Just instance CT b => CT [b] where cList x = mapM cast x instance (CT b2, CF a1) => CT (a1->b2) where cFun f = let f' :: a1 -> Maybe b2 f' x = maybe Nothing (cast . f) (cast x) f'' x = maybe undefined id (f' x) in maybe Nothing (const $ Just f'') (f' undefined) -- This is a universal rather than existential type! data Dyn = Dyn {fromDyn :: forall b. CT b => Maybe b} toDyn :: CF a => a -> Dyn toDyn a = Dyn (cast a) td1 = toDyn True td2 = toDyn [1::Int, 2,3] td3 = toDyn not tf1 = fromDyn td1 :: Maybe Bool tf2 = fromDyn td1 :: Maybe Int tf3 = fromDyn td2 :: Maybe [Int] tf4 :: Maybe Bool = maybe Nothing (\f -> Just $ f True) (fromDyn td2) tf5 :: Maybe Bool = maybe Nothing (\f -> Just $ f True) (fromDyn td3) tf6 :: Maybe Int = maybe Nothing (\f -> Just $ f True) (fromDyn td3)