#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