应用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实例列表中.)

这似乎是以下情况之一:类型检查器认为您正在传递k参数.幸运的是,似乎你可以通过显式传递kind变量来解决它.

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