[GHC] #9000: Kind checking fails when using PolyKinds
#9000: Kind checking fails when using PolyKinds -------------------------------------+------------------------------------- Reporter: facundo.dominguez | Owner: Type: bug | Status: new Priority: normal | Milestone: Component: Compiler (Type | Version: 7.8.2 checker) | Operating System: Linux Keywords: | Type of failure: GHC rejects Architecture: x86_64 (amd64) | valid program Difficulty: Unknown | Test Case: Blocked By: | Blocking: Related Tickets: | -------------------------------------+------------------------------------- GHC HEAD and earlier versions are failing on the following program: {{{ {-# LANGUAGE PolyKinds #-} import GHC.Exts(Any) f = (undefined :: a -> m a) :: Any -> Any Any }}} {{{ ../tmp/test-polykinds.hs:3:6: Couldn't match kind ‘k1’ with ‘*’ ‘k1’ is a rigid type variable bound by an expression type signature: Any -> Any Any at ../tmp/test-polykinds.hs:3:5 Expected type: Any -> Any Any Actual type: Any -> m0 Any In the expression: (undefined :: a -> m a) :: Any -> Any Any In an equation for ‘f’: f = (undefined :: a -> m a) :: Any -> Any Any }}} Rewriting the program as follows has compilation succeed. {{{ f = (undefined :: a -> m a) `asTypeOf` (undefined :: Any -> Any Any) }}} And removing the {{{PolyKinds}}} extension also has compilation succeed. -- Ticket URL: http://ghc.haskell.org/trac/ghc/ticket/9000 GHC http://www.haskell.org/ghc/ The Glasgow Haskell Compiler
#9000: Kind checking fails when using PolyKinds ----------------------------------------------+---------------------------- Reporter: facundo.dominguez | Owner: Type: bug | Status: new Priority: normal | Milestone: Component: Compiler (Type checker) | Version: 7.8.2 Resolution: | 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 facundo.dominguez): * cc: facundominguez@… (added) -- Ticket URL: http://ghc.haskell.org/trac/ghc/ticket/9000#comment:1 GHC http://www.haskell.org/ghc/ The Glasgow Haskell Compiler
#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
#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: ----------------------------------------------+---------------------------- Comment (by facundo.dominguez): The option {{{-fprint-explicit-kinds}}} improves a lot the error message. Thanks for the good summary. -- Ticket URL: http://ghc.haskell.org/trac/ghc/ticket/9000#comment:3 GHC http://www.haskell.org/ghc/ The Glasgow Haskell Compiler
participants (1)
-
GHC