#9201: GHC unexpectedly refines explicit kind signatures ------------------------------------------------+-------------------------- Reporter: ekmett | Owner: Type: bug | Status: new Priority: normal | Milestone: Component: Compiler (Type checker) | Version: 7.8.2 Resolution: | Keywords: Operating System: Unknown/Multiple | Architecture: Type of failure: GHC accepts invalid program | Unknown/Multiple Test Case: | Difficulty: Blocking: | Unknown | Blocked By: | Related Tickets: ------------------------------------------------+-------------------------- Comment (by goldfire): The underlying cause of this is directly related to what's causing #9200. The `ParametricKinds` strategy makes kind variables into `SigTv`s, which are allowed to unify with other `SigTv`s. The intent is that the `SigTv`s are in ''different'' signatures, like this: {{{ class C (a :: k1) where foo :: D a => a -> a class C a => D (a :: k2) where ... }}} Here, `C` and `D` are mutually recursive, and we would want these to type- check. However, according to the `ParametricKinds` strategy, we ''do not'' want to generalize over `k` while kind-checking the group. The only way to get this to work, then, is to unify `k1` and `k2`. This is sensible enough, but it fails utterly in Edward's example, where the `SigTv`s are in the ''same'' signature. The fix here is the same as the fix for #9200: change classes to use `NonParametricKinds`, which does not have this behavior. I should note why `ParametricKinds` does what it does: when I added closed type families last summer, I needed to dig somewhat deep into all of this, to get kind inference for closed families to work. At that point, there were two strategies: the "normal" one and the one used in the presence of a "complete user-supplied kind signature" ("cusk"). See [http://www.haskell.org/ghc/docs/latest/html/users_guide/kind- polymorphism.html section 7.8.3] of the manual. Closed type families didn't fit into either of these categories cleanly. Instead of just adding a few ad-hoc conditionals, I invented the idea of [https://github.com/ghc/ghc/blob/c8295c0bd58485db5572d3c35427d321bdf1b7d0/com... "kind-checking strategies" ] where each of the (now, 3) approaches could be tracked a little more transparently. `ParametricKinds` was intended to behave exactly as kind inference did without a cusk. In retrospect, I had the opportunity to perhaps clean this all up a bit, but I didn't want to challenge the status quo without a concrete reason. -- Ticket URL: http://ghc.haskell.org/trac/ghc/ticket/9201#comment:2 GHC http://www.haskell.org/ghc/ The Glasgow Haskell Compiler

#9201: GHC unexpectedly refines explicit kind signatures -------------------------------------+------------------------------------- Reporter: ekmett | Owner: Type: bug | Status: new Priority: normal | Milestone: 7.10.1 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: accepts invalid program | Test Case: | Blocking: | Differential Revisions: | -------------------------------------+------------------------------------- Comment (by Richard Eisenberg ): In [changeset:"8fea2acde696f9960ffcf84f512235bbf4b481d6/ghc"]: {{{ #!CommitTicketReference repository="ghc" revision="8fea2acde696f9960ffcf84f512235bbf4b481d6" Test #9201 in typecheck/should_fail/T9201 }}} -- Ticket URL: http://ghc.haskell.org/trac/ghc/ticket/9201#comment:4 GHC http://www.haskell.org/ghc/ The Glasgow Haskell Compiler