Using arguments of type Kind, except for type

Question

I would like to be able to explicitly apply a view argument other than Type to a fixture constructor solely for documentation purposes. However, TypeApplications does not seem to support this scenario:

 {-# LANGUAGE GADTs, PolyKinds, ScopedTypeVariables, TypeApplications #-} data EQ :: k -> k -> * where Refl :: EQ aa data Wrap (a :: k) = Wrap (EQ aa) wrap :: forall (a :: k). Wrap a wrap = Wrap @a Refl 

leads to an 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 any way to do this?

Answer 1

I think you found a type checking error.

As view variables are implemented, the GHC goes around an extra type parameter behind the scenes. This type parameter must be implicit and filled with unification, but sometimes it appears. (This is why you sometimes see additional type parameters in Haddocks, for example, in the Proxy list of instances .)

This is apparently one of these situations: the type checker considers that you are passing the parameter k . Fortunately, it looks like you can get around this by explicitly passing a view variable.

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