[GHC] #14317: Solve Coercible constraints over type constructors

[GHC]

#14317: Solve Coercible constraints over type constructors
-------------------------------------+-------------------------------------
        Reporter:  Iceland_jack      |                Owner:  (none)
            Type:  feature request   |               Status:  new
        Priority:  normal            |            Milestone:
       Component:  Compiler          |              Version:  8.2.1
      Resolution:                    |             Keywords:  Roles,
                                     |  QuantifiedContexts
Operating System:  Unknown/Multiple  |         Architecture:
                                     |  Unknown/Multiple
 Type of failure:  None/Unknown      |            Test Case:
      Blocked By:                    |             Blocking:
 Related Tickets:                    |  Differential Rev(s):
       Wiki Page:                    |
-------------------------------------+-------------------------------------

Comment (by RyanGlScott):

 It turns out that my earlier comment:

 Replying to [comment:2 RyanGlScott]:
 > But to my knowledge, there's no reasoning principle which states that `f
 a ~R g a` implies `f ~R g`.

 Is a bit misleading. I've re-read the
 [http://www.seas.upenn.edu/~sweirich/papers/coercible-JFP.pdf Safe Zero-
 cost Coercions for Haskell] paper recently, and it turns out that Section
 2.8 (Supporting higher-order polymorphism) pertains to this very topic:

 > So far, we have only seen `Coercible` applied to types of kind `*`, but
 that is not sufficient to support all coercions that we might want. For
 example, consider a monad transformer such as
 >
 > {{{#!hs
 > data MaybeT m a = MaybeT (m (Maybe a))
 > }}}
 >
 > and a newtype that wraps another monad, e.g.
 >
 > {{{#!hs
 > newtype MyIO a = MyIO (IO a)
 > }}}
 >
 > It is reasonable to expect that `Coercible (MaybeT MyIO a) (MaybeT IO
 a)` can be derived. Using the lifting rule for `MaybeT`, this requires
 `Coercible MyIO IO` to hold. Therefore, for a `newtype` declaration as the
 one above, GHC will //η//-reduce the unwrapping rule to say `Coercible IO
 MyIO` instead of `Coercible (IO a) (MyIO a)`. Using symmetry, this allows
 us to solve `Coercible (MaybeT MyIO a) (MaybeT IO a)`.

 Alas, that is the //only// discussion of eta-reducing unwrapping rules
 that I can find in the entire paper, as it doesn't appear to be brought up
 again at any point. But this would definitely explain why you can
 construct a `Coercion (EITHER USD) (Either Int)` with relative ease.

 Now it is clear to me why you still can't derive `Coercible Identity
 (Compose Identity Identity)` from `Coercible (Identity a) (Compose
 Identity Identity a)`. The reason is because you'd have to be able to
 //η//-reduce this unwrapping rule:

 {{{#!hs
 Coercible (Compose f g a) (f (g a))
 }}}

 But there is no way to //η//-reduce the `a` from `f (g a)`, so GHC
 evidently does not attempt this. So I'm inclined to label this as
 not-a-bug.

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