Can someone point me at a good set of examples for defining Typeable or Typeable1 instances for GADTs in Haskell.

Or, can someone just show my how to define Typeable (manually) for the following GADT.

data V a where
    Unit :: V () 开发者_运维知识库
    Pair :: V a -> V b -> V (a, b) 
    L :: V a -> V (Either a b) 
    R :: V b -> V (Either a b) 
    Fresh :: Int -> V a

Alternately a pointer to the paper that introduced the idea would also be helpful.

Looks like the website is gone now, but the wayback machine still has the site that links to all the original papers: http://web.archive.org/web/20080622204226/http://www.cs.vu.nl/boilerplate/

In any case, Typeable is almost completely mechanical. You can just derive it, even for GADTs, via the DeriveDataTypeable extension. At least when the kind is * -> *, as in your example.

I can also give an example of manually providing a Typeable1 instance, but it will be deprecated in the next version of GHC. The interface used for creating instances by hand is changing.

{-# NOINLINE vTyCon #-}
vTyCon :: TyCon
vTyCon = mkTyCon "ModuleName.V"

instance Typeable1 V where
    typeOf1 _ = mkTyConApp vTyCon []

The NOINLINE pragma is actually important, since mkTyCon does unsafe stuff under the hood. This is why it's best to just let GHC derive the instance manually, if possible.

My understanding is the part that will be changing in future versions of GHC is that you should use a different function, mkTyCon3, which takes the package name, module name, and type name as separate arguments. That's a clear improvement, even if makes supporting multiple version of GHC tougher. See: Changes to Data.Typeable.

All of the above is really old.

From the GHC docs:

Also since GHC 7.8.1, handwritten (ie. not derived) instances of Typeable are forbidden, and will result in an error.

You should never need, or even be allowed, to write a Typeable instance by hand with any modern version of GHC. In fact, you don't even need to tell GHC to derive them - it will do that automatically.