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

 Here, we need more assumptions. We have to assume an instance `Rep p` and
 an instance `Rep (p a)`. (We need it only for the `a` in question, though
 there would almost certainly be an axiom asserting `forall a. Rep (p a)`.)

 So, we assume `(Rep p, Rep (p a), Rep f, Coercible a b)` and wish to prove
 `Coercible (p a (f (F p f a))) (p b (f (F p f b)))`. We would be doing
 this in the context of an instance declaration for `Rep (F p f)`, so we
 can assume that, too.

 1. Use transitivity to break our goal down to two sub-goals: `Coercible (p
 a (f (F p f a))) (p a (f (F p f b)))` and `Coercible (p a (f (F p f b)))
 (p b (f (F p f b)))`.

 2. First sub-goal `Coercible (p a (f (F p f a))) (p a (f (F p f b)))`:
   a. Use rule (*) to break the goal down to `Rep (p a)` and `Coercible (f
 (F p f a)) (f (F p f b))`. The first of these is solved by assumption.
   b. Use rule (*) to get `Rep f` and `Coercible (F p f a) (F p f b)`. The
 first of these is solved by assumption.
   c. Use rule (*) to get `Rep (F p f)` and `Coercible a b`. Both are
 solved by assumption.

 3. Second sub-goal `Coercible (p a (f (F p f b))) (p b (f (F p f b)))`:
   a. Use the #9117 eta rule to reduce the goal to `Coercible (p a) (p b)`.
   b. Use rule (*) to reduce the goal to `(Rep p, Coercible a b)`.
   c. Done by assumption.

 I'm not necessarily saying that the constraint solver is up to this task
 without help (that is, user annotations or other assistance), but `Rep`
 with rule (*) seems to be able to support the derivation once found.

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