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

 Replying to [comment:40 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:
 >
 > {{{#!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.

 ...and this sort of thing as well.

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