diff --git a/README.md b/README.md
--- a/README.md
+++ b/README.md
@@ -1,6 +1,8 @@
 # generics-mrsop
 
-Generic Programming for Mutually Recursive Families in the
+Generic Programming, with combinators, for Mutually Recursive Families in the
 Sums of Products style.
 
-Check the `Generics.MRSOP.Examples.RoseTreeTH` for a quick start.
+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,5 +1,5 @@
 name:                generics-mrsop
-version:             1.0.0.1
+version:             1.2.2
 
 synopsis:            Generic Programming with Mutually Recursive Sums of Products.
 
@@ -20,7 +20,8 @@
 build-type:          Simple
 
 extra-source-files:  ChangeLog.md, README.md
-cabal-version:       2.0
+cabal-version:       1.24
+tested-with:         GHC == 8.2.2, GHC == 8.4.2
 
 
 library
@@ -38,10 +39,12 @@
     Generics.MRSOP.Util,
     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.Examples.SimpTH,
+    Generics.MRSOP.AG
 
   other-extensions: 
     MultiParamTypeClasses,
@@ -59,7 +62,7 @@
     FunctionalDependencies,
     ScopedTypeVariables
 
-  build-depends:       base >= 4.9 && <= 4.12,
+  build-depends:       base >= 4.9 && <= 5,
                        containers,
                        template-haskell,
                        mtl
@@ -76,4 +79,4 @@
 source-repository this
   type:     git
   location: https://github.com/VictorCMiraldo/generics-mrsop
