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.2.0
+version:             0.2.1.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 gound in GADTs.
 -- bug-reports:
@@ -22,7 +22,7 @@
                        Generics.Kind.Examples
   -- other-modules:
   -- other-extensions:
-  build-depends:       base >=4.12 && <5, kind-apply
+  build-depends:       base >=4.12 && <5, kind-apply >= 0.2
   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
@@ -22,12 +22,13 @@
 , module Data.PolyKinded.Atom
   -- * Generic representation types
 , (:+:)(..), (:*:)(..), U1(..), M1(..)
-, F(..), (:=>:)(..), E(..), ERefl(..)
+, F(..), (:=>:)(..), E(..)
   -- * Generic type classes
 , GenericK(..)
 , GenericF, fromF, toF
 , GenericN, fromN, toN
-, GenericS, fromS, toS
+  -- * Getting more instances almost for free
+, fromRepK, toRepK, SubstRep
   -- * Bridging with "GHC.Generics"
 , Conv(..)
 ) where
@@ -57,6 +58,7 @@
 -- >   type RepK Showable = (Show :$: a) :=>: (F V0)
 data (:=>:) (c :: Atom d Constraint) (f :: LoT d -> *) (x :: LoT d) where
   C :: Ty c x => f x -> (c :=>: f) x
+deriving instance (Ty c x => Show (f x)) => Show ((c :=>: f) x)
 
 -- | Existentials: a representation of the form @E f@ describes
 -- a constructor whose inner type is represented by @f@, and where
