Sorry, I got a bit lost in this discussion. Let me try to provide a summary.

Current status: I have a local branch with the new poly-kinded Typeable working fine.
It works as described in [1]. It actually allows deriving Typeable for things involving
the Constraint kind, but this can be easily disabled. Either way, I think most of this
is necessary for whatever might follow next. But I'm not sure of how to push the changes,
because I had to make some changes to these repos: array, containers, dph,
template-haskell, and vector. Worse, I also had to change time, which gets built from
a tarball. It might not be worth contacting the authors of these packages for changes
if we're still going to get rid of "deriving Typeable" altogether, so I've been holding this
back.

It's been proposed to remove the possibility to derive Typeable or write instances for it.
I'm supposing the way that this would be implemented would be:

7.8: Any uses of "deriving Typeable" would give rise to a warning saying that it is no longer
necessary. Any instances of Typeable would give rise to a warning saying that this code
is being ignored, and replaced by an internal Typeable instance. Packages might break,
or change runtime behaviour due to this change.

7.10: Explicit uses of "deriving Typeable" or instances are an error.

Regarding split :: (a ~ f i) => Dict (Typeable f, Typeable i), I'm not sure I can judge how
much work that would be. But let's first try to draft a plan for removing Typeable definitions
from the user, and then consider more extensions.


Cheers,
Pedro

[1] http://hackage.haskell.org/trac/ghc/wiki/GhcKinds/PolyTypeable

On Tue, Oct 16, 2012 at 8:32 AM, Emil Axelsson <emax@chalmers.se> wrote:
2012-10-15 23:50, Gábor Lehel skrev:

On Mon, Oct 15, 2012 at 7:58 AM, Emil Axelsson <emax@chalmers.se> wrote:

I have a use case:


http://hackage.haskell.org/packages/archive/syntactic/1.3/doc/html/Data-DynamicAlt.html

This is a reimplementation of Data.Dynamic to support casting type `a` to
`Dynamic` given a constraint `Typeable (a -> b)`:

   toDyn :: Typeable (a -> b) => P (a -> b) -> a -> Dynamic

With your suggestion, it seems I should be able to use the ordinary
Data.Dynamic instead.

/ Emil


Great! Do you like my plan? Or perhaps know of a better one?

(Relatedly, *does* this have to go through a separate libraries
process? Or are we considering Typeable as getting completely
replaced, and everything pertaining to it gets discussed here?)

Your plan certainly seems general enough! But I'm afraid I can't really speak about the implications on libraries etc.

/ Emil