[GHC] #10122: PolyKinds: inferred type not as polymorphic as possible
#10122: PolyKinds: inferred type not as polymorphic as possible -------------------------------------+------------------------------------- Reporter: thomie | Owner: Type: bug | Status: new Priority: normal | Milestone: Component: Compiler | Version: 7.10.1-rc2 Keywords: | Operating System: Unknown/Multiple Architecture: | Type of failure: None/Unknown Unknown/Multiple | Blocked By: Test Case: | Related Tickets: Blocking: | Differential Revisions: | -------------------------------------+------------------------------------- In the user's guide on [https://downloads.haskell.org/~ghc/latest/docs/html/users_guide/kind- polymorphism.html kind polymorphism] the following example is presented: {{{#!hs f1 :: (forall a m. m a -> Int) -> Int -- f1 :: forall (k:BOX). -- (forall (a:k) (m:k->*). m a -> Int) -- -> Int }}} "Here in f1 there is no kind annotation mentioning the polymorphic kind variable, so k is generalised at the top level of the signature for f1, making the signature for f1 is as polymorphic as possible." When I ask GHCi for the type of `f1`, it is however not as polymorphic as possible: {{{
:t f1 f1 :: (forall a (m :: * -> *). m a -> Int) -> Int }}}
Trying to compile the following program: {{{#!hs {-# LANGUAGE PolyKinds #-} {-# LANGUAGE ExplicitForAll #-} {-# LANGUAGE Rank2Types #-} module PolyFail where f :: (forall a m. m a -> Int) -> Int f g = g (Just 3) }}} Results in this error: {{{ [1 of 1] Compiling PolyFail ( PolyFail.hs, PolyFail.o ) PolyFail.hs:8:10: Kind incompatibility when matching types: m0 :: k -> * Maybe :: * -> * Expected type: m0 a0 Actual type: Maybe a1 Relevant bindings include g :: forall (a :: k) (m :: k -> *). m a -> Int (bound at PolyFail.hs:8:3) f :: (forall (a :: k) (m :: k -> *). m a -> Int) -> Int (bound at PolyFail.hs:8:1) In the first argument of ‘g’, namely ‘(Just 3)’ In the expression: g (Just 3) -- Ticket URL: http://ghc.haskell.org/trac/ghc/ticket/10122 GHC http://www.haskell.org/ghc/ The Glasgow Haskell Compiler
#10122: PolyKinds: inferred type not as polymorphic as possible -------------------------------------+------------------------------------- Reporter: thomie | Owner: Type: bug | Status: new Priority: normal | Milestone: Component: Compiler | Version: 7.10.1-rc2 Resolution: | Keywords: Operating System: Unknown/Multiple | Architecture: Type of failure: None/Unknown | Unknown/Multiple Blocked By: | Test Case: Related Tickets: | Blocking: | Differential Revisions: -------------------------------------+------------------------------------- Changes (by adamgundry): * cc: adamgundry (added) Comment: I don't think there is actually a bug here, although the lack of explicit forall-bound kind variables is certainly unpleasant, and one could argue that the current behaviour may not be the most useful one. If you turn on `-XPolyKinds` in GHCi (note that it is not enough to load a module with `LANGUAGE PolyKinds`) you should find that `:t f1` gives the right answer, at least it does in 7.10-rc1. Without `-XPolyKinds`, the kind polymorphism is correctly eliminated. Moreover, the error in your `PolyFail` example is exactly what the user manual documentation would suggest. The fact that "k is generalised at the top level of the signature for f1" means that `f1` must work for all `k`, but your implementation assumes `k` is `*`. In the usual way of higher- rank types, making the signature for f1 as polymorphic as possible amounts to placing the most restrictions on the function's definition. Suggestions for how to make this clearer in the documentation are welcome. -- Ticket URL: http://ghc.haskell.org/trac/ghc/ticket/10122#comment:1 GHC http://www.haskell.org/ghc/ The Glasgow Haskell Compiler
#10122: PolyKinds: inferred type not as polymorphic as possible -------------------------------------+------------------------------------- Reporter: thomie | Owner: Type: bug | Status: closed Priority: normal | Milestone: Component: Compiler | Version: 7.10.1-rc2 Resolution: invalid | Keywords: Operating System: Unknown/Multiple | Architecture: Type of failure: None/Unknown | Unknown/Multiple Blocked By: | Test Case: Related Tickets: | Blocking: | Differential Revisions: -------------------------------------+------------------------------------- Changes (by thomie): * status: new => closed * resolution: => invalid Comment: Thanks, you're right. I indeed did not set `-XPolyKinds` in GHCi, and didn't fully appreciate the difference between the types of `f1` and `f2`: {{{ f1 :: (forall (a::k) (m::k->*). m a -> Int) -> Int f2 :: (forall (k::BOX) (a::k) (m::k->*). m a -> Int) -> Int }}} I asked a stackoverflow [http://stackoverflow.com/questions/28772695 /rankntypes-and-polykinds question] about this, so that the answer will be easier to find. Possible documentation improvements: * an explanation or link to an explanation for `BOX` is missing (see 'Datatype promotion'). * the documentation shows the initial `forall (k:BOX)` in `f1`'s type, but GHCi and GHC error message leave it out. This could be made more clear. * the inferred type signatures show `:` instead of `::`, unnecessarily. * maybe add one more sentence about the implications the placement of the `kind forall`. -- Ticket URL: http://ghc.haskell.org/trac/ghc/ticket/10122#comment:2 GHC http://www.haskell.org/ghc/ The Glasgow Haskell Compiler
#10122: PolyKinds: inferred type not as polymorphic as possible
-------------------------------------+-------------------------------------
Reporter: thomie | Owner:
Type: bug | Status: closed
Priority: normal | Milestone:
Component: Compiler | Version: 7.10.1-rc2
Resolution: invalid | Keywords:
Operating System: Unknown/Multiple | Architecture:
Type of failure: None/Unknown | Unknown/Multiple
Blocked By: | Test Case:
Related Tickets: | Blocking:
| Differential Revisions:
-------------------------------------+-------------------------------------
Comment (by Simon Peyton Jones
#10122: PolyKinds: inferred type not as polymorphic as possible -------------------------------------+------------------------------------- Reporter: thomie | Owner: Type: bug | Status: closed Priority: normal | Milestone: Component: Compiler | Version: 7.10.1-rc2 Resolution: invalid | Keywords: Operating System: Unknown/Multiple | Architecture: Type of failure: None/Unknown | Unknown/Multiple Blocked By: | Test Case: Related Tickets: | ghci/scripts/T10122 | Blocking: | Differential Revisions: -------------------------------------+------------------------------------- Changes (by simonpj): * testcase: => ghci/scripts/T10122 Comment: Good points -- and an underlying bug fixed too. -- Ticket URL: http://ghc.haskell.org/trac/ghc/ticket/10122#comment:4 GHC http://www.haskell.org/ghc/ The Glasgow Haskell Compiler
#10122: PolyKinds: inferred type not as polymorphic as possible -------------------------------------+------------------------------------- Reporter: thomie | Owner: Type: bug | Status: new Priority: normal | Milestone: 7.12.1 Component: Compiler | Version: 7.10.1-rc2 Resolution: | Keywords: Operating System: Unknown/Multiple | Architecture: Type of failure: None/Unknown | Unknown/Multiple Blocked By: | Test Case: Related Tickets: #7688 | ghci/scripts/T10122 | Blocking: | Differential Revisions: -------------------------------------+------------------------------------- Changes (by thomie): * status: closed => new * resolution: invalid => * related: => #7688 * milestone: => 7.12.1 Comment: Closing in a second. -- Ticket URL: http://ghc.haskell.org/trac/ghc/ticket/10122#comment:5 GHC http://www.haskell.org/ghc/ The Glasgow Haskell Compiler
#10122: PolyKinds: inferred type not as polymorphic as possible -------------------------------------+------------------------------------- Reporter: thomie | Owner: Type: bug | Status: closed Priority: normal | Milestone: 7.12.1 Component: Compiler | Version: 7.10.1-rc2 Resolution: fixed | Keywords: Operating System: Unknown/Multiple | Architecture: Type of failure: None/Unknown | Unknown/Multiple Blocked By: | Test Case: Related Tickets: #7688 | ghci/scripts/T10122 | Blocking: | Differential Revisions: -------------------------------------+------------------------------------- Changes (by thomie): * status: new => closed * resolution: => fixed -- Ticket URL: http://ghc.haskell.org/trac/ghc/ticket/10122#comment:6 GHC http://www.haskell.org/ghc/ The Glasgow Haskell Compiler
#10122: PolyKinds: inferred type not as polymorphic as possible -------------------------------------+------------------------------------- Reporter: thomie | Owner: Type: bug | Status: closed Priority: normal | Milestone: 8.0.1 Component: Compiler | Version: 7.10.1-rc2 Resolution: fixed | Keywords: Operating System: Unknown/Multiple | Architecture: | Unknown/Multiple Type of failure: None/Unknown | Test Case: | ghci/scripts/T10122 Blocked By: | Blocking: Related Tickets: #7688 | Differential Rev(s): Wiki Page: | -------------------------------------+------------------------------------- Description changed by mpickering: @@ -52,0 +52,1 @@ + }}} New description: In the user's guide on [https://downloads.haskell.org/~ghc/latest/docs/html/users_guide/kind- polymorphism.html kind polymorphism] the following example is presented: {{{#!hs f1 :: (forall a m. m a -> Int) -> Int -- f1 :: forall (k:BOX). -- (forall (a:k) (m:k->*). m a -> Int) -- -> Int }}} "Here in f1 there is no kind annotation mentioning the polymorphic kind variable, so k is generalised at the top level of the signature for f1, making the signature for f1 is as polymorphic as possible." When I ask GHCi for the type of `f1`, it is however not as polymorphic as possible: {{{
:t f1 f1 :: (forall a (m :: * -> *). m a -> Int) -> Int }}}
Trying to compile the following program: {{{#!hs {-# LANGUAGE PolyKinds #-} {-# LANGUAGE ExplicitForAll #-} {-# LANGUAGE Rank2Types #-} module PolyFail where f :: (forall a m. m a -> Int) -> Int f g = g (Just 3) }}} Results in this error: {{{ [1 of 1] Compiling PolyFail ( PolyFail.hs, PolyFail.o ) PolyFail.hs:8:10: Kind incompatibility when matching types: m0 :: k -> * Maybe :: * -> * Expected type: m0 a0 Actual type: Maybe a1 Relevant bindings include g :: forall (a :: k) (m :: k -> *). m a -> Int (bound at PolyFail.hs:8:3) f :: (forall (a :: k) (m :: k -> *). m a -> Int) -> Int (bound at PolyFail.hs:8:1) In the first argument of ‘g’, namely ‘(Just 3)’ In the expression: g (Just 3) }}} -- -- Ticket URL: http://ghc.haskell.org/trac/ghc/ticket/10122#comment:8 GHC http://www.haskell.org/ghc/ The Glasgow Haskell Compiler
participants (1)
-
GHC