[GHC] #8541: Coercible should be higher-kinded

[GHC]

#8541: Coercible should be higher-kinded
------------------------------------+-------------------------------------
       Reporter:  nomeata           |             Owner:  nomeata
           Type:  task              |            Status:  new
       Priority:  normal            |         Milestone:
      Component:  Compiler          |           Version:  7.6.3
       Keywords:                    |  Operating System:  Unknown/Multiple
   Architecture:  Unknown/Multiple  |   Type of failure:  None/Unknown
     Difficulty:  Unknown           |         Test Case:
     Blocked By:                    |          Blocking:
Related Tickets:                    |
------------------------------------+-------------------------------------
 Just discussed with SJP: The Coercible should be higher kinded, and it
 seems to be straight forward.

 Given
 {{{
 data T f = T (f Int)
 newtype List a = [a]
 }}}
 we want to be able to derive
 {{{
 Coercible (T (Either Int)) (T (Either Age))
 Coercible (T List) (T [])
 }}}

 We now allow `Coercible` at a kind `* -> k`, with the following intuition:
 {{{
   Coercible A B ⇐⇒ (forall a. Coercible (A a) (B a))
 }}}
 Note that this is ok independent of the role of `A`’s parameter, as we are
 not modifying that parameter here.

 Allowing such constraints, we therefore, we need these constraints exist
 in theory (but are in fact generated on demand, so only those of the rind
 kindnessare visible to the constraint solver) for `Either` and `List`:
 {{{
 instance (Coercible a b, Coercible c d)
                            => Coercible (Either a c) (Either b d) -- old
 instance Coercible a   b =>   Coercible (Either a) (Either b)     -- new
 instance Coercible [a] b =>   Coercible (List a)   b              -- old
 instance Coercible b   [a] => Coercible b          (List a)       -- old
 instance Coercible a   b =>   Coercible (List a)   (List b)       -- old
 instance Coercible []  b =>   Coercible List       b              -- new
 instance Coercible b   [] =>  Coercible b          List           -- new
 }}}

 This solves the cases above. It does not solve all cases, though. Consider
 {{{
 newtype NT1 a = NT1 (a -> Int)
 newtype NT2 a = NT2 (a -> Int)
 }}}
 and we want to solve `Coercible (T NT1) (T NT2)`. Although, by the
 definition above, `Coercible NT1 NT2` should hold, such a coercion cannot
 be created (as far as I can see).

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