为什么 GHC 不能对这个涉及多态性和存在类型的函数进行类型检查？

Question

我有一些无法编译的 Haskell 代码（使用 GHC 8.0.2）。我想我理解了基本问题，但我想更好地理解它，以便将来避免这种情况。

我的库看起来像这样：

{-# language TypeFamilyDependencies #-}
{-# language GADTs #-}
{-# language RankNTypes #-}

module Lib where

type Key = Int

class Handle m where
    type Connection m = c | c -> m
    withConnection :: Connection m -> m a -> IO a

class (Handle m) => Data m where
    getKeyVal :: Key -> m String

data SomeConn where
    SomeConn :: (Data m) => Connection m -> SomeConn

useConnection :: SomeConn -> (forall m. Data m => m String) -> IO String
useConnection (SomeConn c) action = withConnection c action

这个想法是Data m 代表一个类似于ReaderT (Connection m) IO 的单子类。我希望用这个类型类的方法编写通用函数，并让确切的方法实例由SomeConn（在运行时选择）包裹的连接类型确定。

下面的代码

getKeyValWith :: SomeConn -> Key -> IO String
getKeyValWith c = (useConnection c). getKeyVal

从 GHC 8.0.2 给我以下错误：

• Couldn't match type ‘m0 String’
                 with ‘forall (m :: * -> *). Data m => m String’
  Expected type: m0 String -> IO String
    Actual type: (forall (m :: * -> *). Data m => m String)
                 -> IO String
• In the first argument of ‘(.)’, namely ‘useConnection c’
  In the expression: useConnection c . getKeyVal
  In an equation for ‘getKeyValWith’:
      getKeyValWith c = useConnection c . getKeyVal

奇怪的是，以下工作正常：

getKeyValWith c k = useConnection c (getKeyVal k)

不那么令人惊讶的是：

getKeyValWith (SomeConn c) = withConnection c . getKeyVal

是否有一个简单的规则可以理解为什么 GHC 不喜欢第一个示例，但其他示例还可以？有没有一种方法可以让 GHC 在尝试编译第一个定义时获得更多关于它在做什么的信息？我知道这可能不是惯用的 Haskell（有些人称之为“存在/类型类反模式”）。

编辑：

我应该补充一点，即使我在第一个示例中明确添加了 getKeyVal :: Key -> (Data m => m String) 类型，我也会遇到同样的问题。我什至可以用我选择的类型签名（类型检查）给这个函数自己的名字，但我得到了同样的错误。但我现在看到，即使我显式添加类型，在 GHCI 中运行 :t（带有 -XRankNTypes）也会让我返回原始类型，Data m => 浮动到左侧。所以我想我明白为什么 GHC 对我犹豫不决。我可以强制 GHC 使用我选择的类型吗？

Answer 1

这都是关于.。它无法在函数之间传递多态参数，因此如果 f 是 rank-2 多态，f . g 将不起作用。请注意以下工作：

(~.) :: ((∀ m. Data m => m String) -> z) -> (x -> (∀ m. Data m => m String))
          -> x -> z
(~.) f g x = f (g x)

getKeyValWith :: SomeConn -> Key -> IO String
getKeyValWith c = useConnection c ~. getKeyVal

理想情况下，. 的类型应该是

(.) :: ∀ c . ((∀ y . c y => y) -> z) -> x -> ((∀ y . c y => y) -> x)
               -> x -> z

因此涵盖了所有特殊情况，例如上面的~.。但这是不可能的——它需要推断出最弱的约束c 才能在任何给定情况下进行选择——在传统情况下，c y = y~y₀——我很确定这通常是不可计算的。

（一个有趣的问题是，如果编译器在类型检查之前尽可能多地内联.，我们能走多远，就像现在已经对$ 做的那样。如果它做了自动 eta 扩展，它当然可以让 useConnection c . getKeyVal 工作，但自动 eta 扩展通常不是一个好主意...）

通常的解决方法是通过将多态参数包装在 GADT 中来隐藏 Rank-2 多态性，就像您对 SomeConn 所做的那样。