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

[GHC]

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

Comment (by RyanGlScott):

 Since this ticket was originally opened, SPJ started a
 [https://mail.haskell.org/pipermail/ghc-devs/2016-September/012940.html
 very relevant discussion] on the GHC devs mailing list about a way to
 salvage `ImpredicativeTypes`. It wouldn't make the original program in
 this ticket typecheck again, but it would provide a way to possibly
 suggest a workaround in error messages.

 To quote SPJ:

 > When you have `-XImpredicativeTypes`
 >
 > * You can write a polytype in a visible type argument; eg.  `f @(forall
 a. a->a)`
 >
 > * You can write a polytype as an argument of a type in a signature  e.g.
 `f :: [forall a. a->a] -> Int`
 >
 > And that’s all.  A unification variable STILL CANNOT be unified with a
 polytype.  The only way you can call a polymorphic function at a polytype
 is to use Visible Type Application.
 >
 > So using impredicative types might be tiresome.  E.g.
 >
 >   {{{#!hs
 >   type SID = forall a. a->a
 >
 >
 >
 >   xs :: [forall a. a->a]
 >
 >   xs = (:) @SID id ( (:) @SID id ([] @ SID))
 >   }}}
 >
 > In short, if you call a function at a polytype, you must use VTA.
 Simple, easy, predictable; and doubtless annoying.  But possible.

 However, this should undoubtedly go through a GHC proposal. At the very
 least, it's unclear to me whether SPJ's intention was to require actually
 enabling `-XImpredicativeTypes` in order to visibly apply a polytype (the
 title of the GHC devs discussion, "Getting rid of `-XImpredicativeTypes`",
 makes me think "no", but the actual contents of the discussion that I
 quoted would suggest "yes").

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