Skip to content

Derive GenericK for data types that mention type families

Li-yao Xia requested to merge lysxia/kind-generics:tyfam into master

Closes #12 (closed)

When a data type contains type families, we can defunctionalize them into a new Atom which is interpreted by calling Eval from fcf-family.

The new package fcf-family implements the defunctionalization scheme described in #12 (closed), which does not pollute the namespace with data types/defunctionalization symbols.

Due to some limitations in GHC, the deriveGenericK call must be split in two splices:

preDeriveGenericK ''MyType
postDeriveGenericK

The first call defunctionalizes type families, and the second call declares the desired GenericK instances, which rely on type instances from the former to typecheck, hence they must belong to a different recursive group.


Implementation notes

Currently depends on an unreleased library fcf-family. And I have a downstream project where I'd like to test this out (ad-lib). The sample I wrote in #12 (closed) was somehow not supposed to work; it works accidentally when it's all in a single file, but I ran into the aforementioned issue when turning it into a library.

Luckily I still succeeded with another pile of hacks.

Still, because of that issue, users are still forced to break deriveGenericK into two splices, with preDeriveGenericK and postDeriveGenericK. Another way to structure this could be to make deriveGenericK behave as preDeriveGenericK if it detects type families, and then users have to remember to call postDeriveGenericK. This reduces the number of exported functions but I was worried that users won't get an error if they write deriveGenericK but forget postDeriveGenericK with that approach.

The main limitation is that type families cannot be dependently typed, as in type family F a :: G a. Polykinded families are still okay, type family F (a :: k) :: k; the main distinction is whether the result type mentions visible arguments of the family. The source of the limitation is that you cannot even write an Atom that allows such dependencies.

Note that previously, type families were allowed as long as they remained saturated when translating them to an Atom. For example, deriveGenericK already worked for Field in the test suite. I was careful to detect this kind of situation so that they still behave the same.

Edited by Li-yao Xia

Merge request reports