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.1
+version:             0.4.1.2
 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:
diff --git a/src/Generics/Kind.hs b/src/Generics/Kind.hs
--- a/src/Generics/Kind.hs
+++ b/src/Generics/Kind.hs
@@ -15,6 +15,7 @@
 {-# language TypeFamilies              #-}
 {-# language TypeOperators             #-}
 {-# language UndecidableInstances      #-}
+{-# language UndecidableSuperClasses   #-}
 -- | Main module of @kind-generics@. Please refer to the @README@ file for documentation on how to use this package.
 module Generics.Kind (
   module Data.PolyKinded
@@ -45,11 +46,11 @@
 --
 -- > instance GenericK [] (a :&&: LoT0) where
 -- >   type RepK [] = Field Var0 :*: Field ([] :$: Var0)
-newtype Field (t :: Atom d (*)) (x :: LoT d) where
-  -- Field :: forall (r :: RuntimeRep) (k :: TYPE r) (d :: *). Atom d k -> LoT d -> * where
+newtype Field (t :: Atom d Type) (x :: LoT d) where
+  -- Field :: forall (r :: RuntimeRep) (k :: TYPE r) (d :: Type). Atom d k -> LoT d -> Type where
   -- Until https://github.com/ghc-proposals/ghc-proposals/blob/master/proposals/0013-unlifted-newtypes.rst
   -- and https://ghc.haskell.org/trac/ghc/ticket/14917
-  -- are implemented, we are restricted to the (*) kind
+  -- are implemented, we are restricted to the Type kind
   Field :: { unField :: Interpret t x } -> Field t x
 deriving instance Show (Interpret t x) => Show (Field t x)
 
@@ -60,7 +61,7 @@
 -- >
 -- > instance GenericK Showable (a :&&: LoT0) where
 -- >   type RepK Showable = (Show :$: a) :=>: (Field Var0)
-data (:=>:) (c :: Atom d Constraint) (f :: LoT d -> *) (x :: LoT d) where
+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 => Show (f x)) => Show ((c :=>: f) x)
 
@@ -72,9 +73,9 @@
 -- >  E :: t -> Exists
 -- >
 -- > instance GenericK E LoT0 where
--- >   type RepK E = Exists (*) (Field Var0)
-data Exists k (f :: LoT (k -> d) -> *) (x :: LoT d) where
-  Exists :: forall k (t :: k) d (f :: LoT (k -> d) -> *) (x :: LoT d)
+-- >   type RepK E = Exists Type (Field Var0)
+data Exists k (f :: LoT (k -> d) -> Type) (x :: LoT d) where
+  Exists :: forall k (t :: k) d (f :: LoT (k -> d) -> Type) (x :: LoT d)
           .{ unExists :: f (t ':&&: x) } -> Exists k f x
 deriving instance (forall t. Show (f (t ':&&: x))) => Show (Exists k f x)
 
@@ -88,7 +89,7 @@
 -- > instance GenericK (Either a)
 -- > instance GenericK (Either a b)
 class GenericK (f :: k) where
-  type RepK f :: LoT k -> *
+  type RepK f :: LoT k -> Type
 
   -- | Convert the data type to its representation.
   fromK :: f :@@: x -> RepK f x
@@ -126,8 +127,8 @@
        => 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 -> *
+class SubstRep' (f :: LoT (t -> k) -> Type) (x :: t) (xs :: LoT k) where
+  type family SubstRep f x :: LoT k -> Type
   substRep   :: f (x ':&&: xs) -> SubstRep f x xs
   unsubstRep :: SubstRep f x xs -> f (x ':&&: xs)
 
@@ -153,12 +154,25 @@
   substRep   (M1 x) = M1 (substRep   x)
   unsubstRep (M1 x) = M1 (unsubstRep x)
 
-instance (Interpret (SubstAtom c x) xs, Interpret c (x ':&&: xs), SubstRep' f x xs)
+-- The context says that @Interpret (SubstAtom c x) xs@
+-- and @Interpret c (x ':&&: xs)@ are equivalent.
+-- But because @Interpret@ is a type family, and the right-hand side of
+-- a quantified constraint must be a class, we must use "class synonyms"
+-- @InterpretCons@ and @InterpretSubst@.
+instance ( Interpret (SubstAtom c x) xs => InterpretCons c x xs
+         , Interpret c (x ':&&: xs) => InterpretSubst 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   (SuchThat x) = SuchThat (substRep   x)
-  unsubstRep (SuchThat x) = SuchThat (unsubstRep x)
+  substRep   (SuchThat x) = SuchThat (substRep   x) :: InterpretSubst c x xs => SubstRep (c :=>: f) x xs
+  unsubstRep (SuchThat x) = SuchThat (unsubstRep x) :: InterpretCons  c x xs => (c :=>: f) (x ':&&: xs)
 
+class    Interpret c (x ':&&: xs) => InterpretCons c x xs
+instance Interpret c (x ':&&: xs) => InterpretCons c x xs
+
+class    Interpret (SubstAtom c x) xs => InterpretSubst c x xs
+instance Interpret (SubstAtom c x) xs => InterpretSubst c x xs
+
 instance (Interpret (SubstAtom t x) xs ~ Interpret t (x ':&&: xs))
          => SubstRep' (Field t) x xs where
   type SubstRep (Field t) x = Field (SubstAtom t x)
@@ -178,7 +192,7 @@
 -- in "GHC.Generics" with a representation using this module.
 -- You are never expected to manipulate this type class directly,
 -- it is part of the deriving mechanism for 'GenericK'.
-class Conv (gg :: * -> *) (kg :: LoT d -> *) (tys :: LoT d) where
+class Conv (gg :: Type -> Type) (kg :: LoT d -> Type) (tys :: LoT d) where
   toGhcGenerics  :: kg tys -> gg a
   toKindGenerics :: gg a -> kg tys
 
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
@@ -13,6 +13,7 @@
 {-# language UndecidableInstances  #-}
 module Generics.Kind.Examples where
 
+import           Data.Kind
 import           GHC.Generics    (Generic)
 import           GHC.TypeLits
 import           Type.Reflection (Typeable)
@@ -81,24 +82,24 @@
 
 -- Hand-written instance
 
-data SimpleIndex :: * -> * -> * where
+data SimpleIndex :: Type -> Type -> Type where
   MkSimpleIndex :: [a] -> SimpleIndex [a] b
 
 instance GenericK SimpleIndex where
   type RepK SimpleIndex
-    = Exists (*) ((Var1 :~: ([] :$: Var0)) :=>: Field ([] :$: Var0))
+    = Exists Type ((Var1 :~: ([] :$: Var0)) :=>: Field ([] :$: Var0))
   fromK (MkSimpleIndex x) = Exists (SuchThat (Field x))
   toK (Exists (SuchThat (Field x))) = MkSimpleIndex x
 
 instance GenericK (SimpleIndex a) where
   type RepK (SimpleIndex a)
-    = Exists (*) (('Kon a :~: ([] :$: Var0)) :=>: Field ([] :$: Var0))
+    = Exists Type (('Kon a :~: ([] :$: Var0)) :=>: Field ([] :$: Var0))
   fromK (MkSimpleIndex x) = Exists (SuchThat (Field x))
   toK (Exists (SuchThat (Field x))) = MkSimpleIndex x
 
 instance GenericK (SimpleIndex a b) where
   type RepK (SimpleIndex a b)
-    = Exists (*) (('Kon a :~: ([] :$: Var0)) :=>: Field ([] :$: Var0))
+    = Exists Type (('Kon a :~: ([] :$: Var0)) :=>: Field ([] :$: Var0))
   fromK (MkSimpleIndex x) = Exists (SuchThat (Field x))
   toK (Exists (SuchThat (Field x))) = MkSimpleIndex x
 
@@ -109,7 +110,7 @@
 instance GenericK WeirdTree where
   type RepK WeirdTree
     = Field (WeirdTree :$: Var0) :*: Field (WeirdTree :$: Var0)
-      :+: Exists (*) ((Show :$: Var1) :=>: (Field Var0 :*: Field Var1))
+      :+: Exists Type ((Show :$: Var1) :=>: (Field Var0 :*: Field Var1))
 
   fromK (WeirdBranch l r) = L1 $                     Field l :*: Field r
   fromK (WeirdLeaf   a x) = R1 $ Exists $ SuchThat $ Field a :*: Field x
@@ -126,8 +127,8 @@
 instance GenericK WeirdTreeR where
   type RepK WeirdTreeR
     = Field (WeirdTreeR :$: Var0) :*: Field (WeirdTreeR :$: Var0)
-      :+: Exists (*) (((Show :$: Var1) ':&: (Eq :$: Var0) ':&: (Typeable :$: Var0))
-                      :=>: (Field Var0 :*: Field Var1))
+      :+: Exists Type (((Show :$: Var1) ':&: (Eq :$: Var0) ':&: (Typeable :$: Var0))
+                       :=>: (Field Var0 :*: Field Var1))
 
   fromK (WeirdBranchR l r) = L1 $                     Field l :*: Field r
   fromK (WeirdLeafR   a x) = R1 $ Exists $ SuchThat $ Field a :*: Field x
@@ -138,8 +139,8 @@
 instance GenericK (WeirdTreeR a) where
   type RepK (WeirdTreeR a)
     = Field ('Kon (WeirdTreeR a)) :*: Field ('Kon (WeirdTreeR a))
-    :+: Exists (*) (('Kon (Show a) ':&: (Eq :$: Var0) ':&: (Typeable :$: Var0))
-                    :=>: (Field Var0 :*: Field ('Kon a)))
+    :+: Exists Type (('Kon (Show a) ':&: (Eq :$: Var0) ':&: (Typeable :$: Var0))
+                     :=>: (Field Var0 :*: Field ('Kon a)))
 
   fromK (WeirdBranchR l r) = L1 $                     Field l :*: Field r
   fromK (WeirdLeafR   a x) = R1 $ Exists $ SuchThat $ Field a :*: Field x
@@ -167,16 +168,16 @@
 -- Weird-kinded types
 
 data T (a :: k) where
-  MkT :: forall (a :: *). Maybe a -> T a
+  MkT :: forall (a :: Type). Maybe a -> T a
 
 {- GHC rewrites this to the following Core
 data T (a :: k) =
   forall (a' :: Type). (k ~ Type, a ~~ a') => MkT (Maybe a')
 -}
 
-instance GenericK (T :: k -> *) where
-  type RepK (T :: k -> *) =
-    Exists (*) (('Kon (k ~ (*)) ':&: (Var0 :~~: Var1)) :=>: Field (Maybe :$: Var0))
+instance GenericK (T :: k -> Type) where
+  type RepK (T :: k -> Type) =
+    Exists Type (('Kon (k ~ Type) ':&: (Var0 :~~: Var1)) :=>: Field (Maybe :$: Var0))
   fromK (MkT x) = Exists (SuchThat (Field x))
   toK (Exists (SuchThat (Field x))) = MkT x
 
@@ -196,13 +197,13 @@
 data P' j (a :: k) where
   P' :: forall k (a :: k). P' k a
 
-instance GenericK (P' j :: k -> *) where
-  type RepK (P' j :: k -> *) = ('Kon k :~: 'Kon j) :=>: U1
+instance GenericK (P' j :: k -> Type) where
+  type RepK (P' j :: k -> Type) = ('Kon k :~: 'Kon j) :=>: U1
   fromK P' = SuchThat U1
   toK (SuchThat U1) = P'
 
-instance GenericK (P' :: * -> k -> *) where
-  type RepK (P' :: * -> k -> *) = ('Kon k :~: Var0) :=>: U1
+instance GenericK (P' :: Type -> k -> Type) where
+  type RepK (P' :: Type -> k -> Type) = ('Kon k :~: Var0) :=>: U1
   fromK P' = SuchThat U1
   toK (SuchThat U1) = P'