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.0.0
+version:             0.3.1.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
@@ -14,10 +14,14 @@
 module Data.PolyKinded (
   -- * Lists of types and application
   LoT(..), (:@@:), LoT1, LoT2
+  -- ** Singleton for list of types
+, SLoT(..), SForLoT(..), Proxy(..)
   -- * Splitting types
 , SplitF, Nat(..), TyEnv(..), SplitN
 ) where
 
+import Data.Proxy
+
 infixr 5 :&&:
 -- | @LoT k@ represents a list of types which can be applied
 -- to a data type of kind @k@.
@@ -37,6 +41,17 @@
 type family (f :: k) :@@: (tys :: LoT k) :: * where
   f :@@: 'LoT0        = f
   f :@@: (a ':&&: as) = f a :@@: as
+
+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
+  slot = SLoT0
+instance SForLoT ts => SForLoT (t :&&: ts) 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
@@ -7,6 +7,9 @@
 {-# language RankNTypes      #-}
 {-# language AllowAmbiguousTypes  #-}
 {-# language UndecidableInstances #-}
+{-# language ScopedTypeVariables  #-}
+{-# language TypeApplications     #-}
+{-# language ImpredicativeTypes   #-}
 module Data.PolyKinded.Atom where
 
 import Data.Kind
@@ -43,17 +46,29 @@
 type a :~:  b = 'Kon (~) ':@: a ':@: b
 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
+
 type family Interpret (t :: Atom d k) (tys :: LoT d) :: k where
-  Interpret ('Var 'VZ)     (t ':&&: ts) = t
-  Interpret ('Var ('VS v)) (t ':&&: ts) = Interpret ('Var v) ts
-  Interpret ('Kon t)       tys = t
-  Interpret (f ':@: x)     tys = (Interpret f tys) (Interpret x tys)
-  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 ('Var v)     tys = InterpretVar v tys
+  Interpret ('Kon t)     tys = t
+  Interpret (f ':@: x)   tys = (Interpret f tys) (Interpret x tys)
+  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
 
 newtype ForAllI (f :: Atom (d1 -> d) (*)) (tys :: LoT d) where
   ForAllI :: (forall t. Interpret f (t ':&&: tys)) -> ForAllI f tys
+
+newtype WrappedI (f :: Atom d (*)) (tys :: LoT d) =
+  WrapI { unwrapI :: Interpret f tys }
+
+toWrappedI :: forall f tys t. ForAllI f tys -> WrappedI f (t ':&&: tys)
+toWrappedI (ForAllI x) = WrapI (x @t)
+
+fromWrappedI :: forall f tys. (forall t. WrappedI f (t ':&&: tys)) -> ForAllI f tys
+fromWrappedI = coerce @(forall t. WrappedI f (t ':&&: tys))
 
 newtype SuchThatI (c :: Atom d Constraint) (f :: Atom d (*)) (tys :: LoT d) where
   SuchThatI :: (Interpret c tys => Interpret f tys) -> SuchThatI c f tys