TypeFamilies vs. FunctionalDependencies & type-level recursion

[Simon Peyton-Jones]

| I'd like to summarize the relationship between functional dependencies
| and type functions, and propose a solution that should get rid of
| overlapping instances. The solution does not require messing with
| System-FC. In fact, it can be implemented today (although
| ungainly). A small bit of GHC support will be appreciated.

This sounds good.  I am keen to identify features that provide the expressiveness that you and David and others want.  However my brain is small.

Concerning "1. mutual dependencies" I believe that equality superclasses provide the desired expressiveness.  The code may not look quite as nice, but equality superclasses (unlike fundeps) will play nicely with GADTs, type families, etc. Do you agree?

Concerning "2. combination with overlapping instances", you say "The solution has been described already in the HList paper: provide something the typeOf at the type level. That is, assume a type function "TypeOf :: * -> TYPEREP".  

By "the HList paper" do you mean http://homepages.cwi.nl/~ralf/HList/?  I see no TYPEREP in that paper.  Do you think you might perhaps elaborate your proposed solution explicitly?  Perhaps saying explicitly:
  - This is the support we need from GHC
  - This is how you can then code examples X,Y,Z

I know that all of this is embedded variously in your past writings but I'm not very good at finding exactly the right bits and turning them into proposed features!

Incidentally Pedro's new "deriving Generic" stuff does derive a kind of type-level type representation for types, I think.  It's more or less as described in their paper.
http://www.dreixel.net/research/pdf/gdmh_nocolor.pdf

Thanks

Simon