Commutativity of Coercible sometimes doesn't work with QuantifiedConstraints

It seems that there is a surprising interaction between the coercible constraint solver and quantified constraints. Here's some code with some explanation in the comments:

{-# LANGUAGE QuantifiedConstraints #-}
import Data.Coerce

-- I think this should compile, but it doesn't.
--
-- I'd expect the quantified constraint to be instantiated to
-- (Coercible (f b) b), and via commutativity of Coercible, imply
-- (Coercible b (f b))
compileError0 :: forall f b. (forall a. Coercible (f a) a) => b -> f b
compileError0 = coerce

-- The fact that this compiles demonstrates that quantified
-- constraints is needed to demonstrate the issue.
compiles0 :: forall f b. Coercible (f b) b => b -> f b
compiles0 = coerce

-- Instantiation as (Coercible (f b) b) works fine.
compiles1 :: forall f b. (forall a. Coercible (f a) a) => f b -> b
compiles1 = coerce

-- Instantiation of (forall a. Coercible a (f a)) as
-- (Coercible b (f b)) works.
compiles2 :: forall f b. (forall a. Coercible a (f a)) => b -> f b
compiles2 = coerce

-- This is curious!  It turns out that instantiation of
-- (forall a. Coercible a (f a)) does indeed get combined with
-- commutativity to imply (Coercible (f b) b)
compiles3 :: forall f b. (forall a. Coercible a (f a)) => f b -> b
compiles3 = coerce

I get the following error with both GHC-8.6.4 and also GHC built from recent source, 8.9.20190304:

qc.hs:10:17: error:
    • Couldn't match representation of type ‘b’ with that of ‘f b’
        arising from a use of ‘coerce’
      ‘b’ is a rigid type variable bound by
        the type signature for:
          compileError0 :: forall (f :: * -> *) b.
                           (forall a. Coercible (f a) a) =>
                           b -> f b
        at qc.hs:9:1-70
    • In the expression: coerce
      In an equation for ‘compileError0’: compileError0 = coerce
    • Relevant bindings include
        compileError0 :: b -> f b (bound at qc.hs:10:1)
   |
10 | compileError0 = coerce