[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     |           Version:  7.8.2
  checker)                           |  Operating System:  Unknown/Multiple
       Keywords:                     |   Type of failure:  GHC accepts
   Architecture:  Unknown/Multiple   |  invalid program
     Difficulty:  Unknown            |         Test Case:
     Blocked By:                     |          Blocking:
Related Tickets:                     |
-------------------------------------+-------------------------------------
 The following program should be rejected by the type checker:

 {{{
 {-# LANGUAGE PolyKinds, FunctionalDependencies, MultiParamTypeClasses #-}

 class MonoidalCCC (f :: x -> y) (d :: y -> y -> *) | f -> d where
   ret :: d a (f a)
 }}}

 Instead it is accepted, but the kind variables specified above are
 'corrected' during typechecking to:

 {{{
 >>> :browse
 class MonoidalCCC (f :: x -> x) (d :: x -> x -> *) | f -> d where
   ret :: d a (f a)
 }}}

 This may be similar in root cause to issue #9200, but there a valid
 program is rejected, and here an invalid program is accepted, so the fixes
 may be quite different.

 It seems these kind variables are just being allowed to unify rather than
 being checked for subsumption.

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