Opened 5 years ago

Closed 5 years ago

Last modified 3 years ago

#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 mpickering)

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 Changed 5 years ago by adamgundry

Cc: adamgundry added

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.

comment:2 in reply to:  1 Changed 5 years ago by thomie

Resolution: invalid
Status: newclosed

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) in f1'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.
Last edited 5 years ago by thomie (previous) (diff)

comment:3 Changed 5 years ago by Simon Peyton Jones <simonpj@…>

In cabe174877d0c31535e224d69bd78434b2d28651/ghc:

Two kind-polymorphism fixes (Trac #10122)

* The original fix was to improve the documentation, in
  line with the suggestions on Trac #10122

* But in doing so I realised that the kind generalisation in
  TcRnDriver.tcRnType was completely wrong.  So I fixed that
  and updated Note [Kind-generalise in tcRnType] to explain.

comment:4 Changed 5 years ago by simonpj

Test Case: ghci/scripts/T10122

Good points -- and an underlying bug fixed too.

comment:5 Changed 5 years ago by thomie

Milestone: 7.12.1
Resolution: invalid
Status: closednew

Closing in a second.

comment:6 Changed 5 years ago by thomie

Resolution: fixed
Status: newclosed

comment:7 Changed 4 years ago by thoughtpolice

Milestone: 7.12.18.0.1

Milestone renamed

comment:8 Changed 3 years ago by mpickering

Description: modified (diff)
Note: See TracTickets for help on using tickets.