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

 {{{
 newtype StateT s m a = StateT { runStateT :: s -> m (a, s) }
 }}}

 This means that when you go to describe the instance for `Representational
 (StateT s m)` it needs to convert `s -> m (a, s)`  into `s -> m (b, s)`
 given a coercion between a and b.

 But that means we're coercing `(,) a` into `(,) b` -- let's call those f
 and g respectively -- and we're expanding that with the coercion from s
 into s which is trivial.

 If we can't lift `(Representable f, Coercion f g, Coercion a b)` into
 `Coercion (f a) (g b)` but can only go `(Representable f, Coercion a b) =>
 Coercion (f a) (f b)` then we get stuck, as we only have `(Representable
 ((,) a), Coercion ((,) a) (,) b, Coercion s s)`!

 For state you could actually get by with a _different_ weaker rule added
 to the one Richard offered:

 {{{
 ext :: forall (f :: x -> y) (g :: x -> y) (a :: x). Coercion f g ->
 Coercion (f a) (g a)
 }}}

 which I fake with `unsafeCoerce` right now in

 https://github.com/ekmett/roles/blob/master/src/Data/Roles.hs

 But that isn't enough to handle lifting a coercion where what 'a' occurs
 on both sides of the nested, which is what you get for free monads, cofree
 comonads, etc.

 The simplest case that fails is probably:

 {{{
 newtype Pair a = Pair (a, a)
 }}}

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