Datatype-generic programming is a widely used technique to define functions
that work regularly over a class of datatypes. Examples include deriving serialization
of data, equality or even functoriality. The \emph{state-of-the-art} of generic
programming still lacks handling GADTs, multiple type variables, and some other features.
This paper exploits modern GHC extensions, including \texttt{TypeInType}, to
handle arbitrary number of type variables, constraints, and existentials.
We also provide an Agda model of our construction that does \emph{not}
require Russel's paradox, proving the construction is consistent.