TypeFamilies vs. FunctionalDependencies & type-level recursion

[oleg at okmij.org]

> But BetterTypeRep is still a value-level thing.  You want a type-level
> type representation, for reasons I don't yet understand.
>
> 2. Support for overlapping type function equations.

I'd like to have type-level type representations to _implement_
overlapping type function equations. With type level Typeable, you
would not need to do anything about point 2 therefore. The problem 2
will be solved.

> There seems no reason in principle to disallow
> 	type instance F where
> 	  F Int = Bool
> 	  F a = [a]


I would implement this as follows:

> type instance F x = F' (EQ (TYPEOF x) INT) x
> type family F' trep x
> type instance F' TRUE  x = Bool
> type instance F' FALSE x = [x]


Furthermore, type-level Typeable is possible already, although in
quite an ugly way: your can read INT as a Peano numeral, and EQ as
Peano numeral equality. In fact, I have demonstrated such an
implementation (even more complex case, for higher-kinds):
	http://okmij.org/ftp/Haskell/TTypeable/


> That is, the axioms become type-indexed.  I don't know what
> complications that would add.

With TTypeable, none of that would be needed. Overlapping Instances
just become redundant.


> So, let me ask: does anyone (eg Oleg) have concrete proposals on the
> table for things they'd like GHC to do?

First of all, can something be done about the behavior reported by
David and discussed in the first part of the message

   http://www.haskell.org/pipermail/haskell-prime/2011-July/003489.html

That is, if *no* undecidable instances are used, the type checker
should reduce type functions for as long as needed. No context
restrictions should be used.

Second, what is the status of Nat kinds and other type-level data that
Conor was/is working on? Nat kinds and optimized comparison of Nat
kinds would be most welcome. Type level lists are better still
(relieving us from Goedel-encoding type representations).

Would it be possible to add TYPEREP (type-level type representation)
as a kind, similar to that of natural numbers and booleans?

Finally, could GHC automatically derive instances of TTypeable, which
maps types to TYPEREP:
	type family TTypeable (x :: *) :: TYPEREP

	Cheers,
	Oleg