I have implemented type-level TYPEREP (along with a small library for higher-order functional programming at the type level). Overlapping instances may indeed be avoided. The library does not use functional dependencies either. http://okmij.org/ftp/Haskell/TTypeable/ David Mazi`eres suggested a good test
A good test would be whether superclasses let you eliminate N^2 mtl instances and do something equivalent to:
instance (Monad m) => MonadState s (StateT s m) where get = StateT $ \s -> return (s, s) put s = StateT $ \_ -> return ((), s)
instance (Monad (t m), MonadTrans t, MonadState s m) => MonadState s (t m) where get = lift get put = lift . put
Exactly this code is implemented in Example.hs. Here's an excerpt:
-- Default instance
instance (Monad (t m), MonadState m, MonadTrans t) => MonadState' (t m) HFalse where type MState' (t m) HFalse = MState m get' _ = trace "Default get" $ lift get put' _ = lift . put
-- Special instances
instance (Monad m) => MonadState' (StateT s m) HTrue where type MState' (StateT s m) HTrue = s get' _ = trace "Special get" . StateT $ \s -> return (s, s) put' _ s = StateT $ \_ -> return ((), s)
-- add more special instances if needed ...
plus one more general dispatching instance. Because of the additional flag, HTrue vs HFalse, the above instances do not overlap.
The key piece of magic I need here (and in so many other places) is to be able to do one thing at the type level if x is a particular type (e.g., NoSelector) or sometimes one of a small number of types, and to do something else if x is any other type.
TTypeable.hs does exactly that.
You'd need to be able to do things like:
-- Type-level if-then-else closed type family IfEq :: * -> * -> * -> * -> * type instance IfEq a b c d = d type instance IfEq a a c d = c
The code does that.
I also can't quite figure out how to pass around ad-hoc polymorphic functions the way you can with proxy types and a class such as:
class Function f a b | f a -> b where funcall :: f -> a -> b
And that too. Although the code is usable already, a bit of sugaring from GHC would greatly help. At the very least, automatic deriving of TYPEOF. A longer wish is for a a built-in equality comparison on TyCon_name. Perhaps we might wish to begin to consider if overlapping instances could be deprecated?