Haskell中能否泛化类约束？GADT定义报错求助

你遇到的问题是GHC的ScopedTypeVariables扩展在GADT构造器签名中的作用规则导致的——虽然你启用了该扩展，但GADT的类型参数并不会自动进入构造器签名的作用域，必须显式绑定才能引用。

错误原因 #

在你的GADT定义中：

data A' (c :: Type -> Constraint) where
    A' :: forall a. c a => { unA :: a } -> A' c

构造器签名里的c是GADT的类型参数，但默认情况下，GHC不会把这个参数自动纳入构造器签名的作用域。即使启用了ScopedTypeVariables，也需要显式告诉GHC：构造器中的c就是GADT定义里的那个c，否则它会被当作未绑定的新类型变量，从而报错。

两种可行的修正方案 #

方案一：在GADT定义上显式绑定类型参数

通过forall c.在GADT定义层面绑定c，这样构造器签名里的c就能通过ScopedTypeVariables引用到这个外层参数：

{-# LANGUAGE ExistentialQuantification #-}
{-# LANGUAGE GADTs #-}
{-# LANGUAGE KindSignatures #-}
{-# LANGUAGE ScopedTypeVariables #-}
import Data.Kind (Type, Constraint)

class C a where

data forall c. A' (c :: Type -> Constraint) where
    A' :: forall a. c a => { unA :: a } -> A' c

type A = A' C

方案二：在构造器的forall中显式包含c

直接在构造器的量化列表里加上c并指定其种类，让GHC明确它的来源：

{-# LANGUAGE ExistentialQuantification #-}
{-# LANGUAGE GADTs #-}
{-# LANGUAGE KindSignatures #-}
{-# LANGUAGE ScopedTypeVariables #-}
import Data.Kind (Type, Constraint)

class C a where

data A' (c :: Type -> Constraint) where
    A' :: forall (c :: Type -> Constraint) a. c a => { unA :: a } -> A' c

type A = A' C

验证同构性 #

修正后的A类型和你最初定义的A完全同构：两者都包装了任意满足C a约束的a类型值，行为和语义完全一致。

内容的提问来源于stack exchange，提问作者Björn Gohla