Deriving Typeable -- possible improvement

[Simon Peyton-Jones]

| iterIO uses mkTyCon for the simple reason that ((Typeable t, Typeable
| m) => Iter t m) is Typeable1 and there is no automatic way of deriving
| Typeable1.	

This email is triggered by a thread on Haskell Cafe about changes to the Typeable class
http://www.mail-archive.com/haskell-cafe@haskell.org/msg91830.html
It proposes a modification to the way Typeable is derived; and concludes with a question.

Simon


David Mazieres and others comment that you can't derive Typeable for types like this:
	data T f = MkT (f Int)
So he defines his own instance like this
[C]	instance Typable1 f => Typeable (T f) where
          typeOf = ...

So why can't GHC do this?  Well, here's what GHC does. Given a bog standard data type like Maybe
	data Maybe a = Nothing | Just a deriving( Typeable )
GHC generates this instance
[A]	instance Typeable1 Maybe where
	   typeOf = ...
Remember that Typeable1 takes a type *constructor*, of kind (*->*), as its argument.

Now if we need (Typeable (Maybe Int)), GHC first uses an instance from the Typeable library:
[B]	instance (Typeable1 f, Typeable a) => Typeable (f a) where
	  typeOf = ...

And now it uses the (Typeable1 Maybe) instance [A].  So it's kind of cool... the applications are decomposed by [B], leaving the tycon to [A].


But this doesn't work for T above.  We can't make (Typeable1 T) because T has kind ((*->*)->*), not (*->*) as Typeable1 requires.  Hence David defining his own instance.

GHC could do this too.  Indeed it could do so for Maybe too, thus:
	instance Typeable a => Typeable (Maybe a) where 
	  typeOf = ...

But then, alas, we could not get (Typeable (T Maybe)), because [C] needs Maybe to be in Typeable1.

========== PROPOSAL ==============
So here is a compromise, which would at least do better than the current story:

	When deriving Typeable for a data type S of kind
		S :: k1 -> .. -> kn -> * -> ... -> *
	(where kn is not *, and there are M trailing * arguments),
	generate the instance
	   instance (Typeable_x1 a1, ..., Typeable_xn an)
                => TypeableM (S a1 .. an)

That is, knock off all the trailing * args, and then generate an instance for the remaining stub. 

===================== EXAMPLE ============
Example from iterIO:

newtype Iter (t :: *) (m :: *->*) (a :: *)
   = Iter { runIter :: Chunk t -> IterR t m a }
   deriving( Typeable )

This should generate

	instance (Typeable t, Typeable1 m) => Typeable1 (Iter t m) 

where we knock off the trailing (a :: *) argument.

================== QUESTION =================
This approach is not beautiful.  It does not solve the underlying problem, which is a lack of kind polymorphism, but that is a battle for another day.  Until that day, this alternative way of deriving Typeable would automate significantly more cases, I think.  Of course, it also makes it more complicated to explain when "deriving Typeable" will succeed.

Any opinions?  Does anyone care?

Simon