[GHC] #11675: Monomoprhic code makes ImpredicativeTypes infer an existential type

[GHC]

#11675: Monomoprhic code makes ImpredicativeTypes infer an existential type
-------------------------------------+-------------------------------------
        Reporter:  _deepfire         |                Owner:
            Type:  bug               |               Status:  closed
        Priority:  normal            |            Milestone:
       Component:  Compiler (Type    |              Version:  8.0.1-rc2
  checker)                           |
      Resolution:  invalid           |             Keywords:
Operating System:  Unknown/Multiple  |         Architecture:
 Type of failure:  GHC rejects       |  Unknown/Multiple
  valid program                      |            Test Case:
      Blocked By:                    |             Blocking:
 Related Tickets:                    |  Differential Rev(s):
       Wiki Page:                    |
-------------------------------------+-------------------------------------
Changes (by goldfire):

 * status:  new => closed
 * resolution:   => invalid


Comment:

 <snarky-joke>Yes, there is an outright bug: your module includes `{-#
 LANGUAGE ImpredicativeTypes #-}`.</snarky-joke>

 GHC's behavior is according to published typing rules, such as those in my
 recent [http://www.seas.upenn.edu/~sweirich/papers/esop2016-typeapp.pdf
 paper] on the subject. The problem is that nothing encourages GHC to
 instantiate the expression `Nothing` in your first case branch, and so GHC
 doesn't. If you add a type annotation there (or a visible type
 application) the problem should go away. (But I can't test this at the
 moment -- sorry.)

 It is regrettable that `ImpredicativeTypes` is not conservative over
 Haskell98, but the extension is known to be quite broken and is hopefully
 getting an overhaul soon. See ImpredicativePolymorphism.

 Thanks for reporting!

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