Is it possible to have an associated type synonym with variables not mentioned in the type class?

Question

In the synonyms of the associated type (Chakravarty, Keller, Jones), the document appears to indicate that the following is true:

class C a where type S a (k :: * -> *) :: * 

However, when I try to run this, I get a compiler error (with -XTypeFamilies ):

 Not in scope: type variable `k' 

Am I missing something or is the actual implementation in the GHC not the same as what is mentioned in the document?

Answer 1

As you already learned, this is not possible in the GHC :

Just as with associated data declarations, parameters of a named type must be a permutation of a subset of the parameters of a class . Examples

 class C abc where { type T ca :: * } -- OK class D a where { type T ax :: * } -- No: x is not a class parameter class D a where { type T a :: * -> * } -- OK 

The ticket you referenced actually explains the reason that you cannot define something like S It works if you do it like this:

 class C a where type S a :: (* -> *) -> * data TupK ak = TupK (a, ka) instance C [a] where type S [a] = TupK a 

However, now you are stuck in a new data type. Using type synonyms will not work ("A synonym of type" TupK "must have 2 arguments"), and adding additional parameters to S will not help ("The number of parameters must correspond to the declaration of the family, expected 1"), as described on the ticket.

Answer 2

No, but you can make it less powerful:

 class C a where type S a :: (k :: * -> *) -> * 

... which can serve the same purpose if you do not need extra power.