@@ -70,18 +72,7 @@
 data E (f :: LoT (k -> d) -> *) (x :: LoT d) where
   E :: forall (t :: k) d (f :: LoT (k -> d) -> *) (x :: LoT d)
      . f (t ':&&: x) -> E f x
-
--- | Existentials with reflection: similar to 'E',
---   but in addition we remember the type of the existential variable.
---
--- > data Exists where
--- >  E :: Typeable t => t -> Exists
--- >
--- > instance GenericK Exists LoT0 where
--- >   type RepK Exists = ERefl (F V0)
-data ERefl (f :: LoT (k -> d) -> *) (x :: LoT d) where
-  ERefl :: forall (t :: k) d (f :: LoT (k -> d) -> *) (x :: LoT d)
-         . Typeable t => f (t ':&&: x) -> ERefl f x
+deriving instance (forall t. Show (f (t ':&&: x))) => Show (E f x)
 
 -- THE TYPE CLASS
 
@@ -121,17 +112,61 @@
 toN :: forall n t f x. GenericN n t f x => RepK f x -> t
 toN = toK @_ @f
 
--- | @GenericS t f x@ states that the ground type @t@ is split by
--- default as the constructor @f@ and a list of types @x$, and that
--- a 'GenericK' instance exists for that constructor.
---
--- This constraint provides an external interface similar to that
--- provided by 'Generic' in "GHC.Generics".
-type GenericS t f x = (Split t f x, GenericK f x)
-fromS :: forall t f x. GenericS t f x => t -> RepK f x
-fromS = fromF @f
-toS :: forall t f x. GenericS t f x => RepK f x -> t
-toS = toF @f
+-- CONVERSION BETWEEN FEWER AND MORE ARGUMENTS
+
+fromRepK :: forall f x xs. (GenericK f (x ':&&: xs), SubstRep' (RepK f) x xs)
+         => f x :@@: xs -> SubstRep (RepK f) x xs
+fromRepK = substRep . fromK @_ @f @(x ':&&: xs)
+
+toRepK :: forall f x xs. (GenericK f (x ':&&: xs), SubstRep' (RepK f) x xs)
+       => SubstRep (RepK f) x xs -> f x :@@: xs
+toRepK = toK @_ @f @(x ':&&: xs) . unsubstRep
+
+class SubstRep' (f :: LoT (t -> k) -> *) (x :: t) (xs :: LoT k) where
+  type family SubstRep f x :: LoT k -> *
+  substRep   :: f (x ':&&: xs) -> SubstRep f x xs
+  unsubstRep :: SubstRep f x xs -> f (x ':&&: xs)
+
+instance SubstRep' U1 x xs where
+  type SubstRep U1 x = U1
+  substRep   U1 = U1
+  unsubstRep U1 = U1
+
+instance (SubstRep' f x xs, SubstRep' g x xs) => SubstRep' (f :+: g) x xs where
+  type SubstRep (f :+: g)  x = (SubstRep f x) :+: (SubstRep g x)
+  substRep   (L1 x) = L1 (substRep   x)
+  substRep   (R1 x) = R1 (substRep   x)
+  unsubstRep (L1 x) = L1 (unsubstRep x)
+  unsubstRep (R1 x) = R1 (unsubstRep x)
+
+instance (SubstRep' f x xs, SubstRep' g x xs) => SubstRep' (f :*: g) x xs where
+  type SubstRep (f :*: g) x = (SubstRep f x) :*: (SubstRep g x)
+  substRep   (x :*: y) = substRep   x :*: substRep   y
+  unsubstRep (x :*: y) = unsubstRep x :*: unsubstRep y
+
+instance SubstRep' f x xs => SubstRep' (M1 i c f) x xs where
+  type SubstRep (M1 i c f) x = M1 i c (SubstRep f x)
+  substRep   (M1 x) = M1 (substRep   x)
+  unsubstRep (M1 x) = M1 (unsubstRep x)
+
+instance (Ty (SubstAtom c x) xs, Ty c (x ':&&: xs), SubstRep' f x xs)
+         => SubstRep' (c :=>: f) x xs where
+  type SubstRep (c :=>: f) x = (SubstAtom c x) :=>: (SubstRep f x)
+  substRep   (C x) = C (substRep   x)
+  unsubstRep (C x) = C (unsubstRep x)
+
+instance (Ty (SubstAtom t x) xs ~ Ty t (x ':&&: xs))
+         => SubstRep' (F t) x xs where
+  type SubstRep (F t) x = F (SubstAtom t x)
+  substRep   (F x) = F x
+  unsubstRep (F x) = F x
+
+type family SubstAtom (f :: Atom (t -> k) d) (x :: t) :: Atom k d where
+  SubstAtom ('Var 'VZ)     x = 'Kon x
+  SubstAtom ('Var ('VS v)) x = 'Var v
+  SubstAtom ('Kon t)       x = 'Kon t
+  SubstAtom (t1 ':@: t2)   x = (SubstAtom t1 x) ':@: (SubstAtom t2 x)
+  SubstAtom (t1 ':&: t2)   x = (SubstAtom t1 x) ':&: (SubstAtom t2 x)
 
 -- CONVERSION BETWEEN GHC.GENERICS AND KIND-GENERICS
 
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
@@ -7,36 +7,75 @@
 {-# language GADTs                 #-}
 {-# language DeriveGeneric         #-}
 {-# language QuantifiedConstraints #-}
+{-# language UndecidableInstances  #-}
 module Generics.Kind.Examples where
 
 import Data.PolyKinded.Functor
 import GHC.Generics (Generic)
+import GHC.TypeLits
 import Type.Reflection
 
 import Generics.Kind
 
 -- Obtained from Generic
 
-instance Split (Maybe a) Maybe (a ':&&: 'LoT0)
 instance GenericK Maybe (a ':&&: 'LoT0) where
   type RepK Maybe = U1 :+: F V0
+instance GenericK (Maybe a) LoT0 where
+  type RepK (Maybe a) = SubstRep (RepK Maybe) a
+  fromK = fromRepK
+  toK   = toRepK
 
+instance GenericK Either (a ':&&: b ':&&: LoT0) where
+  type RepK Either = F V0 :+: F V1
+instance GenericK (Either a) (b ':&&: LoT0) where
+  type RepK (Either a) = SubstRep (RepK Either) a
+  fromK = fromRepK
+  toK   = toRepK
+instance GenericK (Either a b) LoT0 where
+  type RepK (Either a b) = SubstRep (RepK (Either a)) b
+  fromK = fromRepK
+  toK   = toRepK
+
 -- From the docs
 
 data Tree a = Branch (Tree a) (Tree a) | Leaf a
             deriving Generic
 
-instance Split (Tree a) Tree (a ':&&: 'LoT0)
 instance GenericK Tree (a ':&&: 'LoT0) where
   type RepK Tree = F (Tree :$: V0) :*: F (Tree :$: V0) :+: F V0
+instance GenericK (Tree a) LoT0 where
+  type RepK (Tree a) = SubstRep (RepK Tree) a
+  fromK = fromRepK
+  toK   = toRepK
 
+-- Data family
+
+data family HappyFamily t
+data instance HappyFamily (Maybe a) = HFM Bool
+data instance HappyFamily [a]       = HFL a
+
+instance GenericK HappyFamily (a ':&&: 'LoT0) where
+  type RepK HappyFamily = TypeError (Text "Cannot describe this family uniformly")
+  fromK = undefined
+  toK   = undefined
+
+instance GenericK (HappyFamily (Maybe a)) 'LoT0 where
+  type RepK (HappyFamily (Maybe a)) = F (Kon Bool)
+  fromK (HFM x) = F   x
+  toK   (F   x) = HFM x
+
+instance GenericK (HappyFamily [a]) 'LoT0 where
+  type RepK (HappyFamily [a]) = F (Kon a)
+  fromK (HFL x) = F   x
+  toK   (F   x) = HFL x
+
 -- Hand-written instance
 
 data WeirdTree a where
   WeirdBranch :: WeirdTree a -> WeirdTree a -> WeirdTree a 
   WeirdLeaf   :: Show a => t -> a -> WeirdTree a
 
-instance Split (WeirdTree a) WeirdTree (a ':&&: 'LoT0)
 instance GenericK WeirdTree (a ':&&: 'LoT0) where
   type RepK WeirdTree
     = F (WeirdTree :$: V0) :*: F (WeirdTree :$: V0)
@@ -52,16 +91,26 @@
 
 data WeirdTreeR a where
   WeirdBranchR :: WeirdTreeR a -> WeirdTreeR a -> WeirdTreeR a 
-  WeirdLeafR   :: (Show a, Typeable t, Eq t) => t -> a -> WeirdTreeR a
+  WeirdLeafR   :: (Show a, Eq t, Typeable t) => t -> a -> WeirdTreeR a
 
-instance Split (WeirdTreeR a) WeirdTreeR (a ':&&: 'LoT0)
 instance GenericK WeirdTreeR (a ':&&: 'LoT0) where
   type RepK WeirdTreeR
     = F (WeirdTreeR :$: V0) :*: F (WeirdTreeR :$: V0)
-      :+: ERefl ((Show :$: V1) :=>: ((Eq :$: V0) :=>: (F V0 :*: F V1)))
+      :+: E (((Show :$: V1) :&: (Eq :$: V0) :&: (Typeable :$: V0)) :=>: (F V0 :*: F V1))
 
-  fromK (WeirdBranchR l r) = L1 $                 F l :*: F r
-  fromK (WeirdLeafR   a x) = R1 $ ERefl $ C $ C $ F a :*: F x
+  fromK (WeirdBranchR l r) = L1 $         F l :*: F r
+  fromK (WeirdLeafR   a x) = R1 $ E $ C $ F a :*: F x
 
   toK (L1 (F l :*: F r)) = WeirdBranchR l r
-  toK (R1 (ERefl (C (C (F a :*: F x))))) = WeirdLeafR a x
+  toK (R1 (E (C (F a :*: F x)))) = WeirdLeafR a x
+
+instance GenericK (WeirdTreeR a) 'LoT0 where
+  type RepK (WeirdTreeR a)
+    = F (Kon (WeirdTreeR a)) :*: F (Kon (WeirdTreeR a))
+    :+: E ((Kon (Show a) :&: (Eq :$: V0) :&: (Typeable :$: V0)) :=>: ((F V0 :*: F (Kon a))))
+
+  fromK (WeirdBranchR l r) = L1 $         F l :*: F r
+  fromK (WeirdLeafR   a x) = R1 $ E $ C $ F a :*: F x
+
+  toK (L1 (F l :*: F r)) = WeirdBranchR l r
+  toK (R1 (E (C (F a :*: F x)))) = WeirdLeafR a x