[GHC] #15472: GHC HEAD type inference regression post-"Remove decideKindGeneralisationPlan"

[GHC]

#15472: GHC HEAD type inference regression post-"Remove
decideKindGeneralisationPlan"
-------------------------------------+-------------------------------------
        Reporter:  RyanGlScott       |                Owner:  (none)
            Type:  bug               |               Status:  closed
        Priority:  highest           |            Milestone:  8.8.1
       Component:  Compiler (Type    |              Version:  8.5
  checker)                           |
      Resolution:  invalid           |             Keywords:  TypeInType
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:                    |
-------------------------------------+-------------------------------------

Comment (by RyanGlScott):

 To see why the program in comment:7 is going awry, suppose the `sGo`
 function were defined at the top level:

 {{{#!hs
 sGo :: x -> Proxy LetGo
 sGo _ = foo
 }}}

 This will not kind-check, before or after the offending commit mentioned
 above. That's because we always kind-generalize for top-level definitions,
 so the return kind of `LetGo` will be generalized to `k`, which is too
 polymorphic for the RHS `foo` (which expects the return kind of `LetGo` to
 be `Type`).

 Now, if `sGo` is a locally defined function, as in comment:7:

 {{{#!hs
 sSconcat :: forall x. x
 sSconcat = undefined
    where sGo :: x -> Proxy LetGo
          sGo _ = foo
 }}}

 Before the offending commit, then the return kind of `LetGo` was //not//
 generalized, causing it to default to `Type`, which makes everything go
 through. After the offending commit, however, GHC now kind-generalizes
 local definitions, which means that the return kind of `LetGo` is now
 generalized to `k` again. In other words, `sGo` fails to kind-check for
 the same reasons that it would fail to kind-check if it were defined at
 the top level.

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