# `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:
```haskell
$(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:
```haskell
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:
```haskell
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:
1. Data family instances. In the following example:
```haskell
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)`.
2. Dependent kinds. `kind-generics` is not currently capable of representing
data types such as the following in their full generality:
```haskell
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) `
3. Data types with type family applications. In the following example:
```haskell
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)`.
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:
```haskell
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:
```haskell
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`:
1. Data constructors with rank-_n_ field types (e.g., `(forall a. a -> a)`)
are currently not supported.
2. Data constructors with unlifted field types (e.g., `Int#` or `(# Bool #)`)
are unlikely to work.
3. GADTs that make use of certain forms of kind equalities are currently not
supported. For example:
```haskell
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:
```haskell
data Quux (a :: k) =
forall (a' :: *). (k ~ Type, a' ~~ a) => MkQuux (Maybe a')
```
Therefore, we ought to get a `GenericK` instance like this:
```haskell
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`.