#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