[GHC] #8177: Roles for type families

[GHC]

#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)`.

 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).

 > 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.

--
Ticket URL: <http://ghc.haskell.org/trac/ghc/ticket/8177#comment:39>
GHC <http://www.haskell.org/ghc/>
The Glasgow Haskell Compiler