Nominal type roles and data families

Question

I understand why the new role system and annotations require type (and data) family parameters to be at role nominal.

So I expected when I declared

data family CoordinateRepresentation ty a :: *

that ty and a would get nominal roles. (My actual example is an associated data family, but since I don't think it changes anything I am omitting the extra noise that comes with that.)

What I didn't expect is that when I changed it to

data family CoordinateRepresentation ty :: * -> *

is that the unnamed second type argument still gets a nominal role.

Why is this? Couldn't it safely get a representational role, because doesn't any data instance CoordinateRepresentation ... = ... have to create a fresh constructor? How could that constructor have the opportunity to use its parameter at a nominal role in a way that the compiler can't see? Even though it's an open system and there is separate compilation, I still don't get it.

Answer 1

As a first, minor point: Whether a data family is declared with type variables or with kind signature is currently entirely immaterial, they are just different syntaxes for the same thing. From the GHC User's Guide on data family declarations:

Just as with GADT declarations named arguments are entirely optional, [...]

The major point remains, and has been discussed in this GHC trac thread. Short summary: It is possible, by adding role inference and/or role annotations for data/type families, but it is not yet implemented.