[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 haasn):

 My greatest concern with manually applying type signatures is that, as
 seen in my real world use case, adding an explicit type signature would
 require changing more than just that function, due to ScopedTypeVariables
 being needed.

 But, barring some way to tell GHC to explicitly “generalize (just) this
 function”, and assuming that adding -XNoMonoLocalBinds when it would
 otherwise be implied is a Bad Thing, then I'd be content with the user
 just being told to generalize manually.

 I do think adding a big fat warning label about something not generalizing
 is important, because I personally did not even know this restriction
 existed - and I would not have guessed adding a type signature fixes
 anything because I was operating under the impression that GHC already
 infers the most general rank-1 type for things that are not on the top
 level.

 I believe a false positive for things that could not generalize either way
 is an acceptable trade-off, as long as the message is not *too* obnoxious.

 In this particular case, I believe a good error message could also mention
 the fact that the type variable ‘a0’ is forced to be monomorphic, which is
 ultimately why ‘a’ can't be matched with ‘a0’ (which seems counter-
 intuitive given just the first line of the error message), but perhaps
 mentioning that the binding for ‘f :: a0 -> a0’ is monomorphic would
 suffice. Up to you.

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