[GHC] #9456: Weird behavior with polymorphic function involving existential quantification and GADTs

[GHC]

#9456: Weird behavior with polymorphic function involving existential
quantification and GADTs
-------------------------------------+-------------------------------------
              Reporter:  haasn       |            Owner:
                  Type:  bug         |           Status:  new
              Priority:  normal      |        Milestone:
             Component:  Compiler    |          Version:  7.8.2
  (Type checker)                     |         Keywords:
            Resolution:              |     Architecture:  Unknown/Multiple
      Operating System:              |       Difficulty:  Unknown
  Unknown/Multiple                   |       Blocked By:
       Type of failure:  GHC         |  Related Tickets:
  rejects valid program              |
             Test Case:              |
              Blocking:              |
Differential Revisions:              |
-------------------------------------+-------------------------------------

Comment (by rwbarton):

 This is all expected behavior—for some value of "expected"! See
 https://www.haskell.org/ghc/docs/latest/html/users_guide/other-type-
 extensions.html#mono-local-binds. Your original program does not typecheck
 because

 - the `GADTs` language flag implies `MonoLocalBinds`
 - `f` does not have a user-supplied type signature
 - `f` cannot be floated to top-level because it refers to `box`, and...
 - `box` cannot be floated to top-level either because it is not bound by a
 `let`

 and therefore the type of `f` is not generalized, and so it cannot be used
 polymorphically by `g`.

 Your four other programs each differ in one of these four features.

 Granted, this is all not very obvious; do you have any suggestion for a
 better error message?

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