为什么构造函数不能有必需的类型参数？

Question

假设我定义了以下数据类型：

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

使用

RequiredTypeArguments

，我可以定义一个 function，它将

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
   |                  ^^^^^^^^^^^^^^^^^^

是什么让

(:*)

相对于

(*:)

成为问题？如果 GHC 接受的话，在类型检查期间什么会被破坏/什么会是不可判定的？

Answer 1

免责声明：我不确定这是否是真正的动机，但这似乎是一种可能的动机。

如果我可以写

'a' :* 3

和

'b' :* 5

，我想我也希望能够写出类似的东西

case x of
    'a' :* 3 -> ...
    'b' :* 5 -> ...
    _ -> ...

这似乎是有问题的，因为在运行时，

3

和

5

实际上并不作为数据块存在于任何地方。