Should we remove the second parameter of `GenericK`?

Consider making GenericK a single-parameter class, like Generic, letting the methods toK and fromK universally quantify over the LoT parameter instead.

The main conceptual issue with GenericK having its current two arguments is that it is impossible to express the constraint that a given type constructor f is generic independently of its type parameters, unless one uses QuantifiedConstraints.

I don't mean that QuantifiedConstraints is inherently bad, but GenericK with only one argument would take out its necessity. Furthermore, (I hope) it would even make it easier to generalize code over arbitrary arities of type constructors.

The problems arise when deriving operations involving higher-kinded types which hide the parameters of generic type constructors, such as the following existential type:

data Ex :: (Type -> Type) -> Type where
  Ex :: forall f a. f a -> Ex f

In this gist, the Ex type allows us to define parsers for GADTs f as functions

genericReadEx :: _ => String -> Maybe (Ex f)

so that f's hidden type index may depend on the input:

But what constraint to give genericReadEx? A first attempt would be forall l. GenericK f l. However, GenericK instances explicitly match on the l constructor, so they are not sufficiently parametric: we actually have to write forall a. GenericK f (a :&&: LoT0).

1. We must use QuantifiedConstraints, which might be fine in itself, but does require extra expertise on top of generics.

2. And we have to unfold LoT tuples manually.

For similar reasons, in the implementation, we also need to define a specialized variant of Ex for generic representations, instead of reusing Ex:

data KEx :: (LoT (k -> Type) ->  Type) -> Type where
  KEx :: forall f a. f (a :&&: LoT0) -> KEx f

Moreover, the code is now quite specific to type constructors of arity 1. I conjecture that a lot of the work in generalizing that to higher arities could be refactored into the kind-generics library as part of the removal of GenericK's second argument.

For instance, as a first step in my working example (in the gist linked above), we could generalize the existential type Ex to hide the arguments of a type constructor of arbitrary arity/kind k:

data Ex :: k -> Type where
  Ex :: forall (f :: k) (a :: LoT k). f :@@: a -> Ex f

But that requires making :@@: "lazier" than it is currently.