While we're on the topic, I'll mention that at one point I attempted to modify the singletons [1] library so that it would automatically generate promoted (i.e., type-level) and singled versions of Generic instances for any data type that derived Generic. I wasn't successful, since it turns out singletons are difficult to adapt to data types with higher-kinded types [2] and type classes with associated type families [3], but I did manage to write some examples on a very limited subset of GHC.Generics in this gist [4]. The promoted version of Generic (PGeneric) in that gist works pretty much identically to Oleg's version, but with one notable difference: I don't attempt to put the Generic laws as a superclass of PGeneric. Instead, I make the laws class methods of the singled version of Generic (SGeneric). I found it more convenient to do it this way since I needed to pattern-match on these proofs directly in a generic implementation of decidable equality, but I'm sure this isn't the only way it could be done. Speaking of which, it astounds me that the Generic laws aren't documented in the Haddocks! We really should do that. Ryan S. ----- [1] http://hackage.haskell.org/package/singletons [2] See the extended discussion in https://github.com/goldfirere/singletons/issues/150 [3] https://github.com/goldfirere/singletons/issues/198 [4] https://gist.github.com/RyanGlScott/daeb63be7885244d9882dcbb1bbc10cc