I have the following Rank 2 function:

polyOn :: (f a -> f b -> c) -> (forall k . k -> f k) -> a -> b -> c
polyOn bifunc func x y =
  bifunc (func x) (func y)

I'd like to flip it

flippedPolyOn :: (forall k . k -> f k) -> (f a -> f b -> c) -> a -> b -> c
flippedPolyOn =
  flip polyOn

but ghc complains:

    • Couldn't match type ‘k0 -> f k0’ with ‘forall k. k -> f k’
      Expected type: (f a -> f b -> c) -> (k0 -> f k0) -> a -> b -> c
        Actual type: (f a -> f b -> c)
                     -> (forall k. k -> f k) -> a -> b -> c
    • In the first argument of ‘flip’, namely ‘polyOn’
      In the expression: flip polyOn
      In an equation for ‘flippedPolyOn’: flippedPolyOn = flip polyOn
    • Relevant bindings include
        flippedPolyOn :: (forall k. k -> f k) -> (f a -> f b -> c) -> a -> b -> c
          (bound at XXXXXX:75:1)
   |
76 |   flip polyOn
   |        ^^^^^^

So it looks like ghc at some point specializes the forall k. k -> f k to a specific value of k (which it calls k0).

Why does ghc do this? Is this specialization avoidable?

CodePudding user response：

GHC < 9

The issue is that GHC < 9.x does not support impredicative polymorphism. Essentially, what you are trying to do is to instantiate

flip :: (a0->b0->c0) -> b0->a0->c0

in this way:

a0 ~ (f a -> f b -> c)
b0 ~ (forall k . k -> f k)
c0 ~ a -> b -> c

Type inference has no issues with a0 and c0, but won't allow choosing b0 in that way. Indeed, without support for impredicative polymorphism, a type variable like b0 can only be instantiated with a monotype (a type without foralls).

We need to inline the flip to make this work

flippedPolyOn x y = polyOn y x

GHC >= 9

In GHC 9 by default we still get a type error, but with a better error message, pointing out the impredicativity issue:

  Cannot instantiate unification variable `b0'
  with a type involving polytypes: forall k. k -> f k

We can make your code type-check as is by turning on impredicative types:

{-# LANGUAGE RankNTypes, ImpredicativeTypes #-}