Oleg | > 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] But you have just pushed the problem off to the definition of EQ. And your definition of EQ requires a finite enumeration of all types, I think. But * is open, so that's hard to do. What you want is type instance EQ where EQ a a = TRUE EQ _ _ = FALSE and now we are back where we started. Moreover, encoding the negative conditions that turn an arbitrary collection of equations with a top-to-bottom reading into a set of independent equations, is pretty tedious. | 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 OK. Can you give a small standalone test case to demonstrate the problem, and open a Track ticket for it? | Second, what is the status of Nat kinds and other type-level data that | Conor was/is working on? Julien is working hard on an implementation right now. The Wiki page is here http://hackage.haskell.org/trac/ghc/wiki/GhcKinds Attached there are documents describing what we are up to. | Would it be possible to add TYPEREP (type-level type representation) | as a kind, similar to that of natural numbers and booleans? Yes! See 5.4 of "the theory document". It's still very incoherent, but it's coming along. Simon