多态 "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，我们必须在多态类型 forall a. k a -> b 处实例化变量 y。这是谓词多态性的一个实例。

正如 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 版本之间发生变化时，请不要太惊讶。

多态 "flip" 在 7.10 中失败

Polymorphic "flip" fails in 7.10

haskell

ghc