[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:                    |
-------------------------------------+-------------------------------------

Comment (by goldfire):

 It would make sense that the type-checker rewrite from visible type
 application would break impredicativity even more than usual. Given its
 already-quite-broken state, I didn't try to salvage it.

 I don't want to completely kill it, though, as it sometimes is useful, if
 just for experimentation. And visible types lets you climb out of any hole
 you get in. For example, this works:

 {{{
 {-# LANGUAGE ImpredicativeTypes, ScopedTypeVariables, TypeApplications #-}

 module Bug where

 f :: forall a f. Applicative f => f (Maybe a)
 f = pure (Nothing @a)
 }}}

 All that said, I'll take a look at this one, as it would be nice to be
 less broken. And my hunch is that this will be quite easy to fix.

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