[Haskell-cafe] Sound typeable via type families?

[Ryan Ingram]

On 3/27/08, Dan Doel <dan.doel at gmail.com> wrote:
>  class Typeable t where
>    data TypeRep t :: *
>    typeRep :: TypeRep t

This is a really interesting idea.  Sadly, I can't think of a way to
make it work.

The biggest problem is the TEquality class; by putting teq in a
typeclass, the decision of which teq to call (and thus, whether or not
to return Just Refl or Nothing) is made at compile time.  The GADT
solution puts that decision off until run-time; the case statement in
teq allows a decision to be made at that point.

What we'd really like to do is something like the following:

class Typeable t where
    data TypeRep t :: *
    typeRep :: TypeRep t
    typeEq :: forall t2. TypeRep t2 -> Maybe (TEq t t2)

instance Typeable Int where
    data TypeRep Int = TInt
    typeRep = TInt
    typeEq rep = case rep of
        TInt -> Just Refl
        _ -> Nothing

But you can't case analyze t2 in this way; each TypeRep is an
independent data type and there's no way to determine which one you
have (aside from some sort of typeable/dynamic constraint, and then we
have a circular problem!)

Perhaps there is a solution, but I'm not clever enough to find it.

  -- ryan