[GHC] #10185: Coercible solver incomplete with non-variable transitivity

[GHC]

#10185: Coercible solver incomplete with non-variable transitivity
-------------------------------------+-------------------------------------
              Reporter:  goldfire    |             Owner:
                  Type:  bug         |            Status:  new
              Priority:  low         |         Milestone:  ⊥
             Component:  Compiler    |           Version:  7.11
              Keywords:              |  Operating System:  Unknown/Multiple
          Architecture:              |   Type of failure:  None/Unknown
  Unknown/Multiple                   |        Blocked By:
             Test Case:              |   Related Tickets:
              Blocking:              |
Differential Revisions:              |
-------------------------------------+-------------------------------------
 If I say

 {{{
 import Data.Coerce
 import Data.Proxy

 foo :: (Coercible (a b) (c d), Coercible (c d) (e f)) => Proxy (c d) -> a
 b -> e f
 foo _ = coerce
 }}}

 I get an error, because GHC isn't smart enough to figure out transitivity
 in this case. It ''can'' do it with bare variables, but not variable
 applications. It's possible there's a way to do this, but we'll wait for
 someone to shout before investing effort.

 Do shout if this lack of functionality is ruining your day!

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