Class polymorphism

Question

I recently ran into a problem using good polymorphism with GADT. The answer was to give a “full user view” (CUSK) for my data type. I have read the relevant documentation , but still getting essentially the same error when I try to apply it to the class.

Specifically, as soon as I give CUSK, the following compiles:

{-# LANGUAGE DataKinds, PolyKinds, GADTs #-} data Foo (x :: k) where C :: Foo x -> Foo '(x,x) 

but when I transfer this 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 an error message:

 • 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 something small that I need to do to convince the GHC that f is kind-polymorphic in the second example.

Answer 1

This is work for GHC 8 and TypeInType , which allows for much more fun forms of dependency. The following is a minor edit to your typechecks codes.

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

It is imperative that it is no longer a syntax error to use forall in the type (ha ha!) Of a type parameter.