Quantified variable instantiated to eagerly to a unification variable for impredicative types
Consider the following code:
{-# LANGUAGE ImpredicativeTypes #-}
data MVector s a
data ST s a
data Vector a
v3 :: Vector Int
v3 = undefined
f :: forall s. MVector s Int -> ST s ()
f = undefined
modify :: (forall s . MVector s a -> ST s ()) -> Vector a -> Vector a
modify _ _ = undefined
main = flip modify v3 f `seq` pure ()
It produces the following error:
T.hs:16:23: error:
• Couldn't match expected type ‘forall s. MVector s Int -> ST s ()’
with actual type ‘MVector s0 Int -> ST s0 ()’
• In the third argument of ‘flip’, namely ‘f’
In the first argument of ‘seq’, namely ‘flip modify v3 f’
In the expression: flip modify v3 f `seq` pure ()
|
16 | main = flip modify v3 f `seq` pure ()
| ^
But f
really has the required type. It just seems like the s
variable is instantiated too eagerly to a unification variable.
Expected behavior
Compile without errors.
Environment
- GHC version used: 9.2.1