haskell - 多态 "flip"在 7.10 中失败

Question

monomorphic库包含以下代码段(希望可以在 7.8 中编译):

{-# LANGUAGE DataKinds, ExistentialQuantification, FlexibleContexts, GADTs #-}
{-# LANGUAGE ImpredicativeTypes, PolyKinds, RankNTypes, TypeFamilies       #-}
{-# LANGUAGE TypeOperators, UndecidableInstances                           #-}

class Monomorphicable k where
  type MonomorphicRep k :: *

withPolymorphic :: Monomorphicable k
               => MonomorphicRep k -> (forall a. k a -> b) -> b
withPolymorphic k trans = undefined

-- | Flipped version of 'withPolymorphic'.
liftPoly :: Monomorphicable k
         => (forall a. k a -> b) -> MonomorphicRep k -> b
liftPoly = flip withPolymorphic

但是在 7.10 中，GHC 提示:

Couldn't match type ‘k2 a0 -> b’ with ‘forall (a :: k0). k1 a -> b’
    Expected type: MonomorphicRep k2 -> (k2 a0 -> b) -> b
      Actual type: MonomorphicRep k1
                   -> (forall (a :: k0). k1 a -> b) -> b
    Relevant bindings include
      liftPoly :: (forall (a :: k). k2 a -> b) -> MonomorphicRep k2 -> b
        (bound at Data/Type/Monomorphic.hs:45:1)
    In the first argument of ‘flip’, namely ‘withPolymorphic’
    In the expression: flip withPolymorphic

当然如果我改变了 liftPoly的定义到

liftPoly a b = withPolymorphic b a

那么7.10是快乐的。这里发生了什么？在以某种方式处理多态函数时，7.10 是否应该更严格？它似乎不是单态限制，因为一切都有一个签名。

Answer 1

flip的类型是

flip :: (x -> y -> z) -> (y -> x -> z)

键入检查 liftPoly ，我们必须实例化变量 y在多态型 forall a. k a -> b .这是一个不可预测的多态性的例子。

如 https://ghc.haskell.org/trac/ghc/wiki/ImpredicativePolymorphism 的页面说，

We've made various attempts to support impredicativity, so there is a flag -XImpredicativeTypes. But it doesn't work, and is absolutely unsupported. If you use it, you are on your own; I make no promises about what will happen.

所以，当 ImpredicativeTypes 的行为时不要太惊讶GHC 版本之间的变化。