[GHC] #9201: GHC unexpectedly refines explicit kind signatures

[GHC]

#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/compiler/typecheck/TcHsType.lhs#L902
 "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