kindgenericsth
: Template Haskell support for generating GenericK
instances
This package provides Template Haskell functionality to automatically derive
GenericK
instances. Currently, this only supports the version of GenericK
as found in the kindgenerics
library. (The GenericK
class found in
kindgenericssop
is not supported at the moment.)
How to use this library
To derive instances of GenericK
for a data type, simply pass the Template
Haskellâ€“quoted Name
of the type to the deriveGenericK
function, as in the
following example:
$(deriveGenericK ''Either)
If you wish to pass a data family instance, one can pass the name of a
constructor belonging to the particular family instance, such as in the
following example:
data family Foo a b
data instance Foo Int b = MkFooInt b
$(deriveGenericK 'MkFooInt)
You will likely need to enable most of these language extensions in order for
GHC to accept the generated code:
DataKinds
EmptyCase
(if using an empty data type)
FlexibleInstances
MultiParamTypeClasses
PolyKinds
(if using a polykinded data type)
TemplateHaskell
TypeFamilies
UndecidableInstances
(if using a data type involving type families)
Type families
If the data type uses a type family (more precisely, if a type
variable occurs in a type family application), deriveGenericK
will warn that it won't generate all of the instances that you'd
normally expect, and it will tell you what to do if you do want those
instances or if you want to silence the warning.
type family F a
data T a = C (F a)
$(deriveGenericK ''T)
Warning message:
Found type family in definition of ''T. Some instances have been skipped.
Declared instances:
instance GenericK (T a)
Skipped instances:
instance GenericK T
To enable type family support and obtain those skipped instances:
$(preDeriveGenericK ''T)
$(postDeriveGenericK ''T)
To silence this warning:
$(deriveGenericKQuiet ''T)
How many GenericK
instances are generated
deriveGenericK
typically generates multiple GenericK
instances per data
type, as there is one GenericK
instance per partial application of a data
type constructor. For instance, $(deriveGenericK ''Either)
will generate
three GenericK
instances:
instance GenericK (Either a b) where ...
instance GenericK (Either a) where ...
instance GenericK Either where ...
Not every data type can be partially applied all the way in this fashion,
however. Some notable counterexamples are:

Data family instances. In the following example:
data family Bar a b
data instance Bar a a = MkBar a
One cannot partially apply to Bar a a
to simply Bar a
, so
$(deriveGenericK 'MkBar)
will only generate a single instance for
GenericK (Bar a a)
.

Dependent kinds. kindgenerics
is not currently capable of representing
data types such as the following in their full generality:
data Baz k (a :: k)
Because the k
type variable is used in the kind of a
(i.e., it is used
in a visible, dependent fashion). As a consequence,
$(deriveGenericK ''Baz)
will only generate the following instances:
instance GenericK (Baz k a)
instance GenericK (Baz k)
Limitations
kindgenerics
is capable of representing a wide variety of data types. The
Template Haskell machinery in this library makes a besteffort attempt to
automate the creation of most of these instances, but there are a handful of
corner cases that it does not handle well. This section documents all of the
known limitations of deriveGenericK
:

Data constructors with rankn field types (e.g., (forall a. a > a)
)
are partially supported: forall
and constraints c =>
are allowed only
at the root of a field's type.
data Ok = Ok
{ a :: forall a. a > a
, b :: forall a b. Eq a => a > b
}
data NotOk = NotOk
{ c :: (forall a. a > a) > Bool
}

Data constructors with unlifted field types (e.g., Int#
or (# Bool #)
)
are unlikely to work.

GADTs that make use of certain forms of kind equalities are currently not
supported. For example:
data Quux (a :: k) where
MkQuux :: forall (a :: *). Maybe a > Quux a
If one were to rewrite Quux
to make the existential quantification
explicit, it would look like this:
data Quux (a :: k) =
forall (a' :: *). (k ~ Type, a' ~~ a) => MkQuux (Maybe a')
Therefore, we ought to get a GenericK
instance like this:
instance GenericK (Quux :: k > *) where
type RepK (Quux :: k > *) =
Exists *
((Kon (k ~ Type) :&: (Var0 :~~: Var1)) :=>: Field (Maybe :$: Var0))
...
Devising an algorithm that converts the original GADT definition of Quux
into the explicitly existential form is not straightforward, however. In
particular, deriveGenericK
only detects the k ~ *
part correctly at the
moment, so it will generate an ill kinded instance for Quux
.

While there is support for data types that use type families in their fields,
they cannot be dependently typed, i.e., the result type may not
depend on visible arguments.