diff --git a/README.md b/README.md
--- a/README.md
+++ b/README.md
@@ -77,7 +77,7 @@
 
 ```haskell
 class GenericK (f :: k) where
-  type RepK f :: LoT k -> *
+  type family RepK f :: LoT k -> *
   fromK :: f :@@: x -> RepK f x
   toK   :: RepK f x -> f :@@: x
 ```
@@ -126,7 +126,7 @@
 instance GenericK (Either a b) where ...
 ```
 
-Sometimes it is not possible to write all of these instances, due to restrictions in GHC's type system. The most common case is a data type making use of a type family -- we cannot write something like `Fam :$: Var0` because type families cannot be partially applied. The `kind-generics-th` package contains a thorough description of these limitations.
+Sometimes it is not possible to write all of these instances, due to restrictions in GHC's type system. The `kind-generics-th` package contains a thorough description of these limitations.
 
 ## Describing fields: the functor `Field`
 
@@ -221,6 +221,44 @@
 
 You just need to apply the `Exists` and `SuchThat` constructors every time there is an existential or constraint, respectively. However, since the additional information required by those types is implicitly added by the compiler, you do not need to write anything else.
 
+## Atoms for families: `Eval`
+
+If a field contains a type family application, it can be represented by
+defunctionalization. For example:
+
+```haskell
+type family F a
+
+data T a = C (F a)
+```
+
+`F` can be defunctionalized as follows, using `Fcf.Eval` from
+[`first-class-families`](https://hackage.haskell.org/package/first-class-families).
+
+```haskell
+data DF a
+type Fcf.Eval (DF a) = F a
+```
+
+All type family applications can thus be rewritten as the application of one
+common `Fcf.Eval` to a matchable application. This can then be represented by
+one `Atom` constructor, also named `Eval`:
+
+```haskell
+instance GenericK T where
+  type RepK T = Field (Eval (Kon DF :@: Var0))
+
+  fromK (C x) = Field x
+  toK (Field x) = C x
+```
+
+`kind-generics-th` can generate `GenericK` instances for such types involving
+type families. It also takes care of defunctionalizing type families as needed,
+following a more sophisticated approach than described above, that avoids
+declaring lots of artificial data types. For more details, see
+[`fcf-family`](https://hackage.haskell.org/package/fcf-family)
+and the documentation of `kind-generics-th`.
+
 ## Implementing a generic operation with `kind-generics`
 
 The last stop in our journey through `kind-generics` is being able to implement a generic operation. At this point we assume that the reader is comfortable with the definition of generic operations using `GHC.Generics`, so only the differences with that style are pointed out.
@@ -266,7 +304,7 @@
 
 ```haskell
 class GShow (f :: LoT k -> *) where
-  type ReqsShow f (x :: LoT k) :: Constraint
+  type family ReqsShow f (x :: LoT k) :: Constraint
   gshow :: ReqsShow f x => f x -> String
 
 gshow' :: forall t. (GenericK t LoT0
diff --git a/kind-generics.cabal b/kind-generics.cabal
--- a/kind-generics.cabal
+++ b/kind-generics.cabal
@@ -1,6 +1,6 @@
 cabal-version:       >=1.10
 name:                kind-generics
-version:             0.4.1.4
+version:             0.5.0.0
 synopsis:            Generic programming in GHC style for arbitrary kinds and GADTs.
 description:         This package provides functionality to extend the data type generic programming functionality in GHC to classes of arbitrary kind, and constructors featuring constraints and existentials, as usually found in GADTs.
 -- bug-reports:
@@ -22,7 +22,9 @@
                        Generics.Kind.Examples
   -- other-modules:
   -- other-extensions:
-  build-depends:       base >= 4.12 && < 5, kind-apply >= 0.3
+  build-depends:       base >= 4.12 && < 5
+                     , kind-apply >= 0.4 && < 0.5
+                     , first-class-families >= 0.8 && < 0.9
   hs-source-dirs:      src
   default-language:    Haskell2010
   ghc-options:         -Wall
diff --git a/src/Generics/Kind.hs b/src/Generics/Kind.hs
--- a/src/Generics/Kind.hs
+++ b/src/Generics/Kind.hs
@@ -6,6 +6,7 @@
 {-# language FlexibleContexts          #-}
 {-# language FlexibleInstances         #-}
 {-# language GADTs                     #-}
+{-# language GeneralizedNewtypeDeriving #-}
 {-# language MultiParamTypeClasses     #-}
 {-# language PolyKinds                 #-}
 {-# language QuantifiedConstraints     #-}
@@ -61,6 +62,10 @@
   -- and https://ghc.haskell.org/trac/ghc/ticket/14917
   -- are implemented, we are restricted to the Type kind
   Field :: { unField :: Interpret t x } -> Field t x
+deriving instance Eq (Interpret t x) => Eq (Field t x)
+deriving instance Ord (Interpret t x) => Ord (Field t x)
+deriving instance Semigroup (Interpret t x) => Semigroup (Field t x)
+deriving instance Monoid (Interpret t x) => Monoid (Field t x)
 deriving instance Show (Interpret t x) => Show (Field t x)
 
 -- | Constraints: used to represent constraints in a constructor.
@@ -72,6 +77,8 @@
 -- >   type RepK Showable = (Show :$: a) :=>: (Field Var0)
 data (:=>:) (c :: Atom d Constraint) (f :: LoT d -> Type) (x :: LoT d) where
   SuchThat :: Interpret c x => f x -> (c :=>: f) x
+deriving instance (Interpret c x => Eq (f x)) => Eq ((c :=>: f) x)
+deriving instance (Interpret c x => Ord (f x)) => Ord ((c :=>: f) x)
 deriving instance (Interpret c x => Show (f x)) => Show ((c :=>: f) x)
 
 -- | Existentials: a representation of the form @E f@ describes
@@ -98,7 +105,7 @@
 -- > instance GenericK (Either a)
 -- > instance GenericK (Either a b)
 class GenericK (f :: k) where
-  type RepK f :: LoT k -> Type
+  type family RepK f :: LoT k -> Type
 
   -- | Convert the data type to its representation.
   fromK :: f :@@: x -> RepK f x
diff --git a/src/Generics/Kind/Examples.hs b/src/Generics/Kind/Examples.hs
--- a/src/Generics/Kind/Examples.hs
+++ b/src/Generics/Kind/Examples.hs
@@ -18,6 +18,7 @@
 import           GHC.TypeLits
 import           Type.Reflection (Typeable)
 
+import qualified Fcf.Core as Fcf
 import           Generics.Kind
 
 -- Obtained from Generic
@@ -242,3 +243,26 @@
   fromK = undefined
   toK   = undefined
 -}
+
+-- Type families
+
+-- HKD pattern, defunctionalized variant
+newtype Hkd f a = Hkd (Fcf.Eval (f a))
+
+-- Simplified encoding compared to kind-generics-th.
+-- Fcf.Eval in Hkd could be any other type family, so a general
+-- implementation would have to defunctionalize it.
+instance GenericK Hkd where
+  type RepK Hkd = Field (Eval (Var0 :@: Var1))
+  fromK (Hkd x) = Field x
+  toK (Field x) = Hkd x
+
+instance GenericK (Hkd f) where
+  type RepK (Hkd f) = Field (Eval (Kon f :@: Var0))
+  fromK (Hkd x) = Field x
+  toK (Field x) = Hkd x
+
+instance GenericK (Hkd f a) where
+  type RepK (Hkd f a) = Field (Kon (Fcf.Eval (f a)))
+  fromK (Hkd x) = Field x
+  toK (Field x) = Hkd x