diff --git a/ChangeLog.md b/ChangeLog.md
--- a/ChangeLog.md
+++ b/ChangeLog.md
@@ -1,5 +1,23 @@
 # Revision history for generics-mrsop
 
+## 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/generics-mrsop.cabal b/generics-mrsop.cabal
--- a/generics-mrsop.cabal
+++ b/generics-mrsop.cabal
@@ -1,5 +1,5 @@
 name:                generics-mrsop
-version:             1.2.2
+version:             2.0.0
 
 synopsis:            Generic Programming with Mutually Recursive Sums of Products.
 
@@ -33,7 +33,6 @@
     Generics.MRSOP.Base.Class,
     Generics.MRSOP.Base.Combinators,
     Generics.MRSOP.Base.Metadata,
-    Generics.MRSOP.Base.Show,
     Generics.MRSOP.Base,
     Generics.MRSOP.Opaque,
     Generics.MRSOP.Util,
@@ -62,6 +61,8 @@
     FunctionalDependencies,
     ScopedTypeVariables
 
+  ghc-options: -Wall
+
   build-depends:       base >= 4.9 && <= 5,
                        containers,
                        template-haskell,
@@ -79,4 +80,4 @@
 source-repository this
   type:     git
   location: https://github.com/VictorCMiraldo/generics-mrsop
