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