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

 Reid is, as ever, spot on.

 I think it might not be hard for the error message to say
 {{{
 foo.hs:15:11:
     Couldn't match type ‘a0’ with ‘a’
       because type variable ‘a’ would escape its scope
     This (rigid, skolem) type variable is bound by
       the type signature for g :: a -> a
       at foo.hs:14:12-17
     Expected type: a -> a
       Actual type: a0 -> a0
     Relevant bindings include
       g :: a -> a (bound at foo.hs:15:7)
       f :: a0 -> a0 (bound at foo.hs:10:7)
            NB: let-bound f is monomorphic because of MonoLocalBinds
 <------------
     In the expression: f
     In an equation for ‘g’: g = f
 }}}
 That is, annotate the "relevant bindings" that we did not attempt to
 generalise.

 It would be much harder to annotate only bindings that ''would''
 generalise, but didn't.  For example
 {{{
 foo v = do
   let f x = v

       g :: a -> a
       g = f
 }}}
 Here `f` can't be generalised regardless of `MonoLocalBinds` because it
 mentions `v`.

 The other difficulty is that adding `-XNoMonoLocalBinds` if you have
 `-XGADTs` is extremely dodgy. (It should probably elicit a stern warning,
 although it does not at the moment.)  So implicitly encouraging people to
 switch it off rather than fix the program properly is a bad idea.  Perhaps
 the message should say:
 {{{
     NB: Let-bound f was not generalised
         Possible solution: give it a type signature
 }}}
 Users, what do you think.  Check out the
 [http://www.haskell.org/ghc/docs/latest/html/users_guide/other-type-
 extensions.html#typing-binds user manual section] (7.13.9.3).

 Simon

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