haskell - 应用类型以外的类型的类型级参数

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