Application of type-level arguments of Kind other than Type

Question

I would like to be able to explicitly apply an argument of kind other than Type to a dummy constructor purely for documentation purposes. However TypeApplications does not seem to support this scenario:

{-# 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

leads to the error

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)

Is there a way to do this?

Answer 1

I think you’ve found a type checker bug.

The way kind variables are implemented, GHC passes around an extra type parameter behind the scenes. This type parameter is supposed to be implicit and filled in by unification, but sometimes it shows up. (That's why you sometimes see extra type parameters in Haddocks, eg in Proxy's instance list.)

This appears to be one of those situations: the type checker thinks you’re passing the k parameter. Luckily it seems like you can work around it by passing the kind variable explicitly.

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