Kind 而非 Type 的类型级参数的应用

Question

我希望能够将 Type 以外的其他类型的参数显式应用于虚拟构造函数，纯粹用于文档目的。但是 TypeApplications 似乎不支持这种情况：

{-# LANGUAGE GADTs, PolyKinds, ScopedTypeVariables, TypeApplications #-}

data EQ :: k -> k -> * where
  Refl :: EQ a a

data Wrap (a :: k) = Wrap (EQ a a)

wrap :: forall (a :: k). Wrap a
wrap = Wrap @a Refl

导致错误

ProxyApply.hs:9:14: error:
    • Expected a type, but ‘a’ has kind ‘k’
    • In the type ‘a’
      In the expression: Wrap @a Refl
      In an equation for ‘wrap’: wrap = Wrap @a Refl
    • Relevant bindings include
        wrap :: Wrap a (bound at ProxyApply.hs:9:1)

有办法吗？

Answer 1

我认为您发现了一个类型检查程序错误。

种类变量的实现方式，GHC 在幕后传递了一个额外的类型参数。这个类型参数应该是隐式的，统一填充的，但有时会出现。（这就是为什么您有时会在 Haddocks 中看到额外的类型参数，例如 Proxy's instance list。）

这似乎是其中一种情况：类型检查器认为您正在传递 k 参数。幸运的是，您似乎可以通过显式传递 kind 变量来解决这个问题。

wrap :: forall (a :: k). Wrap a
wrap = Wrap @k @a Refl

Kind 而非 Type 的类型级参数的应用

Application of type-level arguments of Kind other than Type

haskell

type-kinds