diff --git a/ChangeLog.md b/ChangeLog.md
deleted file mode 100644
--- a/ChangeLog.md
+++ /dev/null
@@ -1,29 +0,0 @@
-# Revision history for generics-mrsop
-
-## 2.1.0 -- Jul 2019
-
-- Added datatype `Holes` for representing families annotated with holes.
-- Brought in some monadic attribute grammar combinators
-- Big documentation update on a number of places
-
-## 2.0.0 -- Mar 2019
-
-- `Eq1` and `Show1` are now called `EqHO` and `ShowHO`. This avoids clashing with the
-already existing `Eq1` in `Prelude`. 
-- A number of functions received a `IsNat` constraint.
-- `Generics.MRSOP.Util` is now re-exported by `Generics.MRSOP.Base`.
-- Support for inheritted attributes no longer exists in `Generics.MRSOP.AG`
-- `Fix` is no longer implemented by `AnnFix`. The later now lives in `Generics.MRSOP.AG`
-
-## 1.2.2 -- Sep 2018
-
-- added monadic catamorphism for NP
-- added pattern signature generation for TH
-- require `TestEqualiy` for opaque types singleton
-- Zippers over deep representations
-- Refined `Metadata` handling
-- `Fix` is implemented as `AnnFix`
-
-## 1.0.0.0  -- May 2018
-
-- First version. Released on an unsuspecting world.
diff --git a/README.md b/README.md
deleted file mode 100644
--- a/README.md
+++ /dev/null
@@ -1,8 +0,0 @@
-# generics-mrsop
-
-Generic Programming, with combinators, for Mutually Recursive Families in the
-Sums of Products style.
-
-Check the `Generics.MRSOP.Examples.RoseTreeTH` for a simple quick start,
-or read our [paper](https://icfp18.sigplan.org/event/tyde-2018-sums-of-products-for-mutually-recursive-datatypes), "Sums of Products for Mutually Recursive Datatypes", for a more detailed description.
-
diff --git a/generics-mrsop.cabal b/generics-mrsop.cabal
--- a/generics-mrsop.cabal
+++ b/generics-mrsop.cabal
@@ -1,84 +1,56 @@
-name:                generics-mrsop
-version:             2.1.0
-
-synopsis:            Generic Programming with Mutually Recursive Sums of Products.
-
-description:
-  A library that supports generic programming for mutually
-  recursive families in the sum-of-products style.
-  .
-  A couple usage examples can be found under "Generics.MRSOP.Examples"
-  .
-
-license:             MIT
-license-file:        LICENSE
-author:              Victor Miraldo and Alejandro Serrano
-maintainer:          v.cacciarimiraldo@gmail.com
--- copyright:           
-
-category:            Generics
-build-type:          Simple
-
-extra-source-files:  ChangeLog.md, README.md
-cabal-version:       1.24
-tested-with:         GHC == 8.2.2, GHC == 8.4.2
-
-
-library
-  -- Modules exported by the library.
-  exposed-modules: 
-    Generics.MRSOP.Base.NS,
-    Generics.MRSOP.Base.NP,
-    Generics.MRSOP.Base.Universe,
-    Generics.MRSOP.Base.Class,
-    Generics.MRSOP.Base.Combinators,
-    Generics.MRSOP.Base.Metadata,
-    Generics.MRSOP.Base,
-    Generics.MRSOP.Opaque,
-    Generics.MRSOP.Util,
-    Generics.MRSOP.Holes
-    Generics.MRSOP.TH,
-    Generics.MRSOP.Zipper,
-    Generics.MRSOP.Zipper.Deep,
-    Generics.MRSOP.Examples.RoseTree,
-    Generics.MRSOP.Examples.RoseTreeTH,
-    Generics.MRSOP.Examples.LambdaAlphaEqTH,
-    Generics.MRSOP.Examples.SimpTH,
-    Generics.MRSOP.AG
-
-  other-extensions: 
-    MultiParamTypeClasses,
-    FlexibleInstances,
-    FlexibleContexts,
-    TypeSynonymInstances,
-    RankNTypes,
-    TypeFamilies,
-    TypeOperators,
-    DataKinds,
-    PolyKinds,
-    GADTs,
-    TypeApplications,
-    ConstraintKinds,
-    FunctionalDependencies,
-    ScopedTypeVariables
+cabal-version: 1.12
 
-  ghc-options: -Wall
+-- This file has been generated from package.yaml by hpack version 0.31.2.
+--
+-- see: https://github.com/sol/hpack
+--
+-- hash: 6e4f3e6671cfaeff58301e7f3a59013225b8995b0e8cb2fbb43c1d48c1158cf0
 
-  build-depends:       base >= 4.9 && <= 5,
-                       containers,
-                       template-haskell,
-                       mtl
-  
-  hs-source-dirs:      src
-  
-  default-language:    Haskell2010
-  
+name:           generics-mrsop
+version:        2.2.0
+synopsis:       Generic Programming with Mutually Recursive Sums of Products.
+description:    A library that supports generic programming for mutually recursive families in the sum-of-products style. . A couple usage examples can be found under "Generics.MRSOP.Examples" .
+category:       Generics
+homepage:       https://github.com/VictorCMiraldo/generics-mrsop#readme
+bug-reports:    https://github.com/VictorCMiraldo/generics-mrsop/issues
+author:         Victor Miraldo and Alejandro Serrano
+maintainer:     Victor Miraldo <v.cacciarimiraldo@gmail.com>
+license:        MIT
+license-file:   LICENSE
+build-type:     Simple
 
 source-repository head
-  type:     git
+  type: git
   location: https://github.com/VictorCMiraldo/generics-mrsop
 
-source-repository this
-  type:     git
-  location: https://github.com/VictorCMiraldo/generics-mrsop
-  tag: v2.1.0
+library
+  exposed-modules:
+      Generics.MRSOP.AG
+      Generics.MRSOP.Base
+      Generics.MRSOP.Base.Class
+      Generics.MRSOP.Base.Combinators
+      Generics.MRSOP.Base.Metadata
+      Generics.MRSOP.Base.NP
+      Generics.MRSOP.Base.NS
+      Generics.MRSOP.Base.Universe
+      Generics.MRSOP.Examples.LambdaAlphaEqTH
+      Generics.MRSOP.Examples.RoseTree
+      Generics.MRSOP.Examples.RoseTreeTH
+      Generics.MRSOP.Examples.SimpTH
+      Generics.MRSOP.Holes
+      Generics.MRSOP.Opaque
+      Generics.MRSOP.TH
+      Generics.MRSOP.Util
+      Generics.MRSOP.Zipper
+  other-modules:
+      Paths_generics_mrsop
+  hs-source-dirs:
+      src/
+  ghc-options: -Wall
+  build-depends:
+      base >=4.9 && <5
+    , containers
+    , mtl
+    , sop-core
+    , template-haskell
+  default-language: Haskell2010
diff --git a/src/Generics/MRSOP/Base/Class.hs b/src/Generics/MRSOP/Base/Class.hs
--- a/src/Generics/MRSOP/Base/Class.hs
+++ b/src/Generics/MRSOP/Base/Class.hs
@@ -39,7 +39,7 @@
 sfrom el = sfrom' (getElSNat el) el
 
 -- |For 'sto'' there is a similar more general combinator.
---  If 'ix' implements 'IsNat' we can cast it.
+--  If @ix@ implements 'IsNat' we can cast it.
 sto :: forall fam ki codes ix
      . (Family ki fam codes , IsNat ix)
     => Rep ki (El fam) (Lkup ix codes) -> El fam ix  
diff --git a/src/Generics/MRSOP/Base/Metadata.hs b/src/Generics/MRSOP/Base/Metadata.hs
--- a/src/Generics/MRSOP/Base/Metadata.hs
+++ b/src/Generics/MRSOP/Base/Metadata.hs
@@ -1,3 +1,5 @@
+{-# LANGUAGE UndecidableInstances   #-}
+{-# LANGUAGE FlexibleContexts       #-}
 {-# LANGUAGE RankNTypes             #-}
 {-# LANGUAGE FlexibleInstances      #-}
 {-# LANGUAGE FunctionalDependencies #-}
@@ -10,6 +12,7 @@
 module Generics.MRSOP.Base.Metadata where
 
 import Data.Proxy
+import Data.SOP.Constraint
 
 import Generics.MRSOP.Util
 import Generics.MRSOP.Base.NP
@@ -39,17 +42,20 @@
   New :: ModuleName -> DatatypeName -> ConstructorInfo '[ c ]
       -> DatatypeInfo '[ '[ c ]]
 
+-- |Returns the name of a module
 moduleName :: DatatypeInfo code -> ModuleName
 moduleName (ADT m _ _) = m
 moduleName (New m _ _) = m
 
+-- |Returns the name of a datatype
 datatypeName :: DatatypeInfo code -> DatatypeName
 datatypeName (ADT _ d _) = d
 datatypeName (New _ d _) = d
 
+-- |Returns information about the constructor fields
 constructorInfo :: DatatypeInfo code -> NP ConstructorInfo code
 constructorInfo (ADT _ _ c) = c
-constructorInfo (New _ _ c) = c :* NP0
+constructorInfo (New _ _ c) = c :* Nil
 
 -- |Associativity information for infix constructors.
 data Associativity
@@ -67,6 +73,7 @@
   Infix       :: ConstructorName -> Associativity -> Fixity -> ConstructorInfo '[ x , y ]
   Record      :: ConstructorName -> NP FieldInfo xs -> ConstructorInfo xs
 
+-- |Returns the name of a constructor
 constructorName :: ConstructorInfo con -> ConstructorName
 constructorName (Constructor c) = c
 constructorName (Infix c _ _)   = c
@@ -78,18 +85,14 @@
 
 deriving instance Show (FieldInfo atom)
 
-instance ShowHO FieldInfo where
-  showHO = show
-
-deriving instance Show (ConstructorInfo code)
-
-instance ShowHO ConstructorInfo where
-  showHO = show
+deriving instance (All (Compose Show FieldInfo) code)
+  => Show (ConstructorInfo code)
 
-deriving instance Show (DatatypeInfo code)
+deriving instance (All (Compose Show ConstructorInfo) code)
+  => Show (DatatypeInfo code)
 
 -- |Given a 'Family', provides the 'DatatypeInfo' for the type
---  with index @ix@ in family 'fam'.
+--  with index @ix@ in family @fam@.
 class (Family ki fam codes) => HasDatatypeInfo ki fam codes
     | fam -> codes ki where
   datatypeInfo :: Proxy fam -> SNat ix -> DatatypeInfo (Lkup ix codes)
diff --git a/src/Generics/MRSOP/Base/NP.hs b/src/Generics/MRSOP/Base/NP.hs
--- a/src/Generics/MRSOP/Base/NP.hs
+++ b/src/Generics/MRSOP/Base/NP.hs
@@ -7,74 +7,69 @@
 {-# LANGUAGE DataKinds         #-}
 {-# LANGUAGE PolyKinds         #-}
 -- | Standard representation of n-ary products.
-module Generics.MRSOP.Base.NP where
+module Generics.MRSOP.Base.NP
+  ( SOP.NP(..)
+  , appendNP
+  , listPrfNP
+  , mapNP
+  , mapNPM
+  , elimNP
+  , elimNPM
+  , zipNP
+  , unzipNP
+  , cataNP
+  , cataNPM
+  , eqNP
+  ) where
 
+import           Data.SOP.NP (NP(..))
+import qualified Data.SOP.NP as SOP
 import Generics.MRSOP.Util
 
-infixr 5 :*
--- |Indexed n-ary products. This is analogous to the @All@ datatype
---  in Agda. 
-data NP :: (k -> *) -> [k] -> * where
-  NP0  :: NP p '[]
-  (:*) :: p x -> NP p xs -> NP p (x : xs)
-
-instance EqHO phi => EqHO (NP phi) where
-  eqHO = eqNP eqHO
-
-instance EqHO phi => Eq (NP phi xs) where
-  (==) = eqHO
-
-instance ShowHO phi => ShowHO (NP phi) where
-  showHO NP0 = "NP0"
-  showHO (a :* b) = showHO a ++ " :* " ++ showHO b
-
-instance ShowHO phi => Show (NP phi xs) where
-  show = showHO
-
 -- * Relation to IsList predicate
 
 -- |Append two values of type 'NP'
 appendNP :: NP p xs -> NP p ys -> NP p (xs :++: ys)
-appendNP NP0        ays = ays
+appendNP Nil        ays = ays
 appendNP (a :* axs) ays = a :* appendNP axs ays
 
 -- |Proves that the index of a value of type 'NP' is a list.
 --  This is useful for pattern matching on said list without
 --  having to carry the product around.
 listPrfNP :: NP p xs -> ListPrf xs
-listPrfNP NP0       = Nil
-listPrfNP (_ :* xs) = Cons $ listPrfNP xs
+listPrfNP Nil       = LP_Nil
+listPrfNP (_ :* xs) = LP_Cons $ listPrfNP xs
 
 -- * Map, Elim and Zip
 
 -- |Maps a natural transformation over a n-ary product
 mapNP :: f :-> g -> NP f ks -> NP g ks
-mapNP _ NP0       = NP0
+mapNP _ Nil       = Nil
 mapNP f (k :* ks) = f k :* mapNP f ks
 
 -- |Maps a monadic natural transformation over a n-ary product
 mapNPM :: (Monad m) => (forall x . f x -> m (g x)) -> NP f ks -> m (NP g ks)
-mapNPM _ NP0       = return NP0
+mapNPM _ Nil       = return Nil
 mapNPM f (k :* ks) = (:*) <$> f k <*> mapNPM f ks
 
 -- |Eliminates the product using a provided function.
 elimNP :: (forall x . f x -> a) -> NP f ks -> [a]
-elimNP _ NP0       = []
+elimNP _ Nil       = []
 elimNP f (k :* ks) = f k : elimNP f ks
 
 -- |Monadic eliminator
 elimNPM :: (Monad m) => (forall x . f x -> m a) -> NP f ks -> m [a]
-elimNPM _ NP0       = return []
+elimNPM _ Nil       = return []
 elimNPM f (k :* ks) = (:) <$> f k <*> elimNPM f ks
 
 -- |Combines two products into one.
 zipNP :: NP f xs -> NP g xs -> NP (f :*: g) xs
-zipNP NP0       NP0       = NP0
+zipNP Nil       Nil       = Nil
 zipNP (f :* fs) (g :* gs) = (f :*: g) :* zipNP fs gs
 
 -- |Unzips a combined product into two separate products
 unzipNP :: NP (f :*: g) xs -> (NP f xs , NP g xs)
-unzipNP NP0               = (NP0 , NP0) 
+unzipNP Nil               = (Nil , Nil) 
 unzipNP (Pair f g :* fgs) = (f :*) *** (g :*) $ unzipNP fgs
 
 -- * Catamorphism
@@ -83,7 +78,7 @@
 cataNP :: (forall a as . f a  -> r as -> r (a : as))
        -> r '[]
        -> NP f xs -> r xs
-cataNP _fCons fNil NP0       = fNil
+cataNP _fCons fNil Nil       = fNil
 cataNP fCons  fNil (k :* ks) = fCons k (cataNP fCons fNil ks)
 
 -- |Consumes a value of type 'NP'.
@@ -91,7 +86,7 @@
         => (forall a as . f a  -> r as -> m (r (a : as)))
         -> m (r '[])
         -> NP f xs -> m (r xs)
-cataNPM _fCons fNil NP0       = fNil
+cataNPM _fCons fNil Nil      = fNil
 cataNPM fCons fNil (k :* ks) = cataNPM fCons fNil ks >>= fCons k 
 
 
diff --git a/src/Generics/MRSOP/Base/NS.hs b/src/Generics/MRSOP/Base/NS.hs
--- a/src/Generics/MRSOP/Base/NS.hs
+++ b/src/Generics/MRSOP/Base/NS.hs
@@ -1,42 +1,45 @@
-{-# LANGUAGE RankNTypes             #-}
-{-# LANGUAGE FlexibleContexts       #-}
-{-# LANGUAGE FlexibleInstances      #-}
-{-# LANGUAGE GADTs                  #-}
-{-# LANGUAGE TypeOperators          #-}
-{-# LANGUAGE DataKinds              #-}
-{-# LANGUAGE PolyKinds              #-}
-{-# LANGUAGE ScopedTypeVariables    #-}
-{-# OPTIONS_GHC -Wno-name-shadowing #-}
+{-# LANGUAGE PatternSynonyms             #-}
+{-# LANGUAGE RankNTypes                  #-}
+{-# LANGUAGE FlexibleContexts            #-}
+{-# LANGUAGE FlexibleInstances           #-}
+{-# LANGUAGE GADTs                       #-}
+{-# LANGUAGE TypeOperators               #-}
+{-# LANGUAGE DataKinds                   #-}
+{-# LANGUAGE PolyKinds                   #-}
+{-# LANGUAGE ScopedTypeVariables         #-}
+{-# LANGUAGE ScopedTypeVariables         #-}
+{-# OPTIONS_GHC -Wno-name-shadowing      #-}
 
 -- | Standard representation of n-ary sums.
-module Generics.MRSOP.Base.NS where
+module Generics.MRSOP.Base.NS
+  ( SOP.NS , pattern Here , pattern There
+  , mapNS
+  , mapNSM
+  , elimNS 
+  , zipNS
+  , cataNS
+  , eqNS
+  ) where
 
+import qualified Data.SOP.NS as SOP
+import           Data.SOP.NS (NS(..))
+
 import Control.Monad
 import Generics.MRSOP.Util
 
-
--- |Indexed n-ary sums. This is analogous to the @Any@ datatype
---  in @Agda@. 
---  Combinations of 'Here' and 'There's are also called injections.
-data NS :: (k -> *) -> [k] -> * where
-  There :: NS p xs -> NS p (x : xs)
-  Here  :: p x     -> NS p (x : xs)
-
-instance EqHO phi => EqHO (NS phi) where
-  eqHO = eqNS eqHO
-
-instance EqHO phi => Eq (NS phi xs) where
-  (==) = eqHO
+-- |Pattern synonym to 'SOP.S'
+pattern There :: forall k (a :: k -> *) (b :: [k]). ()
+              => forall (xs :: [k]) (x :: k). (b ~ (x : xs))
+              => NS a xs -> NS a b
+pattern There x = SOP.S x
 
-instance ShowHO phi => ShowHO (NS phi) where
-  showHO x = concat ["(" , go 0 x , ")"]
-    where
-      go :: ShowHO phi => Int -> NS phi xs -> String
-      go n (Here r)  = "C" ++ show n ++ " " ++ showHO r
-      go n (There r) = go (n+1) r
+-- |Pattern synonym to 'SOP.Z'
+pattern Here :: forall k (a :: k -> *) (b :: [k]). ()
+             => forall (x :: k) (xs :: [k]). (b ~ (x : xs))
+             => a x -> NS a b
+pattern Here x = SOP.Z x
 
-instance ShowHO phi => Show (NS phi xs) where
-  show = showHO
+{-# COMPLETE Here, There #-}
 
 -- * Map, Zip and Elim
 
diff --git a/src/Generics/MRSOP/Base/Universe.hs b/src/Generics/MRSOP/Base/Universe.hs
--- a/src/Generics/MRSOP/Base/Universe.hs
+++ b/src/Generics/MRSOP/Base/Universe.hs
@@ -1,13 +1,15 @@
-{-# LANGUAGE RankNTypes           #-}
-{-# LANGUAGE FlexibleContexts     #-}
-{-# LANGUAGE FlexibleInstances    #-}
-{-# LANGUAGE GADTs                #-}
-{-# LANGUAGE TypeOperators        #-}
-{-# LANGUAGE DataKinds            #-}
-{-# LANGUAGE PolyKinds            #-}
-{-# LANGUAGE PatternSynonyms      #-}
-{-# LANGUAGE ScopedTypeVariables  #-}
-{-# LANGUAGE TypeApplications     #-}
+{-# LANGUAGE QuantifiedConstraints       #-}
+{-# LANGUAGE RankNTypes                  #-}
+{-# LANGUAGE FlexibleContexts            #-}
+{-# LANGUAGE FlexibleInstances           #-}
+{-# LANGUAGE GADTs                       #-}
+{-# LANGUAGE TypeOperators               #-}
+{-# LANGUAGE DataKinds                   #-}
+{-# LANGUAGE PolyKinds                   #-}
+{-# LANGUAGE PatternSynonyms             #-}
+{-# LANGUAGE ScopedTypeVariables         #-}
+{-# LANGUAGE TypeApplications            #-}
+{-# OPTIONS_GHC -Wno-incomplete-patterns #-}
 -- |Wraps the definitions of 'NP' and 'NS'
 --  into Representations ('Rep'), essentially providing
 --  the universe view over sums-of-products.
@@ -47,18 +49,12 @@
   NA_I :: (IsNat k) => phi k -> NA ki phi ('I k) 
   NA_K ::              ki  k -> NA ki phi ('K k)
 
-instance (EqHO phi, EqHO ki) => EqHO (NA ki phi) where
-  eqHO = eqNA eqHO eqHO
-
-instance (EqHO phi, EqHO ki) => Eq (NA ki phi at) where
-  (==) = eqHO
-
-instance (ShowHO phi, ShowHO ki) => ShowHO (NA ki phi) where
-  showHO (NA_I i) = "(NA_I " ++ showHO i ++ ")"
-  showHO (NA_K k) = "(NA_K " ++ showHO k ++ ")"
+instance (EqHO phi , EqHO ki) => Eq (NA ki phi at) where
+  (==) = eqNA (==) (==)
 
-instance (ShowHO phi, ShowHO ki) => Show (NA ki phi at) where
-  show = showHO
+instance (ShowHO phi , ShowHO ki) => Show (NA ki phi at) where
+  show (NA_I i) = "(NA_I " ++ show i ++ ")"
+  show (NA_K k) = "(NA_K " ++ show k ++ ")"
 
 instance (TestEquality ki) => TestEquality (NA ki phi) where
   testEquality (NA_I _) (NA_K _) = Nothing
@@ -128,11 +124,8 @@
 newtype Rep (ki :: kon -> *) (phi :: Nat -> *) (code :: [[Atom kon]])
   = Rep { unRep :: NS (PoA ki phi) code }
 
-instance (EqHO phi, EqHO ki) => EqHO (Rep ki phi) where
-  eqHO = eqRep eqHO eqHO
-
 instance (EqHO phi, EqHO ki) => Eq (Rep ki phi at) where
-  (==) = eqHO
+  (==) = eqRep (==) (==)
   
 -- |Product of Atoms is a handy synonym to have.
 type PoA (ki :: kon -> *) (phi :: Nat -> *) = NP (NA ki phi)
@@ -277,18 +270,15 @@
 --
 -- Finally we tie the recursive knot. Given an interpretation
 -- for the constant types, a family of sums-of-products and
--- an index ix into such family, we take the least fixpoint of
+-- an index @ix@ into such family, we take the least fixpoint of
 -- the representation of the code indexed by ix
 
 -- |Indexed least fixpoints
 newtype Fix (ki :: kon -> *) (codes :: [[[ Atom kon ]]]) (n :: Nat)
   = Fix { unFix :: Rep ki (Fix ki codes) (Lkup n codes) }
 
-instance EqHO ki => EqHO (Fix ki codes) where
-  eqHO = eqFix eqHO
-
 instance EqHO ki => Eq (Fix ki codes ix) where
-  (==) = eqFix eqHO
+  (==) = eqFix (==)
 
 -- | Catamorphism over fixpoints
 cata :: (IsNat ix)
diff --git a/src/Generics/MRSOP/Examples/RoseTree.hs b/src/Generics/MRSOP/Examples/RoseTree.hs
--- a/src/Generics/MRSOP/Examples/RoseTree.hs
+++ b/src/Generics/MRSOP/Examples/RoseTree.hs
@@ -86,37 +86,37 @@
 -- this code automatically.
 --
 -- >instance Family Singl FamRose CodesRose where
--- >   sfrom' (SS SZ) (El (a :>: as)) = Rep $ Here (NA_K (SInt a) :* NA_I (El as) :* NP0)
--- >   sfrom' (SS SZ) (El (Leaf a))   = Rep $ There (Here (NA_K (SInt a) :* NP0))
--- >   sfrom' SZ (El [])              = Rep $ Here NP0
--- >   sfrom' SZ (El (x:xs))          = Rep $ There (Here (NA_I (El x) :* NA_I (El xs) :* NP0))
+-- >   sfrom' (SS SZ) (El (a :>: as)) = Rep $ Here (NA_K (SInt a) :* NA_I (El as) :* Nil)
+-- >   sfrom' (SS SZ) (El (Leaf a))   = Rep $ There (Here (NA_K (SInt a) :* Nil))
+-- >   sfrom' SZ (El [])              = Rep $ Here Nil
+-- >   sfrom' SZ (El (x:xs))          = Rep $ There (Here (NA_I (El x) :* NA_I (El xs) :* Nil))
 -- >   sfrom' _ _ = error "unreachable"
 -- > 
--- >   sto' SZ (Rep (Here NP0))
+-- >   sto' SZ (Rep (Here Nil))
 -- >     = El []
--- >   sto' SZ (Rep (There (Here (NA_I (El x) :* NA_I (El xs) :* NP0))))
+-- >   sto' SZ (Rep (There (Here (NA_I (El x) :* NA_I (El xs) :* Nil))))
 -- >     = El (x : xs)
--- >   sto' (SS SZ) (Rep (Here (NA_K (SInt a) :* NA_I (El as) :* NP0)))
+-- >   sto' (SS SZ) (Rep (Here (NA_K (SInt a) :* NA_I (El as) :* Nil)))
 -- >     = El (a :>: as)
--- >   sto' (SS SZ) (Rep (There (Here (NA_K (SInt a) :* NP0))))
+-- >   sto' (SS SZ) (Rep (There (Here (NA_K (SInt a) :* Nil))))
 -- >     = El (Leaf a)
 -- >   sto' _ _ = error "unreachable"
 
 
 instance Family Singl FamRose CodesRose where
-  sfrom' (SS SZ) (El (a :>: as)) = Rep $ Here (NA_K (SInt a) :* NA_I (El as) :* NP0)
-  sfrom' (SS SZ) (El (Leaf a))   = Rep $ There (Here (NA_K (SInt a) :* NP0))
-  sfrom' SZ (El [])              = Rep $ Here NP0
-  sfrom' SZ (El (x:xs))          = Rep $ There (Here (NA_I (El x) :* NA_I (El xs) :* NP0))
+  sfrom' (SS SZ) (El (a :>: as)) = Rep $ Here (NA_K (SInt a) :* NA_I (El as) :* Nil)
+  sfrom' (SS SZ) (El (Leaf a))   = Rep $ There (Here (NA_K (SInt a) :* Nil))
+  sfrom' SZ (El [])              = Rep $ Here Nil
+  sfrom' SZ (El (x:xs))          = Rep $ There (Here (NA_I (El x) :* NA_I (El xs) :* Nil))
   sfrom' _ _ = error "unreachable"
 
-  sto' SZ (Rep (Here NP0))
+  sto' SZ (Rep (Here Nil))
     = El []
-  sto' SZ (Rep (There (Here (NA_I (El x) :* NA_I (El xs) :* NP0))))
+  sto' SZ (Rep (There (Here (NA_I (El x) :* NA_I (El xs) :* Nil))))
     = El (x : xs)
-  sto' (SS SZ) (Rep (Here (NA_K (SInt a) :* NA_I (El as) :* NP0)))
+  sto' (SS SZ) (Rep (Here (NA_K (SInt a) :* NA_I (El as) :* Nil)))
     = El (a :>: as)
-  sto' (SS SZ) (Rep (There (Here (NA_K (SInt a) :* NP0))))
+  sto' (SS SZ) (Rep (There (Here (NA_K (SInt a) :* Nil))))
     = El (Leaf a)
   sto' _ _ = error "unreachable"
 
@@ -125,12 +125,12 @@
     = ADT "module" (Name "[]" :@: (Name "R" :@: Name "Int"))
       $  (Constructor "[]")
       :* (Infix ":" RightAssociative 5)
-      :* NP0
+      :* Nil
   datatypeInfo _ (SS SZ)
     = ADT "module" (Name "R" :@: Name "Int")
       $  (Infix ":>:" NotAssociative 0)
       :* (Constructor "Leaf")
-      :* NP0
+      :* Nil
   datatypeInfo _ _
     = error "unreachable"
 
diff --git a/src/Generics/MRSOP/Examples/SimpTH.hs b/src/Generics/MRSOP/Examples/SimpTH.hs
--- a/src/Generics/MRSOP/Examples/SimpTH.hs
+++ b/src/Generics/MRSOP/Examples/SimpTH.hs
@@ -45,11 +45,19 @@
   | SSkip
   deriving Show
 
-data Decl var
+-- Below is a little type synonym fun, to make sure
+-- generation is working
+data ODecl var
   = DVar var
   | DFun var var (Stmt var)
   deriving Show
 
+-- Note that since we use 'Decl' directly in the family;
+-- there won't be pattern-synonyms generated for 'ODecl' or 'TDecl'
+type Decl x = TDecl x
+
+type TDecl x = ODecl x
+
 data Exp var
   = EVar  var
   | ECall var (Exp var)
@@ -157,6 +165,7 @@
 
 -}
 
+
 test3 :: String -> String -> String -> Decl String
 test3 n1 n2 z = DFun "f" n1
               $ SDecl (DFun "g" n2
@@ -196,12 +205,12 @@
 
 test6 :: Holes Singl CodesStmtString (Const Int) ('I ('S 'Z))
 test6 = HPeel' (CS (CS CZ))
-          (  (HPeel' CZ (HOpq' (SString "lol") :* NP0))
+          (  (HPeel' CZ (HOpq' (SString "lol") :* Nil))
           :* (Hole' (Const 42))
-          :* NP0)
+          :* Nil)
 
 test7 :: HolesAnn (Const Int) Singl CodesStmtString (Const Int) ('I ('S 'Z))
 test7 = HPeel (Const 1) (CS (CS CZ))
-          (  (HPeel (Const 2) CZ (HOpq (Const 4) (SString "lol") :* NP0))
+          (  (HPeel (Const 2) CZ (HOpq (Const 4) (SString "lol") :* Nil))
           :* (Hole (Const 3) (Const 42))
-          :* NP0)
+          :* Nil)
diff --git a/src/Generics/MRSOP/Holes.hs b/src/Generics/MRSOP/Holes.hs
--- a/src/Generics/MRSOP/Holes.hs
+++ b/src/Generics/MRSOP/Holes.hs
@@ -1,4 +1,5 @@
-{-# LANGUAGE UndecidableInstances #-}
+{-# LANGUAGE QuantifiedConstraints #-}
+{-# LANGUAGE UndecidableInstances  #-}
 {-# LANGUAGE PatternSynonyms       #-}
 {-# LANGUAGE FlexibleInstances     #-}
 {-# LANGUAGE RankNTypes            #-}
@@ -190,7 +191,7 @@
 holesRefineAnnM f g (HPeel a c holesnp)
   = HPeel a c <$> mapNPM (holesRefineAnnM f g) holesnp
 
--- |Just like 'holesRefineM', but only refines variables. One example is to implement
+-- |Just like 'holesRefineAnnM', but only refines variables. One example is to implement
 -- 'holesJoin' with it.
 --
 -- > holesJoin = runIdentity . holesRefineVarsM (\_ -> return)
@@ -201,7 +202,7 @@
                  -> m (HolesAnn ann ki codes g at)
 holesRefineVarsM f = holesRefineAnnM f (\a -> return . HOpq a)
 
--- |Pure version of 'holesRefineM'
+-- |Pure version of 'holesRefineAnnM'
 holesRefineAnn :: (forall ix . ann ix     -> f ix -> HolesAnn ann ki codes g ix) -- ^
                -> (forall k  . ann ('K k) -> ki k -> HolesAnn ann ki codes g ('K k))
                -> HolesAnn ann ki codes f at 
@@ -277,18 +278,25 @@
 --  @Const ()@
 type Holes = HolesAnn (Const ())
 
+-- |Synonym to @Hole (Const ())@
 pattern Hole' :: phi at -> Holes ki codes phi at
 pattern Hole' x = Hole (Const ()) x
 
+
+-- |Synonym to @HOpq (Const ())@
 pattern HOpq' :: ki k -> Holes ki codes phi ('K k)
 pattern HOpq' x = HOpq (Const ()) x
 
+
+-- |Synonym to @HPeel (Const ())@
 pattern HPeel' :: () => (IsNat n, IsNat i)
                => Constr (Lkup i codes) n
                -> NP (Holes ki codes phi) (Lkup n (Lkup i codes))
                -> Holes ki codes phi ('I i)
 pattern HPeel' c p = HPeel (Const ()) c p
 
+{-# COMPLETE Hole' , HOpq' , HPeel' #-}
+
 -- |Factors out the largest common prefix of two treefixes.
 --  This is also known as the anti-unification of two
 --  treefixes.
@@ -300,13 +308,13 @@
 --
 --  We use a function to combine annotations in case it is
 --  necessary.
-holesLCP :: (EqHO ki)
+holesLCP :: (forall k . Eq (ki k))
          => Holes ki codes f at
          -> Holes ki codes g at
          -> Holes ki codes (Holes ki codes f :*: Holes ki codes g) at
 holesLCP (HOpq _ kx) (HOpq _ ky)
-  | eqHO kx ky = HOpq' kx
-  | otherwise  = Hole' (HOpq' kx :*: HOpq' ky)
+  | kx == ky  = HOpq' kx
+  | otherwise = Hole' (HOpq' kx :*: HOpq' ky)
 holesLCP (HPeel a cx px) (HPeel b cy py)
   = case testEquality cx cy of
       Nothing   -> Hole'  (HPeel a cx px :*: HPeel b cy py)
@@ -353,21 +361,18 @@
   utx == uty = and $ holesGetHolesAnnWith' (uncurry' cmp) $ holesLCP utx uty
     where
       cmp :: HolesAnn ann ki codes phi at -> HolesAnn ann ki codes phi at -> Bool
-      cmp (Hole _ x) (Hole _ y) = eqHO x y
-      cmp (HOpq _ x) (HOpq _ y) = eqHO x y
+      cmp (Hole _ x) (Hole _ y) = x == y
+      cmp (HOpq _ x) (HOpq _ y) = x == y
       cmp _           _         = False
 
-instance (EqHO phi , EqHO ki) => EqHO (Holes ki codes phi) where
-  eqHO utx uty = utx == uty
-
 holesShow :: forall ki ann f fam codes ix
            . (HasDatatypeInfo ki fam codes , ShowHO ki , ShowHO f)
           => Proxy fam
           -> (forall at . ann at -> ShowS)
           -> HolesAnn ann ki codes f ix
           -> ShowS
-holesShow _ f (Hole a x)       = ('`':) . f a . showString (showHO x) 
-holesShow _ f (HOpq a k)       = f a . showString (showHO k)
+holesShow _ f (Hole a x)       = ('`':) . f a . showString (show x) 
+holesShow _ f (HOpq a k)       = f a . showString (show k)
 holesShow p f h@(HPeel a c rest)
   = showParen (needParens h) $ showString cname
                              . f a
@@ -383,27 +388,19 @@
       (Infix name _ _)   -> "(" ++ name ++ ")"
  
     needParens :: HolesAnn ann ki codes f iy -> Bool
-    needParens (Hole _ _) = False
-    needParens (HOpq _ _) = False
-    needParens (HPeel _ _ NP0) = False
-    needParens _          = True
+    needParens (Hole _ _)      = False
+    needParens (HOpq _ _)      = False
+    needParens (HPeel _ _ Nil) = False
+    needParens _               = True
 
 instance {-# OVERLAPPABLE #-} (HasDatatypeInfo ki fam codes , ShowHO ki , ShowHO f , ShowHO ann)
-    => ShowHO (HolesAnn ann ki codes f) where
-  showHO h = holesShow (Proxy :: Proxy fam) showsAnn h ""
+    => Show (HolesAnn ann ki codes f ix) where
+  show h = holesShow (Proxy :: Proxy fam) showsAnn h ""
     where
       showsAnn ann = showString "{"
-                   . showString (showHO ann)
+                   . showString (show ann)
                    . showString "}"
 
-instance {-# OVERLAPPABLE #-} (HasDatatypeInfo ki fam codes , ShowHO ki , ShowHO f , ShowHO ann)
-    => Show (HolesAnn ann ki codes f at) where
-  show = showHO
-
 instance {-# OVERLAPPING #-} (HasDatatypeInfo ki fam codes , ShowHO ki , ShowHO f)
-    => ShowHO (Holes ki codes f) where
-  showHO h = holesShow (Proxy :: Proxy fam) (const id) h ""
-
-instance {-# OVERLAPPING #-} (HasDatatypeInfo ki fam codes , ShowHO ki , ShowHO f)
     => Show (Holes ki codes f at) where
-  show = showHO
+  show h = holesShow (Proxy :: Proxy fam) (const id) h ""
diff --git a/src/Generics/MRSOP/Opaque.hs b/src/Generics/MRSOP/Opaque.hs
--- a/src/Generics/MRSOP/Opaque.hs
+++ b/src/Generics/MRSOP/Opaque.hs
@@ -14,7 +14,6 @@
 module Generics.MRSOP.Opaque where
 
 import Data.Type.Equality
-import Generics.MRSOP.Util
 
 -- * Opaque Types
 --
@@ -59,12 +58,6 @@
  show (SBool     a) = show a
  show (SChar     a) = show a
  show (SString   a) = show a
-
-instance EqHO Singl where
-  eqHO = (==)
-
-instance ShowHO Singl where
-  showHO = show
 
 -- |Equality over singletons
 eqSingl :: Singl k -> Singl k -> Bool
diff --git a/src/Generics/MRSOP/TH.hs b/src/Generics/MRSOP/TH.hs
--- a/src/Generics/MRSOP/TH.hs
+++ b/src/Generics/MRSOP/TH.hs
@@ -26,34 +26,34 @@
 --  > 
 --  > -- (:>:) pattern syn
 --  > pattern RoseInt_Ifx0 :: kon KInt -> phi (S Z) -> View kon phi (Lkup Z CodesRoseInt)
---  > pattern RoseInt_Ifx0 p q = Tag CZ (NA_K p :* (NA_I q :* NP0))
+--  > pattern RoseInt_Ifx0 p q = Tag CZ (NA_K p :* (NA_I q :* Nil))
 --  > 
 --  > -- Leaf pattern syn
 --  > pattern RoseIntLeaf_ :: kon KInt -> View kon phi (Lkup Z CodesRoseInt)
---  > pattern RoseIntLeaf_ p = Tag (CS CZ) (NA_K p :* NP0)
+--  > pattern RoseIntLeaf_ p = Tag (CS CZ) (NA_K p :* Nil)
 --  > 
 --  > -- [] pattern syn
 --  > pattern ListRoseInt_Ifx0 :: View kon phi (Lkup (S Z) CodesRoseInt)
---  > pattern ListRoseInt_Ifx0 = Tag CZ NP0
+--  > pattern ListRoseInt_Ifx0 = Tag CZ Nil
 --  > 
 --  > -- (:) pattern syn
 --  > pattern ListRoseInt_Ifx1 :: phi Z -> phi (S Z) -> View kon phi (Lkup (S Z) CodesRoseInt)
---  > pattern ListRoseInt_Ifx1 p q = Tag (CS CZ) (NA_I p :* (NA_I q :* NP0))
+--  > pattern ListRoseInt_Ifx1 p q = Tag (CS CZ) (NA_I p :* (NA_I q :* Nil))
 --  > 
 --  > instance Family Singl FamRose CodesRose where
---  >   sfrom' (SS SZ) (El (a :>: as)) = Rep $ Here (NA_K (SInt a) :* NA_I (El as) :* NP0)
---  >   sfrom' (SS SZ) (El (Leaf a))   = Rep $ There (Here (NA_K (SInt a) :* NP0))
---  >   sfrom' SZ (El [])              = Rep $ Here NP0
---  >   sfrom' SZ (El (x:xs))          = Rep $ There (Here (NA_I (El x) :* NA_I (El xs) :* NP0))
+--  >   sfrom' (SS SZ) (El (a :>: as)) = Rep $ Here (NA_K (SInt a) :* NA_I (El as) :* Nil)
+--  >   sfrom' (SS SZ) (El (Leaf a))   = Rep $ There (Here (NA_K (SInt a) :* Nil))
+--  >   sfrom' SZ (El [])              = Rep $ Here Nil
+--  >   sfrom' SZ (El (x:xs))          = Rep $ There (Here (NA_I (El x) :* NA_I (El xs) :* Nil))
 --  >   sfrom' _ _ = error "unreachable"
 --  > 
---  >   sto' SZ (Rep (Here NP0))
+--  >   sto' SZ (Rep (Here Nil))
 --  >     = El []
---  >   sto' SZ (Rep (There (Here (NA_I (El x) :* NA_I (El xs) :* NP0))))
+--  >   sto' SZ (Rep (There (Here (NA_I (El x) :* NA_I (El xs) :* Nil))))
 --  >     = El (x : xs)
---  >   sto' (SS SZ) (Rep (Here (NA_K (SInt a) :* NA_I (El as) :* NP0)))
+--  >   sto' (SS SZ) (Rep (Here (NA_K (SInt a) :* NA_I (El as) :* Nil)))
 --  >     = El (a :>: as)
---  >   sto' (SS SZ) (Rep (There (Here (NA_K (SInt a) :* NP0))))
+--  >   sto' (SS SZ) (Rep (There (Here (NA_K (SInt a) :* Nil))))
 --  >     = El (Leaf a)
 --  >   sto' _ _ = error "unreachable"
 --  > 
@@ -62,12 +62,12 @@
 --  >     = ADT "module" (Name "[]" :@: (Name "R" :@: Name "Int"))
 --  >       $  (Constructor "[]")
 --  >       :* (Infix ":" RightAssociative 5)
---  >       :* NP0
+--  >       :* Nil
 --  >   datatypeInfo _ (SS SZ)
 --  >     = ADT "module" (Name "R" :@: Name "Int")
 --  >       $  (Infix ":>:" NotAssociative 0)
 --  >       :* (Constructor "Leaf")
---  >       :* NP0
+--  >       :* Nil
 --  >   datatypeInfo _ _
 --  >     = error "unreachable"
 --
@@ -135,7 +135,7 @@
 --  > pattern DeclStringDVar_ 
 --  > pattern DeclStringDFun_ 
 --
---  We did ommit the definitions and 'Family' and 'HasDatatypeInfo' instances
+--  We did ommit the definitions and 'Family' and 'Generics.MRSOP.Base.Metadata.HasDatatypeInfo' instances
 --  for brevity here. If you want to see the actual generated code, compile with
 --  
 --  > stack build ghc-options="-ddump-splices -ddump-to-file"
@@ -157,6 +157,7 @@
 import Data.Function (on)
 import Data.Char (isAlphaNum)
 import Data.List (sortBy)
+import qualified Data.SOP.NS as SOP (NS(..))
 
 import Control.Monad
 import Control.Monad.State
@@ -168,7 +169,6 @@
 
 import Generics.MRSOP.Util
 import Generics.MRSOP.Base.Class
-import Generics.MRSOP.Base.NS
 import Generics.MRSOP.Base.NP
 import Generics.MRSOP.Base.Universe hiding (match)
 import qualified Generics.MRSOP.Base.Metadata as Meta
@@ -187,16 +187,16 @@
 -- |Given the name of the first element in the family,
 --  derives:
 --
---    1. The other types in the family and Konstant types one needs.
+--    1. The other types in the family and opaque types one needs.
 --    2. the SOP code for each of the datatypes involved
---    3. One 'Element' instance per datatype
+--    3. The 'Family' instance
 --    4. Metadada information for each of the datatypes involved
 --    5. Uses the opaque-type universe provided.
 deriveFamilyWith :: Name -> Q Type -> Q [Dec]
 deriveFamilyWith opqName t
-  = do sty              <- t >>= convertType 
-       opqData          <- reifyOpaqueType opqName
-       (_ , (Idxs _ m)) <- runIdxsM (reifySTy opqData sty)
+  = do sty                <- t >>= convertType 
+       opqData            <- reifyOpaqueType opqName
+       (_ , (Idxs _ m _)) <- runIdxsM (reifySTy opqData sty)
        -- Now we make sure we have processed all
        -- types
        m' <- mapM extractDTI (M.toList m)
@@ -445,17 +445,18 @@
 data Idxs 
   = Idxs { idxsNext :: Int
          , idxsMap  :: M.Map STy (Int , Maybe (DTI IK))
+         , idxsSyns :: M.Map STy STy
          }
   deriving (Show)
 
 onMap :: (M.Map STy (Int , Maybe (DTI IK)) -> M.Map STy (Int , Maybe (DTI IK)))
       -> Idxs -> Idxs
-onMap f (Idxs n m) = Idxs n (f m)
+onMap f (Idxs n m eqs) = Idxs n (f m) eqs
 
 type IdxsM = StateT Idxs
 
 runIdxsM :: (Monad m) => IdxsM m a -> m (a , Idxs)
-runIdxsM = flip runStateT (Idxs 0 M.empty)
+runIdxsM = flip runStateT (Idxs 0 M.empty M.empty)
 
 -- |The actual monad we need to run all of this;
 type M = IdxsM Q
@@ -466,11 +467,16 @@
 indexOf :: (Monad m) => STy -> IdxsM m Int
 indexOf name
   = do st <- get
-       case M.lookup name (idxsMap st) of
-         Just i  -> return (fst i)
-         Nothing -> let i = idxsNext st
-                     in put (Idxs (i + 1) (M.insert name (i , Nothing) (idxsMap st)))
-                     >> return i
+       case M.lookup name (idxsSyns st) of
+         Just orig -> indexOf orig -- TODO: make sure orig is in the map! :P
+         Nothing ->
+           case M.lookup name (idxsMap st) of
+             Just i  -> return (fst i)
+             Nothing -> let i = idxsNext st
+                         in put (Idxs (i + 1)
+                                      (M.insert name (i , Nothing) (idxsMap st))
+                                      (idxsSyns st))
+                         >> return i
 
 -- |Register some Datatype Information for a given STy
 register :: (Monad m) => STy -> DTI IK -> IdxsM m ()
@@ -482,6 +488,12 @@
 lkup :: (Monad m) => STy -> IdxsM m (Maybe (Int , Maybe (DTI IK)))
 lkup ty = M.lookup ty . idxsMap <$> get
 
+
+-- | Adds another type with the same index as the previous
+addTySynEquiv :: (Monad m) => STy -> STy -> IdxsM m ()
+addTySynEquiv orig new = 
+  modify (\st -> st { idxsSyns = M.insert new orig (idxsSyns st) })
+
 -- defined but not used
 -- lkupInfo :: (Monad m) => STy -> IdxsM m (Maybe Int)
 -- lkupInfo ty = fmap fst <$> lkup ty
@@ -537,23 +549,39 @@
 
     failMsg = fail $ "The opaque-type universe you provided is of the wrong form;"
                   ++ "Check documentation for Generics.MRSOP.TH.reifyOpaqueType"
-
 -- |Performs step 2 of the sketch;
 reifySTy :: OpaqueData -> STy -> M ()
-reifySTy opq sty
-  = do _ <- indexOf sty -- we don't care about the index of sty now, but we
+reifySTy opq sty0
+  = do _ <- indexOf sty0 -- we don't care about the index of sty now, but we
                         -- need to register it
-       uncurry go (styFlatten sty)
+       (dec , args) <- preprocess sty0
+       go dec args
   where
-    go :: STy -> [STy] -> M ()
-    go (ConST name) args
-      = do dec <- lift (reifyDec name >>= decInfo)
-           -- TODO: Check that the precondition holds.
+    preprocess :: STy -> M (DTI STy , [STy])
+    preprocess ty = 
+      let (head , args) = styFlatten ty
+       in case head of
+         ConST name -> do
+           dec <- lift (reifyDec name)
+           resolveTySyn (addTySynEquiv ty) dec args
+         _ -> fail "I can't convert appST or varST in reifySTy"
+
+    resolveTySyn :: (STy -> M ()) -> Dec -> [STy] -> M (DTI STy , [STy])
+    resolveTySyn upd8 (TySynD _ defargs def) localargs = do
+      sdef <- convertType def
+      let dict = zip (map argInfo defargs) localargs
+      let res = styReduce dict sdef
+      upd8 res
+      preprocess res
+    resolveTySyn _ def localargs = (,localargs) <$> lift (decInfo def)
+    
+    go :: DTI STy -> [STy] -> M ()
+    go dec args
+      = do -- TODO: Check that the precondition holds.
            let res = dtiReduce dec args
            (final , todo) <- runWriterT $ dtiMapM (convertSTy (opaqueTable opq)) res
-           register sty final
+           register sty0 final
            mapM_ (reifySTy opq) todo
-    go _ _ = fail "I can't convert appST or varST in reifySTy"
     
     -- Convert the STy's in the fields of the constructors;
     -- tells a list of STy's we still need to process.
@@ -561,7 +589,7 @@
     convertSTy opqTable ty
       -- We remove sty from the list of todos
       -- otherwise we get an infinite loop
-      | ty == sty = AtomI <$> lift (indexOf ty)
+      | ty == sty0 = AtomI <$> lift (indexOf ty)
       | isClosed ty
       = case makeCons opqTable ty of
           Just k  -> return (AtomK k)
@@ -571,7 +599,7 @@
                         return (AtomI ix)
       | otherwise
       = fail $ "I can't convert type variable " ++ show ty
-              ++ " when converting " ++ show sty
+              ++ " when converting " ++ show sty0
 
     makeCons :: M.Map Name Name -> STy -> Maybe Name
     makeCons opqTable (ConST n) = M.lookup n opqTable
@@ -616,33 +644,33 @@
 --   dropping that.
 --
 -- 2.2. constructors
--- > pattern a :>:_ as = Tag CZ      (NA_K a :* NA_I (El as) :* NP0)
--- > pattern Leaf_ a   = Tag (CS CZ) (NA_K a :* NP0)
--- > pattern nil_      = Tag CZ NP0
--- > pattern a :_ as   = Tag (CS CZ) (NA_I a :* NA_I (El as) :* NP0)
+-- > pattern a :>:_ as = Tag CZ      (NA_K a :* NA_I (El as) :* Nil)
+-- > pattern Leaf_ a   = Tag (CS CZ) (NA_K a :* Nil)
+-- > pattern nil_      = Tag CZ Nil
+-- > pattern a :_ as   = Tag (CS CZ) (NA_I a :* NA_I (El as) :* Nil)
 --
 -- 3. The instance:
 -- > instance Family Singl FamRose CodesRose where
 --
 -- 3.1. for each type in (1)
 -- >   sfrom' (SS SZ) (El (a :>: as))
--- >     = Rep $ HT0_ (NA_K (SInt a) :* NA_I (El as) :* NP0)
+-- >     = Rep $ HT0_ (NA_K (SInt a) :* NA_I (El as) :* Nil)
 -- >   sfrom' (SS SZ) (El (Leaf a))
--- >     = Rep $ HT1_ (NA_K (SInt a) :* NP0)
+-- >     = Rep $ HT1_ (NA_K (SInt a) :* Nil)
 -- >   sfrom' SZ (El [])
--- >     = Rep $ HT0_ NP0
+-- >     = Rep $ HT0_ Nil
 -- >   sfrom' SZ (El (x:xs))
--- >     = Rep $ HT1_ (NA_I (El x) :* NA_I (El xs) :* NP0)
+-- >     = Rep $ HT1_ (NA_I (El x) :* NA_I (El xs) :* Nil)
 --
 -- 3.2.
 -- > 
--- >   sto' SZ (Rep (HT0_ NP0))
+-- >   sto' SZ (Rep (HT0_ Nil))
 -- >     = El []
--- >   sto' SZ (Rep (HT1_ (NA_I (El x) :* NA_I (El xs) :* NP0)))
+-- >   sto' SZ (Rep (HT1_ (NA_I (El x) :* NA_I (El xs) :* Nil)))
 -- >     = El (x : xs)
--- >   sto' (SS SZ) (Rep (HT0_ (NA_K (SInt a) :* NA_I (El as) :* NP0)))
+-- >   sto' (SS SZ) (Rep (HT0_ (NA_K (SInt a) :* NA_I (El as) :* Nil)))
 -- >     = El (a :>: as)
--- >   sto' (SS SZ) (Rep (HT1_ (NA_K (SInt a) :* NP0)))
+-- >   sto' (SS SZ) (Rep (HT1_ (NA_K (SInt a) :* Nil)))
 -- >     = El (Leaf a)
 --
 -- 4. Metadata for each type in (1)
@@ -728,7 +756,7 @@
   where
     first (x , _ , _) = x
 
--- | @styToName "List (R Int)" == "ListRInt"@
+-- | @styToName "[R Int]" == "ListRInt"@
 styToName :: STy -> Name
 styToName = mkName . styFold (++) nameBase (fixList . nameBase)
   where
@@ -912,7 +940,7 @@
     ciHasIllegalName ci = any (not . isAlphaNum) $ nameBase (ciName ci)
 
     tagPatSynProd :: [(IK , Name)] -> Q Pat
-    tagPatSynProd []     = [p| NP0 |]
+    tagPatSynProd []     = [p| Nil |]
     tagPatSynProd (h:hs) = [p| $(tagPatSynProdHead h) :* ( $(tagPatSynProd hs) ) |]
 
     int2Constr :: Int -> Q Pat
@@ -937,7 +965,7 @@
 --
 --  > ci2PatExp opq IdxBinTree 3 (Normal "Bin" [VarT a , VarT a])
 --  >   = ( El (Bin x_1 x_2)
---  >     , Rep (There (There (Here (NA_I (El x_1) :* NA_I (El x_2) :* NP0))))
+--  >     , Rep (There (There (Here (NA_I (El x_1) :* NA_I (El x_2) :* Nil))))
 --  >     )
 ci2PatExp :: OpaqueData -> Int -> Int -> CI IK -> Q (Pat , Exp)
 ci2PatExp opq _dtiIx cIdx ci
@@ -946,11 +974,11 @@
        return (ConP (mkName "El") [pat] , bdy)
   where
     mkInj :: Int -> Q Exp -> Q Exp
-    mkInj 0 e = [e| Here $e                |]
-    mkInj n e = [e| There $(mkInj (n-1) e) |]
+    mkInj 0 e = [e| SOP.Z $e               |]
+    mkInj n e = [e| SOP.S $(mkInj (n-1) e) |]
 
     genBdy :: [(Name , IK)] -> Q Exp
-    genBdy []       = [e| NP0 |]
+    genBdy []       = [e| Nil |]
     genBdy (x : xs) = [e| $(mkHead x) :* ( $(genBdy xs) ) |]
 
 
@@ -961,7 +989,7 @@
 -- | Just like 'ci2PatExp', but the other way around.
 --
 --  > ci2ExpPat opq IdxBinTree 2 (Normal "Bin" [VarT a , VarT a])
---  >   = ( Rep (There (There (Here (NA_I (El x_1) :* NA_I (El x_2) :* NP0))))
+--  >   = ( Rep (There (There (Here (NA_I (El x_1) :* NA_I (El x_2) :* Nil))))
 --        , El (Bin x_1 x_2)
 --  >     )
 ci2ExpPat :: OpaqueData -> Int -> Int -> CI IK -> Q (Pat , Exp)
@@ -971,11 +999,11 @@
        return (pat , AppE (ConE $ mkName "El") myexp)
   where
     mkInj :: Int -> Q Pat -> Q Pat
-    mkInj 0 e = [p| Here $e                |]
-    mkInj n e = [p| There $(mkInj (n-1) e) |]
+    mkInj 0 e = [p| SOP.Z $e                |]
+    mkInj n e = [p| SOP.S $(mkInj (n-1) e) |]
     
     genBdy :: [(Name , IK)] -> Q Pat
-    genBdy []       = [p| NP0 |]
+    genBdy []       = [p| Nil |]
     genBdy (x : xs) = [p| $(mkHead x) :* ( $(genBdy xs) ) |]
 
 
@@ -1079,16 +1107,16 @@
         genFix (Fixity i _) = return . LitE . IntegerL . fromIntegral $ i
 
     genFieldInfo :: [ FieldName ] -> Q Exp
-    genFieldInfo []     = [e| NP0 |]
+    genFieldInfo []     = [e| Nil |]
     genFieldInfo (f:fs) = [e| Meta.FieldInfo $(strlit . nameBase $ f) :* ( $(genFieldInfo fs) ) |]
 
     genConInfoNP :: [ CI IK ] -> Q Exp
-    genConInfoNP []       = [e| NP0 |]
+    genConInfoNP []       = [e| Nil |]
     genConInfoNP (ci:cis) = [e| $(genConInfo ci) :* ( $(genConInfoNP cis) ) |]
 
 -- |@genFamily opq init fam@ generates a type-level list
 --  of the codes for the family. It also generates
---  the necessary 'Family' and 'HasDatatypeInfo' instances.
+--  the necessary 'Family' and 'Generics.MRSOP.Base.Metadata.HasDatatypeInfo' instances.
 --
 --  Precondition, input is sorted on second component.
 genFamily :: OpaqueData -> STy -> Input -> Q [Dec]
diff --git a/src/Generics/MRSOP/Util.hs b/src/Generics/MRSOP/Util.hs
--- a/src/Generics/MRSOP/Util.hs
+++ b/src/Generics/MRSOP/Util.hs
@@ -1,13 +1,16 @@
-{-# LANGUAGE ConstraintKinds     #-}
-{-# LANGUAGE GADTs               #-}
-{-# LANGUAGE TypeFamilies        #-}
-{-# LANGUAGE DataKinds           #-}
-{-# LANGUAGE PolyKinds           #-}
-{-# LANGUAGE TypeOperators       #-}
-{-# LANGUAGE RankNTypes          #-}
-{-# LANGUAGE TypeApplications    #-}
-{-# LANGUAGE ScopedTypeVariables #-}
-{-# LANGUAGE PatternSynonyms     #-}
+{-# LANGUAGE TypeSynonymInstances  #-}
+{-# LANGUAGE QuantifiedConstraints #-}
+{-# LANGUAGE ConstraintKinds       #-}
+{-# LANGUAGE GADTs                 #-}
+{-# LANGUAGE TypeFamilies          #-}
+{-# LANGUAGE DataKinds             #-}
+{-# LANGUAGE PolyKinds             #-}
+{-# LANGUAGE TypeOperators         #-}
+{-# LANGUAGE RankNTypes            #-}
+{-# LANGUAGE TypeApplications      #-}
+{-# LANGUAGE ScopedTypeVariables   #-}
+{-# LANGUAGE PatternSynonyms       #-}
+{-# OPTIONS_GHC -Wno-orphans       #-}
 -- |Useful utilities we need accross multiple modules.
 module Generics.MRSOP.Util
   ( -- * Utility Functions and Types
@@ -34,7 +37,7 @@
   , Lkup , Idx , El(..) , getElSNat , into
 
     -- * Higher-order Eq and Show
-  , EqHO(..) , ShowHO(..)
+  , EqHO , ShowHO
   ) where
 
 import Data.Proxy
@@ -45,10 +48,13 @@
 import GHC.TypeLits (TypeError , ErrorMessage(..))
 import Control.Arrow ((***) , (&&&))
 
+-- |Convenient type synonym for 'Product'
 type    (:*:)     = Product
 
+-- |Convnient pattern synonym for 'Pair'
 pattern (:*:) :: f a -> g a -> Product f g a
 pattern (:*:) x y = Pair x y
+{-# COMPLETE (:*:) #-}
 
 -- |Lifted curry
 curry' :: (Product f g x -> a) -> f x -> g x -> a
@@ -86,6 +92,7 @@
 data Nat = S Nat | Z
   deriving (Eq , Show)
 
+-- |Typelevel predecessor operation
 proxyUnsuc :: Proxy ('S n) -> Proxy n
 proxyUnsuc _ = Proxy
 
@@ -94,6 +101,7 @@
   SZ ::           SNat 'Z
   SS :: SNat n -> SNat ('S n)
 
+-- |Returns @n@ as a first class integer.
 snat2int :: SNat n -> Integer
 snat2int SZ     = 0
 snat2int (SS n) = 1 + snat2int n
@@ -151,22 +159,22 @@
 --  This is useful since it enables us to pattern match on
 --  type-level lists whenever we see fit.
 data ListPrf :: [k] -> * where
-  Nil ::  ListPrf '[]
-  Cons :: ListPrf l ->  ListPrf (x ': l)
+  LP_Nil  :: ListPrf '[]
+  LP_Cons :: ListPrf l ->  ListPrf (x ': l)
 
 -- |The @IsList@ class allows us to construct
 --  'ListPrf's in a straight forward fashion.
 class IsList (xs :: [k]) where
   listPrf :: ListPrf xs
 instance IsList '[] where
-  listPrf = Nil
+  listPrf = LP_Nil
 instance IsList xs => IsList (x ': xs) where
-  listPrf = Cons listPrf
+  listPrf = LP_Cons listPrf
 
 -- |Concatenation of lists is also a list.
 appendIsListLemma :: ListPrf xs -> ListPrf ys -> ListPrf (xs :++: ys)
-appendIsListLemma Nil         isys = isys
-appendIsListLemma (Cons isxs) isys = Cons (appendIsListLemma isxs isys)
+appendIsListLemma LP_Nil         isys = isys
+appendIsListLemma (LP_Cons isxs) isys = LP_Cons (appendIsListLemma isxs isys)
 
 -- |Appending type-level lists
 type family (:++:) (txs :: [k]) (tys :: [k]) :: [k] where
@@ -179,35 +187,19 @@
 type L3 xs ys zs    = (IsList xs, IsList ys, IsList zs) 
 type L4 xs ys zs as = (IsList xs, IsList ys, IsList zs, IsList as) 
 
--- TODO: VCM: looking at the implementation for the instances
---            in Generics.MRSOP.Opaque, it seems like we don't really need this.
-
--- |Higher order version of 'Eq'
-class EqHO (f :: ki -> *) where
-  eqHO :: forall k . f k -> f k -> Bool
-
-instance Eq a => EqHO (Const a) where
-  eqHO (Const a) (Const b) = a == b
-
-instance (EqHO f, EqHO g) => EqHO (Product f g) where
-  eqHO (Pair fx gx) (Pair fy gy) = eqHO fx fy && eqHO gx gy
-
-instance (EqHO f, EqHO g) => EqHO (Sum f g) where
-  eqHO (InL fx) (InL fy) = eqHO fx fy
-  eqHO (InR gx) (InR gy) = eqHO gx gy
-  eqHO _        _        = False
-
--- |Higher order version of 'Show'
-class ShowHO (f :: ki -> *) where
-  showHO :: forall k . f k -> String
+-- |Constraint synonym replacing the old @EqHO@ hack.
+-- @since 2.2.0
+type EqHO   f = forall x . Eq   (f x)
 
-instance Show a => ShowHO (Const a) where
-  showHO (Const a) = show a
+-- |Constraint synonym replacing the old @ShowHO@ hack.
+-- @since 2.2.0
+type ShowHO f = forall x . Show (f x)
 
-instance (ShowHO f , ShowHO g) => ShowHO (Product f g) where
-  showHO (Pair x y) = "(" ++ showHO x ++ ", " ++ showHO y ++ ")"
+instance (EqHO f , EqHO g) => Eq ((f :*: g) x) where
+  (fx :*: gx) == (fy :*: gy) = fx == fy && gx == gy
 
-instance (ShowHO f , ShowHO g) => ShowHO (Sum f g) where
-  showHO (InL fx) = "InL " ++ showHO fx
-  showHO (InR gx) = "InR " ++ showHO gx
+instance (EqHO f , EqHO g) => Eq (Sum f g x) where
+  (InL x) == (InL y) = x == y
+  (InR x) == (InR y) = x == y
+  _       == _       = False
 
diff --git a/src/Generics/MRSOP/Zipper.hs b/src/Generics/MRSOP/Zipper.hs
--- a/src/Generics/MRSOP/Zipper.hs
+++ b/src/Generics/MRSOP/Zipper.hs
@@ -12,7 +12,7 @@
 --  universe.
 module Generics.MRSOP.Zipper where
 
-import Generics.MRSOP.Base hiding (Cons , Nil)
+import Generics.MRSOP.Base 
 
 -- |In a @Zipper@, a Location is a a pair of a one hole context
 --  and whatever was supposed to be there. In a sums of products
@@ -24,7 +24,7 @@
 -- |A @Ctxs ki fam codes ix iy@ represents a value of type @El fam ix@
 --  with a @El fam iy@-typed hole in it.
 data Ctxs :: (kon -> *) -> [*] -> [[[Atom kon]]] -> Nat -> Nat -> * where
-  Nil  :: Ctxs ki fam cs ix ix
+  CNil :: Ctxs ki fam cs ix ix
   Cons :: (IsNat ix , IsNat a , IsNat b)
        => Ctx ki fam (Lkup ix cs) b -> Ctxs ki fam cs a ix
        -> Ctxs ki fam cs a b
@@ -52,7 +52,7 @@
 --  with the existential because we don't know, a priori, what
 --  will be the type of such hole.
 mkNPHole :: PoA ki (El fam) xs -> Maybe (NPHoleE ki fam xs)
-mkNPHole NP0 = Nothing
+mkNPHole Nil = Nothing
 mkNPHole (NA_I x :* xs) = Just (ExistsIX x (H xs))
 mkNPHole (NA_K k :* xs)
   = do (ExistsIX el c) <- mkNPHole xs
@@ -93,7 +93,7 @@
 -- take zippers over a deep representation
 fillCtxs :: forall ix fam iy ki c. (IsNat ix, Family ki fam c) => El fam iy -> Ctxs ki fam c ix iy -> El fam ix
 -- not sure if this should be h or Nothing
-fillCtxs h Nil = h
+fillCtxs h CNil = h
 fillCtxs h (Cons ctx ctxs) =
   fillCtxs (sto @fam @ki @c $ fill h ctx) ctxs
 
@@ -117,13 +117,13 @@
 -- |Move one layer upwards within the recursive structure
 up :: (Family ki fam codes, IsNat ix)
    => Loc ki fam codes ix -> Maybe (Loc ki fam codes ix)
-up (Loc _  Nil)             = Nothing
+up (Loc _  CNil)            = Nothing
 up (Loc el (Cons ctx ctxs)) = Just (Loc (sto $ fill el ctx) ctxs)
 
 -- |More one hole to the right
 right :: (Family ki fam codes, IsNat ix)
       => Loc ki fam codes ix -> Maybe (Loc ki fam codes ix)
-right (Loc _  Nil)             = Nothing
+right (Loc _  CNil)            = Nothing
 right (Loc el (Cons ctx ctxs)) = next (\el' ctx' -> Loc el' (Cons ctx' ctxs)) el ctx
 
 -- * Interface
@@ -131,13 +131,13 @@
 -- |Initializes the zipper
 enter :: (Family ki fam codes , IsNat ix)
       => El fam ix -> Loc ki fam codes ix
-enter el = Loc el Nil
+enter el = Loc el CNil
 
 -- |Exits the zipper
 leave :: (Family ki fam codes , IsNat ix)
       => Loc ki fam codes ix -> El fam ix
-leave (Loc x Nil) = x
-leave loc         = maybe undefined leave $ up loc -- up returns a just!
+leave (Loc x CNil) = x
+leave loc          = maybe undefined leave $ up loc -- up returns a just!
 
 -- |Updates the value in the hole.
 update :: (Family ki fam codes , IsNat ix)
diff --git a/src/Generics/MRSOP/Zipper/Deep.hs b/src/Generics/MRSOP/Zipper/Deep.hs
deleted file mode 100644
--- a/src/Generics/MRSOP/Zipper/Deep.hs
+++ /dev/null
@@ -1,98 +0,0 @@
-{-# LANGUAGE RankNTypes           #-}
-{-# LANGUAGE FlexibleContexts     #-}
-{-# LANGUAGE FlexibleInstances    #-}
-{-# LANGUAGE FlexibleInstances    #-}
-{-# LANGUAGE GADTs                #-}
-{-# LANGUAGE TypeOperators        #-}
-{-# LANGUAGE DataKinds            #-}
-{-# LANGUAGE PolyKinds            #-}
-{-# LANGUAGE ScopedTypeVariables  #-}
-{-# LANGUAGE TypeApplications     #-}
--- | Provides one-hole contexts for our universe, but over
---   deep encoded datatypes. These are a bit easier to use
---   computationally.
---
---   This module follows the very same structure as 'Generics.MRSOP.Zipper'.
---   Refer there for further documentation.
-module Generics.MRSOP.Zipper.Deep where
-import Control.Monad (guard)
-import Data.Proxy
-
-import Generics.MRSOP.Base hiding (Cons , Nil)
-
--- |Analogous to 'Generics.MRSOP.Zipper.Ctxs'
-data Ctxs (ki :: kon -> *) (codes :: [[[Atom kon]]]) :: Nat -> Nat -> * where
-  Nil  :: Ctxs ki codes ix ix
-  Cons :: (IsNat ix, IsNat a, IsNat b)
-       => Ctx ki codes (Lkup ix codes) b
-       -> Ctxs ki codes a ix
-       -> Ctxs ki codes a b
-
--- |Analogous to 'Generics.MRSOP.Zipper.Ctx'
-data Ctx (ki :: kon -> *) (codes :: [[[Atom kon]]]) :: [[Atom kon]] -> Nat -> * where
-  Ctx :: Constr c n -> NPHole ki codes ix (Lkup n c) -> Ctx ki codes c ix
-
--- |Analogous to 'Generics.MRSOP.Zipper.NPHole', but uses a deep representation
---  for generic values.
-data NPHole (ki :: kon -> *) (codes :: [[[Atom kon]]]) :: Nat -> [Atom kon] -> * where
-  H :: PoA ki (Fix ki codes) xs -> NPHole ki codes ix ('I ix ': xs)
-  T :: NA ki (Fix ki codes) x
-    -> NPHole ki codes ix xs
-    -> NPHole ki codes ix (x ': xs)
-
-getCtxsIx :: Ctxs ki codes iy ix -> Proxy ix
-getCtxsIx _ = Proxy
-
--- | Given a product with a hole in it, and an element, get back
--- a product
---
--- dual of 'removeNPHole'
-fillNPHole :: IsNat ix
-           => Fix ki codes ix
-           -> NPHole ki codes ix xs
-           -> PoA ki (Fix ki codes) xs
-fillNPHole x (H xs) = NA_I x :* xs
-fillNPHole x (T y ys) = y :* fillNPHole x ys
-
--- |Given a value that fits in a context, fills the context hole.
-fillCtxs :: (IsNat ix)
-         => Fix ki codes iy -> Ctxs ki codes ix iy -> Fix ki codes ix
-fillCtxs h Nil = h
-fillCtxs h (Cons ctx ctxs) = fillCtxs (Fix $ fillCtx h ctx) ctxs
-
-fillCtx :: (IsNat ix)
-        => Fix ki codes ix
-        -> Ctx ki codes c ix
-        -> Rep ki (Fix ki codes) c
-fillCtx x (Ctx c nphole) = inj c (fillNPHole x nphole)
-
--- |Given a value and a context, tries to match to context
--- in the value and, upon success, returns whatever overlaps with
--- the hole.
-removeCtxs :: (EqHO ki, IsNat ix)
-           => Ctxs ki codes ix iy
-           -> Fix ki codes ix
-           -> Maybe (Fix ki codes iy)
-removeCtxs Nil f = pure f
-removeCtxs (Cons ctx ctxs) (Fix r) = do
-    (Fix t) <- removeCtxs ctxs (Fix r)
-    removeCtx t ctx
-  
-removeCtx :: forall ix ki codes c
-           . (EqHO ki, IsNat ix)
-          => Rep ki (Fix ki codes) c
-          -> Ctx ki codes c ix
-          -> Maybe (Fix ki codes ix)
-removeCtx x (Ctx c npHole) =
-  match c x >>= removeNPHole npHole
-
-removeNPHole :: (EqHO ki, IsNat ix)
-             => NPHole ki codes ix xs
-             -> PoA ki (Fix ki codes) xs
-             -> Maybe (Fix ki codes ix)
-removeNPHole (H ys) (NA_I x :* xs) = do
-  guard $ eqHO xs ys
-  pure x
-removeNPHole (T y ys) (x :* xs) = do
-  guard $ eqHO x y
-  removeNPHole ys xs