[GHC] #11339: Possible type-checker regression in GHC 8.0

[GHC]

#11339: Possible type-checker regression in GHC 8.0
-------------------------------------+-------------------------------------
        Reporter:  hvr               |                Owner:  goldfire
            Type:  bug               |               Status:  new
        Priority:  highest           |            Milestone:  8.0.1
       Component:  Compiler (Type    |              Version:  8.1
  checker)                           |
      Resolution:                    |             Keywords:
Operating System:  Unknown/Multiple  |         Architecture:
                                     |  Unknown/Multiple
 Type of failure:  None/Unknown      |            Test Case:
      Blocked By:                    |             Blocking:
 Related Tickets:                    |  Differential Rev(s):
       Wiki Page:                    |
-------------------------------------+-------------------------------------

Comment (by goldfire):

 This is truly bizarre.

 Here are a few things I've learned:
 1. The module compiles with `-XNoMonomorphismRestriction`. This is
 actually correct behavior. The issue is that the inferred type of `t` is
 quantified (by `Applicative f`). The monomorphism restriction forbids
 this. So the new behavior is correct, I think.

 2. Sadly, adding `t :: Applicative f => (a -> f b) -> f t`, by itself,
 doesn't fix the problem

 3. The line that you say doesn't compile does indeed compile if you add `t
 :: Applicative f => (a -> f b) -> f t`

 4. The line that you say doesn't compile does indeed compile if you add
 `-XMonoLocalBinds`.

 5. Saying `t :: _` emits no warning. I have no idea why.

 Here is some interpretation of the above:

 A. Fact (2) is a consequence of the fact that GHC considers itself to be
 inferring a type for all pattern bindings, even if there is a complete
 type signature. (See `TcBinds.decideGeneralisationPlan`) I don't know why
 this is the case; I did not change this behavior. Visible type application
 does a little extra jiggery pokery when inferring types. See `Note
 [Instantiate when inferring a type]` in !TcBinds. This jiggery pokery is
 triggered because we're inferring the type of `t`, even when a type
 signature is given.

 B. Facts (3) and (4) (really the fact that the commented line doesn't
 compile in the first place) is because we're in the quite rare scenario
 where `-XMonLocalBinds` is a good idea, even absent type families / GADTs.
 This is not the first such example, but I don't have a link to a previous
 one. Perhaps `RankNTypes` should imply `MonoLocalBinds`.

 Bottom line: The only real bug in here is (2). It really should compile
 with the type signature, regardless of the monomorphism restriction. But
 it doesn't. However, the example as submitted should be rejected, I
 believe.

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