Opened 4 years ago

Closed 4 years ago

#11675 closed bug (invalid)

Monomoprhic code makes ImpredicativeTypes infer an existential type

Reported by: _deepfire Owned by:
Priority: normal Milestone:
Component: Compiler (Type checker) Version: 8.0.1-rc2
Keywords: Cc: Alejandro, Serrano, Mena, <A.SerranoMena@…>, Simon, Peyton, Jones, <simonpj@…>
Operating System: Unknown/Multiple Architecture: Unknown/Multiple
Type of failure: GHC rejects valid program Test Case:
Blocked By: Blocking:
Related Tickets: Differential Rev(s):
Wiki Page:

Description

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) }’

Change History (1)

comment:1 Changed 4 years ago by goldfire

Resolution: invalid
Status: newclosed

<snarky-joke>Yes, there is an outright bug: your module includes {-# LANGUAGE ImpredicativeTypes #-}.</snarky-joke>

GHC's behavior is according to published typing rules, such as those in my recent paper on the subject. The problem is that nothing encourages GHC to instantiate the expression Nothing in your first case branch, and so GHC doesn't. If you add a type annotation there (or a visible type application) the problem should go away. (But I can't test this at the moment -- sorry.)

It is regrettable that ImpredicativeTypes is not conservative over Haskell98, but the extension is known to be quite broken and is hopefully getting an overhaul soon. See ImpredicativePolymorphism.

Thanks for reporting!

Note: See TracTickets for help on using tickets.