[GHC] #13555: Typechecker regression when combining PolyKinds and MonoLocalBinds

[GHC]

#13555: Typechecker regression when combining PolyKinds and MonoLocalBinds
-------------------------------------+-------------------------------------
        Reporter:  RyanGlScott       |                Owner:  (none)
            Type:  bug               |               Status:  new
        Priority:  highest           |            Milestone:  8.2.1
       Component:  Compiler (Type    |              Version:  8.1
  checker)                           |
      Resolution:                    |             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 goldfire):

 I've figured this out. The new behavior is correct; the old behavior was a
 bug.

 This is all to do with "let should not be generalized". With `TypeInType`,
 I extended that notion to the type level, saying that `MonoLocalBinds`
 implies that we should ''not'' perform kind generalization on type
 signatures that capture outer scoped type variables. This is the right
 behavior for precisely the same reasons it is at the term level: with
 local equalities on kinds and kind families, it's impossible to know how
 to generalize reliably.

 In GHC 8.0, the check for in-scope type variables was subtly wrong and
 missed unified `SigTv`s. The new check is correct, as far as I can tell.

 What's annoying here for users is that this a regression from 7.10, where
 `MonoLocalBinds` did not affect kind generalization. The good news is that
 the fix -- add a kind signature -- is fully backward-compatible. So, we
 could do either

 1. Advertise this as a user-facing change (a bug-fix, really) and tell
 users to add kind signatures, or

 2. Avoid the new logic with `-XNoTypeInType`.

 I prefer (1) because it's simpler, but not strongly.

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