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 |