[GHC] #11319: ImpredicativeTypes even more broken than usual

[GHC]

#11319: ImpredicativeTypes even more broken than usual
-------------------------------------+-------------------------------------
        Reporter:  Iceland_jack      |                Owner:
            Type:  bug               |               Status:  new
        Priority:  normal            |            Milestone:
       Component:  Compiler (Type    |              Version:  7.11
  checker)                           |             Keywords:
      Resolution:                    |  ImpredicativeTypes
Operating System:  Linux             |         Architecture:
 Type of failure:  GHC rejects       |  Unknown/Multiple
  valid program                      |            Test Case:
      Blocked By:                    |             Blocking:
 Related Tickets:                    |  Differential Rev(s):
       Wiki Page:                    |
-------------------------------------+-------------------------------------
Changes (by simonpj):

 * cc: a.serranomena@… (added)


Comment:

 This is definitely fallout from Visible Type Application.  The program in
 comment:3 typechecks fine without `ImpredicativeTypes` (indeed it does in
 Haskell 98!) and surely `ImpredicativeTypes` should be a conservative
 extension.

 But let's not invest much in "fixing" `ImpredicativeTypes` which is simply
 not supported at the moment.  Alejandro Serrano (cc'd) is working on
 impredicativity right now, so I've added him to the cc list.

 Alejandro, what are you doing will be significantly affected by the "lazy
 instantiation" approach of Visible Type Application
 ([https://www.cis.upenn.edu/~eir/pubs.html see paper]), so you might want
 to look carefully.  VTA is in GHC now!

--
Ticket URL: <http://ghc.haskell.org/trac/ghc/ticket/11319#comment:4>
GHC <http://www.haskell.org/ghc/>
The Glasgow Haskell Compiler