-  tag:      1.0.0.0
+  tag: v1.2.2
diff --git a/src/Generics/MRSOP/AG.hs b/src/Generics/MRSOP/AG.hs
new file mode 100644
--- /dev/null
+++ b/src/Generics/MRSOP/AG.hs
@@ -0,0 +1,179 @@
+{-# LANGUAGE RankNTypes #-}
+{-# LANGUAGE PolyKinds #-}
+{-# LANGUAGE DataKinds #-}
+{-# LANGUAGE TypeApplications #-}
+{-# LANGUAGE KindSignatures #-}
+{-# LANGUAGE ScopedTypeVariables #-}
+{-# LANGUAGE GADTs #-}
+
+-- | Attribute grammars over mutual recursive datatypes
+module Generics.MRSOP.AG where
+
+import Data.Coerce
+import Data.Foldable (fold)
+import Data.Functor.Const
+import Data.Functor.Product
+import Data.Monoid (Sum(..), (<>))
+import Generics.MRSOP.Base
+import Generics.MRSOP.Util
+
+zipAnn :: forall phi1 phi2 phi3 ki codes ix.
+          (forall iy. phi1 iy -> phi2 iy -> phi3 iy)
+       -> AnnFix ki codes phi1 ix
+       -> AnnFix ki codes phi2 ix
+       -> AnnFix ki codes phi3 ix
+zipAnn f (AnnFix a1 t1) (AnnFix a2 t2) = AnnFix (f a1 a2) (zipWithRep t1 t2)
+  where
+    zipWithRep :: Rep ki (AnnFix ki codes phi1) xs
+               -> Rep ki (AnnFix ki codes phi2) xs
+               -> Rep ki (AnnFix ki codes phi3) xs
+    zipWithRep (Rep x) (Rep y) = Rep $ zipWithNS x y
+    zipWithNS :: NS (PoA ki (AnnFix ki codes phi1)) ys
+              -> NS (PoA ki (AnnFix ki codes phi2)) ys
+              -> NS (PoA ki (AnnFix ki codes phi3)) ys
+    zipWithNS (Here x) (Here y)   = Here $ zipWithNP x y
+    zipWithNS (There x) (There y) = There $ zipWithNS x y
+    zipWithNP :: PoA ki (AnnFix ki codes phi1) zs
+              -> PoA ki (AnnFix ki codes phi2) zs
+              -> PoA ki (AnnFix ki codes phi3) zs
+    zipWithNP NP0 NP0 = NP0
+    zipWithNP (a :* as) (b :* bs) = zipWithNA a b :* zipWithNP as bs
+    zipWithNA :: NA ki (AnnFix ki codes phi1) ws
+              -> NA ki (AnnFix ki codes phi2) ws
+              -> NA ki (AnnFix ki codes phi3) ws
+    zipWithNA (NA_I t1) (NA_I t2) = NA_I (zipAnn f t1 t2)
+    zipWithNA (NA_K i1) (NA_K i2) = NA_K i1  -- Should be the same!
+
+mapAnn :: (forall iy. chi iy -> phi iy)
+       -> AnnFix ki codes chi ix
+       -> AnnFix ki codes phi ix
+mapAnn f = synthesizeAnn (\x _ -> f x)
+
+-- HACK. why doesn't haskell have this instance?
+instance Show k => Show1 (Const k) where
+  show1 (Const x) = show x
+
+instance (Show1 f, Show1 g) => Show1 (Product f g) where
+  show1 (Pair x y) = "(" ++ show1 x ++ ", " ++ show1 y ++ ")"
+
+-- | Inherited attributes
+
+inheritAnn ::
+     forall ki codes chi phi ix.
+     (forall iy. chi iy -> Rep ki (Const ()) (Lkup iy codes) -> phi iy -> Rep ki phi (Lkup iy codes))
+  -> phi ix
+  -> AnnFix ki codes chi ix
+  -> AnnFix ki codes phi ix
+inheritAnn f start (AnnFix ann rep) =
+  let newFix = f ann (mapRep (const (Const ())) rep) start
+      zipWithRep ::
+           Rep ki (AnnFix ki codes chi) xs
+        -> Rep ki phi xs
+        -> Rep ki (AnnFix ki codes phi) xs
+      zipWithRep (Rep x) (Rep y) = Rep $ zipWithNS x y
+      zipWithNS ::
+           NS (PoA ki (AnnFix ki codes chi)) ys
+        -> NS (PoA ki phi) ys
+        -> NS (PoA ki (AnnFix ki codes phi)) ys
+      zipWithNS (Here x) (Here y) = Here $ zipWithNP x y
+      zipWithNS (There x) (There y) = There $ zipWithNS x y
+      zipWithNP ::
+           PoA ki (AnnFix ki codes chi) zs
+        -> PoA ki phi zs
+        -> PoA ki (AnnFix ki codes phi) zs
+      zipWithNP NP0 NP0 = NP0
+      zipWithNP (a :* as) (b :* bs) = zipWithNA a b :* zipWithNP as bs
+      zipWithNA ::
+           NA ki (AnnFix ki codes chi) ws
+        -> NA ki phi ws
+        -> NA ki (AnnFix ki codes phi) ws
+      zipWithNA (NA_I i1) (NA_I i2) = NA_I (inheritAnn f i2 i1)
+      zipWithNA (NA_K i1) (NA_K i2) = NA_K i1
+   in AnnFix start (zipWithRep rep newFix)
+
+inherit ::
+     forall ki phi codes ix.
+     (forall iy. Rep ki (Const ()) (Lkup iy codes) -> phi iy -> Rep ki phi (Lkup iy codes))
+  -> phi ix
+  -> Fix ki codes ix
+  -> AnnFix ki codes phi ix
+inherit f start (Fix rep) =
+  let newFix = (f (mapRep (const (Const ())) rep) start)
+      zipWithRep ::
+           Rep ki (Fix ki codes) xs
+        -> Rep ki phi xs
+        -> Rep ki (AnnFix ki codes phi) xs
+      zipWithRep (Rep x) (Rep y) = Rep $ zipWithNS x y
+      zipWithNS ::
+           NS (PoA ki (Fix ki codes)) ys
+        -> NS (PoA ki phi) ys
+        -> NS (PoA ki (AnnFix ki codes phi)) ys
+      zipWithNS (Here x) (Here y) = Here $ zipWithNP x y
+      zipWithNS (There x) (There y) = There $ zipWithNS x y
+      zipWithNP ::
+           PoA ki (Fix ki codes) zs
+        -> PoA ki phi zs
+        -> PoA ki (AnnFix ki codes phi) zs
+      zipWithNP NP0 NP0 = NP0
+      zipWithNP (a :* as) (b :* bs) = zipWithNA a b :* zipWithNP as bs
+      zipWithNA ::
+           NA ki (Fix ki codes) ws
+        -> NA ki phi ws
+        -> NA ki (AnnFix ki codes phi) ws
+      zipWithNA (NA_I i1) (NA_I i2) = NA_I (inherit f i2 i1)
+      zipWithNA (NA_K i1) (NA_K i2) = NA_K i1
+   in AnnFix start (zipWithRep rep newFix)
+
+-- | Synthesized attributes
+
+synthesizeAnn ::
+     forall ki codes chi phi ix.
+     (forall iy. chi iy -> Rep ki phi (Lkup iy codes) -> phi iy)
+  -> AnnFix ki codes chi ix
+  -> AnnFix ki codes phi ix
+synthesizeAnn f = annCata alg
+  where
+    alg ::
+         forall iy.
+         chi iy
+      -> Rep ki (AnnFix ki codes phi) (Lkup iy codes)
+      -> AnnFix ki codes phi iy
+    alg ann rep = AnnFix (f ann (mapRep getAnn rep)) rep
+    
+
+synthesize :: forall ki phi codes ix
+            . (IsNat ix)
+           => (forall iy . (IsNat iy) => Rep ki phi (Lkup iy codes) -> phi iy)
+           -> Fix ki codes ix
+           -> AnnFix ki codes phi ix
+synthesize f = cata alg
+  where
+    alg :: forall iy
+         . (IsNat iy)
+        => Rep ki (AnnFix ki codes phi) (Lkup iy codes)
+        -> AnnFix ki codes phi iy
+    alg xs = AnnFix (f (mapRep getAnn xs)) xs
+
+monoidAlgebra :: Monoid m => Rep ki (Const m) xs -> Const m iy
+monoidAlgebra = elimRep mempty coerce fold
+
+-- If haskell had semirings in base, or edward kmett had a package for it
+-- we could do :
+-- semiringAlgebra :: Semiring w => Rep ki (Const w) xs -> Const w iy
+-- semiringAlgebra = (one <>) . monoidAlgebra
+--
+-- sizeAlgebra :: Rep ki (Const (Sum Int)) xs -> Const (Sum Int) iy
+-- sizeAlgebra = semiringAlgebra
+
+sizeAlgebra :: Rep ki (Const (Sum Int)) xs -> Const (Sum Int) iy
+sizeAlgebra = (Const 1 <>) . monoidAlgebra
+
+-- | Annotate each node with the number of subtrees
+sizeGeneric' :: (IsNat ix)
+             => Fix ki codes ix -> AnnFix ki codes (Const (Sum Int)) ix
+sizeGeneric' = synthesize sizeAlgebra
+
+-- | Count the number of nodes
+sizeGeneric :: (IsNat ix)
+            => Fix ki codes ix -> Const (Sum Int) ix
+sizeGeneric = cata sizeAlgebra
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
@@ -12,6 +12,7 @@
 -- |Provides the main class of the library, 'Family'.
 module Generics.MRSOP.Base.Class where
 
+import Data.Functor.Const
 import Data.Function (on)
 
 import Generics.MRSOP.Base.Universe
@@ -89,5 +90,5 @@
 deep :: forall fam ty ki codes ix
       . (Family ki fam codes,
          ix ~ Idx ty fam, Lkup ix fam ~ ty, IsNat ix)
-     => ty -> Fix ki codes ix
+     => ty -> AnnFix ki codes (Const ()) ix
 deep = dfrom . into
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
@@ -85,18 +85,17 @@
 
 -- |Given a 'Family', provides the 'DatatypeInfo' for the type
 --  with index @ix@ in family 'fam'.
-class (Family ki fam codes) => HasDatatypeInfo ki fam codes ix
+class (Family ki fam codes) => HasDatatypeInfo ki fam codes
     | fam -> codes ki where
-  datatypeInfo :: (IsNat ix)
-               => Proxy fam -> Proxy ix -> DatatypeInfo (Lkup ix codes)
+  datatypeInfo :: Proxy fam -> SNat ix -> DatatypeInfo (Lkup ix codes)
 
 -- |Sometimes it is more convenient to use a proxy of the type
 --  in the family instead of indexes.
 datatypeInfoFor :: forall ki fam codes ix ty
-                 . ( HasDatatypeInfo ki fam codes ix
+                 . ( HasDatatypeInfo ki fam codes
                    , ix ~ Idx ty fam , Lkup ix fam ~ ty , IsNat ix)
                 => Proxy fam -> Proxy ty -> DatatypeInfo (Lkup ix codes)
-datatypeInfoFor pf pty = datatypeInfo pf (proxyIdx pf pty)
+datatypeInfoFor pf pty = datatypeInfo pf (getSNat $ proxyIdx pf pty)
   where
     proxyIdx :: Proxy fam -> Proxy ty -> Proxy (Idx ty fam)
     proxyIdx _ _ = Proxy
@@ -113,4 +112,14 @@
     go CZ     (ci :* _)   = ci
     go (CS c) (_  :* cis) = go c cis
 
+
+-- |Returns the constructor information for a given
+--  type in the family.
+constrInfoFor :: (HasDatatypeInfo ki fam codes)
+              => Proxy fam
+              -> SNat ix
+              -> Constr (Lkup ix codes) c
+              -> ConstructorInfo (Lkup c (Lkup ix codes))
+constrInfoFor pfam six c = constrInfoLkup c (datatypeInfo pfam six)
+               
 
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
@@ -18,6 +18,11 @@
   NP0  :: NP p '[]
   (:*) :: p x -> NP p xs -> NP p (x : xs)
 
+
+instance Eq1 ki => Eq1 (NP ki) where
+  eq1 = eqNP eq1
+  
+
 -- * Relation to IsList predicate
 
 -- |Append two values of type 'NP'
@@ -59,6 +64,11 @@
 zipNP NP0       NP0       = NP0
 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 ((f :*: g) :* fgs) = (f :*) *** (g :*) $ unzipNP fgs
+
 -- * Catamorphism
 
 -- |Consumes a value of type 'NP'.
@@ -67,6 +77,16 @@
        -> NP f xs -> r xs
 cataNP fCons fNil NP0       = fNil
 cataNP fCons fNil (k :* ks) = fCons k (cataNP fCons fNil ks)
+
+
+-- |Consumes a value of type 'NP'.
+cataNPM :: (Monad m)
+        => (forall x xs . f x  -> r xs -> m (r (x : xs)))
+        -> m (r '[])
+        -> NP f xs -> m (r xs)
+cataNPM fCons fNil NP0       = fNil
+cataNPM fCons fNil (k :* ks) = cataNPM fCons fNil ks >>= fCons k 
+
 
 -- * Equality
 
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
@@ -20,6 +20,9 @@
   There :: NS p xs -> NS p (x : xs)
   Here  :: p x     -> NS p (x : xs)
 
+instance Eq1 ki => Eq1 (NS ki) where
+  eq1 = eqNS eq1
+
 -- * Map, Zip and Elim
 
 -- |Maps over a sum
diff --git a/src/Generics/MRSOP/Base/Show.hs b/src/Generics/MRSOP/Base/Show.hs
--- a/src/Generics/MRSOP/Base/Show.hs
+++ b/src/Generics/MRSOP/Base/Show.hs
@@ -20,7 +20,7 @@
 import Generics.MRSOP.Util
 
 -- https://stackoverflow.com/questions/9082642/implementing-the-show-class
-instance (Show (fam k)) => Show (NA ki fam (I k)) where
+{-instance (Show (fam k)) => Show (NA ki fam (I k)) where
   showsPrec p (NA_I v) = showParen (p > 10) $ showString "I " . showsPrec 11 v
 instance (Show (ki  k)) => Show (NA ki fam (K k)) where
   showsPrec p (NA_K v) = showParen (p > 10) $ showString "K " . showsPrec 11 v
@@ -42,9 +42,37 @@
 -- TODO:
 -- This needs undecidable instances. We don't like undecidable instances
 instance Show (NS (PoA ki phi) code) => Show (Rep ki phi code) where
-  show (Rep x) = show x
+  show (Rep x) =
+-}
 
-instance Show (NS (PoA ki (Fix ki codes)) (Lkup ix codes))
-      => Show (Fix ki codes ix)
-    where
-  show (Fix x) = show x
+
+instance (Show1 phi, Show1 ki) => Show (NA ki (AnnFix ki codes phi) a) where
+  show = showNA
+
+showNA :: (Show1 phi, Show1 ki) => NA ki (AnnFix ki codes phi) a -> String
+showNA (NA_I i) = "(NA_I " ++ showFix i ++ ")"
+showNA (NA_K k) = "(NA_K " ++ show1 k ++ ")"
+
+instance (Show1 phi, Show1 ki) => Show (PoA ki (AnnFix ki codes phi) xs) where
+  show = showNP
+
+showNP :: (Show1 phi, Show1 ki) => PoA ki (AnnFix ki codes phi) xs -> String
+showNP NP0 = "NP0"
+showNP (a :* b) = showNA a ++ " :* " ++ showNP b
+
+instance (Show1 phi, Show1 ki) => Show (Rep ki (AnnFix ki codes phi) xs) where
+  show = showRep
+  
+showRep :: (Show1 phi, Show1 ki) => Rep ki (AnnFix ki codes phi) xs -> String
+showRep x =
+  case sop x of
+    Tag c poa -> 
+      "(" ++ show c ++ " " ++ showNP poa ++ ")"
+   
+
+instance (Show1 phi, Show1 ki) => Show (AnnFix ki codes phi ix) where
+  show = showFix
+
+showFix :: (Show1 phi, Show1 ki) => AnnFix ki codes phi ix -> String
+showFix (AnnFix a x) = "(" ++ show1 a ++  " " ++ showRep x  ++ ")"
+
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
@@ -5,6 +5,7 @@
 {-# LANGUAGE TypeOperators        #-}
 {-# LANGUAGE DataKinds            #-}
 {-# LANGUAGE PolyKinds            #-}
+{-# LANGUAGE PatternSynonyms      #-}
 {-# LANGUAGE ScopedTypeVariables  #-}
 {-# LANGUAGE TypeApplications     #-}
 -- |Wraps the definitions of 'NP' and 'NS'
@@ -16,6 +17,7 @@
 import Data.Type.Equality
 import Data.Proxy
 
+import Data.Functor.Const
 import Control.Monad
 
 import Generics.MRSOP.Base.NS
@@ -38,6 +40,7 @@
   | I Nat
   deriving (Eq, Show)
 
+
 -- |@NA ki phi a@ provides an interpretation for an atom @a@,
 --  using either @ki@ or @phi@ to interpret the type variable
 --  or opaque type.
@@ -45,6 +48,29 @@
   NA_I :: (IsNat k) => phi k -> NA ki phi (I k) 
   NA_K ::              ki  k -> NA ki phi (K k)
 
+instance (Eq1 phi, Eq1 ki) => Eq1 (NA ki phi) where
+  eq1 = eqNA eq1 eq1
+
+
+instance (TestEquality ki) => TestEquality (NA ki phi) where
+  testEquality (NA_I i) (NA_K k) = Nothing
+  testEquality (NA_K i) (NA_I k) = Nothing
+  testEquality (NA_I i) (NA_I i') =
+    case testEquality (sNatFixIdx i) (sNatFixIdx i') of
+      Just Refl -> Just Refl
+      Nothing -> Nothing
+  testEquality (NA_K k) (NA_K k') =
+    -- we learn that
+    -- a ~ (K k1)
+    -- b ~ (K k2)
+    case testEquality k k' of
+      -- we learn that  k1 ~ k2
+      Just Refl ->
+        -- thus we learn that a ~ b. Q.e.d
+        Just Refl
+      Nothing -> Nothing
+
+
 -- ** Map, Elim and Zip
 
 -- |Maps a natural transformation over an atom interpretation
@@ -94,6 +120,9 @@
 newtype Rep (ki :: kon -> *) (phi :: Nat -> *) (code :: [[Atom kon]])
   = Rep { unRep :: NS (PoA ki phi) code }
 
+instance (Eq1 phi, Eq1 ki) => Eq1 (Rep ki phi) where
+  eq1 = eqRep eq1 eq1
+  
 -- |Product of Atoms is a handy synonym to have.
 type PoA (ki :: kon -> *) (phi :: Nat -> *) = NP (NA ki phi)
 
@@ -156,8 +185,8 @@
   = cat <.> elimNS (elimNPM (elimNA fk fi)) . unRep
 
 -- |Pure eliminator.
-elimRep :: (forall k . ki k -> a)
-        -> (forall k . f  k -> a)
+elimRep :: (forall k .            ki k -> a)
+        -> (forall k . IsNat k => f  k -> a)
         -> ([a] -> b)
         -> Rep ki f c -> b
 elimRep kp fp cat
@@ -216,7 +245,7 @@
 -- |Finally, we can view a sum-of-products as a constructor
 --  and a product-of-atoms.
 data View :: (kon -> *) -> (Nat -> *) -> [[ Atom kon ]] -> * where
-  Tag :: Constr sum n -> PoA ki fam (Lkup n sum) -> View ki fam sum
+  Tag :: IsNat n => Constr sum n -> PoA ki fam (Lkup n sum) -> View ki fam sum
 
 -- |Unwraps a 'Rep' into a 'View'
 sop :: Rep ki fam sum -> View ki fam sum
@@ -227,6 +256,10 @@
     go (There s)   = case go s of
                         Tag c poa -> Tag (CS c) poa
 
+-- |Wraps a 'View' into a 'Rep'
+fromView :: View ki fam sum -> Rep ki fam sum
+fromView (Tag c x) = inj c x
+
 -- * Least Fixpoints
 --
 -- $leastFixpoints
@@ -237,13 +270,54 @@
 -- the representation of the code indexed by ix
 
 -- |Indexed least fixpoints
-newtype Fix (ki :: kon -> *) (codes :: [[[ Atom kon ]]]) (n :: Nat)
+{-newtype Fix (ki :: kon -> *) (codes :: [[[ Atom kon ]]]) (n :: Nat)
   = Fix { unFix :: Rep ki (Fix ki codes) (Lkup n codes) }
+-}
 
+
+-- | Annotated version of Fix.   This is basically the 'Cofree' datatype,
+-- but for n-ary functors
+data AnnFix (ki :: kon -> *) (codes :: [[[Atom kon]]]) (phi :: Nat -> *) (n :: Nat) =
+  AnnFix (phi n)
+         (Rep ki (AnnFix ki codes phi) (Lkup n codes))
+
+type Fix ki codes = AnnFix ki codes (Const ())
+
+pattern Fix x = AnnFix (Const ()) x
+
+unFix :: Fix ki codes ix -> Rep ki (Fix ki codes) (Lkup ix codes)
+unFix (Fix x) = x
+
+-- | Catamorphism over fixpoints
+cata :: (IsNat ix)
+  => (forall iy. IsNat iy => Rep ki phi (Lkup iy codes) -> phi iy)
+  -> Fix ki codes ix
+  -> phi ix
+cata f (Fix x) = f (mapRep (cata f) x)
+
+
+getAnn :: AnnFix ki codes ann ix -> ann ix
+getAnn (AnnFix a x) = a
+
+annCata :: (forall iy. chi iy -> Rep ki phi (Lkup iy codes) -> phi iy)
+        -> AnnFix ki codes chi ix
+        -> phi ix
+annCata f (AnnFix a x) = f a (mapRep (annCata f) x)
+
+-- | Forget the annotations
+forgetAnn :: AnnFix ki codes a ix -> Fix ki codes ix
+forgetAnn (AnnFix _ rep) = Fix (mapRep forgetAnn rep)
+
+instance Eq1 ki => Eq1 (Fix ki codes) where
+  eq1 = eqFix eq1
+
 -- |Retrieves the index of a 'Fix'
-proxyFixIdx :: Fix ki fam ix -> Proxy ix
+proxyFixIdx :: phi ix -> Proxy ix
 proxyFixIdx _ = Proxy
 
+sNatFixIdx :: IsNat ix => phi ix -> SNat ix
+sNatFixIdx x = getSNat (proxyFixIdx x)
+
 -- |Maps over the values of opaque types within the
 --  fixpoint.
 mapFixM :: (Monad m)
@@ -256,9 +330,13 @@
       -> Fix ki fam ix -> Fix ki fam ix -> Bool
 eqFix p = eqRep p (eqFix p) `on` unFix
 
+instance Eq1 ki => Eq  (Fix ki codes ix) where
+  (==) = eqFix eq1
+
 -- |Compare two indexes of two fixpoints
 --  Note we can't use a 'testEquality' instance because
 --  of the 'IsNat' constraint.
 heqFixIx :: (IsNat ix , IsNat ix')
          => Fix ki fam ix -> Fix ki fam ix' -> Maybe (ix :~: ix')
 heqFixIx fa fb = testEquality (getSNat Proxy) (getSNat Proxy)
+
diff --git a/src/Generics/MRSOP/Examples/LambdaAlphaEqTH.hs b/src/Generics/MRSOP/Examples/LambdaAlphaEqTH.hs
--- a/src/Generics/MRSOP/Examples/LambdaAlphaEqTH.hs
+++ b/src/Generics/MRSOP/Examples/LambdaAlphaEqTH.hs
@@ -82,10 +82,6 @@
 
 type FIX = Fix Singl CodesTerm
 
-pattern Term_    = SZ
-pattern Var_ s   = Tag CZ (NA_K s :* NP0)
-pattern Abs_ x t = Tag (CS CZ) (NA_K x :* NA_I t :* NP0)
-
 -- |Decides whether or not two terms are alpha equivalent.
 alphaEq :: Term -> Term -> Bool
 alphaEq x y = runAlpha $ galphaEqT (deep @FamTerm x) (deep @FamTerm y)
@@ -110,12 +106,12 @@
        => SNat ix -> Rep (Singl :*: Singl) (FIX :*: FIX)
                          (Lkup ix CodesTerm)
        -> m Bool
-    go Term_ x = case sop x of
+    go IdxTerm x = case sop x of
       -- Without -XPolyKinds this is impossible; weird errors all over the place.
       Var_ (SString v1 :*: SString v2)
         -> v1 =~= v2
       Abs_ (SString v1 :*: SString v2) (t1 :*: t2)
-        -> onNewScope (addRule v1 v2 >> galphaEq Term_ t1 t2)
+        -> onNewScope (addRule v1 v2 >> galphaEq IdxTerm t1 t2)
       _ -> step x
 
 -- * Tests
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
@@ -56,15 +56,13 @@
   sto' (SS SZ) (Rep (There (Here (NA_K (SInt a) :* NP0))))
     = El (Leaf a)
 
-instance HasDatatypeInfo Singl FamRose CodesRose Z where
-  datatypeInfo _ _
+instance HasDatatypeInfo Singl FamRose CodesRose where
+  datatypeInfo _ SZ
     = ADT "module" (Name "[]" :@: (Name "R" :@: Name "Int"))
       $  (Constructor "[]")
       :* (Infix ":" RightAssociative 5)
       :* NP0
-
-instance HasDatatypeInfo Singl FamRose CodesRose (S Z) where
-  datatypeInfo _ _
+  datatypeInfo _ (SS SZ)
     = ADT "module" (Name "R" :@: Name "Int")
       $  (Infix ":>:" NotAssociative 0)
       :* (Constructor "Leaf")
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
@@ -55,24 +55,12 @@
 
 deriveFamily [t| Stmt String |]
 
-pattern Decl_ = SS (SS SZ)
-pattern Exp_  = SS SZ
-pattern Stmt_ = SZ
-
-pattern SAssign_ v e = Tag CZ (NA_K v :* NA_I e :* NP0)
-
-pattern DVar_ v     = Tag CZ (NA_K v :* NP0)
-pattern DFun_ f x s = Tag (CS CZ) (NA_K f :* NA_K x :* NA_I s :* NP0)
-
-pattern EVar_ v    = Tag CZ      (NA_K v :* NP0)
-pattern ECall_ f x = Tag (CS CZ) (NA_K f :* NA_I x :* NP0)
-
 type FIX = Fix Singl CodesStmtString
 
 -- * Alpha Equality Functionality
 
 alphaEqD :: Decl String -> Decl String -> Bool
-alphaEqD = (galphaEq Decl_) `on` (deep @FamStmtString)
+alphaEqD = (galphaEq IdxDeclString) `on` (deep @FamStmtString)
   where
     -- Generic programming boilerplate;
     -- could be removed. WE are just passing SNat
@@ -110,24 +98,24 @@
        -> Rep (Singl :*: Singl) (FIX :*: FIX)
               (Lkup iy CodesStmtString)
        -> m Bool
-    go Stmt_ x
+    go IdxStmtString x
       = case sop x of
-          SAssign_ (SString v1 :*: SString v2) e1e2
-            -> addRule v1 v2 >> uncurry' (galphaEq' Exp_) e1e2
+          StmtStringSAssign_ (SString v1 :*: SString v2) e1e2
+            -> addRule v1 v2 >> uncurry' (galphaEq' IdxExpString) e1e2
           otherwise
             -> step x
-    go Decl_ x
+    go IdxDeclString x
       = case sop x of
-          DVar_ (SString v1 :*: SString v2)
+          DeclStringDVar_ (SString v1 :*: SString v2)
             -> addRule v1 v2 >> return True
-          DFun_ (SString f1 :*: SString f2) (SString x1 :*: SString x2) s
+          DeclStringDFun_ (SString f1 :*: SString f2) (SString x1 :*: SString x2) s
             -> addRule f1 f2 >> onNewScope (addRule x1 x2 >> uncurry' galphaEqT s)
           _ -> step x
-    go Exp_ x
+    go IdxExpString x
       = case sop x of
-          EVar_ (SString v1 :*: SString v2)
+          ExpStringEVar_ (SString v1 :*: SString v2)
             -> v1 =~= v2
-          ECall_ (SString f1 :*: SString f2) e
+          ExpStringECall_ (SString f1 :*: SString f2) e
             -> (&&) <$> (f1 =~= f2) <*> uncurry' galphaEqT e
           _ -> step x 
     go _ x = step x
@@ -201,6 +189,6 @@
       $ into @FamStmtString (test4 10)
   where
     mk42 :: SNat ix -> El FamStmtString ix -> El FamStmtString ix
-    mk42 Exp_ _ = El $ ELit 42
-    mk42 _    x = x
+    mk42 IdxExpString _ = El $ ELit 42
+    mk42 _            x = x
 
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
@@ -15,6 +15,7 @@
 
 import Data.Function (on)
 import Data.Proxy
+import Data.Type.Equality
 
 import Generics.MRSOP.Util
 
@@ -64,3 +65,13 @@
 eqSingl :: Singl k -> Singl k -> Bool
 eqSingl = (==)
 
+instance TestEquality Singl where
+  testEquality (SInt _) (SInt _)         = Just Refl
+  testEquality (SInteger _) (SInteger _) = Just Refl
+  testEquality (SFloat _) (SFloat _)     = Just Refl
+  testEquality (SDouble _) (SDouble _)   = Just Refl
+  testEquality (SBool _) (SBool _)       = Just Refl
+  testEquality (SChar _) (SChar _)       = Just Refl
+  testEquality (SString _) (SString _)   = Just Refl
+  testEquality _ _                       = Nothing
+  
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
@@ -12,7 +12,12 @@
 --   We are borrowing a some code from generic-sop
 --   ( https://hackage.haskell.org/package/generics-sop-0.3.2.0/docs/src/Generics-SOP-TH.html )
 --
-module Generics.MRSOP.TH (deriveFamily, genFamilyDebug) where
+module Generics.MRSOP.TH
+  ( deriveFamilyWith
+  , deriveFamilyWithTy
+  , deriveFamily
+  , genFamilyDebug
+  ) where
 
 import Data.Function (on)
 import Data.Char (ord , isAlphaNum)
@@ -36,23 +41,34 @@
 
 import qualified Data.Map as M
 
+data OpaqueData = OpaqueData
+  { opaqueName   :: Name
+  -- | Map assigning a Haskell type to its corresponding promoted
+  --   Kon
+  , opaqueTable  :: M.Map Name Name
+  -- | Map assigning a promoted Kon to the constructor it uses
+  , opaqueCons   :: M.Map Name Name
+  } deriving (Eq , Show)
+
 -- |Given the name of the first element in the family,
 --  derives:
 --
 --    1. The other types in the family and Konstant types one needs.
 --    2. the SOP code for each of the datatypes involved
 --    3. One 'Element' instance per datatype
---    TODO: 4. Metadada information for each of the datatypes involved
-deriveFamily :: Q Type -> Q [Dec]
-deriveFamily t
+--    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 
-       (_ , (Idxs _ m)) <- runIdxsM (reifySTy sty)
+       opqData          <- reifyOpaqueType opqName
+       (_ , (Idxs _ m)) <- runIdxsM (reifySTy opqData sty)
        -- Now we make sure we have processed all
        -- types
        m' <- mapM extractDTI (M.toList m)
        let final = sortBy (compare `on` second) m' 
        dbg <- genFamilyDebug sty final
-       res <- genFamily sty final 
+       res <- genFamily opqData sty final 
        return (dbg ++ res)
   where
     second (_ , x , _) = x
@@ -62,6 +78,17 @@
     extractDTI (sty , (ix , Just dti))
       = return (sty , ix , dti)
 
+deriveFamilyWithTy :: Q Type -> Q Type -> Q [Dec]
+deriveFamilyWithTy opq ty
+  = do opqTy <- opq
+       case opqTy of
+         ConT opqName -> deriveFamilyWith opqName ty
+         _            -> fail $ "Type " ++ show opqTy ++ " must be a name!"
+
+deriveFamily :: Q Type -> Q [Dec]
+deriveFamily = deriveFamilyWith (mkName "Singl")
+
+
 -- Sketch;
 --
 --   Given a module:
@@ -128,6 +155,10 @@
 dtiMapM f (ADT name args ci) = ADT name args <$> mapM (ciMapM f) ci
 dtiMapM f (New name args ci) = New name args <$> ciMapM f ci
 
+dtiName :: DTI ty -> DataName
+dtiName (ADT name _ _) = name
+dtiName (New name _ _) = name
+
 dti2ci :: DTI ty -> [CI ty]
 dti2ci (ADT _ _ cis) = cis
 dti2ci (New _ _ ci)  = [ ci ]
@@ -326,9 +357,51 @@
 -- * Preprocessing Data * --
 ----------------------------
 
+-- |Given an opaque type name, return the name of the constructors
+--  that wrap which Haskell types.
+--
+--  This provides a way to customize what the generation engine
+--  sees as opaque types.
+--
+--  For instance, suppose,
+--
+--  > data MySingl :: * -> * where
+--  >   MyInt  :: Int  -> MySingl KInt
+--  >   MyBool :: Bool -> MySingl KBool
+--
+--  Then,
+--
+--  > reifyOpaqueType ''MySingl
+--  >  = M.fromList [(''Int , "KInt") , (''Bool, "KBool")]
+--  >  , M.fromList [("KInt" , "MyInt") , ("KBool" , "MyBool")]
+--
+reifyOpaqueType :: Name -> Q OpaqueData
+reifyOpaqueType opq
+  = do triples <- (extract <.> reifyDec) opq
+       let (hsTyMap , consMap) = genMaps triples
+       return $ OpaqueData opq hsTyMap consMap
+  where
+    genMaps :: [(Name , Name , Name)] -> (M.Map Name Name , M.Map Name Name)
+    genMaps xys = (M.fromList (map (\(x , y , _) -> (x , y)) xys)
+                 ,M.fromList (map (\(_ , x , y) -> (x , y)) xys))
+    
+    extract :: Dec -> Q [(Name , Name , Name)]
+    extract (DataD _ _ _ _ cs _) = mapM extractCon cs
+    extract _
+      = failMsg
+
+    extractCon :: Con -> Q (Name , Name , Name)
+    extractCon (GadtC [opqC] [(_ , ConT hsTy)] (AppT _ (PromotedT ty)))
+      = return (hsTy , ty , opqC)
+    extractCon _
+      = failMsg
+
+    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 :: STy -> M ()
-reifySTy sty
+reifySTy :: OpaqueData -> STy -> M ()
+reifySTy opq sty
   = do ix <- indexOf sty
        uncurry go (styFlatten sty)
   where
@@ -337,19 +410,19 @@
       = do dec <- lift (reifyDec name >>= decInfo)
            -- TODO: Check that the precondition holds.
            let res = dtiReduce dec args
-           (final , todo) <- runWriterT $ dtiMapM convertSTy res
+           (final , todo) <- runWriterT $ dtiMapM (convertSTy (opaqueTable opq)) res
            register sty final
-           mapM_ reifySTy todo
+           mapM_ (reifySTy opq) todo
     
     -- Convert the STy's in the fields of the constructors;
     -- tells a list of STy's we still need to process.
-    convertSTy :: STy -> WriterT [STy] M IK
-    convertSTy ty
+    convertSTy :: M.Map Name Name -> STy -> WriterT [STy] M IK
+    convertSTy opqTable ty
       -- We remove sty from the list of todos
       -- otherwise we get an infinite loop
       | ty == sty = AtomI <$> lift (indexOf ty)
       | isClosed ty
-      = case makeCons ty of
+      = case makeCons opqTable ty of
           Just k  -> return (AtomK k)
           Nothing -> do ix     <- lift (indexOf ty)
                         hasDti <- lift (hasData ty)
@@ -359,19 +432,9 @@
       = fail $ "I can't convert type variable " ++ show ty
               ++ " when converting " ++ show sty
 
-    makeCons :: STy -> Maybe Name
-    makeCons (ConST n) = M.lookup n consTable
-    makeCons _         = Nothing
-
-    consTable = M.fromList . map (id *** mkName)
-      $ [ ( ''Int     , "KInt")
-        , ( ''Char    , "KChar")
-        , ( ''Integer , "KInteger")
-        , ( ''Float   , "KFloat")
-        , ( ''Bool    , "KBool")
-        , ( ''String  , "KString")
-        , ( ''Double  , "KDouble")
-        ]
+    makeCons :: M.Map Name Name -> STy -> Maybe Name
+    makeCons opqTable (ConST n) = M.lookup n opqTable
+    makeCons opqTable _         = Nothing
 
 -----------------------------
 -- * Generating the Code * --
@@ -403,6 +466,14 @@
 -- > pattern HT0_ d = Here d
 -- > pattern HT1_ d = There (Here d)
 --
+--  TODO:
+--   This has an issue; if we import two modules with code generation
+--   the HT0, HT1, ... HTn names will clash.
+--   Same with D0_, D1_, Dn_ in part (1.2) above.
+--   These were an effort in circumventing the GHC memory leak,
+--   but since it does not solve the problem, we should consider
+--   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)
@@ -434,9 +505,9 @@
 -- >     = El (Leaf a)
 --
 -- 4. Metadata for each type in (1)
--- > instance HasDatatypeInfo Singl FamRose CodesRose Z where ...
--- > instance HasDatatypeInfo Singl FamRose codesRose (S Z) where ...
--- 
+-- > instance HasDatatypeInfo Singl FamRose CodesRose where
+-- >   datatypeInfo Proxy CZ = ...
+-- >   datatypeInfo Proxy (CS CZ) = ... 
 
 -- |The input data for the generation is an ordered list
 --  (on the second component of the tuple) of STy's and
@@ -486,6 +557,9 @@
 ik2Codes (AtomI n) = AppT tyI $ int2Type n -- ConT (int2TySynName n)
 ik2Codes (AtomK k) = AppT tyK $ PromotedT k
 
+{-
+  VCM: GHC performance HACK
+
 -- Generates piece (1.2); we do so by
 -- finding what's the maximum type index used
 -- in all DatatypeInformation we have and then generate
@@ -504,6 +578,7 @@
     getMaxIdx = foldr (ikElim max (const id)) 0
 
     genTySynNum i = TySynD (int2TySynName i) [] (int2Type i)
+-}
 
 -- generates rhs of piece (1.1)
 inputToFam :: Input -> Q Type
@@ -534,7 +609,7 @@
 
 genPiece1 :: STy -> Input -> Q [Dec]
 genPiece1 first ls
-  = do -- nums  <- inputToTySynNums ls
+  = do -- nums  <- inputToTySynNums ls -- TODO: Remove this hack
        codes <- TySynD <$> codesName first
                        <*> return []
                        <*> inputToCodes ls
@@ -549,6 +624,9 @@
 idxPatSyn :: STy -> Pat
 idxPatSyn = flip ConP [] . idxPatSynName
 
+{-
+  VCM: HACK
+
 -- |@htPatSynName ci@ will generate the
 --  pattern synonym name for constructor ci.
 --
@@ -565,12 +643,14 @@
 htPatSynExp :: Int -> CI IK -> Q Exp
 htPatSynExp dtiIx = return . ConE . htPatSynName dtiIx
 
-genIdxPatSyn :: STy -> Int -> Q Dec
-genIdxPatSyn sty ix
-  = return (PatSynD (idxPatSynName sty) (PrefixPatSyn []) ImplBidir (int2SNatPat ix))
+-}
+{-
+  We tried this in order to help the exhaustiveness checker in GHC.
+  I'm removing this hack to avoid name clashes. Our experiments
+  showed that this did not help at all.
 
-genHereTherePatSyn :: STy -> Input -> Q [Dec]
-genHereTherePatSyn first ls
+genHereTherePatSyn :: OpaqueData -> STy -> Input -> Q [Dec]
+genHereTherePatSyn opq first ls
   = flat . concat <$> mapM (\(_ , ix , dti) -> genHereThereFor ix dti) ls
   where
     flat             = foldl' (\ac (x , y) -> x:y:ac) []
@@ -592,55 +672,141 @@
              -> (,) <$> genHT_decl dtiCode dtiIx ix ci
                     <*> genHT_def          dtiIx ix ci
 
+    opqName = return (ConT $ opaqueName opq)
+
     genHT_decl dtiCode dtiIx ix ci
       = PatSynSigD (htPatSynName dtiIx ci)
-          <$> [t| PoA Singl (El $famName) $(return $ ci2Codes ci)
-                -> NS (PoA Singl (El $famName)) $(return dtiCode) |]
+          <$> [t| PoA $opqName (El $famName) $(return $ ci2Codes ci)
+                -> NS (PoA $opqName (El $famName)) $(return dtiCode) |]
 
     genHT_def dtiIx ix ci
       = do var <- newName "d"
            PatSynD (htPatSynName dtiIx ci) (PrefixPatSyn [var]) ImplBidir
              <$> inj ix (return $ VarP var)
-           
+-}
 
--- |Generating pattern sinonyms for the type indexes
---  and the 'Here/There' combinations. (pieces 2.1 and 2.1.1)
+genIdxPatSyn :: STy -> Int -> Q Dec
+genIdxPatSyn sty ix
+  = return (PatSynD (idxPatSynName sty) (PrefixPatSyn []) ImplBidir (int2SNatPat ix))
+
+-- |Generating pattern synonyms for the type indexes
+--  and the pattern synonyms for the constructors.
 --
 --  > pattern IdxRInt = SZ
 --  > pattern IdxListRInt = SS SZ
 --
-genPiece2 :: STy -> Input -> Q [Dec]
-genPiece2 first ls
+genPiece2 :: OpaqueData -> STy -> Input -> Q [Dec]
+genPiece2 opq first ls
   = do p21  <- mapM (\(sty , ix , dti) -> genIdxPatSyn sty ix) ls
-       p211 <- genHereTherePatSyn first ls
-       return $ p21 ++ p211
+       p22  <- genPiece2_2 opq first ls
+       -- p211 <- genHereTherePatSyn opq first ls
+       return $ p21 ++ p22
 
-genPiece3 :: STy -> Input -> Q Dec
-genPiece3 first ls
-  = head <$> [d| instance Family Singl
+-- |Generating pattern synonyms for constructors with 'Tag'
+--
+--  This is trickier than it looks at first sight.
+--  If we have occurences of @Maybe A@ and @Maybe B@ in our
+--  mutually recursive family, we have to generate two sets of
+--  @Just@s and @Nothing@s, otherwise we will have a name clash.
+--
+--  Infix constructors also receive special treatment.
+--  suppose @(:*:)@ is the 4th constructor of a type @Op x@,
+--  The pattern syn for an instantiation of @x@ to @Int@, @Op Int@,
+--  will be named @OpInt_Ifx4@.
+--
+genPiece2_2 :: OpaqueData -> STy -> Input -> Q [Dec]
+genPiece2_2 opq first ls
+  = concat <$> mapM (\(sty , ix , dti) -> genTagPatSyns sty ix dti) ls
+  where
+    genTagPatSyns :: STy -> Int -> DTI IK -> Q [Dec]
+    genTagPatSyns sty ix dti
+      = concat <$> mapM (uncurry $ genTagPatSynFor ix sty)
+                        (zip [0..] $ dti2ci dti)
+
+    genTagPatSynFor :: Int -> STy -> Int -> CI IK -> Q [Dec]
+    genTagPatSynFor ix sty cidx ci
+      = let fields = ci2ty ci
+         in do vars <- mapM (const (newName "p")) fields
+               let namedFields = zip fields vars
+               name <- patSynName sty cidx ci
+               pat <- [p| Tag $(int2Constr cidx) $(tagPatSynProd namedFields) |]
+               let pDef = PatSynD name (PrefixPatSyn vars) ImplBidir pat
+               phiN <- newName "phi"
+               konN <- newName "kon"
+               patTy <- genTagPatType ix phiN konN fields
+               let pTy = PatSynSigD name patTy
+               return [pTy , pDef]
+
+    genTagPatType :: Int -> Name -> Name -> [IK] -> Q Type
+    genTagPatType tyIx phi kon (AtomK konst : rest)
+      = [t| $(return $ VarT kon) $(return (ConT konst))
+            -> $(genTagPatType tyIx phi kon rest) |] 
+    genTagPatType tyIx phi kon (AtomI ni : rest)
+      = [t| $(return (VarT phi)) $(return $ int2Type ni)
+            -> $(genTagPatType tyIx phi kon rest) |]
+    genTagPatType tyIx phi kon []
+      = [t| View $(return $ VarT kon)
+                 $(return $ VarT phi)
+                 (Lkup $(return $ int2Type tyIx)
+                       $(ConT <$> codesName first))
+        |]
+
+    patSynName :: STy -> Int -> CI IK -> Q Name
+    patSynName sty cidx ci
+      | ciHasIllegalName ci
+      = let styname = nameBase $ styToName sty
+         in return . mkName $ styname ++ "_Ifx" ++ show cidx
+    -- This is a constructor of a type that is not applied
+    -- to any argument; hence there is no risk of name clashing.
+      | ConST _ <- sty
+      = return . mkName $ nameBase (ciName ci) ++ "_"
+    -- Here we will preffix the the constructor name with the
+    -- type it belongs to.
+      | otherwise
+      = let styname = nameBase $ styToName sty
+         in return . mkName $ styname ++ nameBase (ciName ci) ++ "_"
+
+    ciHasIllegalName :: CI ty -> Bool
+    ciHasIllegalName (Infix _ _ _ _) = True
+    ciHasIllegalName ci = any (not . isAlphaNum) $ nameBase (ciName ci)
+
+    tagPatSynProd :: [(IK , Name)] -> Q Pat
+    tagPatSynProd []     = [p| NP0 |]
+    tagPatSynProd (h:hs) = [p| $(tagPatSynProdHead h) :* ( $(tagPatSynProd hs) ) |]
+
+    int2Constr :: Int -> Q Pat
+    int2Constr 0 = [p| CZ |]
+    int2Constr n = [p| CS $(int2Constr (n-1)) |]
+
+    tagPatSynProdHead :: (IK , Name) -> Q Pat
+    tagPatSynProdHead (AtomI _ , name) = [p| NA_I $(return . VarP $ name) |]
+    tagPatSynProdHead (AtomK _ , name) = [p| NA_K $(return . VarP $ name) |]
+
+genPiece3 :: OpaqueData -> STy -> Input -> Q Dec
+genPiece3 opq first ls
+  = head <$> [d| instance Family $(return $ ConT $ opaqueName opq)
                                  $(ConT <$> familyName first)
                                  $(ConT <$> codesName first)
-                   where sfrom' = $(genPiece3_1 ls)
-                         sto'   = $(genPiece3_2 ls) |]
+                   where sfrom' = $(genPiece3_1 opq ls)
+                         sto'   = $(genPiece3_2 opq ls) |]
 
 -- |Given a datatype information, generates a pattern
 --  and an expression from it. The int here
 --  indicates the number of the constructor.
 --
---  > ci2PatExp IdxBinTree (Normal "Bin" [VarT a , VarT a])
+--  > ci2PatExp opq IdxBinTree 3 (Normal "Bin" [VarT a , VarT a])
 --  >   = ( El (Bin x_1 x_2)
---  >     , Rep (PatBin_IdxBinTree (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) :* NP0))))
 --  >     )
-ci2PatExp :: Int -> CI IK -> Q (Pat , Exp)
-ci2PatExp dtiIx ci
+ci2PatExp :: OpaqueData -> Int -> Int -> CI IK -> Q (Pat , Exp)
+ci2PatExp opq dtiIx cIdx ci
   = do (vars , pat) <- ci2Pat ci
-       bdy          <- [e| Rep $(inj $ genBdy (zip vars (ci2ty ci))) |]
+       bdy          <- [e| Rep $(inj cIdx $ genBdy (zip vars (ci2ty ci))) |]
        return (ConP (mkName "El") [pat] , bdy)
   where
-    inj :: Q Exp -> Q Exp
-    -- inj 0 e = [e| Here $e              |]
-    -- inj n e = [e| There $(inj (n-1) e) |]
-    inj e = [e| $(htPatSynExp dtiIx ci) $e |]
+    inj :: Int -> Q Exp -> Q Exp
+    inj 0 e = [e| Here $e              |]
+    inj n e = [e| There $(inj (n-1) e) |]
 
     genBdy :: [(Name , IK)] -> Q Exp
     genBdy []       = [e| NP0 |]
@@ -648,26 +814,24 @@
 
 
     mkHead (x , AtomI _) = [e| NA_I (El $(return (VarE x))) |]
-    mkHead (x , AtomK k) = [e| NA_K $(return (AppE (ConE (mkK k)) (VarE x))) |]
-
-    mkK k = mkName $ 'S':tail (nameBase k)
+    mkHead (x , AtomK k) = [e| NA_K $(makeK opq k (\r -> AppE (ConE r) (VarE x))) |]
+    -- mkHead (x , AtomK k) = [e| NA_K $(return (AppE (ConE (mkK k)) (VarE x))) |]
 
 -- | Just like 'ci2PatExp', but the other way around.
 --
---  > ci2ExpPat IdxBinTree (Normal "Bin" [VarT a , VarT a])
---  >   = ( Rep (PatBin_IdxBinTree (NA_I (El x_1) :* NA_I (El x_2) :* NP0))
+--  > 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))))
 --        , El (Bin x_1 x_2)
 --  >     )
-ci2ExpPat :: Int -> CI IK -> Q (Pat , Exp)
-ci2ExpPat dtiIx ci
+ci2ExpPat :: OpaqueData -> Int -> Int -> CI IK -> Q (Pat , Exp)
+ci2ExpPat opq dtiIx cIdx ci 
   = do (vars , exp) <- ci2Exp ci
-       pat          <- [p| Rep $(inj $ genBdy (zip vars (ci2ty ci))) |]
+       pat          <- [p| Rep $(inj cIdx $ genBdy (zip vars (ci2ty ci))) |]
        return (pat , AppE (ConE $ mkName "El") exp)
   where
-    inj :: Q Pat -> Q Pat
-    -- inj 0 e = [p| Here $e              |]
-    -- inj n e = [p| There $(inj (n-1) e) |]
-    inj e = ConP (htPatSynName dtiIx ci) . (:[]) <$> e
+    inj :: Int -> Q Pat -> Q Pat
+    inj 0 e = [p| Here $e              |]
+    inj n e = [p| There $(inj (n-1) e) |]
     
     genBdy :: [(Name , IK)] -> Q Pat
     genBdy []       = [p| NP0 |]
@@ -675,11 +839,17 @@
 
 
     mkHead (x , AtomI _) = [p| NA_I (El $(return (VarP x))) |]
-    mkHead (x , AtomK k) = [p| NA_K $(return (ConP (mkK k) [VarP x])) |]
+    mkHead (x , AtomK k) = [p| NA_K $(makeK opq k (flip ConP [VarP x])) |]
+    -- mkHead (x , AtomK k) = [p| NA_K $(return (ConP (mkK k) [VarP x])) |]
 
-    mkK k = mkName $ 'S':tail (nameBase k)
 
+makeK :: OpaqueData -> Name -> (Name -> a) -> Q a
+makeK opq n cont
+  = case M.lookup n (opaqueCons opq) of
+      Nothing -> fail $  "makeK: Can't find constructor for " ++ show n ++ " in opaque def"
+      Just c  -> return $ cont c
 
+
 match :: Pat -> Exp -> Match
 match pat bdy = Match pat (NormalB bdy) []
 
@@ -692,8 +862,8 @@
   where
     err = AppE (VarE (mkName "error")) (LitE (StringL "matchAll"))
 
-genPiece3_1 :: Input -> Q Exp
-genPiece3_1 input
+genPiece3_1 :: OpaqueData -> Input -> Q Exp
+genPiece3_1 opq input
   = LamCaseE <$> mapM (\(sty , ix , dti) -> clauseForIx sty ix dti) input
   where
     clauseForIx :: STy -> Int -> DTI IK -> Q Match
@@ -701,10 +871,11 @@
                        <$> (LamCaseE <$> genMatchFor ix dti)
     
     genMatchFor :: Int -> DTI IK -> Q [Match]
-    genMatchFor ix dti = map (uncurry match) <$> mapM (ci2PatExp ix) (dti2ci dti)
+    genMatchFor ix dti = map (uncurry match) <$> mapM (uncurry $ ci2PatExp opq ix)
+                                                      (zip [0..] $ dti2ci dti)
       
-genPiece3_2 :: Input -> Q Exp
-genPiece3_2 input
+genPiece3_2 :: OpaqueData -> Input -> Q Exp
+genPiece3_2 opq input
   = LamCaseE . matchAll <$> mapM (\(sty , ix , dti) -> clauseForIx sty ix dti) input
   where    
     clauseForIx :: STy -> Int -> DTI IK -> Q Match
@@ -712,18 +883,26 @@
                        <$> (LamCaseE . matchAll <$> genMatchFor ix dti)
       
     genMatchFor :: Int -> DTI IK -> Q [Match]
-    genMatchFor ix dti = map (uncurry match) <$> mapM (ci2ExpPat ix) (dti2ci dti)
+    genMatchFor ix dti = map (uncurry match) <$> mapM (uncurry $ ci2ExpPat opq ix)
+                                                      (zip [0..] $ dti2ci dti)
 
-genPiece4 :: STy -> Input -> Q [Dec]
-genPiece4 first ls = concat <$> mapM genDatatypeInfoInstance ls
+genPiece4 :: OpaqueData -> STy -> Input -> Q [Dec]
+genPiece4 opq first ls
+  = [d| instance Meta.HasDatatypeInfo $opqName
+                                      $(ConT <$> familyName first)
+                                      $(ConT <$> codesName first)
+          where datatypeInfo _ = $(genDatatypeInfoClauses ls) |]
   where
-    genDatatypeInfoInstance :: (STy , Int , DTI IK) -> Q [Dec]
-    genDatatypeInfoInstance (sty , idx , dti)
-      = [d| instance Meta.HasDatatypeInfo Singl $(ConT <$> familyName first)
-                                                $(ConT <$> codesName first)
-                                                $(return (int2Type idx))
-              where datatypeInfo _ _ = $(genInfo sty dti) |]
+    opqName = return (ConT $ opaqueName opq)
 
+    genDatatypeInfoClauses :: Input -> Q Exp
+    genDatatypeInfoClauses input
+      = LamCaseE <$> mapM genDatatypeInfoMatch input
+    
+    genDatatypeInfoMatch :: (STy , Int , DTI IK) -> Q Match
+    genDatatypeInfoMatch (sty , idx , dti)
+      = match (int2SNatPat idx) <$> genInfo sty dti 
+
     genMod :: Name -> Q Exp
     genMod = strlit . maybe "" id . nameModule
 
@@ -763,18 +942,17 @@
     genConInfoNP []       = [e| NP0 |]
     genConInfoNP (ci:cis) = [e| $(genConInfo ci) :* ( $(genConInfoNP cis) ) |]
 
--- |@genFamily init fam@ generates a type-level list
+-- |@genFamily opq init fam@ generates a type-level list
 --  of the codes for the family. It also generates
 --  the necessary 'Element' instances.
---  TODO: generate the 'HasDatatypeInfo' instances too!
 --
 --  Precondition, input is sorted on second component.
-genFamily :: STy -> Input -> Q [Dec]
-genFamily first ls
+genFamily :: OpaqueData -> STy -> Input -> Q [Dec]
+genFamily opq first ls
   = do p1 <- genPiece1 first ls
-       p2 <- genPiece2 first ls
-       p3 <- genPiece3 first ls
-       p4 <- genPiece4 first ls
+       p2 <- genPiece2 opq first ls
+       p3 <- genPiece3 opq first ls
+       p4 <- genPiece4 opq first ls
        return $ p1 ++ p2 ++ [p3] ++ p4
 
 -- |Generates a bunch of strings for debug purposes.
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
@@ -14,7 +14,7 @@
   , (:->) , (<.>)
 
     -- * Poly-kind indexed product
-  , (:*:)(..) , curry' , uncurry'
+  , (:*:)(..) , curry' , uncurry' , delta'
 
     -- * Type-level Naturals
   , Nat(..) , proxyUnsuc
@@ -41,6 +41,10 @@
 -- |Poly-kind-indexed product
 data (:*:) (f :: k -> *) (g :: k -> *) (x :: k)
   = f x :*: g x
+
+-- |Distributes the index over the product
+delta' :: (f :*: g) x -> (f x , g x)
+delta' (f :*: g) = (f , g)
 
 -- |Lifted curry
 curry' :: ((f :*: g) x -> a) -> f x -> g x -> a
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
@@ -19,7 +19,7 @@
 
 -- |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
---  fashion, it consists of a choice of constructor and
+--  fashion, it consists of a choice of constructor and 
 --  a position in the type of that constructor.
 data Loc :: (kon -> *) -> [*] -> [[[Atom kon]]] -> Nat -> * where
   Loc :: IsNat ix => El fam ix -> Ctxs ki fam cs iy ix -> Loc ki fam cs iy
@@ -86,9 +86,19 @@
   = do (ExistsIX el nphole) <- mkNPHole p
        return (f el (Ctx c nphole))
 
+
 -- |Fills up a hole.
 fill :: (IsNat ix) => El fam ix -> Ctx ki fam c ix -> Rep ki (El fam) c
 fill el (Ctx c nphole) = inj c (fillNPHole el nphole)
+
+-- |Recursively fills a stack of holes
+-- however, the Family constraint ain't so nice. so we perhaps want to
+-- 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 (Cons ctx ctxs) =
+  fillCtxs (sto @fam @ki @c $ fill h ctx) ctxs
 
 -- |Walks to the next hole and execute an action.
 next :: (IsNat ix)
diff --git a/src/Generics/MRSOP/Zipper/Deep.hs b/src/Generics/MRSOP/Zipper/Deep.hs
new file mode 100644
--- /dev/null
+++ b/src/Generics/MRSOP/Zipper/Deep.hs
@@ -0,0 +1,106 @@
+{-# 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.Util hiding (Cons , Nil)
+import Generics.MRSOP.Base
+
+-- |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 ::
+     (Eq1 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.
+     (Eq1 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 ::
+     (Eq1 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 $ eq1 xs ys
+  pure x
+removeNPHole (T y ys) (x :* xs) = do
+  guard $ eq1 x y
+  removeNPHole ys xs