[GHC] #8808: ImpredicativeTypes type checking fails depending on syntax of arguments

[GHC]

#8808: ImpredicativeTypes type checking fails depending on syntax of arguments
----------------------------------------------+----------------------------
        Reporter:  guest                      |            Owner:
            Type:  bug                        |           Status:  new
        Priority:  normal                     |        Milestone:
       Component:  Compiler (Type checker)    |          Version:
      Resolution:                             |  7.8.1-rc1
Operating System:  Unknown/Multiple           |         Keywords:
 Type of failure:  GHC rejects valid program  |     Architecture:
       Test Case:                             |  Unknown/Multiple
        Blocking:                             |       Difficulty:  Unknown
                                              |       Blocked By:
                                              |  Related Tickets:
----------------------------------------------+----------------------------

Comment (by simonpj):

 Yes, I'm afraid that `ImpredicativeTypes` is a non-feature right now.  As
 I wrote to the GHC users list yesterday:

 `ImpredicativeTypes` is not properly finished.  When I first implemented
 it I implemented a fairly ambitious design based on "boxy types" (see
 paper with that in the title).  But it proved unsustainably complicated,
 both in the implementation and indeed for programmers to reason about
 which programs should be accepted and which should not.

 So I took most of it out.  There are some vestiges but to a first
 approximation it isn't really there at all.

 My plan is to do something along the lines of QML (again, look at the
 paper), plus add explicit type application.  But there are always too many
 other things to do.

 This is swampy territory, and I have spent more time on it that I care to
 tell you without producing a design that I am satisfied with.  So while I
 would be very happy if someone wants to start helping, you do need a good
 grasp of type inference first.  It's not a project to learn on.

 However the ''internal'' intermediate language, Core, is fully
 impredicative and always has been.  No difficulties there.

 Simon

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