Roles for type families

Now that we have roles, it might be helpful to be able to give a role signature for a data/type family.

At the moment, data/type family constructors have all parameters conservatively assigned to be role N. Thus

data family D a    -- Parameter conservatively assumed to be N

class C a where
  op :: D a -> a

instance C Int where ....

newtype N a = MkN a deriving( C )  -- Rejected

The generalised-newtype-deriving clause deriving( C ) is rejected because D might use its parameter at role N thus:

data instance D [b] = MkD (F b)   -- F is a type function

It would be strictly more expressive if we could

• Declare the roles of D's arguments (as we can declare their kinds). E.g.

data family D a@R

• Check that each family instance obeys that role signature. E.g. given the preceding role signature, reject this instance:

data instance D [b] = MkD (F b)   -- F is a type function

I think there is no technical difficulty here. Just a question of doing it.

Trac metadata

Trac field	Value
Version	7.6.3
Type	Bug
TypeOfFailure	OtherFailure
Priority	normal
Resolution	Unresolved
Component	Compiler
Test case
Differential revisions
BlockedBy
Related
Blocking
CC	goldfire
Operating system
Architecture

changed weight to 5

added Tbug Trac import labels

I would argue that, given the declaration for D above, the following instance should also be rejected:

data instance D (Maybe c) = MkD2 c

Why should that instance be rejected? Because it pattern-matches on its argument. Before thinking about implementing this (which I agree should be straightforward), we need to agree on the design. Here are a few questions to spur discussion:

• What should the default role be for families? Is it different for data and for type families? (I would prefer N for both.)
• Am I right that the instance above should be rejected?
• Consider

type family Flip x@R y@R type instance Flip x y = (y, x)

Is that accepted? I think "yes".

Here are some proposed rules:

• If a parameter is at role N, its use is unrestricted in instances.
• If a parameter is at role R, it cannot be matched against and it must only appear in R (or P) positions in the RHS of instances.
• If a parameter is at role P, it cannot be matched against and it must only appear in P positions in the RHS of instances.

Thoughts? Let's have the conversation here, and I will put the resolution on the wiki along with writing the implementation.

Harump. You are right. type families are the very source of pattern matching so of course type families should have argument of role N.

You could argue that there might be a parameter of the family that is never matched. Thus:

type family F a@R b@N
type instance F a Int = a -> a
type instance F a Bool = (a,a)

But it's a bit marginal; in most cases you could re-order the args

type family F b@N :: * -> *

and similarly for the instances.

I think it's the same for data families. For example, it'd be utterly wrong to make a newtype coercion between (D Age) and (D Int); so D's parameter must clearly be role N.

In short, the main merit of this ticket would be to allow parametric (non-indexed) parameters to appear before index parameters. That seems a fairly marginal gain.

Simon

I'm not convinced that this is useless, actually. For example, I don't think Simon's last example F could be written without role annotations on type families, even if we switch the order of parameters. And, the kind signature trick doesn't work at all with data families:

data family Q1 :: * -> *

is equivalent to

data family Q2 a

In particular, under the current implementation, instances of Q1 can pattern-match on the parameter. Accordingly, Q1's parameter is currently given role N, just like Q2's.

So, I do think this idea would yield a real expressiveness gain, and I mused about it while implementing the main chunk of roles. Is it worth the extra complexity? Perhaps.

mentioned in issue #8516

mentioned in issue #8672 (closed)

A post on #8672 (closed) seems more relevant here:

Simon PJ says: Richard, two questions. First (Q1), can't a data instance have a representational role inferred? Eg this ought to work. The definition of g is currently rejected.

data family T a
data instance T [b] = MkT b

newtype Age = MkAge Int

g :: T [Age] -> T [Int]
g x = coerce x

Second question (Q2). Are role annotations allowed on data family declarations, where they could indicate which parameters are the indices:

type role T representational nominal  -- Only second param can be an index
data family T a b

data instance T a Bool = ...   -- Allowed
data instance T Bool b = ...   -- Rejected

(And similarly for type families.)

Similarly are role annotations allowed on data instance declarations, where they would be useful in exactly the same way that they are on data decls

data family T a

type role T [a] (a:nominal)
data instance T [a] = MkT a

Here we are running out of syntax! This isn't supported now because I think all parameters are automatically nominal (see Q1 for why they shouldn't be).

Simon

assigned to @rae

