Difference between (Coercible f g) and (forall x. Coercible (f x) (g x))

{-# LANGUAGE QuantifiedConstraints, RankNTypes #-}
{-# LANGUAGE AllowAmbiguousTypes, TypeApplications #-}
import Data.Coerce
import Data.Functor.Identity
import Data.Functor.Compose

coeA :: Coercible f g => f x -> g x
coeA = coerce

-- This doesn't work:
--    • Couldn't match representation of type ‘Identity’
--                               with that of ‘Compose Identity Identity’
--        arising from a use of ‘coeA’
--
-- exA :: Identity a -> Compose Identity Identity a
-- exA = coeA

-- This works however.
exB :: Identity a -> Compose Identity Identity a
exB = coerce

-- and also
coeC :: (forall x. Coercible (f x) (g x)) => f x -> g x
coeC = coerce

exC :: Identity a -> Compose Identity Identity a
exC = coeC

-- So this works:
forward :: Coercible f g => ((forall x. Coercible (f x) (g x)) => r) -> r
forward k = k

-- but this doesn't?
-- backwards :: (forall x. Coercible (f x) (g x)) => (Coercible f g => r) -> r
-- backwards k = k

-- but what is the difference between
--
--    Coercible f g
--
-- and
--
--    (forall x. Coercible (f x) (g x))
--
-- As far as I can tell from reading zero-cost coercions paper,
-- Co_App rule:
--
--  Γ ⊢ γ₁ : τ₁ ~ρ σ₁
--  Γ ⊢ γ₂ : τ₂ ∼N σ₂
--  Γ ⊢ τ₁ τ₂ : κ
--  Γ ⊢ σ₁ σ₂ : κ
--  --------------------------
--  Γ ⊢ γ₁ γ₂ : τ₁ τ₂ ~ρ σ₁ σ₂
--
-- Is used to show the forward direction,
-- but why the backwards, functional-extensionality -like, direction is not included?
-- What will break?
--
-- It feels that there could be some kind of Co_Abs rule, essentially doing the opposite of Co_App.

EDIT: This obviously affects ~ equality too. I don't see why f ~ g and forall x. f x ~ g x would not be equivalent in GHC type system.