#8177: Roles for type families -------------------------------------+------------------------------------- Reporter: simonpj | Owner: goldfire Type: bug | Status: new Priority: normal | Milestone: ⊥ Component: Compiler | Version: 7.6.3 Resolution: | Keywords: TypeFamilies Operating System: Unknown/Multiple | Architecture: | Unknown/Multiple Type of failure: None/Unknown | Test Case: Blocked By: | Blocking: Related Tickets: | Differential Rev(s): Phab:D3662 Wiki Page: | -------------------------------------+------------------------------------- Comment (by goldfire): Replying to [comment:39 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 comment:5.
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 `TyCon`s 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`.
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 perhaps you want just roles for ''type'' families for now, not ''data'' families.
So in your above example:
{{{#!hs 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: {{{#!hs 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. -- Ticket URL: http://ghc.haskell.org/trac/ghc/ticket/8177#comment:40 GHC http://www.haskell.org/ghc/ The Glasgow Haskell Compiler