Q1: Yes, that's possible. I didn't do it mostly because my stomach lurched when thinking about parsing role annotation concrete syntax for data family instances -- I was going to wait until someone shouted. I considered having data instances go through role inference without allowing for role annotations, but that meant it would be impossible to create a properly abstract data family instance.

Q2: That's possible but currently unimplemented (see earlier posts to this bug report).

So, if we could just figure out a decent concrete syntax, I could make it all work. The hardest part will be updating the parser and HsSyn stuff. The role inference/checking should be almost no work at all.

As a strawman syntax, what about

type role instance T [nominal]

for the case above. Note the word instance to specify that we're talking about the roles on an instance, not on the family T. Then, role names would appear wherever type variables appear in the corresponding instance declaration. Underscores would be supported in these positions, as well (like normal role annotations). The corresponding data (or newtype) instance would have to be in the same module, as usual. The appearance of the word type (as opposed to data) in the role annotation syntax is regrettable, but it conforms to the universal use of the word type in all role annotations.

Though it makes me want to cry, I suppose we should allow associated role instance annotations, in class instance definitions alongside associated data/newtype instances.

Does anyone out there actually want to use this feature? Eager users would help motivate all this! :)

@goldfire, conflating list syntax seems red flaggy...

that said, having some way of describing these properties seems important, though i'm not sure if i'm sufficiently sophisticated a library author yet to see a use case for myself as yet

But that's the annotation for the instance

data instance T [a]

If we had an instance

data instance T (Int, Maybe a)

the role annotation would be

type role instance T (Int, Maybe representational)

for example. (Though, that particular annotation would be a no-op, as representational would be inferred.) I don't believe I'm conflating list syntax here...

you may be right! I'll reread this ticket when i'm a bit more awake :)

See also this thread on the GHC users list, which offers (I think) another example of the importance of this feature.

Simon

I agree that the vector issue is related to this feature. In summary, we would like the following to work (greatly simplified from vector WLOG):

class MVectorClass (v :: * -> * -> *) a where
    basicLength :: v s a -> Int

data family MVector s a

data instance MVector s Int -- implementation not important

newtype Age = Age Int deriving (MVectorClass MVector) -- rejected

The deriving is rejected because it generates

basicLength =
    coerce (basicLength :: MVector s Int -> Int) :: MVector s Age -> Int

If my understanding of role inference is correct, allowing

type role instance MVector nominal representational

would allow for this coerce to take place.

This means that we can't currently derive Unbox instances for vectors of newtypes (see https://github.com/haskell/vector/issues/16), which is rather unfortunate.

changed weight to 7

Trac metadata

Trac field	Value
Priority	normal → high

Trac metadata

Trac field	Value
CC	goldfire → goldfire, hackage.haskell.org@liyang.hu

changed weight to 5

Hmm... well, this just got a little more complicated. The full example John just posted would not be solved by fixing this ticket. That's because the data instance for MVector pattern-matches on Int. Currently in GHC, it would be sound to have both the instance given and a separate instance ending in Age, and have these instances be unrelated. Accordingly, if the MVector were declared to have a representational role for its last parameter, the instance given would be rejected for pattern-matching on a representational parameter.

What it seems John wants is something new -- a data family that does representational matching, not nominal matching. Such a beast would consider data instance MVector s Int and data instance MVector s Age to overlap. Along similar lines, if a MVector s Age were requested, GHC would serve up the instance for MVector s Int.

