`kind-generics-th`

: 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 `kind-generics`

library. (The `GenericK`

class found in
`kind-generics-sop`

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 poly-kinded data type)
`TemplateHaskell`

`TypeFamilies`

## 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) LoT0 where ...
instance GenericK (Either a) (b :&&: LoT0) where ...
instance GenericK Either (a :&&: b :&&: LoT0) 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) LoT0`

.

Dependent kinds. `kind-generics`

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) LoT0`

`instance GenericK (Baz k) (a :&&: LoT0)`

Data types with type family applications. In the following example:

```
type family Fam a
newtype WrappedFam a = WrapFam (Fam a)
```

It is impossible to write a `GenericK`

instance for a partial application
of `WrappedFam`

, since the representation type would necessarily need to
partially apply `Fam`

, which GHC does not permit. Therefore,
`$(deriveGenericK ''WrappedFam)`

will only generate a single instance for
`GenericK (WrappedFam a) LoT0`

.

There are some uses of type families that are not supported altogether.
For instance, if a type family is applied to an *existentially* quantified
type variable, as in the following example:

```
data ExFam where
MkExFam :: forall a. Fam a -> ExFam
```

Representing `ExFam`

would fundamentally require a partial application of
`Fam`

, as `type RepK ExFam = Exists * (Field (Fam :$: Var0))`

. As a result,
it is impossible to give `ExFam`

a `GenericK`

instance.

Note that not all type families are problematic. For instance:

```
type family Fam2 :: * -> *
newtype WrappedFam2 a = WrapFam2 (Fam2 a)
```

In this example, `Fam2`

is perfectly fine to partially apply, so
`$(deriveGenericK ''WrappedFam2)`

will generate two instances (as opposed
to just one, as was the case for `WrappedFam`

).

## Limitations

`kind-generics`

is capable of representing a wide variety of data types. The
Template Haskell machinery in this library makes a best-effort 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 rank-*n* field types (e.g., `(forall a. a -> a)`

)
are currently not supported.

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 -> *) (a :&&: LoT0) 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`

.