¿Es posible tener un sinónimo de tipo asociado con variables no mencionadas en la clase de tipo?

Question

En Associated Type Synonyms (Chakravarty, Keller, Jones) el papel parece indicar que lo siguiente es válido:

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

Sin embargo, cuando intento ejecutar este recibo un error del compilador (con -XTypeFamilies):

Not in scope: type variable `k' 

¿Me falta algo, o la implementación real en GHC no es la misma que se menciona en el documento?

Answer 1

Como ya se enteraron, this is not possible in GHC:

Exactamente como en el caso de una declaración de datos asociada, los parámetros de tipo con nombre debe ser una permutación de un subconjunto de los parámetros de clase. Ejemplos

class C a b c where { type T c a :: * } -- OK 
class D a where { type T a x :: * }  -- No: x is not a class parameter 
class D a where { type T a :: * -> * } -- OK 

El billete se ha referido al hecho explica la razón de no poder definir algo como S. Funciona si lo haces así:

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

Sin embargo, ahora estás atrapado con un nuevo tipo de datos. El uso de sinónimos tipo no funcionará ("Tipo sinónimo 'TupK' debe tener 2 argumentos"), y agregar más parámetros a S no ayudará ("El número de parámetros debe coincidir con la declaración familiar; esperado 1"), como se documenta en boleto.

Answer 2

No, pero se puede hacer a los menos poderosos:

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

... que podría servir para el mismo propósito, si usted no necesita la potencia adicional.