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

15 Oct 2016


      #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

    