[GHC] #9123: Need for higher kinded roles

[GHC]

#9123: Need for higher kinded roles
-------------------------------------+------------------------------------
        Reporter:  simonpj           |            Owner:
            Type:  bug               |           Status:  new
        Priority:  normal            |        Milestone:
       Component:  Compiler          |          Version:  7.8.2
      Resolution:                    |         Keywords:
Operating System:  Unknown/Multiple  |     Architecture:  Unknown/Multiple
 Type of failure:  None/Unknown      |       Difficulty:  Unknown
       Test Case:                    |       Blocked By:
        Blocking:                    |  Related Tickets:
-------------------------------------+------------------------------------

Comment (by goldfire):

 I'm in support, generally, of Edward's suggestion on that thread. His idea
 does ''not'' go "all the way", in that there are some ideas we might want
 to express but cannot, as Edward points out. But, if the current roles
 story works for 95% of cases (where the `join` problem is an important
 member of the 5%), the current story + Edward's suggestion would probably
 cover 99.5%. And, the beauty of Edward's idea is that it is requires no
 change to Core and can mostly be implemented in user-land. GHC should
 support with magically-generated instances (like we already do for
 `Coercible`) and will need to incorporate these ideas into the `Coercible`
 solver, but these are relatively minor changes.

 Suppose that the class involved is named `Representational`, as Edward
 suggests. (I actually am against that name, because it makes the ''wrong''
 thing sound representational. But, let's leave bikeshedding over names
 until later.) Should we make `Representational` a superclass of `Functor`?
 It "makes sense" that every `Functor` should treat its argument
 representationally. And, doing so would make GND work trivially with the
 new `Monad`. And, doing so would make `Traversable` GND'able (it currently
 is not). But, of course, it would mean that users may want to write
 `Functor` instances that are ''not'' representational and now cannot. (For
 example,
 [https://github.com/ekmett/lens/blob/master/src/Control/Lens/Internal/Magma.hs#L73
 this one].)

 If we decide ''not'' to make `Representational` a (transitive) superclass
 of `Monad`, then `Monad` with `join` would only be GND'able if the GND
 instance has a `Representational` constraint in its context. This context
 could probably be inferred. But, any user writing a standalone GND for
 `Monad` (not an uncommon occurrence, I imagine) would have to be aware of
 this issue.

 These issues aren't meant to be "push-back" -- just some ramifications we
 should consider as we move forward.

 It is interesting to note that, had we gone with the POPL'11
 implementation of roles, which included support for "higher-kinded" roles,
 we would be even more stuck here. That implementation tied a role in with
 a type's kind, which means that we would be ''forced'' to make every
 `Monad` representational in order to get GND to work with `join`. With the
 current plan, we have this free design choice. The current roles story may
 be somewhat less powerful than roles in POPL'11, but they are surely more
 flexible.

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