2008/3/3 Hugo Pacheco
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.
It's not entirely syntactical sugar; I believe that when a type family is a member of a type-class it makes the assertion that only the class variables are part of the "function". In the class declaration:
class C a where type S a (k :: * -> *) :: *
there are two arguments to the type function S, but the class C only provides one. Contrast with the following
type Pair a k = (a, k a) class C a where type S a :: (* -> *) -> * instance C [a] where type S [a] = Pair a
datakind Nat = Zero or datakind Nat = Zero | Succ Nat
datakinds are listed under "future work" in the papers I have read; they aren't implemented yet. -- ryan