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

 Replying to [comment:30 simonpj]:
 > You want to ''infer'' a rather complicated context.  I don't know how to
 do that.

 Sure you do!

 Currently, the code in !TcDeriv instructs the solver to try to reduce
 certain constraints. This reduction results in an unsolved implication
 constraint -- exactly the one we need to quantify over. The !TcDeriv code,
 at this point, extracts out the flat (er... now called ''simple'')
 constraints, checks to see if they're exotic, and then reports an error if
 there are any exotic simple constraints or if there are any leftover
 implication constraints. Currently, there's a leftover implication, and so
 we report an error.

 If, instead, we quantified over the leftover implication, we'd be done,
 with an inferred implication constraint.

 A separate question is whether or not this is desirable from a user's
 standpoint. `deriving` quite rightly restricts what it will quantify over.
 And implication constraints seem quite exotic. We could, though, say that
 implication constraints aren't exotic. Or, we could bake in the particular
 implication constraint `(forall a b. Coercible a b => Coercible (m a) (m
 b))`, recognize that, rewrite it to use Simon's type synonym `RepArg1 m`,
 and then it doesn't seem so exotic after all. That's terribly hacky, but
 it just might be useful enough to do. Or, we could punt and require users
 to write the constraint when they want it -- the error message will give
 them guidance. I don't have a strong opinion in any direction here.

 It is worth noting that, if `join :: m (m a) -> m a` is in `Monad`, most
 GNDs of `Monad` would work today. The ones that trip up are when the
 newtype wraps a monad transformer. That's a common-enough case that we
 don't want to make it impossible, but a rare enough case that I'm OK with
 making it annoying, if we can't do better.

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