While I can imagine implementing such a feature (essentially by preventing newtypes from appearing in instance declarations, much like how type families can't appear in instance declarations today... and then normalizing with respect to newtypes at usage sites), the ramifications of the design are far from clear. In particular, what if the constructor of a newtype is not available? It would also mean, for example, that if a library exports a newtype Foo abstractly, a user wishing to have an MVector instance for Foo would need to know Foo's representation type, something that the library author thought was hidden from users. It's all a little murky.

So, I'm saying that John's use case does not qualify for this ticket, and I'll un-bump its priority. John, if in light of my analysis (and if you agree with it!) you still want this feature, create a new feature request with the priority you feel is appropriate. This seems related but quite separable to the features requested in this ticket.

Trac metadata

Trac field	Value
Priority	high → normal

It's only outside the scope of this request if you insist on the rule that parameters at role R can't be matched against. I think I agree with Richard's analysis that this would entail a data family that does representational matching.

I do think this is a valuable feature as ghc-7.8 broke code some code in the wild, so I'll make a new ticket.

mentioned in issue #9112

This would be helpful for one implementation that Bjorn Buckwalter and I are working on for the next generation version of the dimensional library.

dmcclean: can you say more precisely what "this" is? There are various designs floating about in this ticket, and ticket:8177#comment:82781 indicates that the one in the Ticket Description would not solve the problem identified in ticket:8177#comment:82776.

Better still, can you give a concrete, standalone example of what you want/need?

Simon

Yes, my apologies Simon.

This is actually going to be an interesting example, perhaps, because I learned something about this since yesterday when I wrote that comment.

This example is slightly longer than I would like, I'm eliding a few things but I'm not sure exactly which details (e.g. the data family being associated) matter.

class KnownVariant (var :: Variant) where
  -- | A dimensional value, either a 'Quantity' or a 'Unit', parameterized by its 'Dimension' and representation.
  data Dimensional var :: Dimension -> * -> *
  -- elided: some functions to allow us to introduce and eliminate the quantities or units

instance KnownVariant DQuantity where
  newtype Dimensional DQuantity d v = Quantity' v
    deriving (Eq, Ord, Enum)
  -- elided: function implementations

instance KnownVariant (DUnit p) where
  data Dimensional (DUnit p) d v = Unit' UnitName v
  -- elided: function implementations

data Variant = DQuantity | DUnit Prefixability
type Quantity = Dimensional DQuantity
type Unit p = Dimensional (DUnit p)

So I set up all that machinery, and then I was curious whether we could coerce in and out of the Dimensional DQuantity d newtype. So I thought that the way to find out was by asking GHCi what the role of Dimensional was. In concept it's nominal phantom representational, but it would be extremely complicated for the compiler to see that because it would have to examine all the (both the) instances and so forth, so I didn't know what to expect.

Numeric.Units.Dimensional.DK> :i Dimensional
class KnownVariant (var :: Variant) where
  type role Dimensional nominal nominal nominal
  data family Dimensional (var :: Variant) ($a :: Dimension) $b
  ...

So I read that, and thought that it meant we were out of luck.

But, unexpectedly to me, but undoubtedly for a reason that is quite obvious to someone, and this is the part I only discovered last night:

> let x = 3.7 :: Double
> x
3.7
> let y = (coerce x) :: Mass Double
> y
3.7 kg
> let x' = (coerce y) :: Double
> x'
3.7

Somehow it even seems to be OK when you abstract over the dimension with RankNTypes, which isn't really a need but is just something I thought to investigate to see if that was the difference between my expectation of how this would work and how it in fact did work.

> let f = coerce :: (forall d.Double -> Quantity d Double)
> (f 3) :: Mass Double
3.0 kg

In conclusion, I now believe that I was too hasty yesterday, and that in fact this ticket doesn't impact me at all.

My sincere apologies to everyone copied on this ticket. If someone happened to have the time and knew the answer, it would be awesome if you you could help me fix my understanding about whether this should or shouldn't work and what the interplay with roles is, but otherwise I will merrily go about my business. :)

Roles for data families (associated or not) cannot be inferred, because they are open. But, theoretically, they can be declared and then checked. That is the subject of this ticket. So, it conceivable to give the roles you ask for.

But, you don't seem to need those roles, because you seem interested in coercing in and out of the newtype, not among different instantiations of the newtype. This is possible as long as the newtype constructor (Quantity') is in scope. Roles aren't a part of the story, in your case.

Hmmm.

I was concerned there for a second, because actually Quantity' won't be in scope for my users. Its not exported from the module because you can use it to do nefarious things.

So I thought that my test in GHCi had been insufficiently thorough, because GHCi doesn't respect the export list and lets you get at unexported things for convenience.

So I made a new module to try it.

import Numeric.Units.Dimensional.DK.Prelude
import Data.Coerce

main = do
         let x = 3.7 :: Double
         let y = (coerce x) :: Mass Double
         putStrLn . show $ y
         -- putStrLn . show $ Quantity' x -- doesn't compile with this line here

