Incorrect non-exhaustive pattern match warning with higher rank types

Summary

I was experimenting with some very impredicative types when I got a seemingly redundant warning.

Steps to reproduce

{-# LANGUAGE ImpredicativeTypes #-}
data Freer c0 f a = Pure (c0 a) | forall x. Freer (f x) (forall c. c x -> Freer c f a)

bind :: (forall c. Freer c f a) -> (forall c. c a -> Freer c f b) -> (forall c. Freer c f b)
bind (Pure x) k = k x
bind (Freer op k) k' = Freer op (kcompose k' k)

kcompose :: (forall c. c y -> Freer c f z) -> (forall c. c x -> Freer c f y) -> (forall c. c x -> Freer c f z) 
kcompose k1 k2 x =
  case k2 x of
    Pure y -> k1 y
    Freer op k3 -> Freer op (kcompose k1 k3)

This gave me the warning:

Pattern match(es) are non-exhaustive
In an equation for ‘bind’:
    Patterns of type ‘forall (c :: k -> *). Freer c f a’,
                     ‘forall (c :: k -> *). c a -> Freer c f b’ not matched:
        _ _

Expected behavior

I expected no warnings.

Environment

• GHC version used: 9.4.4