Hello, Recently, someone (I forgot who, exactly) mentioned in #haskell this article: http://okmij.org/ftp/Haskell/types.html#unsound-typeable where Oleg demonstrates that Typeable makes the type system unsound, and one can get back unsafeCoerce (which is used in the implementation, I suspect). However, this evening, Ryan Ingram showed how to construct a safe Typeable using GADTs. The problem with that, of course, is that GADTs aren't open, so one can only have a predefined number of Typeables. However, it occurred to me that data families don't have that problem, so I took a shot and came up with the following: {-# LANGUAGE TypeFamilies, ScopedTypeVariables, GADTs , MultiParamTypeClasses, FlexibleInstances, OverlappingInstances #-} class Typeable t where data TypeRep t :: * typeRep :: TypeRep t instance Typeable Int where data TypeRep Int = TInt typeRep = TInt instance Typeable Integer where data TypeRep Integer = TInteger typeRep = TInteger instance Typeable () where data TypeRep () = TUnit typeRep = TUnit data TEq a b where Refl :: TEq a a class (Typeable a, Typeable b) => TEquality a b where teq :: TypeRep a -> TypeRep b -> Maybe (TEq a b) instance (Typeable a) => TEquality a a where teq _ _ = Just Refl instance (Typeable a, Typeable b) => TEquality a b where teq _ _ = Nothing cast :: forall a b. (TEquality a b) => a -> Maybe b cast a = do Refl <- teq ta tb return a where ta :: TypeRep a ta = typeRep tb :: TypeRep b tb = typeRep Which, somewhat to my surprise, actually works. And, of course, if one tries to pull off Oleg's trick: newtype Oleg a = Oleg { unOleg :: a } instance Typeable (Oleg a) where TypeRep (Oleg a) = ... typeRep = ?? Well, it won't work, because TypeRep () ~/~ TypeRep (Oleg a). However, obviously, this depends on overlapping instances (if there's some other way, I'd be happy to know; if type inequality contexts are available, I wasn't able to find them), and I've heard that type families don't play well with overlap. Does that not apply to data families? Will this construction still work in 6.10 and beyond? Also, this doesn't seem to be a suitable basis for Dynamic. Trying to extend the GADT solution presented resulted in errors unless incoherent instances were turned on (clearly not a good sign), and even then, it didn't actually work. Is it possible to do better, and come away with something that will actually work for Dynamic, and be sound? Is there some other trick waiting to pull unsafeCoerce out of this setup (seems doubtful, as it isn't used in the code, and the type families folks have no doubt done plenty of work to ensure soundness)? Comments appreciated. -- Dan