#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 RyanGlScott): 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:
{{{#!hs 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)`.
I'm a bit worried about problems with what happens if a type constructor
**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
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 `TyCon`s 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: {{{#!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). 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. 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. -- Ticket URL: http://ghc.haskell.org/trac/ghc/ticket/8177#comment:39 GHC http://www.haskell.org/ghc/ The Glasgow Haskell Compiler