# `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`
* `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.
```haskell
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:
```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) `
## 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 partially supported: `forall` and constraints `c =>` are allowed only
at the root of a field's type.
```haskell
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
}
```
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`.
4. 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.