Skip to content

Using ($) allows sneaky impredicativity on its left

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.

Trac metadata
Trac field Value
Version 7.10.1
Type Bug
TypeOfFailure OtherFailure
Priority normal
Resolution Unresolved
Component Compiler (Type checker)
Test case
Differential revisions
BlockedBy
Related
Blocking
CC
Operating system
Architecture
To upload designs, you'll need to enable LFS and have an admin enable hashed storage. More information