#10122 closed bug (fixed)
PolyKinds: inferred type not as polymorphic as possible
Reported by: | thomie | Owned by: | |
---|---|---|---|
Priority: | normal | Milestone: | 8.0.1 |
Component: | Compiler | Version: | 7.10.1-rc2 |
Keywords: | Cc: | adamgundry | |
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 (last modified by )
In the user's guide on kind polymorphism the following example is presented:
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:
{-# 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)
Change History (8)
comment:1 follow-up: 2 Changed 5 years ago by
Cc: | adamgundry added |
---|
comment:2 Changed 5 years ago by
Resolution: | → invalid |
---|---|
Status: | new → closed |
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 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)
inf1
's type, but GHCi and GHC error message leave it out. This could be made more clear (use-fprint-explicit-foralls
). - the inferred type signatures show
:
instead of::
, unnecessarily. - maybe add one more sentence about the implications the placement of the
kind forall
.
comment:4 Changed 5 years ago by
Test Case: | → ghci/scripts/T10122 |
---|
Good points -- and an underlying bug fixed too.
comment:5 Changed 5 years ago by
Milestone: | → 7.12.1 |
---|---|
Related Tickets: | → #7688 |
Resolution: | invalid |
Status: | closed → new |
Closing in a second.
comment:6 Changed 5 years ago by
Resolution: | → fixed |
---|---|
Status: | new → closed |
comment:8 Changed 3 years ago by
Description: | modified (diff) |
---|
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 withLANGUAGE 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 thatf1
must work for allk
, but your implementation assumesk
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.