Kind-polymorphism in classes

Question

I recently ran into a problem using kind polymorphism with GADTs. The answer there was to give a "complete user-specified kind" (CUSK) for my data type. I've read the relevant documentation, but I'm still getting essentially the same error when I try to apply that to a class.

Concretely, once I give a CUSK, the following does compile:

{-# LANGUAGE DataKinds, PolyKinds, GADTs #-}

data Foo (x :: k) where
  C :: Foo x -> Foo '(x,x)

but when I move that definition to a class:

{-# LANGUAGE DataKinds, PolyKinds #-}

class Foo (f :: k -> *) where
  foo :: (f :: k1 -> *) (x :: k1) -> (f :: (k1,k1) -> *) ('(x,x) :: (k1,k1))

I get the error:

• Expected kind ‘(k1, k1) -> *’, but ‘f’ has kind ‘k -> *’
• In the type signature:
    foo :: (f :: k1 -> *) (x :: k1) -> (f :: (k1, k1) -> *) ('(x, x) :: (k1, k1))
  In the class declaration for ‘Foo’

I expect there's something small I need to do to convince GHC that f is kind-polymorphic in the second example.

Answer 1

This is a job for GHC 8 and TypeInType, which allows much more amusing forms of dependency. The following minor edit of your code typechecks.

{-# LANGUAGE PolyKinds, RankNTypes, KindSignatures,
    DataKinds, TypeInType  #-}

module KP where

import Data.Kind

class Foo (f :: forall k. k -> *) where
  foo :: (f :: k1 -> *) (x :: k1) -> (f :: (k1,k1) -> *) ('(x,x) :: (k1,k1))

Crucially, it is no longer a syntax error to use forall in the (ha ha!) type of a type class parameter.