为何Haskell数据构造器无法使用RequiredTypeArguments？

先看初始的类型定义：

data fmt :* (n :: Nat) where
    Rep :: fmt -> fmt :* n

借助RequiredTypeArguments扩展，我们可以定义一个将n作为必需类型参数的函数：

(*:) :: fmt -> forall n -> fmt :* n
fmt *: n = Rep fmt

但如果尝试直接把数据构造器写成如下形式，GHC 9.10.1会报错：

data a :* (n :: Nat) where
    (:*) :: a -> forall n -> a :* n

对应的报错信息：

• Illegal visible, dependent quantification in the type of a term
    • In the definition of data constructor ‘:*’
   |
83 |     (:*) :: a -> forall n -> a :* n
   |                  ^^^^^^^^^^^^^^^^^^

核心原因：函数与数据构造器的本质差异 #

函数是计算导向的实体，它的类型里的可见量化（forall n ->）只是约束调用者必须显式提供类型参数，本质是给类型检查增加了一个明确的输入规则，GHC完全能处理这种显式的参数传递逻辑。

但数据构造器是数据类型的“构建蓝图”，它的行为必须严格贴合对应数据类型的结构定义：

• 索引绑定冲突
  这里的a :* n是一个索引类型，n是属于整个类型的顶层索引参数。如果在构造器里引入forall n ->，就会创建一个局部的n绑定，和顶层的类型索引n重名，GHC无法区分构造器返回类型中的n到底是指顶层索引还是局部参数，直接破坏了类型的绑定一致性。
• 类型系统的可判定性要求
  数据构造器的类型必须满足严格的索引一致性和正性条件。允许构造器使用可见依赖量化的话，构造器可以返回依赖于局部类型参数的动态类型，这会让数据类型的结构变得不确定——GHC无法静态验证构造出来的值是否真的属于定义的数据类型，最终会导致类型检查变得不可判定。
• 构造器的职责边界
  数据类型的参数是在定义类型时就确定好的，构造器只能使用这些已声明的参数来构建值，不能私自引入新的可见依赖参数。构造器的核心职责是“实例化”已定义的类型，而不是扩展类型的参数空间。

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