-  tag: v1.2.2
+  tag: v2.0.0
diff --git a/src/Generics/MRSOP/AG.hs b/src/Generics/MRSOP/AG.hs
--- a/src/Generics/MRSOP/AG.hs
+++ b/src/Generics/MRSOP/AG.hs
@@ -1,146 +1,75 @@
-{-# LANGUAGE RankNTypes #-}
-{-# LANGUAGE PolyKinds #-}
-{-# LANGUAGE DataKinds #-}
-{-# LANGUAGE TypeApplications #-}
-{-# LANGUAGE KindSignatures #-}
+{-# LANGUAGE RankNTypes          #-}
+{-# LANGUAGE PolyKinds           #-}
+{-# LANGUAGE DataKinds           #-}
+{-# LANGUAGE TypeApplications    #-}
+{-# LANGUAGE KindSignatures      #-}
 {-# LANGUAGE ScopedTypeVariables #-}
-{-# LANGUAGE GADTs #-}
+{-# 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
+-- | 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))
 
-instance (Show1 f, Show1 g) => Show1 (Product f g) where
-  show1 (Pair x y) = "(" ++ show1 x ++ ", " ++ show1 y ++ ")"
+getAnn :: AnnFix ki codes ann ix -> ann ix
+getAnn (AnnFix a _) = a
 
--- | Inherited attributes
+annCata :: IsNat ix
+        => (forall iy. IsNat 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)
 
-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)
+-- | Forget the annotations
+forgetAnn :: AnnFix ki codes a ix -> Fix ki codes ix
+forgetAnn (AnnFix _ rep) = Fix (mapRep forgetAnn rep)
 
-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)
+mapAnn :: (IsNat ix)
+       => (forall iy. chi iy -> phi iy)
+       -> AnnFix ki codes chi ix
+       -> AnnFix ki codes phi ix
+mapAnn f = synthesizeAnn (\x _ -> f x)
 
 -- | 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 :: forall ki codes chi phi ix
+               . (IsNat 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 :: 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
     
 
+-- |Example of using 'synthesize' to annotate a tree with its size
+-- at every node.
+--
+--   > 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
+--
+-- Note how using just 'cata' will simply count the number of nodes
+--
+--   > sizeGeneric :: (IsNat ix)
+--   >             => Fix ki codes ix -> Const (Sum Int) ix
+--   > sizeGeneric = cata sizeAlgebra
+--
 synthesize :: forall ki phi codes ix
             . (IsNat ix)
            => (forall iy . (IsNat iy) => Rep ki phi (Lkup iy codes) -> phi iy)
@@ -154,26 +83,3 @@
         -> 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.hs b/src/Generics/MRSOP/Base.hs
--- a/src/Generics/MRSOP/Base.hs
+++ b/src/Generics/MRSOP/Base.hs
@@ -15,5 +15,5 @@
 import Generics.MRSOP.Base.Class       as Export
 import Generics.MRSOP.Base.Metadata    as Export
 import Generics.MRSOP.Base.Combinators as Export
-import Generics.MRSOP.Base.Show        as Export
+import Generics.MRSOP.Util             as Export
 
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,9 +12,6 @@
 -- |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
 import Generics.MRSOP.Util
 
@@ -90,5 +87,5 @@
 deep :: forall fam ty ki codes ix
       . (Family ki fam codes,
          ix ~ Idx ty fam, Lkup ix fam ~ ty, IsNat ix)
-     => ty -> AnnFix ki codes (Const ()) ix
+     => ty -> Fix ki codes ix
 deep = dfrom . into
diff --git a/src/Generics/MRSOP/Base/Combinators.hs b/src/Generics/MRSOP/Base/Combinators.hs
--- a/src/Generics/MRSOP/Base/Combinators.hs
+++ b/src/Generics/MRSOP/Base/Combinators.hs
@@ -14,12 +14,8 @@
 
 import Data.Function (on)
 
-import Control.Applicative
-import Control.Monad
 import Control.Monad.Identity
 
-import Generics.MRSOP.Base.NS          
-import Generics.MRSOP.Base.NP          
 import Generics.MRSOP.Base.Universe    
 import Generics.MRSOP.Base.Class       
 import Generics.MRSOP.Util
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
@@ -12,7 +12,6 @@
 import Data.Proxy
 
 import Generics.MRSOP.Util
-import Generics.MRSOP.Base.NS
 import Generics.MRSOP.Base.NP
 import Generics.MRSOP.Base.Universe
 import Generics.MRSOP.Base.Class
@@ -77,11 +76,17 @@
 data FieldInfo :: Atom kon -> * where
   FieldInfo :: { fieldName :: FieldName } -> FieldInfo k
 
-deriving instance Show (NP ConstructorInfo code)
-deriving instance Show (NP FieldInfo code)
+deriving instance Show (FieldInfo atom)
+
+instance ShowHO FieldInfo where
+  showHO = show
+
 deriving instance Show (ConstructorInfo code)
+
+instance ShowHO ConstructorInfo where
+  showHO = show
+
 deriving instance Show (DatatypeInfo code)
-deriving instance Show (FieldInfo atom)
 
 -- |Given a 'Family', provides the 'DatatypeInfo' for the type
 --  with index @ix@ in family 'fam'.
@@ -109,8 +114,8 @@
 constrInfoLkup c = go c . constructorInfo
   where
     go :: Constr sum c -> NP ConstructorInfo sum -> ConstructorInfo (Lkup c sum)
-    go CZ     (ci :* _)   = ci
-    go (CS c) (_  :* cis) = go c cis
+    go CZ      (ci :* _)   = ci
+    go (CS c0) (_  :* cis) = go c0 cis
 
 
 -- |Returns the constructor information for a given
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,11 +18,19 @@
   NP0  :: NP p '[]
   (:*) :: p x -> NP p xs -> NP p (x : xs)
 
+instance EqHO phi => EqHO (NP phi) where
+  eqHO = eqNP eqHO
 
-instance Eq1 ki => Eq1 (NP ki) where
-  eq1 = eqNP eq1
-  
+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'
@@ -41,22 +49,22 @@
 
 -- |Maps a natural transformation over a n-ary product
 mapNP :: f :-> g -> NP f ks -> NP g ks
-mapNP f NP0       = NP0
+mapNP _ NP0       = NP0
 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 f NP0       = return NP0
+mapNPM _ NP0       = return NP0
 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 f NP0       = []
+elimNP _ NP0       = []
 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 f NP0       = return []
+elimNPM _ NP0       = return []
 elimNPM f (k :* ks) = (:) <$> f k <*> elimNPM f ks
 
 -- |Combines two products into one.
@@ -66,25 +74,24 @@
 
 -- |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
+unzipNP NP0               = (NP0 , NP0) 
+unzipNP (Pair f g :* fgs) = (f :*) *** (g :*) $ unzipNP fgs
 
 -- * Catamorphism
 
 -- |Consumes a value of type 'NP'.
-cataNP :: (forall x xs . f x  -> r xs -> r (x : xs))
+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 (k :* ks) = fCons k (cataNP fCons fNil ks)
-
+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)))
+        => (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 NP0       = 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,11 +1,13 @@
-{-# LANGUAGE RankNTypes          #-}
-{-# LANGUAGE FlexibleContexts    #-}
-{-# LANGUAGE FlexibleInstances   #-}
-{-# LANGUAGE GADTs               #-}
-{-# LANGUAGE TypeOperators       #-}
-{-# LANGUAGE DataKinds           #-}
-{-# LANGUAGE PolyKinds           #-}
-{-# LANGUAGE ScopedTypeVariables #-}
+{-# LANGUAGE RankNTypes             #-}
+{-# LANGUAGE FlexibleContexts       #-}
+{-# LANGUAGE FlexibleInstances      #-}
+{-# LANGUAGE GADTs                  #-}
+{-# LANGUAGE TypeOperators          #-}
+{-# LANGUAGE DataKinds              #-}
+{-# LANGUAGE PolyKinds              #-}
+{-# LANGUAGE ScopedTypeVariables    #-}
+{-# OPTIONS_GHC -Wno-name-shadowing #-}
+
 -- | Standard representation of n-ary sums.
 module Generics.MRSOP.Base.NS where
 
@@ -20,9 +22,22 @@
   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
+instance EqHO phi => EqHO (NS phi) where
+  eqHO = eqNS eqHO
 
+instance EqHO phi => Eq (NS phi xs) where
+  (==) = eqHO
+
+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
+
+instance ShowHO phi => Show (NS phi xs) where
+  show = showHO
+
 -- * Map, Zip and Elim
 
 -- |Maps over a sum
@@ -49,12 +64,13 @@
 
 -- * Catamorphism
 
+
 -- |Consumes a value of type 'NS'
 cataNS :: (forall x xs . f x  -> r (x ': xs))
        -> (forall x xs . r xs -> r (x ': xs))
        -> NS f xs -> r xs
-cataNS fHere fThere (Here x)  = fHere x
-cataNS fHere fThere (There x) = fThere (cataNS fHere fThere x)
+cataNS fHere _fThere (Here x)  = fHere x
+cataNS fHere fThere  (There x) = fThere (cataNS fHere fThere x)
 
 -- * Equality
 
diff --git a/src/Generics/MRSOP/Base/Show.hs b/src/Generics/MRSOP/Base/Show.hs
deleted file mode 100644
--- a/src/Generics/MRSOP/Base/Show.hs
+++ /dev/null
@@ -1,78 +0,0 @@
-{-# LANGUAGE RankNTypes           #-}
-{-# LANGUAGE FlexibleContexts     #-}
-{-# LANGUAGE FlexibleInstances    #-}
-{-# LANGUAGE UndecidableInstances #-}
-{-# LANGUAGE GADTs                #-}
-{-# LANGUAGE TypeOperators        #-}
-{-# LANGUAGE DataKinds            #-}
-{-# LANGUAGE PolyKinds            #-}
-{-# LANGUAGE ScopedTypeVariables  #-}
-{-# LANGUAGE TypeApplications     #-}
--- |Implements a rudimentary show instance for our representations.
---  We keep this isolated because the instance for @Show (Rep ki phi code)@
---  requires undecidable instances. Isolating this allows us to turn on this
---  extension for this module only.
-module Generics.MRSOP.Base.Show where
-
-import Generics.MRSOP.Base.NS
-import Generics.MRSOP.Base.NP
-import Generics.MRSOP.Base.Universe
-import Generics.MRSOP.Util
-
--- https://stackoverflow.com/questions/9082642/implementing-the-show-class
-{-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
-
-instance Show (NP p '[]) where
-  show NP0 = "NP0"
-instance (Show (p x), Show (NP p xs)) => Show (NP p (x : xs)) where
-  showsPrec p (v :* vs)
-    = let consPrec = 5
-       in showParen (p > consPrec)
-        $ showsPrec (consPrec + 1) v . showString " :* " . showsPrec consPrec vs
-
-instance Show (NS p '[]) where
-  show _ = error "This code is unreachable"
-instance (Show (p x), Show (NS p xs)) => Show (NS p (x : xs)) where
-  showsPrec p (Here  x) = showParen (p > 10) $ showString "H " . showsPrec 11 x
-  showsPrec p (There x) = showString "T " . showsPrec p x
-
--- 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) =
--}
-
-
-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
@@ -17,7 +17,6 @@
 import Data.Type.Equality
 import Data.Proxy
 
-import Data.Functor.Const
 import Control.Monad
 
 import Generics.MRSOP.Base.NS
@@ -45,16 +44,25 @@
 --  using either @ki@ or @phi@ to interpret the type variable
 --  or opaque type.
 data NA  :: (kon -> *) -> (Nat -> *) -> Atom kon -> * where
-  NA_I :: (IsNat k) => phi k -> NA ki phi (I k) 
-  NA_K ::              ki  k -> NA ki phi (K k)
+  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 (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 (ShowHO phi, ShowHO ki) => Show (NA ki phi at) where
+  show = showHO
+
 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 _) (NA_K _) = Nothing
+  testEquality (NA_K _) (NA_I _) = Nothing
   testEquality (NA_I i) (NA_I i') =
     case testEquality (sNatFixIdx i) (sNatFixIdx i') of
       Just Refl -> Just Refl
@@ -77,23 +85,23 @@
 mapNA :: (forall k  .             ki k  -> kj k)
       -> (forall ix . IsNat ix => f  ix -> g  ix)
       -> NA ki f a -> NA kj g a
-mapNA fk fi (NA_I f) = NA_I (fi f)
-mapNA fk fi (NA_K k) = NA_K (fk k)
+mapNA _  fi (NA_I f) = NA_I (fi f)
+mapNA fk _  (NA_K k) = NA_K (fk k)
 
 -- |Maps a monadic natural transformation over an atom interpretation
 mapNAM :: (Monad m)
        => (forall k  .             ki k  -> m (kj k))
        -> (forall ix . IsNat ix => f  ix -> m (g  ix))
        -> NA ki f a -> m (NA kj g a)
-mapNAM fk fi (NA_K k) = NA_K <$> fk k
-mapNAM fk fi (NA_I f) = NA_I <$> fi f
+mapNAM fk _  (NA_K k) = NA_K <$> fk k
+mapNAM _  fi (NA_I f) = NA_I <$> fi f
 
 -- |Eliminates an atom interpretation
-elimNA :: (forall k . ki  k -> b)
+elimNA :: (forall k .            ki  k -> b)
        -> (forall k . IsNat k => phi k -> b)
        -> NA ki phi a -> b
-elimNA kp fp (NA_I x) = fp x
-elimNA kp fp (NA_K x) = kp x
+elimNA _  fp (NA_I x) = fp x
+elimNA kp _  (NA_K x) = kp x
 
 -- |Combines two atoms into one
 zipNA :: NA ki f a -> NA kj g a -> NA (ki :*: kj) (f :*: g) a
@@ -120,8 +128,11 @@
 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
+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
   
 -- |Product of Atoms is a handy synonym to have.
 type PoA (ki :: kon -> *) (phi :: Nat -> *) = NP (NA ki phi)
@@ -211,12 +222,12 @@
 -- |A value @c :: Constr ks n@ specifies a position
 --  in a type-level list. It is, in fact, isomorphic to @Fin (length ks)@.
 data Constr :: [k] -> Nat -> * where
-  CS :: Constr xs n -> Constr (x : xs) (S n)
-  CZ ::                Constr (x : xs) Z
+  CS :: Constr xs n -> Constr (x : xs) ('S n)
+  CZ ::                Constr (x : xs) 'Z
 
 instance TestEquality (Constr codes) where
   testEquality CZ     CZ     = Just Refl
-  testEquality (CS x) (CS y) = apply (Refl :: S :~: S) <$> testEquality x y
+  testEquality (CS x) (CS y) = apply (Refl :: 'S :~: 'S) <$> testEquality x y
   testEquality _      _      = Nothing
 
 instance (IsNat n) => Show (Constr xs n) where
@@ -270,23 +281,14 @@
 -- 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
+instance EqHO ki => EqHO (Fix ki codes) where
+  eqHO = eqFix eqHO
 
-unFix :: Fix ki codes ix -> Rep ki (Fix ki codes) (Lkup ix codes)
-unFix (Fix x) = x
+instance EqHO ki => Eq (Fix ki codes ix) where
+  (==) = eqFix eqHO
 
 -- | Catamorphism over fixpoints
 cata :: (IsNat ix)
@@ -295,22 +297,6 @@
   -> 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 :: phi ix -> Proxy ix
 proxyFixIdx _ = Proxy
@@ -330,13 +316,10 @@
       -> 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)
+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
@@ -10,12 +10,15 @@
 {-# LANGUAGE GADTs                 #-}
 {-# LANGUAGE TypeApplications      #-}
 {-# LANGUAGE PatternSynonyms       #-}
+{-# OPTIONS_GHC -Wno-missing-pattern-synonym-signatures #-}
+{-# OPTIONS_GHC -Wno-missing-signatures                 #-}
+{-# OPTIONS_GHC -Wno-incomplete-patterns                #-}
+{-# OPTIONS_GHC -Wno-orphans                            #-}
 -- This is the minimun language extensions we
 -- need for using the library.
 -- |Provide a generic alpha equality decider for the lambda calculus.
 module Generics.MRSOP.Examples.LambdaAlphaEqTH where
 
-import Control.Monad
 import Control.Monad.State
 
 import Generics.MRSOP.Util
@@ -28,7 +31,6 @@
           | Abs String Term
           | App Term Term
 
-
 deriveFamily [t| Term |]
 
 -- * The alpha-eq monad
@@ -51,7 +53,7 @@
 
 onHead :: (a -> a) -> [a] -> [a]
 onHead f (x : xs) = f x : xs
-onHead f []       = []
+onHead _ []       = []
 
 -- |Given a list of scopes, which consist in a list of pairs each, checks
 --  whether or not two names are equivalent.
@@ -89,12 +91,12 @@
     galphaEqT :: forall ix m . (MonadAlphaEq m , IsNat ix)
               => FIX ix -> FIX ix
               -> m Bool
-    galphaEqT x y = galphaEq (getSNat' @ix) x y
+    galphaEqT i j = galphaEq (getSNat' @ix) i j
 
     galphaEq :: forall ix m . (MonadAlphaEq m , IsNat ix)
              => SNat ix -> FIX ix -> FIX ix
              -> m Bool
-    galphaEq ix (Fix x) (Fix y) = maybe (return False) (go ix) (zipRep x y)
+    galphaEq ix (Fix x0) (Fix y0) = maybe (return False) (go ix) (zipRep x0 y0)
 
     step :: forall m c . (MonadAlphaEq m)
          => Rep (Singl :*: Singl) (FIX :*: FIX) c -> m Bool
@@ -106,13 +108,13 @@
        => SNat ix -> Rep (Singl :*: Singl) (FIX :*: FIX)
                          (Lkup ix CodesTerm)
        -> m Bool
-    go IdxTerm x = case sop x of
+    go IdxTerm x0 = case sop x0 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 IdxTerm t1 t2)
-      _ -> step x
+      Abs_ (SString v1 :*: SString v2) (c1 :*: c2)
+        -> onNewScope (addRule v1 v2 >> galphaEq IdxTerm c1 c2)
+      _ -> step x0
 
 -- * 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
@@ -10,6 +10,9 @@
 {-# LANGUAGE ScopedTypeVariables     #-}
 {-# LANGUAGE FunctionalDependencies  #-}
 {-# LANGUAGE PatternSynonyms         #-}
+{-# OPTIONS_GHC -Wno-missing-pattern-synonym-signatures #-}
+{-# OPTIONS_GHC -Wno-incomplete-patterns                #-}
+{-# OPTIONS_GHC -Wno-orphans                            #-}
 -- |This module is analogous to 'Generics.MRSOP.Examples.RoseTreeTH',
 --  but we use no Template Haskell here.
 module Generics.MRSOP.Examples.RoseTree where
@@ -18,7 +21,6 @@
 
 import Generics.MRSOP.Base
 import Generics.MRSOP.Opaque
-import Generics.MRSOP.Util
 
 -- * Standard Rose-Tree datatype
 
@@ -26,15 +28,15 @@
          | Leaf a
          deriving Show
 
-value1, value2 :: R Int
+value1, value2, value3 :: R Int
 value1 = 1 :>: [2 :>: [], 3 :>: []]
 value2 = 1 :>: [2 :>: [] , Leaf 12]
 value3 = 3 :>: [Leaf 23 , value1 , value2]
 
 -- ** Family Structure
 
-type ListCode = '[ '[] , '[I (S Z) , I Z] ]
-type RTCode   = '[ '[K KInt , I Z] , '[K KInt] ]
+type ListCode = '[ '[] , '[ 'I ('S 'Z) , 'I 'Z] ]
+type RTCode   = '[ '[ 'K 'KInt , 'I 'Z] , '[ 'K 'KInt] ]
 
 type CodesRose = '[ListCode , RTCode]
 type FamRose   = '[ [R Int] , R Int] 
@@ -46,6 +48,7 @@
   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' _ _ = error "unreachable"
 
   sto' SZ (Rep (Here NP0))
     = El []
@@ -55,6 +58,7 @@
     = El (a :>: as)
   sto' (SS SZ) (Rep (There (Here (NA_K (SInt a) :* NP0))))
     = El (Leaf a)
+  sto' _ _ = error "unreachable"
 
 instance HasDatatypeInfo Singl FamRose CodesRose where
   datatypeInfo _ SZ
@@ -67,6 +71,8 @@
       $  (Infix ":>:" NotAssociative 0)
       :* (Constructor "Leaf")
       :* NP0
+  datatypeInfo _ _
+    = error "unreachable"
 
 -- * Eq Instance
 
diff --git a/src/Generics/MRSOP/Examples/RoseTreeTH.hs b/src/Generics/MRSOP/Examples/RoseTreeTH.hs
--- a/src/Generics/MRSOP/Examples/RoseTreeTH.hs
+++ b/src/Generics/MRSOP/Examples/RoseTreeTH.hs
@@ -12,21 +12,20 @@
 {-# LANGUAGE TemplateHaskell         #-}
 {-# LANGUAGE LambdaCase              #-}
 {-# LANGUAGE PatternSynonyms         #-}
+{-# OPTIONS_GHC -Wno-missing-pattern-synonym-signatures #-}
+{-# OPTIONS_GHC -Wno-missing-signatures                 #-}
+{-# OPTIONS_GHC -Wno-incomplete-patterns                #-}
+{-# OPTIONS_GHC -Wno-orphans                            #-}
 -- |Usage example with template haskell support.
 module Generics.MRSOP.Examples.RoseTreeTH where
 
 {-# OPTIONS_GHC -ddump-splices #-}
 import Data.Function (on)
-import Data.Proxy
 
 import Generics.MRSOP.Base
 import Generics.MRSOP.Opaque
-import Generics.MRSOP.Util
 
 import Generics.MRSOP.TH
-
-import Control.Monad
-
 
 -- * Defining the datatype
 --
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
@@ -11,6 +11,10 @@
 {-# LANGUAGE TemplateHaskell         #-}
 {-# LANGUAGE LambdaCase              #-}
 {-# LANGUAGE PatternSynonyms         #-}
+{-# OPTIONS_GHC -Wno-missing-pattern-synonym-signatures #-}
+{-# OPTIONS_GHC -Wno-missing-signatures                 #-}
+{-# OPTIONS_GHC -Wno-incomplete-patterns                #-}
+{-# OPTIONS_GHC -Wno-orphans                            #-}
 -- |Uses a more involved example to test some
 --  of the functionalities of @generics-mrsop@.
 module Generics.MRSOP.Examples.SimpTH where
@@ -19,7 +23,6 @@
 
 import Generics.MRSOP.Base
 import Generics.MRSOP.Opaque
-import Generics.MRSOP.Util
 import Generics.MRSOP.Zipper
 
 import Generics.MRSOP.Examples.LambdaAlphaEqTH hiding (FIX, alphaEq)
@@ -27,7 +30,6 @@
 import Generics.MRSOP.TH
 
 import Control.Monad
-import Control.Monad.State
 
 -- * Simple IMPerative Language:
 
@@ -78,9 +80,6 @@
     galphaEq' iy (Fix x)
       = maybe (return False) (go iy) . zipRep x . unFix
 
-    unSString :: Singl k -> String
-    unSString (SString s) = s
-
     -- Performs one default ste by eliminating the topmost Rep
     -- using galphaEqT on the recursive positions and isEqv
     -- on the atoms.
@@ -102,8 +101,7 @@
       = case sop x of
           StmtStringSAssign_ (SString v1 :*: SString v2) e1e2
             -> addRule v1 v2 >> uncurry' (galphaEq' IdxExpString) e1e2
-          otherwise
-            -> step x
+          _ -> step x
     go IdxDeclString x
       = case sop x of
           DeclStringDVar_ (SString v1 :*: SString v2)
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
@@ -13,10 +13,7 @@
 --   by the everyday Haskell programmer.
 module Generics.MRSOP.Opaque where
 
-import Data.Function (on)
-import Data.Proxy
 import Data.Type.Equality
-
 import Generics.MRSOP.Util
 
 -- * Opaque Types
@@ -44,22 +41,22 @@
 
 -- |A singleton GADT for the allowed 'Kon'stants.
 data Singl (kon :: Kon) :: * where
-  SInt     :: Int     -> Singl KInt
-  SInteger :: Integer -> Singl KInteger
-  SFloat   :: Float   -> Singl KFloat
-  SDouble  :: Double  -> Singl KDouble
-  SBool    :: Bool    -> Singl KBool
-  SChar    :: Char    -> Singl KChar
-  SString  :: String  -> Singl KString
+  SInt     :: Int     -> Singl 'KInt
+  SInteger :: Integer -> Singl 'KInteger
+  SFloat   :: Float   -> Singl 'KFloat
+  SDouble  :: Double  -> Singl 'KDouble
+  SBool    :: Bool    -> Singl 'KBool
+  SChar    :: Char    -> Singl 'KChar
+  SString  :: String  -> Singl 'KString
 
 deriving instance Show (Singl k)
 deriving instance Eq   (Singl k)
 
-instance Eq1 Singl where
-  eq1 = (==)
+instance EqHO Singl where
+  eqHO = (==)
 
-instance Show1 Singl where
-  show1 = show
+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
@@ -4,7 +4,9 @@
 {-# LANGUAGE DeriveTraversable #-}
 {-# LANGUAGE DeriveFunctor     #-}
 {-# LANGUAGE TemplateHaskell   #-}
-{-# OPTIONS_GHC -cpp           #-}
+{-# OPTIONS_GHC -cpp                      #-}
+{-# OPTIONS_GHC -Wno-name-shadowing       #-}
+{-# OPTIONS_GHC -Wno-unused-pattern-binds #-}
 -- | Provides a simple way for the end-user deriving
 --   the mechanical, yet long, Element instances
 --   for a family.
@@ -20,19 +22,18 @@
   ) where
 
 import Data.Function (on)
-import Data.Char (ord , isAlphaNum)
-import Data.List (sortBy, foldl')
+import Data.Char (isAlphaNum)
+import Data.List (sortBy)
 
 import Control.Monad
 import Control.Monad.State
-import Control.Monad.Writer
-import Control.Monad.Identity
+import Control.Monad.Writer   (WriterT, tell, runWriterT)
+import Control.Monad.Identity (runIdentity)
 
 import Language.Haskell.TH hiding (match)
 import Language.Haskell.TH.Syntax (liftString)
 
 import Generics.MRSOP.Util
-import Generics.MRSOP.Opaque
 import Generics.MRSOP.Base.Class
 import Generics.MRSOP.Base.NS
 import Generics.MRSOP.Base.NP
@@ -73,7 +74,7 @@
   where
     second (_ , x , _) = x
     
-    extractDTI (sty , (ix , Nothing))
+    extractDTI (sty , (_ix , Nothing))
       = fail $ "Type " ++ show sty ++ " has no datatype information."
     extractDTI (sty , (ix , Just dti))
       = return (sty , ix , dti)
@@ -155,9 +156,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
+-- defined but not used
+-- dtiName :: DTI ty -> DataName
+-- dtiName (ADT name _ _) = name
+-- dtiName (New name _ _) = name
 
 dti2ci :: DTI ty -> [CI ty]
 dti2ci (ADT _ _ cis) = cis
@@ -194,8 +196,8 @@
 
 styFold :: (a -> a -> a) -> (Name -> a) -> (Name -> a) -> STy -> a
 styFold app var con (AppST a b) = app (styFold app var con a) (styFold app var con b)
-styFold app var con (VarST n)   = var n
-styFold app var con (ConST n)   = con n
+styFold _   var _   (VarST n)   = var n
+styFold _   _   con (ConST n)   = con n
 
 -- |Does a STy have a varible name?
 isClosed :: STy -> Bool
@@ -220,14 +222,14 @@
   | n == mkName "[]" = ListT
   | isTupleN n       = TupleT $ length (show n) - 1
   | otherwise        = ConT n
-  where isTupleN n = take 2 (show n) == "(,"
+  where isTupleN n0 = take 2 (show n0) == "(,"
 
 -- |Handy substitution function.
 --
 --  @stySubst t m n@ substitutes m for n within t, that is: t[m/n]
 stySubst :: STy -> Name -> STy -> STy
 stySubst (AppST a b) m n = AppST (stySubst a m n) (stySubst b m n)
-stySubst (ConST a)   m n = ConST a
+stySubst (ConST a)   _ _ = ConST a
 stySubst (VarST x)   m n
   | x == m    = n
   | otherwise = VarST x
@@ -257,7 +259,7 @@
 
 -- Extracts a DTI from a Dec
 decInfo :: Dec -> Q (DTI STy)
-decInfo (TySynD     name args      ty)     = fail "Type Synonyms not supported"
+decInfo (TySynD     _name _args _ty)       = fail "Type Synonyms not supported"
 decInfo (DataD    _ name args    _ cons _) = ADT name (map argInfo args) <$> mapM conInfo cons
 decInfo (NewtypeD _ name args    _ con _)  = New name (map argInfo args) <$> conInfo con
 decInfo _                                  = fail "Only type declarations are supported"
@@ -300,9 +302,10 @@
   | AtomK Name
   deriving (Eq , Show)
 
-ikElim :: (Int -> a) -> (Name -> a) -> IK -> a
-ikElim i k (AtomI n) = i n
-ikElim i k (AtomK n) = k n
+-- defined but not used
+-- ikElim :: (Int -> a) -> (Name -> a) -> IK -> a
+-- ikElim i k (AtomI n) = i n
+-- ikElim i k (AtomK n) = k n
 
 data Idxs 
   = Idxs { idxsNext :: Int
@@ -344,8 +347,9 @@
 lkup :: (Monad m) => STy -> IdxsM m (Maybe (Int , Maybe (DTI IK)))
 lkup ty = M.lookup ty . idxsMap <$> get
 
-lkupInfo :: (Monad m) => STy -> IdxsM m (Maybe Int)
-lkupInfo ty = fmap fst <$> lkup ty
+-- defined but not used
+-- lkupInfo :: (Monad m) => STy -> IdxsM m (Maybe Int)
+-- lkupInfo ty = fmap fst <$> lkup ty
 
 lkupData :: (Monad m) => STy -> IdxsM m (Maybe (DTI IK))
 lkupData ty = join . fmap snd <$> lkup ty
@@ -402,7 +406,8 @@
 -- |Performs step 2 of the sketch;
 reifySTy :: OpaqueData -> STy -> M ()
 reifySTy opq sty
-  = do ix <- indexOf sty
+  = do _ <- indexOf sty -- we don't care about the index of sty now, but we
+                        -- need to register it
        uncurry go (styFlatten sty)
   where
     go :: STy -> [STy] -> M ()
@@ -413,6 +418,7 @@
            (final , todo) <- runWriterT $ dtiMapM (convertSTy (opaqueTable opq)) res
            register sty 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.
@@ -434,7 +440,7 @@
 
     makeCons :: M.Map Name Name -> STy -> Maybe Name
     makeCons opqTable (ConST n) = M.lookup n opqTable
-    makeCons opqTable _         = Nothing
+    makeCons _        _         = Nothing
 
 -----------------------------
 -- * Generating the Code * --
@@ -525,8 +531,8 @@
 
 -- generate the name of the type synonym corresponding to
 -- this int.
-int2TySynName :: Int -> Name
-int2TySynName i = mkName $ "D" ++ show i ++ "_"
+-- int2TySynName :: Int -> Name
+-- int2TySynName i = mkName $ "D" ++ show i ++ "_"
 
 -- generates a Snat for the given Int
 int2SNatPat :: Int -> Pat
@@ -534,6 +540,7 @@
 int2SNatPat n = ConP (mkName "SS") [int2SNatPat $ n-1]
 
 -- Our promoted type constructors
+tyS , tyZ , tyI , tyK :: Type
 tyS = PromotedT (mkName "S")
 tyZ = PromotedT (mkName "Z")
 tyI = PromotedT (mkName "I")
@@ -697,7 +704,7 @@
 --
 genPiece2 :: OpaqueData -> STy -> Input -> Q [Dec]
 genPiece2 opq first ls
-  = do p21  <- mapM (\(sty , ix , dti) -> genIdxPatSyn sty ix) ls
+  = do p21  <- mapM (\(sty , ix , _dti) -> genIdxPatSyn sty ix) ls
        p22  <- genPiece2_2 opq first ls
        -- p211 <- genHereTherePatSyn opq first ls
        return $ p21 ++ p22
@@ -715,7 +722,7 @@
 --  will be named @OpInt_Ifx4@.
 --
 genPiece2_2 :: OpaqueData -> STy -> Input -> Q [Dec]
-genPiece2_2 opq first ls
+genPiece2_2 _opq first ls
   = concat <$> mapM (\(sty , ix , dti) -> genTagPatSyns sty ix dti) ls
   where
     genTagPatSyns :: STy -> Int -> DTI IK -> Q [Dec]
@@ -799,14 +806,14 @@
 --  >     , Rep (There (There (Here (NA_I (El x_1) :* NA_I (El x_2) :* NP0))))
 --  >     )
 ci2PatExp :: OpaqueData -> Int -> Int -> CI IK -> Q (Pat , Exp)
-ci2PatExp opq dtiIx cIdx ci
+ci2PatExp opq _dtiIx cIdx ci
   = do (vars , pat) <- ci2Pat ci
-       bdy          <- [e| Rep $(inj cIdx $ genBdy (zip vars (ci2ty ci))) |]
+       bdy          <- [e| Rep $(mkInj cIdx $ genBdy (zip vars (ci2ty ci))) |]
        return (ConP (mkName "El") [pat] , bdy)
   where
-    inj :: Int -> Q Exp -> Q Exp
-    inj 0 e = [e| Here $e              |]
-    inj n e = [e| There $(inj (n-1) e) |]
+    mkInj :: Int -> Q Exp -> Q Exp
+    mkInj 0 e = [e| Here $e                |]
+    mkInj n e = [e| There $(mkInj (n-1) e) |]
 
     genBdy :: [(Name , IK)] -> Q Exp
     genBdy []       = [e| NP0 |]
@@ -824,14 +831,14 @@
 --        , El (Bin x_1 x_2)
 --  >     )
 ci2ExpPat :: OpaqueData -> Int -> Int -> CI IK -> Q (Pat , Exp)
-ci2ExpPat opq dtiIx cIdx ci 
-  = do (vars , exp) <- ci2Exp ci
-       pat          <- [p| Rep $(inj cIdx $ genBdy (zip vars (ci2ty ci))) |]
-       return (pat , AppE (ConE $ mkName "El") exp)
+ci2ExpPat opq _dtiIx cIdx ci 
+  = do (vars , myexp) <- ci2Exp ci
+       pat            <- [p| Rep $(mkInj cIdx $ genBdy (zip vars (ci2ty ci))) |]
+       return (pat , AppE (ConE $ mkName "El") myexp)
   where
-    inj :: Int -> Q Pat -> Q Pat
-    inj 0 e = [p| Here $e              |]
-    inj n e = [p| There $(inj (n-1) e) |]
+    mkInj :: Int -> Q Pat -> Q Pat
+    mkInj 0 e = [p| Here $e                |]
+    mkInj n e = [p| There $(mkInj (n-1) e) |]
     
     genBdy :: [(Name , IK)] -> Q Pat
     genBdy []       = [p| NP0 |]
@@ -960,7 +967,7 @@
 genFamilyDebug _ ms = concat <$> mapM genDec ms
   where
     genDec :: (STy , Int , DTI IK) -> Q [Dec]
-    genDec (sty , ix , dti)
+    genDec (_sty , ix , dti)
       = [d| $( genPat ix ) = $(mkBody dti) |]
 
     mkBody :: DTI IK -> Q Exp
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
@@ -7,15 +7,19 @@
 {-# LANGUAGE RankNTypes          #-}
 {-# LANGUAGE TypeApplications    #-}
 {-# LANGUAGE ScopedTypeVariables #-}
+{-# LANGUAGE PatternSynonyms     #-}
 -- |Useful utilities we need accross multiple modules.
 module Generics.MRSOP.Util
   ( -- * Utility Functions and Types
     (&&&) , (***)
   , (:->) , (<.>)
 
-    -- * Poly-kind indexed product
-  , (:*:)(..) , curry' , uncurry' , delta'
+    -- * Poly-kind indexed product functionality
+  , Product(..), (:*:), pattern (:*:) , Delta , curry' , uncurry' , delta
 
+    -- * Poly-kind indexed sums
+  , Sum(..) , either' , either''
+
     -- * Type-level Naturals
   , Nat(..) , proxyUnsuc
   , SNat(..) , snat2int
@@ -30,33 +34,49 @@
   , Lkup , Idx , El(..) , getElSNat , into
 
     -- * Higher-order Eq and Show
-  , Eq1(..) , Show1(..)
+  , EqHO(..) , ShowHO(..)
   ) where
 
 import Data.Proxy
 import Data.Type.Equality
+import Data.Functor.Product
+import Data.Functor.Sum
+import Data.Functor.Const
 import GHC.TypeLits (TypeError , ErrorMessage(..))
 import Control.Arrow ((***) , (&&&))
 
--- |Poly-kind-indexed product
-data (:*:) (f :: k -> *) (g :: k -> *) (x :: k)
-  = f x :*: g x
+type    (:*:)     = Product
 
--- |Distributes the index over the product
-delta' :: (f :*: g) x -> (f x , g x)
-delta' (f :*: g) = (f , g)
+pattern (:*:) :: f a -> g a -> Product f g a
+pattern (:*:) x y = Pair x y
 
 -- |Lifted curry
-curry' :: ((f :*: g) x -> a) -> f x -> g x -> a
-curry' f fx gx = f (fx :*: gx)
+curry' :: (Product f g x -> a) -> f x -> g x -> a
+curry' f fx gx = f (Pair fx gx)
 
 -- |Lifted uncurry
-uncurry' :: (f x -> g x -> a) -> (f :*: g) x -> a
-uncurry' f (fx :*: gx) = f fx gx
+uncurry' :: (f x -> g x -> a) -> Product f g x -> a
+uncurry' f (Pair fx gx) = f fx gx
 
 -- |Natural transformations
 type f :-> g = forall n . f n -> g n
 
+-- |Diagonal indexed functor
+type Delta f = Product f f
+
+-- |Duplicates its argument
+delta :: f :-> Delta f
+delta fx = Pair fx fx
+
+-- |Higher-order sum eliminator
+either' :: (f :-> r) -> (g :-> r) -> Sum f g :-> r
+either' f _ (InL x) = f x
+either' _ g (InR x) = g x
+
+-- |Just like 'either'', but the result type is of kind Star
+either'' :: (forall x . f x -> a) -> (forall y . g y -> a) -> Sum f g r -> a
+either'' f g = getConst . either' (Const . f) (Const . g)
+
 infixr 8 <.>
 -- |Kleisli Composition
 (<.>) :: (Monad m) => (b -> m c) -> (a -> m b) -> a -> m c
@@ -66,13 +86,13 @@
 data Nat = S Nat | Z
   deriving (Eq , Show)
 
-proxyUnsuc :: Proxy (S n) -> Proxy n
+proxyUnsuc :: Proxy ('S n) -> Proxy n
 proxyUnsuc _ = Proxy
 
 -- |Singleton Term-level natural
 data SNat :: Nat -> * where
-  SZ ::           SNat Z
-  SS :: SNat n -> SNat (S n)
+  SZ ::           SNat 'Z
+  SS :: SNat n -> SNat ('S n)
 
 snat2int :: SNat n -> Integer
 snat2int SZ     = 0
@@ -81,9 +101,9 @@
 -- |And their conversion to term-level integers.
 class IsNat (n :: Nat) where
   getSNat :: Proxy n -> SNat n
-instance IsNat Z where
-  getSNat p = SZ
-instance IsNat n => IsNat (S n) where
+instance IsNat 'Z where
+  getSNat _ = SZ
+instance IsNat n => IsNat ('S n) where
   getSNat p = SS (getSNat $ proxyUnsuc p)
 
 getNat :: (IsNat n) => Proxy n -> Integer
@@ -102,15 +122,15 @@
 
 -- |Type-level list lookup
 type family Lkup (n :: Nat) (ks :: [k]) :: k where
-  Lkup Z     (k : ks) = k
-  Lkup (S n) (k : ks) = Lkup n ks
-  Lkup _     '[]      = TypeError (Text "Lkup index too big")
+  Lkup 'Z     (k : ks) = k
+  Lkup ('S n) (k : ks) = Lkup n ks
+  Lkup _      '[]      = TypeError ('Text "Lkup index too big")
 
 -- |Type-level list index
 type family Idx (ty :: k) (xs :: [k]) :: Nat where
-  Idx x (x ': ys) = Z
-  Idx x (y ': ys) = S (Idx x ys)
-  Idx x '[]       = TypeError (Text "Element not found")
+  Idx x (x ': ys) = 'Z
+  Idx x (y ': ys) = 'S (Idx x ys)
+  Idx x '[]       = TypeError ('Text "Element not found")
 
 -- |Also list lookup, but for kind * only.
 data El :: [*] -> Nat -> * where
@@ -126,7 +146,6 @@
      => ty -> El fam ix
 into = El
 
-
 -- |An inhabitant of @ListPrf ls@ is *not* a singleton!
 --  It only proves that @ls@ is, in fact, a type level list.
 --  This is useful since it enables us to pattern match on
@@ -164,10 +183,31 @@
 --            in Generics.MRSOP.Opaque, it seems like we don't really need this.
 
 -- |Higher order version of 'Eq'
-class Eq1 (f :: k -> *) where
-  eq1 :: forall k . f k -> f k -> Bool
+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 Show1 (f :: k -> *) where
-  show1 :: forall k . f k -> String
+class ShowHO (f :: ki -> *) where
+  showHO :: forall k . f k -> String
+
+instance Show a => ShowHO (Const a) where
+  showHO (Const a) = show a
+
+instance (ShowHO f , ShowHO g) => ShowHO (Product f g) where
+  showHO (Pair x y) = "(" ++ showHO x ++ ", " ++ showHO y ++ ")"
+
+instance (ShowHO f , ShowHO g) => ShowHO (Sum f g) where
+  showHO (InL fx) = "InL " ++ showHO fx
+  showHO (InR gx) = "InR " ++ showHO gx
 
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,10 +12,7 @@
 --  universe.
 module Generics.MRSOP.Zipper where
 
-import Data.Type.Equality
-
-import Generics.MRSOP.Util hiding (Cons , Nil)
-import Generics.MRSOP.Base
+import Generics.MRSOP.Base hiding (Cons , Nil)
 
 -- |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
@@ -42,7 +39,7 @@
 -- |A @NPHole ki fam ix prod@ is a recursive position
 --  of type @ix@ in @prod@.
 data NPHole :: (kon -> *) -> [*] -> Nat -> [Atom kon] -> * where
-  H :: PoA ki (El fam) xs -> NPHole ki fam ix (I ix : xs)
+  H :: PoA ki (El fam) xs -> NPHole ki fam ix ('I ix : xs)
   T :: NA ki (El fam) x -> NPHole ki fam ix xs -> NPHole ki fam ix (x : xs)
 
 -- |Existential abstraction; needed for walking the possible
@@ -83,8 +80,8 @@
 first :: (forall ix . IsNat ix => El fam ix -> Ctx ki fam c ix -> a)
       -> Rep ki (El fam) c -> Maybe a
 first f el | Tag c p <- sop el
-  = do (ExistsIX el nphole) <- mkNPHole p
-       return (f el (Ctx c nphole))
+  = do (ExistsIX el0 nphole) <- mkNPHole p
+       return (f el0 (Ctx c nphole))
 
 
 -- |Fills up a hole.
@@ -120,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 el Nil)             = Nothing
+up (Loc _  Nil)             = 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 el Nil)             = Nothing
+right (Loc _  Nil)             = Nothing
 right (Loc el (Cons ctx ctxs)) = next (\el' ctx' -> Loc el' (Cons ctx' ctxs)) el ctx
 
 -- * Interface
@@ -144,6 +141,6 @@
 
 -- |Updates the value in the hole.
 update :: (Family ki fam codes , IsNat ix)
-       => (forall ix . SNat ix -> El fam ix -> El fam ix)
+       => (forall iy . SNat iy -> El fam iy -> El fam iy)
        -> Loc ki fam codes ix -> Loc ki fam codes ix
 update f (Loc el ctxs) = Loc (f (getElSNat el) el) ctxs
diff --git a/src/Generics/MRSOP/Zipper/Deep.hs b/src/Generics/MRSOP/Zipper/Deep.hs
--- a/src/Generics/MRSOP/Zipper/Deep.hs
+++ b/src/Generics/MRSOP/Zipper/Deep.hs
@@ -18,29 +18,25 @@
 import Control.Monad (guard)
 import Data.Proxy
 
-import Generics.MRSOP.Util hiding (Cons , Nil)
-import Generics.MRSOP.Base
+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
+  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
+  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
+  T :: NA ki (Fix ki codes) x
     -> NPHole ki codes ix xs
     -> NPHole ki codes ix (x ': xs)
 
@@ -51,56 +47,52 @@
 -- a product
 --
 -- dual of 'removeNPHole'
-fillNPHole ::
-     IsNat ix
-  => Fix ki codes ix
-  -> NPHole ki codes ix xs
-  -> PoA ki (Fix ki codes) xs
+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 :: (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 :: (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 :: (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.
-     (Eq1 ki, IsNat ix)
-  => Rep ki (Fix ki codes) c
-  -> Ctx ki codes c ix
-  -> Maybe (Fix ki codes ix)
+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 ::
-     (Eq1 ki, IsNat ix)
-  => NPHole ki codes ix xs
-  -> PoA ki (Fix ki codes) xs
-  -> Maybe (Fix ki codes ix)
+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 $ eq1 xs ys
+  guard $ eqHO xs ys
   pure x
 removeNPHole (T y ys) (x :* xs) = do
-  guard $ eq1 x y
+  guard $ eqHO x y
   removeNPHole ys xs