Roles of Nominal Types and Data Families

Question

I understand why the new system of roles and annotations require that the parameters of the family (and data) be in the role of nominal .

So, I was expecting to announce

 data family CoordinateRepresentation ty a :: * 

so ty and a get nominal roles. (My actual example is a related data family, but since I don't think it is changing anything, I miss the extra noise that comes with it.)

I did not expect that when I changed it to

 data family CoordinateRepresentation ty :: * -> * 

lies in the fact that the indefinite argument of the second type still gets the role of nominal .

Why is this? Could he safely get the representational role because there is no need for a data instance CoordinateRepresentation ... = ... create a new constructor? How could this constructor use its parameter in the role of nominal so that the compiler could not see? Despite the fact that this is an open system and there is a separate compilation, I still do not understand it.

Answer 1

As a first, minor point: regardless of whether a data family is declared with type variables or with a type signature, they are currently completely irrelevant, they are just different syntaxes for the same thing. From the GHC User Guide in data collection declarations:

As with GADT declarations, named arguments are completely optional, [...]

The highlight remains, and has been discussed in this GHC trace stream . Short description: perhaps adding notes about the role and / or role for data / type families, but it has not yet been implemented.