[GHC] #9117: Coercible constraint solver misses one

[GHC]

#9117: Coercible constraint solver misses one
------------------------------------+-------------------------------------
       Reporter:  goldfire          |             Owner:
           Type:  bug               |            Status:  new
       Priority:  normal            |         Milestone:
      Component:  Compiler          |           Version:  7.8.2
       Keywords:                    |  Operating System:  Unknown/Multiple
   Architecture:  Unknown/Multiple  |   Type of failure:  None/Unknown
     Difficulty:  Unknown           |         Test Case:
     Blocked By:                    |          Blocking:
Related Tickets:                    |
------------------------------------+-------------------------------------
 When I say

 {{{
 import Data.Type.Coercion
 import Data.Coerce

 eta :: Coercible f g => Coercion (f a) (g a)
 eta = Coercion
 }}}

 I get

 {{{
     Could not coerce from ‘f a’ to ‘g a’
       because ‘f a’ and ‘g a’ are different types.
       arising from a use of ‘Coercion’
     from the context (Coercible f g)
       bound by the type signature for
                  eta :: Coercible f g => Coercion (f a) (g a)
       at /Users/rae/temp/Roles.hs:6:8-44
     In the expression: Coercion
     In an equation for ‘eta’: eta = Coercion
 }}}

 But, this coercion is easily expressible in Core. If `(co :: f ~R# g)`
 then `(co <a> :: f a ~R# g a)`, where `<a>` is the notation for a
 reflexivity coercion for the type `a`. The constraint solver should be
 able to do this.

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