类型变量“a0”不明确

Question

我不明白为什么以下代码不能编译：

{-# LANGUAGE GADTs, ScopedTypeVariables #-}
data A = A
class C a where
  c :: a -> Bool
instance C A where
  c _ = True
data D a where
  D :: C a => D a
toBool :: D a -> Bool
toBool D = c (undefined::a)

这是错误消息：

Could not deduce (C a0) arising from a use of ‘c’
from the context (C a)
  bound by a pattern with constructor
             D :: forall a. C a => D a,
           in an equation for ‘toBool’
  at test.hs:15:8
The type variable ‘a0’ is ambiguous
Note: there is a potential instance available:
  instance C A -- Defined at test.hs:8:10
In the expression: c (undefined :: a)
In an equation for ‘toBool’: toBool D = c (undefined :: a)

有人能解释一下发生了什么吗？

Answer 1

顶级类型声明中引入的类型变量与函数体中引入的变量不同。另一种说法是嵌套类型声明引入了"新鲜"变量。另一种说法是，在代码中放入显式foralls，Haskell会自动引入它们，并静默：

toBool :: forall a . D a -> Bool
toBool D = c (undefined :: forall a . a)   -- another forall here?

你真正想要的是

toBool :: forall a . D a -> Bool
toBool D = c (undefined :: a)   -- capture `a` from prior scope

而且，你很幸运。事实证明，几乎每个人都不时需要这种功能，因此存在一个非常常见的Haskell扩展，称为ScopedTypeVariables。以下代码应该编译

{-# LANGUAGE ScopedTypeVariables #-}
toBool :: forall a . D a -> Bool
toBool D = c (undefined :: a)

请注意，为了调用ScopedTypeVariables，您现在必须手动引入要特殊处理的forall。如果没有这本手册，forall Haskell将自动在所有正常位置引入它们。