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.
|Component||Compiler (Type checker)|