diff --git a/executables/HDiff.hs b/executables/HDiff.hs
--- a/executables/HDiff.hs
+++ b/executables/HDiff.hs
@@ -1,3 +1,4 @@
+{-# LANGUAGE QuantifiedConstraints #-}
 {-# LANGUAGE RankNTypes            #-}
 {-# LANGUAGE FlexibleInstances     #-}
 {-# LANGUAGE TypeSynonymInstances  #-}
@@ -348,6 +349,6 @@
         Just fb' <- tryApply v ba fa Nothing
         when (v == Loud) (putStrLnErr "!! apply ab fb")
         Just fa' <- tryApply v ab fb Nothing
-        if eqFix eqHO fb' fa'
+        if fb' == fa'
         then return ExitSuccess
         else return (ExitFailure 2)
diff --git a/executables/Languages/Clojure/AST.hs b/executables/Languages/Clojure/AST.hs
--- a/executables/Languages/Clojure/AST.hs
+++ b/executables/Languages/Clojure/AST.hs
@@ -1,14 +1,16 @@
-{-# LANGUAGE KindSignatures #-}
-{-# LANGUAGE TemplateHaskell #-}
-{-# LANGUAGE DataKinds #-}
-{-# LANGUAGE GADTs #-}
-{-# LANGUAGE BangPatterns #-}
-{-# LANGUAGE StandaloneDeriving #-}
-{-# LANGUAGE PatternSynonyms #-}
-{-# LANGUAGE TypeSynonymInstances #-}
-{-# LANGUAGE FlexibleInstances #-}
+{-# LANGUAGE KindSignatures        #-}
+{-# LANGUAGE TemplateHaskell       #-}
+{-# LANGUAGE DataKinds             #-}
+{-# LANGUAGE GADTs                 #-}
+{-# LANGUAGE BangPatterns          #-}
+{-# LANGUAGE StandaloneDeriving    #-}
+{-# LANGUAGE PatternSynonyms       #-}
+{-# LANGUAGE TypeSynonymInstances  #-}
+{-# LANGUAGE FlexibleInstances     #-}
 {-# LANGUAGE MultiParamTypeClasses #-}
-
+{-# OPTIONS_GHC -Wno-missing-signatures                 #-}
+{-# OPTIONS_GHC -Wno-missing-pattern-synonym-signatures #-}
+{-# OPTIONS_GHC -Wno-orphans                            #-}
 module Languages.Clojure.AST where
 
 import Data.Type.Equality
@@ -22,7 +24,6 @@
 import Generics.MRSOP.HDiff.Digest
 import Generics.MRSOP.HDiff.Renderer
 
-
 data SepExprList =
    Nil 
  | Cons Expr !Sep SepExprList 
@@ -69,8 +70,6 @@
 
 deriving instance Show (CljSingl k)
 deriving instance Eq (CljSingl k)
-instance ShowHO CljSingl where showHO = show
-instance EqHO CljSingl where eqHO = (==)
 
 instance TestEquality CljSingl where
   testEquality (SCljText _) (SCljText _) = Just Refl
diff --git a/executables/Languages/Interface.hs b/executables/Languages/Interface.hs
--- a/executables/Languages/Interface.hs
+++ b/executables/Languages/Interface.hs
@@ -1,3 +1,4 @@
+{-# LANGUAGE QuantifiedConstraints #-}
 {-# LANGUAGE ConstraintKinds #-}
 {-# LANGUAGE RankNTypes #-}
 {-# LANGUAGE DataKinds #-}
@@ -22,9 +23,8 @@
 import Generics.MRSOP.HDiff.Renderer
 import Generics.MRSOP.HDiff.Digest
 
-
 data LangParser :: * where
-  LangParser :: (LangCnstr ki fam codes ix)
+  LangParser :: (LangCnstr ki fam codes ix, EqHO ki , ShowHO ki)
              -- |Language extension
              => String
              -- |Parser that
@@ -32,23 +32,22 @@
              -> LangParser
 
 data VectorOf (a :: *) (n :: Nat) :: * where
-  V0 :: VectorOf a Z
-  VS :: a -> VectorOf a n -> VectorOf a (S n)
+  V0 :: VectorOf a 'Z
+  VS :: a -> VectorOf a n -> VectorOf a ('S n)
 
 vecMapM :: (Monad m) => (a -> m b) -> VectorOf a n -> m (VectorOf b n)
-vecMapM f V0 = return V0
+vecMapM _ V0 = return V0
 vecMapM f (VS x xs) = VS <$> f x <*> vecMapM f xs
 
 type LangCnstr ki fam codes ix
-  = (HasDatatypeInfo ki fam codes , EqHO ki , RendererHO ki , IsNat ix, ShowHO ki
-    ,DigestibleHO ki,TestEquality ki)
+  = (HasDatatypeInfo ki fam codes, RendererHO ki, IsNat ix, DigestibleHO ki, TestEquality ki)
 
 -- |Given a list of languages, parses a number of files
 withParsedEl :: LangParser
-             -> VectorOf FilePath (S n)
+             -> VectorOf FilePath ('S n)
              -> (forall kon (ki :: kon -> *) fam codes ix
-                 . (LangCnstr ki fam codes ix)
-                => VectorOf (Fix ki codes ix) (S n)
+                 . (LangCnstr ki fam codes ix , EqHO ki , ShowHO ki)
+                => VectorOf (Fix ki codes ix) ('S n)
                 -> IO res)
              -> ExceptT String IO res
 withParsedEl (LangParser ext parser) vec f
@@ -60,24 +59,23 @@
                  -> (FilePath -> IO (Fix ki codes ix))
                  -> FilePath
                  -> ExceptT String IO (Fix ki codes ix)
-    parseWithExt ext parser file
-      | ("." ++ ext) `isSuffixOf` file = liftIO $ parser file
+    parseWithExt e p file
+      | ("." ++ ext) `isSuffixOf` file = liftIO $ p file
       | otherwise
-      = throwError ("Wrong Extension; expecting: " ++ show ext ++ "\n")
+      = throwError ("Wrong Extension; expecting: " ++ show e ++ "\n")
 
 -- |Tries a variety of parsers on a number of
 --  files.
 withParsedEls :: [LangParser]
-              -> VectorOf FilePath (S n)
+              -> VectorOf FilePath ('S n)
               -> (forall kon (ki :: kon -> *) fam codes ix
-                  . (LangCnstr ki fam codes ix)
-                 => VectorOf (Fix ki codes ix) (S n)
+                  . (LangCnstr ki fam codes ix , EqHO ki , ShowHO ki)
+                 => VectorOf (Fix ki codes ix) ('S n)
                  -> IO res)
               -> ExceptT String IO res
 withParsedEls []     _     _ = throwError "No parser succeeded\n"
-withParsedEls (p:ps) files f
-  = withParsedEl p files f
-  <|> withParsedEls ps files f
+withParsedEls (p:ps) files f = withParsedEl  p  files f
+                           <|> withParsedEls ps files f
 
 
 -- * Fixed interface for one, two and three files
@@ -91,36 +89,35 @@
 withParsed1 :: [LangParser]
             -> FilePath
             -> (forall kon (ki :: kon -> *) fam codes ix
-                 . (LangCnstr ki fam codes ix)
+                 . (LangCnstr ki fam codes ix , EqHO ki , ShowHO ki)
                 => Fix ki codes ix
                 -> IO res)
             -> IO res
 withParsed1 parsers file f
   = redirectErr
   $ withParsedEls parsers (VS file V0)
-  $ \(VS file V0) -> f file
+  $ \(VS x V0) -> f x
 
-         
 withParsed2 :: [LangParser]
             -> FilePath -> FilePath
             -> (forall kon (ki :: kon -> *) fam codes ix
-                 . (LangCnstr ki fam codes ix)
+                 . (LangCnstr ki fam codes ix , EqHO ki , ShowHO ki)
                 => Fix ki codes ix -> Fix ki codes ix
                 -> IO res)
             -> IO res
 withParsed2 parsers a b f
   = redirectErr
   $ withParsedEls parsers (VS a (VS b V0))
-  $ \(VS a (VS b V0)) -> f a b
+  $ \(VS x (VS y V0)) -> f x y
          
 withParsed3 :: [LangParser]
             -> FilePath -> FilePath -> FilePath
             -> (forall kon (ki :: kon -> *) fam codes ix
-                 . (LangCnstr ki fam codes ix)
+                 . (LangCnstr ki fam codes ix , EqHO ki , ShowHO ki)
                 => Fix ki codes ix -> Fix ki codes ix -> Fix ki codes ix
                 -> IO res)
             -> IO res
 withParsed3 parsers a b c f
   = redirectErr
   $ withParsedEls parsers (VS a (VS b (VS c V0)))
-  $ \(VS a (VS b (VS c V0))) -> f a b c
+  $ \(VS x (VS y (VS z V0))) -> f x y z
diff --git a/executables/Languages/Lines.hs b/executables/Languages/Lines.hs
--- a/executables/Languages/Lines.hs
+++ b/executables/Languages/Lines.hs
@@ -1,3 +1,4 @@
+{-# LANGUAGE StandaloneDeriving    #-}
 {-# LANGUAGE RankNTypes            #-}
 {-# LANGUAGE FlexibleInstances     #-}
 {-# LANGUAGE TypeSynonymInstances  #-}
@@ -9,22 +10,18 @@
 {-# LANGUAGE GADTs                 #-}
 {-# LANGUAGE MultiParamTypeClasses #-}
 {-# LANGUAGE TypeApplications      #-}
+{-# OPTIONS_GHC -Wno-missing-signatures                 #-}
+{-# OPTIONS_GHC -Wno-missing-pattern-synonym-signatures #-}
 module Languages.Lines where
 
-import System.IO
 import           Data.Type.Equality
 import           Data.Text.Prettyprint.Doc (pretty)
-import           Data.Text.Prettyprint.Doc.Render.Text
-import qualified Data.Text as T
 
 import Generics.MRSOP.Base hiding (Infix)
-import Generics.MRSOP.Util
 import Generics.MRSOP.TH
 import Generics.MRSOP.HDiff.Renderer
 import Generics.MRSOP.HDiff.Digest
 
-import Debug.Trace
-
 -----------------------
 -- * Parser
 
@@ -45,14 +42,11 @@
 data W :: WKon -> * where
   W_String  :: String  -> W WString
 
-instance EqHO W where
-  eqHO (W_String s)  (W_String ss) = s == ss
+deriving instance Show (W x)
+deriving instance Eq (W x)
 
 instance DigestibleHO W where
   digestHO (W_String s)  = hashStr s
-
-instance ShowHO W where
-  showHO (W_String s)  = s
 
 -- Now we derive the 'Family' instance
 -- using 'W' for the constants.
diff --git a/executables/Languages/Lua.hs b/executables/Languages/Lua.hs
--- a/executables/Languages/Lua.hs
+++ b/executables/Languages/Lua.hs
@@ -1,14 +1,15 @@
-{-# LANGUAGE TemplateHaskell #-}
-{-# LANGUAGE GADTs #-}
-{-# LANGUAGE StandaloneDeriving #-}
-{-# LANGUAGE PatternSynonyms #-}
-{-# LANGUAGE TypeFamilies #-}
-{-# LANGUAGE TypeSynonymInstances #-}
+{-# LANGUAGE TemplateHaskell       #-}
+{-# LANGUAGE GADTs                 #-}
+{-# LANGUAGE StandaloneDeriving    #-}
+{-# LANGUAGE PatternSynonyms       #-}
+{-# LANGUAGE TypeFamilies          #-}
+{-# LANGUAGE TypeSynonymInstances  #-}
 {-# LANGUAGE MultiParamTypeClasses #-}
-{-# LANGUAGE FlexibleInstances #-}
-{-# LANGUAGE DataKinds #-}
-{-# LANGUAGE TypeApplications #-}
-{-# LANGUAGE CPP #-}
+{-# LANGUAGE FlexibleInstances     #-}
+{-# LANGUAGE DataKinds             #-}
+{-# LANGUAGE TypeApplications      #-}
+{-# LANGUAGE CPP                   #-}
+
 module Languages.Lua where
 
 #ifdef ENABLE_LUA_SUPPORT
@@ -56,8 +57,6 @@
 
 deriving instance Show (LuaSingl k)
 deriving instance Eq (LuaSingl k)
-instance ShowHO LuaSingl where showHO = show
-instance EqHO LuaSingl where eqHO = (==)
 
 instance TestEquality LuaSingl where
   testEquality (SLuaText _) (SLuaText _) = Just Refl
diff --git a/executables/Languages/While.hs b/executables/Languages/While.hs
--- a/executables/Languages/While.hs
+++ b/executables/Languages/While.hs
@@ -1,3 +1,4 @@
+{-# LANGUAGE StandaloneDeriving    #-}
 {-# LANGUAGE RankNTypes            #-}
 {-# LANGUAGE FlexibleInstances     #-}
 {-# LANGUAGE TypeSynonymInstances  #-}
@@ -9,7 +10,7 @@
 {-# LANGUAGE GADTs                 #-}
 {-# LANGUAGE MultiParamTypeClasses #-}
 {-# LANGUAGE TypeApplications      #-}
-{-# OPTIONS_GHC -Wno-missing-signatures #-}
+{-# OPTIONS_GHC -Wno-missing-signatures                 #-}
 {-# OPTIONS_GHC -Wno-missing-pattern-synonym-signatures #-}
 module Languages.While where
 
@@ -76,20 +77,13 @@
   W_String  :: String  -> W 'WString
   W_Bool    :: Bool    -> W 'WBool
 
-instance EqHO W where
-  eqHO (W_Integer i) (W_Integer j) = i == j
-  eqHO (W_String s)  (W_String ss) = s == ss
-  eqHO (W_Bool b)    (W_Bool c)    = b == c
+deriving instance Eq (W x)
+deriving instance Show (W x)
 
 instance DigestibleHO W where
   digestHO (W_Integer i) = hashStr (show i)
   digestHO (W_String s)  = hashStr s
   digestHO (W_Bool b)    = hashStr (show b)
-
-instance ShowHO W where
-  showHO (W_Integer i) = show i
-  showHO (W_String s)  = s
-  showHO (W_Bool b)    = show b
 
 -- Now we derive the 'Family' instance
 -- using 'W' for the constants.
diff --git a/hdiff.cabal b/hdiff.cabal
--- a/hdiff.cabal
+++ b/hdiff.cabal
@@ -4,10 +4,10 @@
 --
 -- see: https://github.com/sol/hpack
 --
--- hash: b37884aac4ee07f3aa56e35f35c9f4e9a3e6f1e608768849bd352a9ec364a3c0
+-- hash: 2a593069031274f1574dee4f16bb500347e9eeba60f7a3faaaf2b3e92fc9c7b8
 
 name:           hdiff
-version:        0.0.0
+version:        0.0.1
 synopsis:       Pattern-Expression-based differencing of arbitrary types.
 description:    This package provides an executable and a library to compute and manipulate pattern-expression based differences between values of arbitrary datatypes. For more detailed information check the README at our GitHub page.
 category:       Other
@@ -58,7 +58,7 @@
     , bytestring
     , containers
     , cryptonite
-    , generics-mrsop >=2.1.0
+    , generics-mrsop >=2.2.0
     , generics-mrsop-gdiff
     , hspec
     , memory
@@ -88,7 +88,7 @@
     , bytestring
     , containers
     , cryptonite
-    , generics-mrsop >=2.1.0
+    , generics-mrsop >=2.2.0
     , generics-mrsop-gdiff
     , gitrev
     , hdiff
@@ -122,7 +122,7 @@
     , bytestring
     , containers
     , cryptonite
-    , generics-mrsop >=2.1.0
+    , generics-mrsop >=2.2.0
     , generics-mrsop-gdiff
     , hdiff
     , hspec
diff --git a/src/Data/Exists.hs b/src/Data/Exists.hs
--- a/src/Data/Exists.hs
+++ b/src/Data/Exists.hs
@@ -1,6 +1,7 @@
-{-# LANGUAGE PolyKinds  #-}
-{-# LANGUAGE RankNTypes #-}
-{-# LANGUAGE GADTs      #-}
+{-# LANGUAGE QuantifiedConstraints #-}
+{-# LANGUAGE PolyKinds             #-}
+{-# LANGUAGE RankNTypes            #-}
+{-# LANGUAGE GADTs                 #-}
 module Data.Exists where
 
 data Exists (f :: k -> *) :: * where
@@ -14,4 +15,7 @@
 
 exElim :: (forall x . f x -> a) -> Exists f -> a
 exElim f (Exists x) = f x
+
+instance (forall i . Show (x i)) => Show (Exists x) where
+  show (Exists x) = show x
 
diff --git a/src/Data/HDiff/Change.hs b/src/Data/HDiff/Change.hs
--- a/src/Data/HDiff/Change.hs
+++ b/src/Data/HDiff/Change.hs
@@ -1,3 +1,4 @@
+{-# LANGUAGE QuantifiedConstraints #-}
 {-# LANGUAGE TypeOperators         #-}
 {-# LANGUAGE FlexibleInstances     #-}
 {-# LANGUAGE MultiParamTypeClasses #-}
diff --git a/src/Data/HDiff/Change/Apply.hs b/src/Data/HDiff/Change/Apply.hs
--- a/src/Data/HDiff/Change/Apply.hs
+++ b/src/Data/HDiff/Change/Apply.hs
@@ -1,3 +1,4 @@
+{-# LANGUAGE QuantifiedConstraints #-}
 {-# LANGUAGE FlexibleInstances     #-}
 {-# LANGUAGE ConstraintKinds       #-}
 {-# LANGUAGE TupleSections         #-}
@@ -63,8 +64,7 @@
 -- |A instantiation substitution from metavariable numbers to some treefix
 type Subst ki codes phi = M.Map Int (Exists (Holes ki codes phi))
 
-type Applicable ki codes phi = (ShowHO ki , EqHO ki , TestEquality ki , TestEquality phi
-                              , HasIKProjInj ki phi , EqHO phi)
+type Applicable ki codes phi = (TestEquality ki , TestEquality phi , HasIKProjInj ki phi )
 
 -- |We try to unify @pa@ and @pq@ onto @ea@. The idea is that
 --  we instantiate the variables of @pa@ with their corresponding expression
@@ -72,7 +72,7 @@
 --  we ignore whatever was on @ea@ and give that variable instead.
 --
 --  We are essentially applying 
-genericApply :: (Applicable ki codes phi)
+genericApply :: (Applicable ki codes phi , EqHO phi , EqHO ki)
              => CChange ki codes at
              -> Holes ki codes phi at
              -> Either (ApplicationErr ki codes phi) (Holes ki codes phi at)
@@ -100,13 +100,13 @@
 
 -- |@pmatch pa x@ traverses @pa@ and @x@ instantiating the variables of @pa@.
 -- Upon sucessfully instantiating the variables, returns the substitution.
-pmatch :: (Applicable ki codes phi)
+pmatch :: (Applicable ki codes phi , EqHO phi , EqHO ki)
        => Holes ki codes (MetaVarIK ki) ix
        -> Holes ki codes phi ix
        -> Except (ApplicationErr ki codes phi) (Subst ki codes phi)
 pmatch pat = pmatch' M.empty pat
 
-pmatch' :: (Applicable ki codes phi)
+pmatch' :: (Applicable ki codes phi , EqHO phi , EqHO ki)
    => Subst ki codes phi
    -> Holes ki codes (MetaVarIK ki) ix
    -> Holes ki codes phi ix
@@ -114,7 +114,7 @@
 pmatch' s (Hole _ var) x  = substInsert s var x
 pmatch' _ pa (Hole _ var) = throwError (IncompatibleHole pa var)
 pmatch' s (HOpq _ oa) (HOpq _ ox)
-  | eqHO oa ox = return s
+  | oa == ox  = return s
   | otherwise = throwError (IncompatibleOpqs oa ox)
 pmatch' s pa@(HPeel _ ca ppa) x@(HPeel _ cx px) =
   case testEquality ca cx of
@@ -143,7 +143,7 @@
 
 -- |Attempts to insert a new binding into a substitution. If the variable is already
 -- bound, we check the existing binding for equality
-substInsert :: (Applicable ki codes phi)
+substInsert :: (Applicable ki codes phi , EqHO ki , EqHO phi)
             => Subst ki codes phi
             -> MetaVarIK ki ix
             -> Holes ki codes phi ix
diff --git a/src/Data/HDiff/Change/Classify.hs b/src/Data/HDiff/Change/Classify.hs
--- a/src/Data/HDiff/Change/Classify.hs
+++ b/src/Data/HDiff/Change/Classify.hs
@@ -1,8 +1,9 @@
-{-# LANGUAGE FlexibleInstances #-}
-{-# LANGUAGE TypeOperators     #-}
-{-# LANGUAGE PolyKinds         #-}
-{-# LANGUAGE GADTs             #-}
-{-# OPTIONS_GHC -Wno-orphans   #-}
+{-# LANGUAGE QuantifiedConstraints #-}
+{-# LANGUAGE FlexibleInstances     #-}
+{-# LANGUAGE TypeOperators         #-}
+{-# LANGUAGE PolyKinds             #-}
+{-# LANGUAGE GADTs                 #-}
+{-# OPTIONS_GHC -Wno-orphans       #-}
 -- |change classification algorithm
 module Data.HDiff.Change.Classify where
 
diff --git a/src/Data/HDiff/Change/Thinning.hs b/src/Data/HDiff/Change/Thinning.hs
--- a/src/Data/HDiff/Change/Thinning.hs
+++ b/src/Data/HDiff/Change/Thinning.hs
@@ -1,3 +1,4 @@
+{-# LANGUAGE QuantifiedConstraints #-}
 {-# LANGUAGE FlexibleContexts      #-}
 {-# LANGUAGE FlexibleInstances     #-}
 {-# LANGUAGE ConstraintKinds       #-}
@@ -42,6 +43,7 @@
                (CChange ki codes at)
 thin chg dom = uncurry' cmatch <$> thinUTx2 (cCtxDel chg :*: cCtxIns chg) dom
 
+
 tr :: (ShowHO ki , TestEquality ki, EqHO ki)
    => CChange ki codes at
    -> CChange ki codes at
@@ -110,7 +112,7 @@
                  (Holes ki codes (MetaVarIK ki) at)
     go p (Hole _ var)   = record_eq var p >> return p
     go p@(Hole _ var) q = record_eq var q >> return p
-    go p q | eqHO p q   = return p
+    go p q | p == q     = return p
            | otherwise  = throwError (IncompatibleTerms p q)
 
     -- Whenever we see a variable being matched against a term
@@ -132,7 +134,7 @@
         -- It's not the first time we thin 'var'; previously, we had
         -- that 'var' was supposed to be p'. We will check whether it
         -- is the same as q, if not, we will have to thin p' with q.
-        Just q' -> unless (eqHO q' q)
+        Just q' -> unless (q' == q)
                  $ void $ utxThin q' q
           
 
diff --git a/src/Data/HDiff/Change/TreeEditDistance.hs b/src/Data/HDiff/Change/TreeEditDistance.hs
--- a/src/Data/HDiff/Change/TreeEditDistance.hs
+++ b/src/Data/HDiff/Change/TreeEditDistance.hs
@@ -1,8 +1,9 @@
-{-# LANGUAGE TypeOperators       #-}
-{-# LANGUAGE GADTs               #-}
-{-# LANGUAGE PolyKinds           #-}
-{-# LANGUAGE DataKinds           #-}
-{-# LANGUAGE ScopedTypeVariables #-}
+{-# LANGUAGE QuantifiedConstraints #-}
+{-# LANGUAGE TypeOperators         #-}
+{-# LANGUAGE GADTs                 #-}
+{-# LANGUAGE PolyKinds             #-}
+{-# LANGUAGE DataKinds             #-}
+{-# LANGUAGE ScopedTypeVariables   #-}
 module Data.HDiff.Change.TreeEditDistance where
 
 import qualified Data.Map as M
@@ -33,11 +34,11 @@
   = LC Int a (ListES a)
   | LD Int a (ListES a)
   | LI Int a (ListES a)
-  | LNil
+  | LLP_Nil
   deriving (Eq , Show)
 
 cost :: ListES a -> Int
-cost LNil       = 0
+cost LLP_Nil       = 0
 cost (LC c _ _) = c
 cost (LI c _ _) = c
 cost (LD c _ _) = c
@@ -46,18 +47,18 @@
 -- For example, 
 --
 --   > λ> lcs [0,1,2] [0,1,1,1,2]
---   > LC 0 (LC 1 (LI 1 (LI 1 (LC 2 LNil))))
+--   > LC 0 (LC 1 (LI 1 (LI 1 (LC 2 LLP_Nil))))
 --
 -- Note how the 1 is copied to the first position, then
 -- the other ones are inserted.
 --
 --   > λ> pushCopiesIns $ lcsW (const 1) [0,1,2] [0,1,1,1,2]
---   > LC 0 (LI 1 (LI 1 (LC 1 (LC 2 LNil))))
+--   > LC 0 (LI 1 (LI 1 (LC 1 (LC 2 LLP_Nil))))
 --
 -- Here instead, we insert two 1's then copy the last one.
 -- This really helps with synchronization.
 pushCopiesIns :: (Eq a) => ListES a -> ListES a
-pushCopiesIns LNil = LNil
+pushCopiesIns LLP_Nil = LLP_Nil
 pushCopiesIns (LC _ c (LI _ c' es))
   | c == c'   = LI 0 c' (pushCopiesIns (LC 0 c es))
   | otherwise = LC 0 c  (pushCopiesIns (LI 0 c' es))
@@ -90,7 +91,7 @@
                       return $ res
 
    lcs'' :: STRef s (Table a) -> [a] -> [a] -> ST s (ListES a)
-   lcs'' _   []      []     = return LNil
+   lcs'' _   []      []     = return LLP_Nil
    lcs'' tbl (x:xs)  []     = lcs' tbl xs [] >>= \d -> return (LD (weight x + cost d) x d)
    lcs'' tbl []      (y:ys) = lcs' tbl [] ys >>= \i -> return (LI (weight y + cost i) y i)
    lcs'' tbl  (x:xs) (y:ys) =
@@ -122,7 +123,7 @@
         Right s  ->
           let sizes_s = M.map (exElim holesSize) s
               ves     = pushCopiesIns $ lcsW (\v -> sizes_s M.! v) vd vi
-           in runExcept (runReaderT (compress <$> delPhase (del :* NP0) (ins :* NP0)) (s , ves))
+           in runExcept (runReaderT (compress <$> delPhase (del :* Nil) (ins :* Nil)) (s , ves))
 
 type ToES ki codes = ReaderT (Subst ki codes (MetaVarIK ki) , ListES Int)
                              (Except String)
@@ -151,13 +152,13 @@
 compress :: (EqHO ki , TestEquality ki) => GD.ES ki codes is ds -> GD.ES ki codes is ds
 compress GD.ES0 = GD.ES0
 compress (GD.Del _ v (GD.Ins c' v' e)) =
-  case GD.heqCof v v' of
+  case GD.cofHeq v v' of
     Just (Refl , Refl) -> gcpy v (compress e)
     Nothing            -> gdel v (compress $ GD.Ins c' v' e)
 compress (GD.Del _ v e)
   = gdel v $ compress e
 compress (GD.Ins _ v (GD.Del c' v' e)) =
-  case GD.heqCof v v' of
+  case GD.cofHeq v v' of
     Just (Refl , Refl) -> gcpy v (compress e)
     Nothing            -> gins v (compress $ GD.Del c' v' e)
 compress (GD.Ins _ v e)
@@ -168,7 +169,7 @@
 cpyOnly :: (EqHO ki , ShowHO ki , TestEquality ki)
         => NP (Holes ki codes (MetaVarIK ki)) xs
         -> ToES ki codes (GD.ES ki codes xs xs)
-cpyOnly NP0 = return GD.ES0
+cpyOnly Nil = return GD.ES0
 cpyOnly (Hole  _ var :* xs) = fetch var >>= cpyOnly . (:* xs) 
 cpyOnly (HOpq  _ k   :* xs) = gcpy (GD.ConstrK k)               <$> cpyOnly xs
 cpyOnly (HPeel _ c d :* xs) = gcpy (GD.ConstrI c (listPrfNP d)) <$> cpyOnly (appendNP d xs)
@@ -176,7 +177,7 @@
 delOnly :: (EqHO ki , ShowHO ki , TestEquality ki)
         => NP (Holes ki codes (MetaVarIK ki)) ds
         -> ToES ki codes (GD.ES ki codes ds '[])
-delOnly NP0 = return GD.ES0
+delOnly Nil = return GD.ES0
 delOnly (Hole  _ var :* xs) = fetch var >>= delOnly . (:* xs) 
 delOnly (HOpq  _ k   :* xs) = gdel (GD.ConstrK k)               <$> delOnly xs
 delOnly (HPeel _ c d :* xs) = gdel (GD.ConstrI c (listPrfNP d)) <$> delOnly (appendNP d xs)
@@ -184,35 +185,35 @@
 insOnly :: (EqHO ki , ShowHO ki , TestEquality ki)
         => NP (Holes ki codes (MetaVarIK ki)) is
         -> ToES ki codes (GD.ES ki codes '[] is)
-insOnly NP0 = return GD.ES0
+insOnly Nil = return GD.ES0
 insOnly (Hole  _ var :* xs) = fetch var >>= insOnly . (:* xs) 
 insOnly (HOpq  _ k   :* xs) = gins (GD.ConstrK k)               <$> insOnly xs
 insOnly (HPeel _ c d :* xs) = gins (GD.ConstrI c (listPrfNP d)) <$> insOnly (appendNP d xs)
 
 listAssoc :: ListPrf a -> Proxy b -> Proxy c
           -> ListPrf ((a :++: b) :++: c) :~: ListPrf (a :++: (b :++: c))
-listAssoc Nil       _  _  = Refl
-listAssoc (Cons pa) pb pc = case listAssoc pa pb pc of
+listAssoc LP_Nil       _  _  = Refl
+listAssoc (LP_Cons pa) pb pc = case listAssoc pa pb pc of
                               Refl -> Refl
 
 listDrop :: ListPrf i -> ListPrf (i :++: t) -> ListPrf t
-listDrop Nil a             = a
-listDrop (Cons x) (Cons a) = listDrop x a
+listDrop LP_Nil a             = a
+listDrop (LP_Cons x) (LP_Cons a) = listDrop x a
 
 esDelListPrf :: GD.ES ki codes ds is -> ListPrf ds
-esDelListPrf GD.ES0 = Nil
-esDelListPrf (GD.Cpy _ v e) = Cons $ listDrop (cofListPrf v) (esDelListPrf e)
-esDelListPrf (GD.Del _ v e) = Cons $ listDrop (cofListPrf v) (esDelListPrf e)
+esDelListPrf GD.ES0 = LP_Nil
+esDelListPrf (GD.Cpy _ v e) = LP_Cons $ listDrop (cofListPrf v) (esDelListPrf e)
+esDelListPrf (GD.Del _ v e) = LP_Cons $ listDrop (cofListPrf v) (esDelListPrf e)
 esDelListPrf (GD.Ins _ _ e) = esDelListPrf e
 
 esInsListPrf :: GD.ES ki codes ds is -> ListPrf is
-esInsListPrf GD.ES0 = Nil
-esInsListPrf (GD.Cpy _ v e) = Cons $ listDrop (cofListPrf v) (esInsListPrf e)
-esInsListPrf (GD.Ins _ v e) = Cons $ listDrop (cofListPrf v) (esInsListPrf e)
+esInsListPrf GD.ES0 = LP_Nil
+esInsListPrf (GD.Cpy _ v e) = LP_Cons $ listDrop (cofListPrf v) (esInsListPrf e)
+esInsListPrf (GD.Ins _ v e) = LP_Cons $ listDrop (cofListPrf v) (esInsListPrf e)
 esInsListPrf (GD.Del _ _ e) = esInsListPrf e
 
 cofListPrf :: GD.Cof ki codes at l -> ListPrf l
-cofListPrf (GD.ConstrK _)   = Nil
+cofListPrf (GD.ConstrK _)   = LP_Nil
 cofListPrf (GD.ConstrI _ p) = p
 
 esDelListProxy :: GD.ES ki codes ds is -> Proxy ds
@@ -275,7 +276,7 @@
                      then throwError "delSync: var mismatch"
                      else do
                        t   <- fetch var
-                       es0 <- delOnly (t :* NP0)
+                       es0 <- delOnly (t :* Nil)
                        es1 <- local (second (const es'))
                             $ delPhase ds is
                        return (appendES es0 es1)
@@ -297,7 +298,7 @@
                      then throwError "insSync: var mismatch"
                      else do
                        t   <- fetch var
-                       es0 <- insOnly (t :* NP0)
+                       es0 <- insOnly (t :* Nil)
                        es1 <- local (second (const es'))
                             $ insPhase ds is
                        return (appendES es0 es1)
@@ -313,7 +314,7 @@
         then throwError "insSync: var mismatch"
         else do
           t   <- fetch var
-          es0 <- cpyOnly (t :* NP0)
+          es0 <- cpyOnly (t :* Nil)
           es1 <- local (second (const es'))
                $ delPhase ds' is
           case testEquality var var'' of
@@ -322,21 +323,21 @@
       -- Otherwise, we must enter the deletion phase until
       -- we find it.
       _ -> delPhase ds (Hole' var :* is)
-    LNil -> throwError "insSync: premature LNil"
+    LLP_Nil -> throwError "insSync: premature LLP_Nil"
 
 delPhase , insPhase
   :: (EqHO ki , ShowHO ki , TestEquality ki)
   => NP (Holes ki codes (MetaVarIK ki)) ds
   -> NP (Holes ki codes (MetaVarIK ki)) is
   -> ToES ki codes (GD.ES ki codes ds is)
-delPhase NP0 is  = insOnly is
+delPhase Nil is  = insOnly is
 delPhase (d :* ds) is =
   case d of
     Hole  _ var -> delSync var ds is
     HOpq  _ k   -> gdel (GD.ConstrK k)               <$> insPhase ds is
     HPeel _ c p -> gdel (GD.ConstrI c (listPrfNP p)) <$> insPhase (appendNP p ds) is
 
-insPhase ds NP0 = delOnly ds
+insPhase ds Nil = delOnly ds
 insPhase ds (i :* is) = 
   case i of
     Hole  _ var -> insSync var ds is
diff --git a/src/Data/HDiff/Diff.hs b/src/Data/HDiff/Diff.hs
--- a/src/Data/HDiff/Diff.hs
+++ b/src/Data/HDiff/Diff.hs
@@ -1,11 +1,12 @@
-{-# LANGUAGE FlexibleInstances   #-}
-{-# LANGUAGE ScopedTypeVariables #-}
-{-# LANGUAGE TypeOperators       #-}
-{-# LANGUAGE PatternSynonyms     #-}
-{-# LANGUAGE RankNTypes          #-}
-{-# LANGUAGE DataKinds           #-}
-{-# LANGUAGE PolyKinds           #-}
-{-# LANGUAGE GADTs               #-}
+{-# LANGUAGE QuantifiedConstraints #-}
+{-# LANGUAGE FlexibleInstances     #-}
+{-# LANGUAGE ScopedTypeVariables   #-}
+{-# LANGUAGE TypeOperators         #-}
+{-# LANGUAGE PatternSynonyms       #-}
+{-# LANGUAGE RankNTypes            #-}
+{-# LANGUAGE DataKinds             #-}
+{-# LANGUAGE PolyKinds             #-}
+{-# LANGUAGE GADTs                 #-}
 module Data.HDiff.Diff
   ( diffOpts'
   , diffOpts
diff --git a/src/Data/HDiff/Diff/Types.hs b/src/Data/HDiff/Diff/Types.hs
--- a/src/Data/HDiff/Diff/Types.hs
+++ b/src/Data/HDiff/Diff/Types.hs
@@ -45,7 +45,7 @@
 
 -- |Specifies the options for the diffing algorithm
 data DiffOptions = DiffOptions
-  -- |Minimum height of trees considered for sharing
+  -- ^ Minimum height of trees considered for sharing
   { doMinHeight      :: Int
   , doOpaqueHandling :: DiffOpaques
   , doMode           :: DiffMode
diff --git a/src/Data/HDiff/Example.hs b/src/Data/HDiff/Example.hs
--- a/src/Data/HDiff/Example.hs
+++ b/src/Data/HDiff/Example.hs
@@ -111,23 +111,23 @@
 unif1 = HPeel' CZ (HOpq' (SInt 100)
                  :* Hole' (NA_I $ Const 1)
                  :* Hole' (NA_I $ Const 2)
-                 :* NP0)
+                 :* Nil)
 unif12 :: TreeTerm
 unif12 = HPeel' CZ (HOpq' (SInt 500)
                  :* Hole' (NA_I $ Const 1)
                  :* Hole' (NA_I $ Const 2)
-                 :* NP0)
+                 :* Nil)
 
 unif2 :: TreeTerm
 unif2 = HPeel' CZ (HOpq' (SInt 200)
                  :* Hole' (NA_I $ Const 4)
                  :* Hole' (NA_I $ Const 5)
-                 :* NP0)
+                 :* Nil)
 unif22 :: TreeTerm
 unif22 = HPeel' CZ (HOpq' (SInt 500)
                  :* Hole' (NA_I $ Const 4)
                  :* Hole' (NA_I $ Const 5)
-                 :* NP0)
+                 :* Nil)
 
 
 
@@ -140,9 +140,9 @@
                  :* HPeel' (CS CZ)
                     (Hole' (NA_K $ Annotate 6 (SInt 42))
                      :* Hole' (NA_I $ Const 2)
-                     :* HPeel' (CS (CS CZ)) NP0
-                     :* HPeel' (CS (CS CZ)) NP0
-                     :* NP0)
-                 :* HPeel' (CS (CS CZ)) NP0
-                 :* NP0)
+                     :* HPeel' (CS (CS CZ)) Nil
+                     :* HPeel' (CS (CS CZ)) Nil
+                     :* Nil)
+                 :* HPeel' (CS (CS CZ)) Nil
+                 :* Nil)
 -}
diff --git a/src/Data/HDiff/MetaVar.hs b/src/Data/HDiff/MetaVar.hs
--- a/src/Data/HDiff/MetaVar.hs
+++ b/src/Data/HDiff/MetaVar.hs
@@ -1,3 +1,4 @@
+{-# LANGUAGE QuantifiedConstraints #-}
 {-# LANGUAGE FlexibleInstances     #-}
 {-# LANGUAGE TypeSynonymInstances  #-}
 {-# LANGUAGE PolyKinds             #-}
@@ -33,12 +34,12 @@
 data Annotate (x :: *) (f :: k -> *) :: k -> * where
   Annotate :: x -> f i -> Annotate x f i
 
-instance (ShowHO f , Show x) => ShowHO (Annotate x f) where
-  showHO (Annotate i f)
-    = showHO f ++ "[" ++ show i ++ "]"
+instance (ShowHO f , Show x) => Show (Annotate x f k) where
+  show (Annotate i f)
+    = show f ++ "[" ++ show i ++ "]"
 
-instance (EqHO f , Eq x) => EqHO (Annotate x f) where
-  eqHO (Annotate x1 f1) (Annotate x2 f2) = x1 == x2 && eqHO f1 f2
+instance (EqHO f , Eq x) => Eq (Annotate x f k) where
+  (==) (Annotate x1 f1) (Annotate x2 f2) = x1 == x2 && f1 == f2
 
 instance (TestEquality ki) => TestEquality (Annotate x ki) where
   testEquality (Annotate _ x) (Annotate _ y)
diff --git a/src/Data/HDiff/Patch.hs b/src/Data/HDiff/Patch.hs
--- a/src/Data/HDiff/Patch.hs
+++ b/src/Data/HDiff/Patch.hs
@@ -1,8 +1,9 @@
-{-# LANGUAGE TupleSections    #-}
-{-# LANGUAGE FlexibleContexts #-}
-{-# LANGUAGE DataKinds        #-}
-{-# LANGUAGE PolyKinds        #-}
-{-# LANGUAGE GADTs            #-}
+{-# LANGUAGE QuantifiedConstraints #-}
+{-# LANGUAGE TupleSections         #-}
+{-# LANGUAGE FlexibleContexts      #-}
+{-# LANGUAGE DataKinds             #-}
+{-# LANGUAGE PolyKinds             #-}
+{-# LANGUAGE GADTs                 #-}
 module Data.HDiff.Patch where
 
 import           Control.Monad.State
@@ -160,7 +161,7 @@
     go l r (Hole _ var) ex = (,r) <$> substInsert' "l" l var ex 
     go l r pa (Hole _ var) = (l,) <$> substInsert' "r" r var pa
     go l r (HOpq _ oa) (HOpq _ ox)
-      | eqHO oa ox = return (l , r)
+      | oa == ox  = return (l , r)
       | otherwise = throwError (IncompatibleOpqs oa ox)
     go l r pa@(HPeel _ ca ppa) x@(HPeel _ cx px) =
       case testEquality ca cx of
diff --git a/src/Data/HDiff/Patch/Merge.hs b/src/Data/HDiff/Patch/Merge.hs
--- a/src/Data/HDiff/Patch/Merge.hs
+++ b/src/Data/HDiff/Patch/Merge.hs
@@ -1,3 +1,4 @@
+{-# LANGUAGE QuantifiedConstraints #-}
 {-# LANGUAGE FlexibleInstances     #-}
 {-# LANGUAGE TypeSynonymInstances  #-}
 {-# LANGUAGE MultiParamTypeClasses #-}
@@ -67,6 +68,7 @@
 --  of @p@ so that it could be applied to an element in the
 --  image of @q@.
 (//) :: ( Applicable ki codes (Holes2 ki codes)
+        , EqHO ki , ShowHO ki
         , HasDatatypeInfo ki fam codes 
         )
      => Patch ki codes ix
@@ -83,7 +85,7 @@
 --  Precondition: before calling @reconcile p q@, make sure
 --                @p@ and @q@ are different.
 reconcile :: forall ki codes fam at
-           . ( Applicable ki codes (Holes2 ki codes)
+           . ( Applicable ki codes (Holes2 ki codes) , EqHO ki , ShowHO ki
              , HasDatatypeInfo ki fam codes 
              ) 
           => RawPatch ki codes at
@@ -135,10 +137,6 @@
     go []     = M.empty
     go (v:vs) = M.alter (Just . maybe 1 (+1)) v (go vs)
 
-
-instance ShowHO x => Show (Exists x) where
-  show (Exists x) = showHO x
-
 -- |This will process two changes, represented as a spine and
 -- inner changes, into a potential merged patch. The result of @process sp sq@
 -- is supposed to instruct how to construct a patch that
@@ -150,7 +148,7 @@
 -- need to adapt @sp@ to @sq@. After we are done, we know whether
 -- we need to adapt @sp@, return @sp@ as is, or there is a conflict.
 --
-process :: (Applicable ki codes (Holes2 ki codes))
+process :: (Applicable ki codes (Holes2 ki codes) , EqHO ki , ShowHO ki)
         => HolesHoles2 ki codes at -> HolesHoles2 ki codes at
         -> ProcessOutcome ki codes
 process sp sq =
@@ -203,7 +201,7 @@
     -- |Step2 checks a condition for the own-variable mappints
     -- of the anti-unification of p and q! note this is different
     -- altogether from step 1!!!
-    step2 :: (Applicable ki codes (Holes2 ki codes))
+    step2 :: (Applicable ki codes (Holes2 ki codes) , EqHO ki , ShowHO ki)
           => HolesHoles2 ki codes at -> HolesHoles2 ki codes at
           -> ExceptT String (State (Subst ki codes (Holes2 ki codes))) ()
     step2 pp qq = do
diff --git a/src/Data/HDiff/Patch/Show.hs b/src/Data/HDiff/Patch/Show.hs
--- a/src/Data/HDiff/Patch/Show.hs
+++ b/src/Data/HDiff/Patch/Show.hs
@@ -1,10 +1,11 @@
-{-# LANGUAGE UndecidableInstances #-}
-{-# LANGUAGE FlexibleInstances    #-}
-{-# LANGUAGE RankNTypes           #-}
-{-# LANGUAGE PolyKinds            #-}
-{-# LANGUAGE DataKinds            #-}
-{-# LANGUAGE GADTs                #-}
-{-# OPTIONS_GHC -Wno-orphans      #-}
+{-# LANGUAGE QuantifiedConstraints #-}
+{-# LANGUAGE UndecidableInstances  #-}
+{-# LANGUAGE FlexibleInstances     #-}
+{-# LANGUAGE RankNTypes            #-}
+{-# LANGUAGE PolyKinds             #-}
+{-# LANGUAGE DataKinds             #-}
+{-# LANGUAGE GADTs                 #-}
+{-# OPTIONS_GHC -Wno-orphans       #-}
 module Data.HDiff.Patch.Show where
 
 import           System.IO
@@ -124,8 +125,8 @@
       => Show (Delta (Holes ki codes phi) at) where
   show (del :*: ins)
     = unlines $ doubleColumn 75
-        (holesPretty (Proxy :: Proxy fam) id (pretty . showHO) del)
-        (holesPretty (Proxy :: Proxy fam) id (pretty . showHO) ins)
+        (holesPretty (Proxy :: Proxy fam) id (pretty . show) del)
+        (holesPretty (Proxy :: Proxy fam) id (pretty . show) ins)
   show _ = undefined -- ghc seems to really want this to see the patterns are complete.
 
 
diff --git a/src/Data/HDiff/Patch/Thinning.hs b/src/Data/HDiff/Patch/Thinning.hs
--- a/src/Data/HDiff/Patch/Thinning.hs
+++ b/src/Data/HDiff/Patch/Thinning.hs
@@ -1,3 +1,4 @@
+{-# LANGUAGE QuantifiedConstraints #-}
 {-# LANGUAGE FlexibleContexts      #-}
 {-# LANGUAGE FlexibleInstances     #-}
 {-# LANGUAGE ConstraintKinds       #-}
@@ -20,12 +21,15 @@
 import           Data.HDiff.Change
 import qualified Data.HDiff.Change.Thinning as CT
 
-thin :: (ShowHO ki , TestEquality ki, EqHO ki)
+thin :: forall ki codes at
+      . (ShowHO ki , TestEquality ki, EqHO ki)
      => RawPatch ki codes at
      -> RawPatch ki codes at
      -> Either (CT.ThinningErr ki codes) (RawPatch ki codes at)
 thin p q = holesMapM (uncurry' go) $ holesLCP p (q `withFreshNamesFrom` p)
   where
+    go :: RawPatch ki codes at' -> RawPatch ki codes at'
+       -> Either (CT.ThinningErr ki codes) (CChange ki codes at') 
     go cp cq = let cp' = distrCChange cp
                    cq' = distrCChange cq 
                 in CT.thin cp' (domain cq')
diff --git a/src/Data/HDiff/Patch/TreeEditDistance.hs b/src/Data/HDiff/Patch/TreeEditDistance.hs
--- a/src/Data/HDiff/Patch/TreeEditDistance.hs
+++ b/src/Data/HDiff/Patch/TreeEditDistance.hs
@@ -1,9 +1,10 @@
-{-# LANGUAGE ViewPatterns        #-}
-{-# LANGUAGE TypeOperators       #-}
-{-# LANGUAGE GADTs               #-}
-{-# LANGUAGE PolyKinds           #-}
-{-# LANGUAGE DataKinds           #-}
-{-# LANGUAGE ScopedTypeVariables #-}
+{-# LANGUAGE QuantifiedConstraints #-}
+{-# LANGUAGE ViewPatterns          #-}
+{-# LANGUAGE TypeOperators         #-}
+{-# LANGUAGE GADTs                 #-}
+{-# LANGUAGE PolyKinds             #-}
+{-# LANGUAGE DataKinds             #-}
+{-# LANGUAGE ScopedTypeVariables   #-}
 module Data.HDiff.Patch.TreeEditDistance where
 
 import           Data.Type.Equality
@@ -29,13 +30,13 @@
                <$> toES' ppa px
 
 listId :: ListPrf a -> ListPrf a :~: ListPrf (a :++: '[]) 
-listId Nil      = Refl
-listId (Cons a) = case listId a of
-                    Refl -> Refl
+listId LP_Nil      = Refl
+listId (LP_Cons a) = case listId a of
+                      Refl -> Refl
 
 toES' :: (EqHO ki , ShowHO ki , TestEquality ki)
       => NP (RawPatch ki codes) sum -> PoA ki (Fix ki codes) sum
       -> Either String (GD.ES ki codes sum sum)
-toES' NP0 NP0             = return GD.ES0
+toES' Nil Nil             = return GD.ES0
 toES' (p :* ps) (x :* xs) = TED.appendES <$> toES p x <*> toES' ps xs
 
diff --git a/src/Generics/MRSOP/HDiff/Renderer.hs b/src/Generics/MRSOP/HDiff/Renderer.hs
--- a/src/Generics/MRSOP/HDiff/Renderer.hs
+++ b/src/Generics/MRSOP/HDiff/Renderer.hs
@@ -44,7 +44,7 @@
          -> Constr (Lkup ix codes) c
          -> NP (Const (Doc ann)) (Lkup c (Lkup ix codes))
          -> Doc ann
-renderNP pf sty idx c NP0
+renderNP pf sty idx c Nil
   = sty $ PP.pretty (constructorName (constrInfoFor pf idx c))
 renderNP pf sty idx c p
   = let ci = constrInfoFor pf idx c
diff --git a/src/Languages/RTree.hs b/src/Languages/RTree.hs
--- a/src/Languages/RTree.hs
+++ b/src/Languages/RTree.hs
@@ -1,3 +1,4 @@
+{-# LANGUAGE StandaloneDeriving    #-}
 {-# LANGUAGE TupleSections         #-}
 {-# LANGUAGE RankNTypes            #-}
 {-# LANGUAGE FlexibleInstances     #-}
@@ -40,8 +41,7 @@
 data W :: WKon -> * where
   W_String  :: String  -> W 'WString
 
-instance EqHO W where
-  eqHO (W_String s)  (W_String ss) = s == ss
+deriving instance Eq (W x)
 
 instance DigestibleHO W where
   digestHO (W_String s)  = hashStr s
@@ -49,8 +49,8 @@
 instance RendererHO W where
   renderHO (W_String s) = pretty s
 
-instance ShowHO W where
-  showHO (W_String s)  = s
+instance Show (W x) where
+  show (W_String s)  = s
 
 instance TestEquality W where
   testEquality (W_String _)  (W_String _)  = Just Refl