[GHC] #9123: Need for higher kinded roles

[GHC]

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

Comment (by simonpj):

 At the nub of this is the following observation. If a function has type
 {{{
 forall m. (forall a b. Coercible a b => Coercible (m a) (m b)) =>
 ...blah...
 }}}
 then that, in effect, restricts `m` to type constructors whose first
 argument has nominal role -- exactly the problem posed in the Description
 of this ticket.

 Very good observation.

 But the inferred context for `deriving` clauses is deliberately
 restricted.  If you say
 {{{
 newtype T m a = MkT (m a) deriving( C )
 }}}
 (again from the Description) GHC will insist on a simple context, i.e. a
 class applied to type variables.  You want to ''infer'' a rather
 complicated context.  I don't know how to do that.

 You could perhaps ''declare'' it like this, using "standalone deriving"
 {{{
 deriving instance (C m, forall a. Coercible a b => Coercible (m a) (m b))
                => C (T m)
 }}}
 but GHC users might not be so happy with that whenever they say `deriving(
 Monad )`.

 Or perhaps
 {{{
 type RepArg1 m = forall a b. (Coercible a b => Coercible (m a) (m b))

 deriving instance (C m, RepArg1 m) => C (T m)
 }}}
 And now we are close to [wiki:Roles2].  (But we still don't have
 `deriving( Monad )` unannotated.

 Simon

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