[GHC] #9000: Kind checking fails when using PolyKinds

[GHC]

#9000: Kind checking fails when using PolyKinds
----------------------------------------------+----------------------------
        Reporter:  facundo.dominguez          |            Owner:
            Type:  bug                        |           Status:  closed
        Priority:  normal                     |        Milestone:
       Component:  Compiler (Type checker)    |          Version:  7.8.2
      Resolution:  invalid                    |         Keywords:
Operating System:  Linux                      |     Architecture:  x86_64
 Type of failure:  GHC rejects valid program  |  (amd64)
       Test Case:                             |       Difficulty:  Unknown
        Blocking:                             |       Blocked By:
                                              |  Related Tickets:
----------------------------------------------+----------------------------
Changes (by goldfire):

 * status:  new => closed
 * resolution:   => invalid


Comment:

 This (admittedly bizarre) behavior is (arguably) correct.

 Let's look at the kinds of the different pieces. In the type `a -> m a`,
 the kinds are fixed. We must have `(a :: *)` and `(m :: * -> *)`. However,
 in the type `Any -> Any Any`, a kind variable comes in. Annotating each
 `Any`, we get `(Any :: *) -> (Any :: k1 -> *) (Any :: k1)`. Why are these
 different? Because the `a` is repeated in the first type, but every `Any`
 is independent in the second.

 In the failing version of the code, the outer type signature is more
 general than the inner one, which is no good.

 With `asTypeOf`, in contrast, GHC unifies the two types, and the kind
 variable `k1` is unified with `*`, yielding a successful compilation.
 Although it may seem strange that the `::` use case and the `asTypeOf` use
 case differ, consider `False :: a` and {{{False `asTypeOf` (undefined ::
 a)}}}. The first fails and the second succeeds.

 Because kinds are implicit by default, this sort of unexpected behavior
 comes up fairly often. My best suggestion is to use `-fprint-explicit-
 kinds` liberally to try to detect when this is happening.

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