Good day! I realise that ImpredicativeTypes is a problematic extension, but I have found something that looks like an outright bug -- no polymorphism involved: ,---- | {-# LANGUAGE ImpredicativeTypes #-} | | module Foo where | | foo :: IO (Maybe Int) | foo = do | pure $ case undefined :: Maybe String of | Nothing | -> Nothing | Just _ | -> (undefined :: Maybe Int) `---- produces the following errors: ,---- | foo.hs:7:3: error: | • Couldn't match type ‘forall a. Maybe a’ with ‘Maybe Int’ | Expected type: IO (Maybe Int) | Actual type: IO (forall a. Maybe a) | • In a stmt of a 'do' block: | pure | $ case undefined :: Maybe String of { | Nothing -> Nothing | Just _ -> (undefined :: Maybe Int) } | In the expression: | do { pure | $ case undefined :: Maybe String of { | Nothing -> Nothing | Just _ -> (undefined :: Maybe Int) } } | In an equation for ‘foo’: | foo | = do { pure | $ case undefined :: Maybe String of { | Nothing -> Nothing | Just _ -> (undefined :: Maybe Int) } } | | foo.hs:11:19: error: | • Couldn't match type ‘a’ with ‘Int’ | ‘a’ is a rigid type variable bound by | a type expected by the context: | forall a. Maybe a | at foo.hs:11:19 | Expected type: forall a. Maybe a | Actual type: Maybe Int | • In the expression: (undefined :: Maybe Int) | In a case alternative: Just _ -> (undefined :: Maybe Int) | In the second argument of ‘($)’, namely | ‘case undefined :: Maybe String of { | Nothing -> Nothing | Just _ -> (undefined :: Maybe Int) }’ `---- -- с уважениeм / respectfully, Косырев Сергей