[Haskell-cafe] Sound typeable via type families?

[Dan Doel]

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