Haskell中IdentityT实例里m的隐式量化位置及显式化方法

首先明确@pash的核心观点：Haskell里不存在真正“未量化”的类型签名——所有未显式标注的类型变量，都会被编译器自动添加隐式的全称量化（forall），只是量化的位置不同而已。

先看原始可编译代码 #

你提到的IdentityT Monad实例大概是这样的：

newtype IdentityT m a = IdentityT { runIdentityT :: m a }

instance Monad m => Monad (IdentityT m) where
  return = IdentityT . return
  IdentityT ma >>= f = IdentityT $ ma >>= runIdentityT . f

这里>>=定义里的m没有显式写forall，但编译器能正常处理。

类型推理在哪给m添加量化？ #

这里的m不是方法>>=的自由变量——它是实例定义的参数，在实例头Monad m => Monad (IdentityT m)里已经被绑定。编译器会在整个实例的最外层给m添加隐式的forall，相当于：

instance forall m. Monad m => Monad (IdentityT m) where
  -- ... 方法定义 ...

也就是说，m的量化范围是整个实例，所有方法里的m都共享这个绑定，不需要在每个方法里单独量化。

为什么显式加forall会编译失败？ #

如果你尝试在f的类型签名里加forall m.，比如写成：

IdentityT ma >>= (f :: forall m. a -> IdentityT m b) = ...

这里的m是局部量化的新变量，和实例头绑定的m完全不是同一个，导致类型不匹配——编译器会认为你要把任意Monad的IdentityT组合起来，而非当前实例的m，自然编译失败。

如果直接在>>=的签名里加forall m.，同样会覆盖实例头的m绑定，破坏Monad m的约束，引发类型错误。

如何移除所有隐式量化？ #

要彻底去掉隐式量化，需要开启两个GHC扩展：ScopedTypeVariables和ExplicitForAll，然后显式绑定实例和方法的所有类型变量：

{-# LANGUAGE ScopedTypeVariables #-}
{-# LANGUAGE ExplicitForAll #-}

newtype IdentityT m a = IdentityT { runIdentityT :: m a }

-- 在实例头显式量化m，让它能被方法签名引用
instance forall m. Monad m => Monad (IdentityT m) where
  -- 显式量化方法的自由变量a，m从实例头继承
  return :: forall a. a -> IdentityT m a
  return = IdentityT . return

  -- 显式量化a、b，m复用实例头的绑定
  (>>=) :: forall a b. IdentityT m a -> (a -> IdentityT m b) -> IdentityT m b
  IdentityT ma >>= f = IdentityT $ ma >>= runIdentityT . f

• ScopedTypeVariables的作用是让实例头量化的m能在方法签名里被直接引用，不会被当作新的局部变量
• ExplicitForAll允许我们显式写出所有forall，彻底消除隐式量化

内容的提问来源于stack exchange，提问作者Janus Troelsen