It works just fine and prints "3.7 m". With the commented line it doesn't compile, complaining that Quantity' is (as I intended) not in scope. (If it had been in scope, it would still fail because the dimension is ambiguous, but that's not the point.)

So it seems that whether or not the newtype constructor is in scope is not the determining factor here. If it was intended to be, than this may be a bug?

That does look fishy, but I don't see a definition of Mass so I can be sure. Do you have a minimal test case, or a way I can check this myself? If so, please post that as a new ticket, as it's only very tangentially related to this one. Thanks!

mentioned in issue #9580 (closed)

Replying to [ticket:8177#comment:88020 dmcclean]:

Hmmm.

I was concerned there for a second, because actually Quantity' won't be in scope for my users. Its not exported from the module because you can use it to do nefarious things.

BTW I'm confused by this comment, because the things you can do with Quantity' are just the things you can do with coerce, no?

Yes. I was badly confused when I wrote that comment, sorry.

See 9580 for where I broke this out as requested by goldfire. It turns out that the rule is indeed supposed to be that you can only do this coercion when Quantity' is in scope, which makes sense because that is when you could do it longhand, but that 7.8.3 currently implements a more lenient unintentional rule that also lets you do it (at least sometimes?) when you only have the data family in scope.

changed milestone to %⊥

In trying to sweep up remaining tickets assigned to me before the feature freeze, I came across this one.

In ticket:8177#comment:78287, I ask for real users who want role annotations for type and/or data families (and/or their respective instances) to do real work -- preferably with an example of said real work. Though two people came out of the woodwork and tried to meet this need, neither one really qualifies:

• The example from jwlato requires something fundamentally different from this ticket -- the ability to do representational matching on families. That, essentially, has been moved to #9112. The solution there may also require getting this ticket sorted out, but I don't think this ticket is the blocking issue.

• The example from dmmclean is also, by dmmclean's own admission, not applicable here.

Fixing this would take several days worth of work, and days are precious. So I'm going to let this one slip unless convinced otherwise. Thanks!

Making a note here to look at :browse and :info in GHCi if/when we implement this. See also #8672 (closed).

Just a quick note to verify that goldfire is entirely correct WRT #9112; I agree that my example doesn't have much bearing on this ticket at this point.

goldfire, I do have a need for this in order to do "real work"... at some point in the future after #9123 (closed) is fixed :)

My use case is laid out in this comment in #8516. I'm interested in using higher-kinded roles to increase the number of datatypes for which you can derive Generic1 instances by replacing Functor constraints with Representational constraints (where Representational is the typeclass proposed here). Unfortunately, at the moment, my proposed plan would actually //decrease// that number, because there are datatypes defined in terms of type families for which you can declare Functor instances. However, type families always default to nominal roles for its type arguments, which means they can't be Representational! Ack!

It definitely seems like //some// type families should be able to have Representational (or even Phantom!) roles for its arguments. A prime example is from this comment:

type family Id a where
  Id a = a

I have a strong hunch that a should be have a representational role. Unfortunately, I have no way to inform GHC of this.

mentioned in issue #13083 (closed)

I'd like to share my usecase for wanting this feature

Given the following type:

-- | Family of N-ary operator types.
type family Op n a b where
  Op 'Z     a b = b
  Op ('S n) a b = a -> Op n a b

I'd love to be able to

coerce :: Coercible a b => Op n a c -> Op n b c

I want this feature too. My use case is this:

data family EffDict (eff :: k) (m :: Type -> Type)

this data family represents effect methods for some monad m. Its data instances match on eff only, never on m. For example:

data StateEff s
data instance EffDict (StateEff s) m =
  StateDict
    { _state :: forall a . (s -> (a,s)) -> m a,
      _get :: m s,
      _put :: s -> m () }

Define a composition of monad transformers as follows:

newtype TComp t1 t2 m a = TComp (t1 (t2 m) a)

Then I want to be able to do this:

coerce :: Dict eff (t1 (t2 m)) -> Dict eff (TComp t1 t2 m)

Trac metadata

Trac field	Value
CC	RyanGlScott, dmcclean, ecrockett0@gmail.com, goldfire, hackage.haskell.org@liyang.hu → RyanGlScott, dmcclean, ecrockett0@gmail.com, goldfire, hackage.haskell.org@liyang.hu, int-index

I've uploaded a rough attempt at implementing support for roles for closed type families at D3662, although there are still some bugs to work out (for instance, the program in ticket:8177#comment:134941 doesn't typecheck yet, unfortunately).

Trac metadata

Trac field	Value
Differential revisions	- → D3662

I've uploaded a rough attempt at implementing support for roles for closed type families

Great work! But I really would prefer to see a specification first :-). There's a lot of discussion on this thread about what the specification should even be.

It's hard to review an implementation without a spec, covering

• Syntax
• Typing rules (at least in clear English)
• Lots of examples

Of course, we'd ultimately like a proof of soundness of the rules, but the "Richard thinks this is right" tests is at least a start.

Indeed, I will readily admit that I'm mostly parking this Diff here for Richard's sake (when he gets a chance to look at it). However, since you asked politely, I wrote up an (informal) specification of how I envision this would work here, based on the conversations I've had with Richard about this topic, as well as the commentary in this ticket.

I've commented on the wiki page (the specification) and on the diff.

Thanks for replying, Richard! I'll respond to your comments here (since I don't like using wiki pages as a medium of conversation).

