[Haskell-cafe] Issues(Bugs?) with GHC Type Families

[Manuel M T Chakravarty]

Hugo Pacheco:
> I have recently tried to replicate some examples from in the  
> articles about type families but found some possible bugs.
>
> In [2], the example
>
> class C a where
>     type S a (k :: * -> *) :: *
> instance C [a] where
>     type S [a] k = (a,k a)
>
> does not compile under the claim that the type variable k is not in  
> scope.
>
> However, if we extract the type family from the class
>
> type family S a (k :: * -> *) :: *
> type instance S [a] k = (a, k a)
> class C a
>
> it compiles correctly.
> According to [3], the difference is purely syntactic sugar, does  
> that mean that both examples should compile and behave the same or  
> is there some subtlety that justifies the class example not to  
> compile?

I am sorry for the confusion this causes, but we wrote the paper  
before the implementation in GHC was finalised.  Hence, the  
implementation deviates from the paper in some aspects.  Generally,  
please use

   http://haskell.org/haskellwiki/GHC/Type_families

(which will be integrated into GHC's Users Manual for 6.10) as the  
definite guide to the implementation.

Here a brief rational for this change in design.  We originally  
intended to distinguish between type parameters that do use type  
indexing (the a in (S a k)) and those that do not (the k in (S a  
k)).    However, we found later that this leads to implementation  
problems.  The new rule is that any explicitly named parmeters, eg, s  
and k in

   type family S a (k :: * -> *) :: *

are indexed.  If you don't want to use the second parameter as an  
index, write

   type S a :: (* -> *) -> *

This is also simpler to explain, as simply *all* explicitly named  
parameters in a type family declaration are indicies.

> Another issue is that data kinds (used in both [2] and [3]) do not  
> seem to be supported at all by the compiler, are they already  
> implemented in GHC?
>
> Simple examples such as
>
> datakind Nat = Zero
> or
> datakind Nat = Zero | Succ Nat
>
> fail to compile.

No, datakinds aren't supported yet.  We still intend to add them, but  
our first priority is to thoroughly debug the existing functionality  
and especially to make sure the interaction with GADTs works well.

Thanks for the feedback.

Manuel