Opened 4 years ago

Last modified 2 years ago

#10709 new bug

Using ($) allows sneaky impredicativity on its left

Reported by: goldfire Owned by: goldfire
Priority: normal Milestone:
Component: Compiler (Type checker) Version: 7.10.1
Keywords: ImpredicativeTypes Cc: jstolarek
Operating System: Unknown/Multiple Architecture: Unknown/Multiple
Type of failure: None/Unknown Test Case:
Blocked By: Blocking:
Related Tickets: Differential Rev(s):
Wiki Page:

Description

Observe the following shady interaction with GHCi:

GHCi, version 7.10.1: http://www.haskell.org/ghc/  :? for help
Prelude> import GHC.IO
Prelude GHC.IO> import Control.Monad
Prelude GHC.IO Control.Monad> :t mask
mask :: forall b. ((forall a. IO a -> IO a) -> IO b) -> IO b
Prelude GHC.IO Control.Monad> :t replicateM 2 . mask

<interactive>:1:16:
    Couldn't match type ‘a’ with ‘(forall a2. IO a2 -> IO a2) -> IO a1’
      ‘a’ is a rigid type variable bound by
          the inferred type of it :: a -> IO [a1] at Top level
    Expected type: a -> IO a1
      Actual type: ((forall a. IO a -> IO a) -> IO a1) -> IO a1
    In the second argument of ‘(.)’, namely ‘mask’
    In the expression: replicateM 2 . mask
Prelude GHC.IO Control.Monad> :t (replicateM 2 . mask) undefined

<interactive>:1:17:
    Cannot instantiate unification variable ‘a0’
    with a type involving foralls: (forall a1. IO a1 -> IO a1) -> IO a
      Perhaps you want ImpredicativeTypes
    In the second argument of ‘(.)’, namely ‘mask’
    In the expression: replicateM 2 . mask
Prelude GHC.IO Control.Monad> :t (replicateM 2 . mask) $ undefined
(replicateM 2 . mask) $ undefined :: forall a. IO [a]

Due to the way that GHC processes ($), it allows this form of impredicativity on the LHS of ($). This case is inspired by https://github.com/ghc/nofib/blob/master/smp/threads006/Main.hs which contains the line

   tids <- replicateM nthreads . mask $ \_ -> forkIO $ return ()

I think that line should be rejected.

The problem stems from the treatment of OpenKind as described in Note [OpenTypeKind accepts foralls] in TcMType.

Unrelated work changes this behavior by rejecting the nofib program. The point of this ticket is to provoke discussion about what is right and what is wrong here, not to request a fix.

Change History (3)

comment:1 Changed 4 years ago by rwbarton

From IRC discussion, something weird is happening that is not specific to $. All these type check:

 (replicateM 2 . mask) (\_ -> return ())
 (replicateM 2 . mask) (\x -> undefined x)
 (replicateM 2 . mask) (id (\_ -> undefined))

but these do not:

 (replicateM 2 . mask) (const undefined)
 (replicateM 2 . mask) ((\x -> undefined x) :: a -> b)

comment:2 Changed 4 years ago by jstolarek

Cc: jstolarek added

comment:3 Changed 2 years ago by simonpj

Keywords: ImpredicativeTypes added
Note: See TracTickets for help on using tickets.