• *RAE**: "feels"? Let's prove it! End **RAE**

Hoo boy, I was afraid you were going to demand a proof. I certainly don't have one at the moment.

• *RAE**: There is a difference between roles for data families and data instances. And both might usefully have role annotations. For example:

data family DF a b
type role DF nominal representational

data instance DF Int b = MkDFInt b
-- NB: No scrutinizing the second parameter.
-- Also, b is not used in a nominal context

data instance DF [c] b = MkDFList c b
type role DF [nominal] representational

data instance DF (Maybe d) b = MkDFMaybe d b
type role DF (Maybe representational) representational

With this, we have Coercible (DF (Maybe Age) Int) (DF (Maybe Int) Age) but not Coercible (DF [Age] Int) (DF [Int] Age).

Ah, I think there's a bit of confusion regarding the extent of this design. To be clear, I am not proposing that we give users the power to specify roles the type variables in each //equation//, only the type variables of the parent type family itself. This is because:

1. As your example hints at, we'd need to invent a new syntax for role annotations that match on particular types, and I don't feel anywhere near motivated enough to implement that.
2. The current implementation of role inference does not lend itself well to this design. GHC assigns roles by using a map from TyCon names to roles, but type family equations have neither TyCons nor any kind of unique identifier from which we could look up its roles after inference.
3. This kind of power isn't necessary for the kind of stuff I'd want to do anyways. All I really care about is that the second parameter is designated as representational. I don't really want the ability to coerce between DF (Maybe Age) Int and DF (Maybe Age) Int.

So in your above example:

data family DF a b
type role DF nominal representational
data instance DF [c] b = MkDFList c b
data instance DF (Maybe d) b = MkDFMaybe d b

I would propose that the tyvars in any type pattern which saturates a should inherit the role of a, so c and d would get role nominal in their respective equations. It's not as permissive as it //could// be, but for reasons that I explained above (and I'll make a note of this in the wiki).

I'm a bit worried about problems with what happens if a type constructor that appears as part of a type pattern for an instance is actually a newtype with a role annotation -- could we be breaking soundness with this? Need to think harder.

I don't understand this point.

• *RAE**: This works well for closed type families, but is ineffective with open type/data families (associated or not). I propose that open families default to nominal roles. This is quite like how open families' type variables default to kind Type. Edit: I see this addressed below, but the opening paragraph for this section mentions inference for open families. **End RAE**

Yep, that's my bad. I'll update the intro so as not to mislead readers.

Replying to [ticket:8177#comment:138405 RyanGlScott]:

Hoo boy, I was afraid you were going to demand a proof. I certainly don't have one at the moment.

"Demand"? No. But it would be nice if the design could at least update the various relevant judgments in the "Safe coercions" paper (use the JFP version). It shouldn't be terribly much work, and it's likely that the process of doing so will reveal any glaring problems. And once you have the updated judgments, it's also not terribly hard to follow along the JFP proof and see what lemmas have to be updated.

I'm always daunted by having to revisit the type safety proof. But every time I go through the process, my brain feels nice, limber, and at peace. It's all very much like a good yoga session: it's hard to find the time to do it, it involves painful contortions, and yet you feel quite good at the end.

Ah, I think there's a bit of confusion regarding the extent of this design. To be clear, I am not proposing that we give users the power to specify roles the type variables in each //equation//, only the type variables of the parent type family itself.

Note that instance-specific roles apply only to data families, not type families.

This is because:

1. As your example hints at, we'd need to invent a new syntax for role annotations that match on particular types, and I don't feel anywhere near motivated enough to implement that.

And neither was I, as you'll see in my ticket:8177#comment:78287.

1. The current implementation of role inference does not lend itself well to this design. GHC assigns roles by using a map from TyCon names to roles, but type family equations have neither TyCons nor any kind of unique identifier from which we could look up its roles after inference.

This isn't as bad as you say. Data family instances do have a TyCon. See the DataFamilyInst constructor of FamInstEnv.FamFlavor.

1. This kind of power isn't necessary for the kind of stuff I'd want to do anyways. All I really care about is that the second parameter is designated as representational. I don't really want the ability to coerce between DF (Maybe Age) Int and DF (Maybe Age) Int.

So perhaps you want just roles for type families for now, not data families.

So in your above example:

data family DF a b
type role DF nominal representational
data instance DF [c] b = MkDFList c b
data instance DF (Maybe d) b = MkDFMaybe d b

I would propose that the tyvars in any type pattern which saturates a should inherit the role of a, so c and d would get role nominal in their respective equations. It's not as permissive as it //could// be, but for reasons that I explained above (and I'll make a note of this in the wiki).

