Sorry for the late reply.
GHC does not accept the following program: {-# LANGUAGE TypeFamilies #-} x :: () x = const () (eq a b) where a :: S(S(S(S(S(S(S(S(S(S(S(S(S(S(S(S(S(S(S(S(S(Z))))))))))))))))))))) a = undefined b :: S(S(S(S(S(S(S(S(S(S(S(S(S(S(S(S(S(S(S(S(S(Z))))))))))))))))))))) b = undefined eq :: a -> b -> NatEq a b eq _ _ = undefined
Notice that there are no undecidable instances required to compile this function (or the portions of your TTypeable that this function depends on). Yet GHC is still limiting my context stack (to 21 by default). Obviously any kind of unicode encoding of type names is going to run into the same sort of problem.
I would call this a bug, a recent one. Old versions of GHC (before 6.10, I think) imposed no context stack restrictions on programs with decidable instances. Such a restriction is a recent addition (perhaps introduced as a safe-guard since it was discovered that the old versions of GHC did not properly implement the coverage condition). I would recommend to file this as a bug, including the sample code above. Your old message argues well why this new behavior should be considered as a bug.
But now the comparison of types is depending on this context stack and likely worsening the problem.
I agree that dependence on the arbitrary limit is unsatisfactory. That is why I was hoping that Nat kinds will eventually make their way into GHC (there are many arguments for their inclusion, and some people are reportedly have been working on them).
Finally, I still think most of the "magic" in everything we've been talking about boils down to being able to have a type variable that can take on any type *except* a certain handful. This would allow us to avoid overlapping instances of both classes and type families, would allow us to define TypeEq, etc. Moreover, it would be a more direct expression of what programmers intend, and so make code easier to read. Such a constraint cannot be part of the context, because
Alas, such `type variables' with inequality constraints are quite complex, and the consequences of their introduction are murky. Let me illustrate. First of all, the constraint /~ (to be used as t1 /~ Int) doesn't help to define TypeEq, etc. because constraints are not used when selecting an instance. Instances are selected only by matching a type to the instance head. Instance selection based on constraints is quite a change in the type checker, and is unlikely to be implemented. Let us see how the selection based on mismatch could be implemented. To recall, the constraint "t1 ~ t2" means that there exists a substitution on free type variables such that its application to t1 and t2 makes the types identical. In symbols, \exists\sigma. t1\sigma = t2\sigma We call the type t matches the instance whose head is th if \exists\sigma. th\sigma = t Now, we wish to define selection of an instance based on dis-equality. We may say, for example, that the instance with the head th is selected for type t if \not\exists\sigma. th\sigma = t In other words, we try to match t against th. On mismatch, we select the instance. Let us attempt to define TypeEq class TypeEq a b c | a b -> c instance TypeEq x x True instance TypeEq x (NOT x) False and resolve (TypeEq Int Bool x). We start with Bool: Bool matches x, so the second instance cannot be selected. The first instance can't be selected either. Thus, we fail. One may say: we should have started by matching Int first, which would instantiate x. Matching Bool against so instantiated x will fail, and the second instance will be selected. The dependence on the order of matching leaves a bad taste. It is not clear that there is always some order; it is not clear how difficult it is to find one. I submit that introducing disequality selection is quite a subtle matter. The TTypeable approach was designed to avoid large changes in the type checker. If you attend the Haskell implementors workshop, you might wish to consider giving a talk about overlapping instances and the ways to get around them or implement properly. About dynamic loading [perhaps this should be moved in a separate thread?]
I wish I knew ML better, but from looking at that paper, I can't figure out the key piece of information, which is how to detect overlapping type instance declarations. (Does ML even have something equivalent?)
ML does not have type-classes; they can easily be emulated via dictionary passing. Also, local open (recently introduced in OCaml) suffices quite frequently, as it turns out. I admit though I don't fully understand the problem:
In the absence of type families, I'm okay using something like haskell-plugins that returns Dynamic. ... With type families, I'm at a loss to figure out how this could even work. You would need to know have a runtime representation of every type family that's ever been instantiated, and you would need to check
Type instance selection (including type family applications) are all performed at compile time. At run-time, when a plug-in is loaded, no instance selection is performed. If you wish to adjust the interfaces of the plug-in based on the host environment, you have to program this directly (by passing dictionaries explicitly). This is not very difficult. Incidentally, several approaches to `typed compilation' (or, de-serialization of typed code) are described at http://okmij.org/ftp/tagless-final/tagless-typed.html#typed-compilation illustrating how to implement a simple type-checker, to run alongside the serializer.