PolyKinds: inferred type not as polymorphic as possible
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)