[GHC] #10709: Using ($) allows sneaky impredicativity on its left

29 Jul 2015

      #10709: Using ($) allows sneaky impredicativity on its left
-------------------------------------+-------------------------------------
              Reporter:  goldfire    |             Owner:  goldfire
                  Type:  bug         |            Status:  new
              Priority:  normal      |         Milestone:
             Component:  Compiler    |           Version:  7.10.1
  (Type checker)                     |
              Keywords:              |  Operating System:  Unknown/Multiple
          Architecture:              |   Type of failure:  None/Unknown
  Unknown/Multiple                   |
             Test Case:              |        Blocked By:
              Blocking:              |   Related Tickets:
Differential Revisions:              |
-------------------------------------+-------------------------------------
 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.

--
Ticket URL: http://ghc.haskell.org/trac/ghc/ticket/10709
GHC http://www.haskell.org/ghc/
The Glasgow Haskell Compiler