But any time a pattern introduces a new tyvar (that's not just a renaming of the tycon tyvar), then the "parent" tyvar's role is always nominal (because you're doing pattern matching). As you note, this is not as permissive as possible. But, I would argue that if you were as permissive as possible, then you'd have no way of making a fully-abstract data family instance. So your design is self-consistent.

I'm a bit worried about problems with what happens if a type constructor that appears as part of a type pattern for an instance is actually a newtype with a role annotation -- could we be breaking soundness with this? Need to think harder.

I don't understand this point.

I was worried about something like this:

newtype Inty a = MkInty Int
type role Inty representational  -- just because I can

data family F a
type role F nominal

data instance F (Inty a) = MkF a
type role F (Inty nominal)

Is this a good idea? I don't know. Keep in mind that data families are injective.

Replying to [ticket:8177#comment:138406 goldfire]:

I'm always daunted by having to revisit the type safety proof.

It's doubly daunting for me because I wouldn't be //re//visiting the proof—I'd be trudging through it for the first time. :)

Not to say that I'm not willing to do this at some point, but it will take me a significant amount of time to invest in understanding the terminology (keep in mind I'm far from an expert on the intricacies of System FC), not to mention figuring out how to typeset all of those crazy typing judgments in TeX.

So perhaps you want just roles for type families for now, not data families.

Well, I //do// want to have roles for data families at some point (I started with closed type families since they're considerably easier to implement). I just don't want to worry about the additional baggage that per-data-instance role annotations would entail.

But any time a pattern introduces a new tyvar (that's not just a renaming of the tycon tyvar), then the "parent" tyvar's role is always nominal (because you're doing pattern matching). As you note, this is not as permissive as possible. But, I would argue that if you were as permissive as possible, then you'd have no way of making a fully-abstract data family instance. So your design is self-consistent.

Absolutely. I'm fine with making nominal roles be overly restrictive, since it dodges thorny issues like data abstraction...

I was worried about something like this:

newtype Inty a = MkInty Int
type role Inty representational  -- just because I can

data family F a
type role F nominal

data instance F (Inty a) = MkF a
type role F (Inty nominal)

Is this a good idea? I don't know. Keep in mind that data families are injective.

1. ..and this sort of thing as well.

mentioned in issue #14101 (closed)

mentioned in issue #15683

Trac metadata

Trac field	Value
Differential revisions	D3662 → -

added Pnormal label

I think this needs a combination of @rae's constrained typed families and Coercible in kinds / data contexts affecting role checking (https://github.com/ghc-proposals/ghc-proposals/pull/233).

data family (Coercible a b => Coercible (T a) (T b)) => T t

I like this better than the original motivation for https://github.com/ghc-proposals/ghc-proposals/pull/233 because unlike with closed definitions, it is impossible to recover properties about all instances after the fact. All you get are the requirements.

This is perhaps not so surprising in hindsight, but one consequence of making data family parameters always have nominal roles is that it prevents you from defining certain instances for them. To see why this the case, let me first set the scene by talking about Traversable. One common complaint about the Traversable class is that it cannot be derived using GeneralizedNewtypeDeriving. This is because of the the type that traverse has:

class (Functor t, Foldable t) => Traversable t where
  traverse :: forall f a b. Applicative f => (a -> f b) -> t a -> f (t b)

Note that traverse is polymorphic over an Applicative f, which means that it's impossible to know a priori what role f's argument has. As a result, one cannot coerce the t b in f (t b), even if t is a newtype. Bottom line: GeneralizedNewtypeDeriving and Traversable do not mix.

One blog post proposes a solution to this problem: add a quantified Coercible superclass to Functor:

class (forall x y. Coercible x y => Coercible (t x) (t y)) => Functor t where ...

Because Functor is a superclass of Applicative, this would then allow one to coerce underneath an Applicative f, which is exactly the scenario we encountered above in the type of traverse. Now we would have the ability to combine GeneralizedNewtypeDeriving and Traversable...

...or so it would seem. As it turns out, there is an unexpected price one must pay in order to add a quantified Coercible superclass to Functor. Consider this simplified code from the GHC.Generics module in base:

data family URec a p
data instance URec Int p deriving Functor

This code would no longer typecheck with the modified form of Functor above:

error:
    • Couldn't match type ‘x’ with ‘y’
        arising from the superclasses of an instance declaration
      ‘x’ is a rigid type variable bound by
        a quantified context
      ‘y’ is a rigid type variable bound by
        a quantified context
    • In the instance declaration for ‘Functor (URec Int)’

The issue here is that URec is a data family, which requires that all of its parameters be nominal. Functor, however, requires that the last parameter act representationally, but GHC provides no mechanism to make data families have this property. As a result, one cannot give data families Functor instances under this design, and as a result, one would not be able to compile even the base library.

added TypeFamilies label

added roles label

#8177 (comment 257671) is a good point. Note that there is nothing stopping us from implementing this ticket. So once there is sufficient motivation, we can do so.

To clarify, by "nothing stopping", I mean that the theory of roles is compatible with putting roles on data/type families, as long as we do so with care. Of course, giving data families roles would also mean giving data instances roles (which might be different from the data family's roles), and then we'd need a syntax for it all. It looks like some of this work is sketched out at https://gitlab.haskell.org/ghc/ghc/wikis/roles#proposal-roles-for-type-families.

mentioned in issue #13153

I just ran into an edge case where this would be very useful trying to encode Structure of Array style arrays using generics and data families (essentially identical to how Data.Vector.Unboxed works). Are we any closer to this issue being solved?

Are we any closer to this issue being solved?

We are neither close nor far.

We're not close because there is no fleshed-out, concrete design for this idea. It would need a syntax to add role annotations to type/data families and also data instances. Also for associated ones. I don't think this design is all that challenging, but someone's got to write it down.

We're not far because, though roles are daunting, I believe that the current theory behind roles extends to this new use-case. If you want to move this along, the first step would be a ghc-proposal, as this would mean a change in the language.

I know this answer isn't really all that encouraging, but there's Real Work to do here!

Would there be any fundamental difficulty in roles for GADTs, as per https://stackoverflow.com/questions/41158070/future-of-roles-for-gadt-like-type-variables?

I've posted to StackOverflow. In short: I have no idea how to proceed with the GADTs issue. That's quite different from the subject of this ticket, which is theoretically straightforward.

I'm a bit less pessimistic. We already have no trouble solving Coercible '[Age, Int, String] '[Int, Age, String] while refusing to solve Coercible '[Age, Int, String] '[String, String, Int]. So the simple annotation type role HList representational may very well do.

The problem is that we would need a much fancier rule for pushing coercions into saturated (representational-GADT worker) constructor applications to be able to give this a reasonable semantics. (This is important both theoretically, for proving progress/preservation theorems, and practically, so the simplifier can work unhindered by these coercions.)

---

We can do something similar today with the following:

type HListR :: [Type] -> Type
type role HListR representational
data HListR a where
  HNilR  :: Coercible li '[] => HListR li
  HConsR :: Coercible li (x ': xs) => x -> HListR xs -> HListR li

But because this only provides a Coercible constraint on the field type, use-sites are very likely to have to coerce the fields of an HListR defined in this way. Additionally, the Coercible li (x ': xs) constraint does not yet allow a user to solve li ~ (y ': ys) for any y, ys, and likewise does not allow type families to branch on the outermost constructor of li.

---

As it applies to this issue (#8177), this raises the question: Can the following definition be allowed?

type role Fst representational
type Fst :: forall a b. (a, b) -> a
type family Fst p where
  Fst '(x, _) = x

It clearly does not satisfy the "If a parameter is at role R, it cannot be matched against and it must only appear in R (or P) positions in the RHS of instances" condition proposed above. But users cannot make trouble by introducing newtypes in the tuple kind (a, b) that would have the same representation as '(x, _) but a different name. The key thing here is that the type family is matching only against a data constructor from an ADT.