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