Coercible solver incomplete with non-variable transitivity

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!

Trac metadata

Trac field	Value
Version	7.11
Type	Bug
TypeOfFailure	OtherFailure
Priority	low
Resolution	Unresolved
Component	Compiler
Test case
Differential revisions
BlockedBy
Related
Blocking
CC
Operating system
Architecture