[GHC] #10122: PolyKinds: inferred type not as polymorphic as possible

27 Feb 2015


      #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