Re: [GHC] #11355: TypeApplications + RankNTypes permits "impredicativity"

10 Jan 2016

      #11355: TypeApplications + RankNTypes permits "impredicativity"
-------------------------------------+-------------------------------------
        Reporter:  adamgundry        |                Owner:  goldfire
            Type:  bug               |               Status:  new
        Priority:  normal            |            Milestone:
       Component:  Compiler          |              Version:  7.11
      Resolution:                    |             Keywords:
                                     |  TypeApplications
Operating System:  Unknown/Multiple  |         Architecture:
                                     |  Unknown/Multiple
 Type of failure:  None/Unknown      |            Test Case:
      Blocked By:                    |             Blocking:
 Related Tickets:                    |  Differential Rev(s):
       Wiki Page:                    |
-------------------------------------+-------------------------------------

Comment (by adamgundry):

 I see, the above works with the `:t` command in GHCi, but trying to
 evaluate it or compile it in a module gives this error:
 {{{
     • Illegal polymorphic or qualified type: forall a1. a1 -> a1
       GHC doesn't yet support impredicative polymorphism
     • When checking the inferred type
         t :: forall b.
              ((forall a. a -> a) -> b) -> [forall a. a -> a] -> [b]
 }}}

 Should this message mention `ImpredicativeTypes`? In theory, it ought
 to be possible to actually use `ImpredicativeTypes` now if you insert
 enough type applications.

 However, the following example compiles, and I think it shouldn't:
 {{{#!hs
 {-# LANGUAGE RankNTypes, TypeApplications #-}
 module T11355 where
 t = map @(forall a . a -> a) ($ True) [id]
 }}}

--
Ticket URL: http://ghc.haskell.org/trac/ghc/ticket/11355#comment:3
GHC http://www.haskell.org/ghc/
The Glasgow Haskell Compiler