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.1.0
+version:             0.3.2.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:
diff --git a/src/Data/PolyKinded.hs b/src/Data/PolyKinded.hs
--- a/src/Data/PolyKinded.hs
+++ b/src/Data/PolyKinded.hs
@@ -7,6 +7,7 @@
 {-# language PatternSynonyms #-}
 {-# language UndecidableInstances   #-}
 {-# language FlexibleContexts       #-}
+{-# language FlexibleInstances      #-}
 {-# language ScopedTypeVariables    #-}
 {-# language MultiParamTypeClasses  #-}
 {-# language FunctionalDependencies #-}
@@ -14,6 +15,7 @@
 module Data.PolyKinded (
   -- * Lists of types and application
   LoT(..), (:@@:), LoT1, LoT2
+, HeadLoT, TailLoT, SpineLoT
   -- ** Singleton for list of types
 , SLoT(..), SForLoT(..), Proxy(..)
   -- * Splitting types
@@ -39,18 +41,43 @@
 -- >>> :kind! Either :@@: (Int :&&: Bool :&&: LoT0)
 -- Either Int Bool :: *
 type family (f :: k) :@@: (tys :: LoT k) :: * where
-  f :@@: 'LoT0        = f
-  f :@@: (a ':&&: as) = f a :@@: as
+  f :@@: _  = f
+  f :@@: as = f (HeadLoT as) :@@: (TailLoT as)
 
+-- | Head of a non-empty list of types.
+--
+-- >>> :kind! HeadLoT (Int :&&: LoT0)
+-- Int :: *
+type family HeadLoT (tys :: LoT (k -> k')) :: k where
+  HeadLoT (a :&&: _) = a
+
+-- | Tail of a non-empty list of types.
+--
+-- >>> :kind! TailLoT (Int :&&: Bool :&&: LoT0)
+-- Bool :&&: LoT0 :: LoT (Type -> Type)
+type family TailLoT (tys :: LoT (k -> k')) :: LoT k' where
+  TailLoT (_ :&&: as) = as
+
+-- | Construct the spine of a list of types whose length is known.
+--
+-- It can be useful to introduce unification variables for lists of types which
+-- will be fully instantiated during constraint resolution.
+-- 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 (*)) = LoT0
+
 data SLoT (l :: LoT k) where
   SLoT0 :: SLoT LoT0
   SLoTA :: Proxy t -> SLoT ts -> SLoT (t :&&: ts)
 
 class SForLoT (l :: LoT k) where
   slot :: SLoT l
-instance SForLoT LoT0 where
+instance (l ~ LoT0) => SForLoT (l :: LoT (*)) where
   slot = SLoT0
-instance SForLoT ts => SForLoT (t :&&: ts) where
+instance (l ~ (t :&&: ts), SForLoT ts) => SForLoT (l :: LoT (k -> k')) where
   slot = SLoTA Proxy slot
 
 -- | Split a type @t@ until the constructor @f@ is found.
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
@@ -47,8 +47,8 @@
 type a :~~: b = 'Kon (~~) ':@: a ':@: b
 
 type family InterpretVar (t :: TyVar d k) (tys :: LoT d) :: k where
-  InterpretVar 'VZ     (t ':&&: ts) = t
-  InterpretVar ('VS v) (t ':&&: ts) = InterpretVar v ts
+  InterpretVar 'VZ     tys = HeadLoT tys
+  InterpretVar ('VS v) tys = InterpretVar v (TailLoT tys)
 
 type family Interpret (t :: Atom d k) (tys :: LoT d) :: k where
   Interpret ('Var v)     tys = InterpretVar v tys