diff --git a/kind-apply.cabal b/kind-apply.cabal
--- a/kind-apply.cabal
+++ b/kind-apply.cabal
@@ -1,6 +1,6 @@
 cabal-version:       >=1.10
 name:                kind-apply
-version:             0.3.2.1
+version:             0.4.0.0
 synopsis:            Utilities to work with lists of types
 description:         This packages reifies the concept of list of types, and application of those to list constructors.
 -- bug-reports:
@@ -24,6 +24,7 @@
   -- other-modules:
   -- other-extensions:
   build-depends:       base >=4.12 && <5
+                     , first-class-families >= 0.8 && < 0.9
   hs-source-dirs:      src
   default-language:    Haskell2010
   ghc-options:         -Wall
diff --git a/src/Data/PolyKinded.hs b/src/Data/PolyKinded.hs
--- a/src/Data/PolyKinded.hs
+++ b/src/Data/PolyKinded.hs
@@ -1,13 +1,13 @@
-{-# language ConstraintKinds       #-}
-{-# language FlexibleContexts      #-}
-{-# language FlexibleInstances     #-}
-{-# language GADTs                 #-}
-{-# language MultiParamTypeClasses #-}
-{-# language ScopedTypeVariables   #-}
-{-# language TypeFamilies          #-}
-{-# language TypeInType            #-}
-{-# language TypeOperators         #-}
-{-# language UndecidableInstances  #-}
+{-# language ConstraintKinds        #-}
+{-# language FlexibleContexts       #-}
+{-# language FlexibleInstances      #-}
+{-# language GADTs                  #-}
+{-# language MultiParamTypeClasses  #-}
+{-# language ScopedTypeVariables    #-}
+{-# language TypeFamilyDependencies #-}
+{-# language TypeInType             #-}
+{-# language TypeOperators          #-}
+{-# language UndecidableInstances   #-}
 -- | Representation of types as constructor + list of types.
 module Data.PolyKinded (
   -- * Lists of types and application
@@ -65,9 +65,9 @@
 -- A constraint @p ~ SpineLoT p@ will thus instantiate the spine of @p@.
 --
 -- On concrete lists, this is the identity function.
-type family SpineLoT (ts :: LoT k) :: LoT k where
-  SpineLoT (ts :: LoT (k -> k')) = HeadLoT ts ':&&: SpineLoT (TailLoT ts)
-  SpineLoT (ts :: LoT Type)      = 'LoT0
+type family SpineLoT (tys :: LoT k) = (tys' :: LoT k) | tys' -> tys where
+  SpineLoT (a ':&&: as) = a ':&&: SpineLoT as
+  SpineLoT 'LoT0        = 'LoT0
 
 data SLoT (l :: LoT k) where
   SLoT0 :: SLoT 'LoT0
diff --git a/src/Data/PolyKinded/Atom.hs b/src/Data/PolyKinded/Atom.hs
--- a/src/Data/PolyKinded/Atom.hs
+++ b/src/Data/PolyKinded/Atom.hs
@@ -29,6 +29,7 @@
 import           Data.Kind
 import           Data.PolyKinded
 import           GHC.Exts
+import           Fcf.Core (Exp, Eval)
 
 -- | Well-scoped de Bruijn representation of type variables.
 -- @TyVar d@ represents all the possible type variables which
@@ -59,6 +60,45 @@
 --
 -- >>> :kind Kon [] :@: Var0 -- the type [a] for unknown a
 -- Kon [] :@: Var0 :: Atom (* -> xs) *
+--
+-- === __Representation of type families__
+--
+-- Type families are represented using
+-- <https://hackage.haskell.org/package/first-class-families first-class-families>.
+--
+-- For example, the type-level @n + m :: 'GHC.TypeNats.Nat'@-- may expand to the following--
+--
+-- @
+-- n + m         -- using @('GHC.TypeNats.+')@ from "GHC.TypeNats"
+-- ~
+-- 'Fcf.Core.Eval' (n 'Fcf.Data.Nat.+' m)  -- using 'Fcf.Core.Eval' from "Fcf.Core" and @('Fcf.Data.Nat.+')@ from "Fcf.Data.Nat"
+-- @
+--
+-- which may be encoded as the following 'Atom' (using 'Var0' for @n@ and 'Var1' for @m@):
+--
+-- @
+-- 'Data.PolyKinded.Atom.Eval' (('Kon' ('Fcf.Data.Nat.+') ':@:' 'Var0') ':@:' 'Var1')  -- 'Data.PolyKinded.Atom.Eval' as 'Atom'\'s constructor
+--   :: 'Atom' (Nat -> Nat -> Type) Nat
+-- @
+--
+-- <https://hackage.haskell.org/package/kind-generics kind-generics>
+-- uses a different, more systematic encoding of type families for @GenericK@ instances;
+-- see <https://hackage.haskell.org/package/fcf-family fcf-family> for more details.
+-- For example, @n + m@ is instead expanded to the following:
+--
+-- @
+-- n + m
+-- ~
+-- 'Fcf.Core.Eval' ('Fcf.Family.NDFamily' ('Fcf.Family.MkName' "base" \"GHC.TypeNats\" \"+\") 'Fcf.Family.P0' \'(n, \'(m, \'())))
+-- @
+--
+-- which gets encoded as the following 'Atom':
+--
+-- @
+-- 'Data.PolyKinded.Atom.Eval' ('Kon' ('Fcf.Family.NDFamily' ('Fcf.Family.MkName' "base" \"GHC.TypeNats\" \"+\") 'Fcf.Family.P0')
+--         ':@:' (('Kon' \'(,) ':@:' 'Var0') ':@:' (('Kon' \'(,) ':@:' 'Var1') ':@:' 'Kon' \'())))
+--   :: 'Atom' (Nat -> Nat -> Type) Nat
+-- @
 data Atom (d :: Type) (k :: TYPE r) where
   -- | Represents a type variable.
   Var :: TyVar d k -> Atom d k
@@ -72,6 +112,8 @@
   ForAll  :: Atom (d1 -> d) Type -> Atom d Type
   -- | Represents constraint requirement, the "thick arrow" @=>@.
   (:=>>:) :: Atom d Constraint -> Atom d Type -> Atom d Type
+  -- | Represents a type family application.
+  Eval :: Atom d (Exp k) -> Atom d k
 
 -- | Represents an applied constructor.
 -- Instead of @Kon [] :@: Var0$ you can write @[] :$: Var0$.
@@ -108,6 +150,7 @@
   Interpret (c ':&: d)   tys = (Interpret c tys, Interpret d tys)
   Interpret ('ForAll f)  tys = ForAllI f tys
   Interpret (c ':=>>: f) tys = SuchThatI c f tys
+  Interpret ('Eval f)    tys = Eval (Interpret f tys)
 
 -- | Auxiliary type for interpretation of the 'ForAll' atom.
 -- Required because a type family like 'Interpret' cannot return
@@ -132,9 +175,9 @@
 -- Required because a type family like 'Interpret' cannot return
 -- a type with constraints.
 newtype SuchThatI (c :: Atom d Constraint) (f :: Atom d Type) (tys :: LoT d) where
-  SuchThatI :: (Interpret c tys => Interpret f tys) -> SuchThatI c f tys
+  SuchThatI :: { unSuchThatI :: Interpret c tys => Interpret f tys } -> SuchThatI c f tys
 
--- | Interprets a list of 'Atoms' representing constraints
+-- | Interprets a list of 'Atom' representing constraints
 -- into the actual constraints. This is a specialization of
 -- 'Interpret' for the case of constraints.
 --