haskell - GADT 和 ghc 7.8.2 上的显式 forall

Question

我在 ghc 7.8.2 上玩 GADT 和显式 forall。让我们看下面这个简单的例子:

{-# LANGUAGE GADTs, RankNTypes #-}

data T1 a where
   T1 :: (b -> a) -> b -> T1 a

data T2 a where
   T2 :: forall b. (b -> a) -> b -> T2 a

这里 ghc 失败了:

Test.hs:7:26: Not in scope: type variable ‘a’
Test.hs:7:35: Not in scope: type variable ‘a’

当 T2 被注释掉时，类型检查成功。但是 T1 和 T2 看起来是等价的。这是 ghc 中的错误还是 GADT 的某些限制？如果是后者，那么两者有什么区别？

Answer 1

我最初假设 T1 构造函数中的 a 绑定(bind)在 data T1 a 声明中。但它实际上是在构造函数本身中隐式量化的。因此 T2 构造函数是错误的，因为它显式量化了 b 而没有量化 a。