diff --git a/generics-mrsop.cabal b/generics-mrsop.cabal
--- a/generics-mrsop.cabal
+++ b/generics-mrsop.cabal
@@ -4,10 +4,10 @@
 --
 -- see: https://github.com/sol/hpack
 --
--- hash: 6e4f3e6671cfaeff58301e7f3a59013225b8995b0e8cb2fbb43c1d48c1158cf0
+-- hash: 70539c4715fe3541bae476f1a318b450ec2afab772fca5e4d87aa41b9eab122a
 
 name:           generics-mrsop
-version:        2.2.0
+version:        2.3.0
 synopsis:       Generic Programming with Mutually Recursive Sums of Products.
 description:    A library that supports generic programming for mutually recursive families in the sum-of-products style. . A couple usage examples can be found under "Generics.MRSOP.Examples" .
 category:       Generics
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
@@ -6,6 +6,7 @@
 {-# LANGUAGE TypeOperators     #-}
 {-# LANGUAGE DataKinds         #-}
 {-# LANGUAGE PolyKinds         #-}
+{-# OPTIONS_GHC -Wno-orphans   #-}
 -- | Standard representation of n-ary products.
 module Generics.MRSOP.Base.NP
   ( SOP.NP(..)
@@ -25,6 +26,19 @@
 import           Data.SOP.NP (NP(..))
 import qualified Data.SOP.NP as SOP
 import Generics.MRSOP.Util
+
+-- |@since 2.3.0
+instance EqHO f => EqHO (NP f) where
+  eqHO (x :* xs) (y :* ys) = eqHO x y && eqHO xs ys
+  eqHO Nil       Nil       = True
+
+-- |@since 2.3.0
+instance ShowHO f => ShowHO (NP f) where
+  showsPrecHO _ Nil = showString "Nil"
+  showsPrecHO d (x :* xs) = showParen (d > ifx_prec) $
+    showsPrecHO (ifx_prec+1) x . showString " :* " . showsPrecHO (ifx_prec+1) xs
+   where ifx_prec = 5
+
 
 -- * Relation to IsList predicate
 
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
@@ -9,6 +9,7 @@
 {-# LANGUAGE ScopedTypeVariables         #-}
 {-# LANGUAGE ScopedTypeVariables         #-}
 {-# OPTIONS_GHC -Wno-name-shadowing      #-}
+{-# OPTIONS_GHC -Wno-orphans             #-}
 
 -- | Standard representation of n-ary sums.
 module Generics.MRSOP.Base.NS
@@ -41,6 +42,21 @@
 
 {-# COMPLETE Here, There #-}
 
+-- |@since 2.3.0
+instance EqHO f => EqHO (NS f) where
+  eqHO (Here fx) (Here fy) = eqHO fx fy
+  eqHO (There x) (There y) = eqHO x y
+  eqHO _         _         = False
+
+-- |@since 2.3.0
+instance ShowHO f => ShowHO (NS f) where
+  showsPrecHO d (Here fx) = showParen (d > app_prec) $
+    showString "Here " . showsPrecHO (app_prec+1) fx
+   where app_prec = 10
+  showsPrecHO d (There fx) = showParen (d > app_prec) $
+    showString "There " . showsPrecHO (app_prec+1) fx
+   where app_prec = 10
+
 -- * Map, Zip and Elim
 
 -- |Maps over a sum
@@ -66,7 +82,6 @@
 zipNS _         _         = mzero
 
 -- * Catamorphism
-
 
 -- |Consumes a value of type 'NS'
 cataNS :: (forall x xs . f x  -> r (x ': xs))
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
@@ -49,12 +49,16 @@
   NA_I :: (IsNat k) => phi k -> NA ki phi ('I k) 
   NA_K ::              ki  k -> NA ki phi ('K k)
 
-instance (EqHO phi , EqHO ki) => Eq (NA ki phi at) where
-  (==) = eqNA (==) (==)
+instance (EqHO phi , EqHO ki) => EqHO (NA ki phi) where
+  eqHO = eqNA eqHO eqHO
 
-instance (ShowHO phi , ShowHO ki) => Show (NA ki phi at) where
-  show (NA_I i) = "(NA_I " ++ show i ++ ")"
-  show (NA_K k) = "(NA_K " ++ show k ++ ")"
+instance (ShowHO phi , ShowHO ki) => ShowHO (NA ki phi) where
+  showsPrecHO d (NA_I i) = showParen (d > app_prec) $
+      showString "NA_I " . showsPrecHO (app_prec+1) i
+    where app_prec = 10
+  showsPrecHO d (NA_K k) = showParen (d > app_prec) $
+      showString "NA_K " . showsPrecHO (app_prec+1) k
+    where app_prec = 10
 
 instance (TestEquality ki) => TestEquality (NA ki phi) where
   testEquality (NA_I _) (NA_K _) = Nothing
@@ -124,8 +128,13 @@
 newtype Rep (ki :: kon -> *) (phi :: Nat -> *) (code :: [[Atom kon]])
   = Rep { unRep :: NS (PoA ki phi) code }
 
-instance (EqHO phi, EqHO ki) => Eq (Rep ki phi at) where
-  (==) = eqRep (==) (==)
+instance (EqHO phi, EqHO ki) => EqHO (Rep ki phi) where
+  eqHO = eqRep eqHO eqHO
+
+instance (ShowHO ki , ShowHO phi) => ShowHO (Rep ki phi) where
+  showsPrecHO d (Rep ns) = showParen (d > app_prec) $
+      showString "Rep " . showsPrecHO (app_prec+1) ns
+    where app_prec = 10
   
 -- |Product of Atoms is a handy synonym to have.
 type PoA (ki :: kon -> *) (phi :: Nat -> *) = NP (NA ki phi)
@@ -277,8 +286,13 @@
 newtype Fix (ki :: kon -> *) (codes :: [[[ Atom kon ]]]) (n :: Nat)
   = Fix { unFix :: Rep ki (Fix ki codes) (Lkup n codes) }
 
-instance EqHO ki => Eq (Fix ki codes ix) where
-  (==) = eqFix (==)
+instance EqHO ki => EqHO (Fix ki codes) where
+  eqHO = eqFix eqHO
+
+instance (ShowHO ki) => ShowHO (Fix ki codes) where
+  showsPrecHO d (Fix rep) = showParen (d > app_prec) $
+      showString "Fix " . showsPrecHO (app_prec+1) rep
+    where app_prec = 10
 
 -- | Catamorphism over fixpoints
 cata :: (IsNat ix)
diff --git a/src/Generics/MRSOP/Holes.hs b/src/Generics/MRSOP/Holes.hs
--- a/src/Generics/MRSOP/Holes.hs
+++ b/src/Generics/MRSOP/Holes.hs
@@ -308,13 +308,13 @@
 --
 --  We use a function to combine annotations in case it is
 --  necessary.
-holesLCP :: (forall k . Eq (ki k))
+holesLCP :: (EqHO ki)
          => Holes ki codes f at
          -> Holes ki codes g at
          -> Holes ki codes (Holes ki codes f :*: Holes ki codes g) at
 holesLCP (HOpq _ kx) (HOpq _ ky)
-  | kx == ky  = HOpq' kx
-  | otherwise = Hole' (HOpq' kx :*: HOpq' ky)
+  | eqHO kx ky = HOpq' kx
+  | otherwise  = Hole' (HOpq' kx :*: HOpq' ky)
 holesLCP (HPeel a cx px) (HPeel b cy py)
   = case testEquality cx cy of
       Nothing   -> Hole'  (HPeel a cx px :*: HPeel b cy py)
@@ -357,12 +357,12 @@
 
 -- -* Instances
 
-instance (EqHO phi , EqHO ki) => Eq (Holes ki codes phi ix) where
-  utx == uty = and $ holesGetHolesAnnWith' (uncurry' cmp) $ holesLCP utx uty
+instance (EqHO phi , EqHO ki) => EqHO (Holes ki codes phi) where
+  eqHO utx uty = and $ holesGetHolesAnnWith' (uncurry' cmp) $ holesLCP utx uty
     where
       cmp :: HolesAnn ann ki codes phi at -> HolesAnn ann ki codes phi at -> Bool
-      cmp (Hole _ x) (Hole _ y) = x == y
-      cmp (HOpq _ x) (HOpq _ y) = x == y
+      cmp (Hole _ x) (Hole _ y) = x `eqHO` y
+      cmp (HOpq _ x) (HOpq _ y) = x `eqHO` y
       cmp _           _         = False
 
 holesShow :: forall ki ann f fam codes ix
@@ -371,8 +371,8 @@
           -> (forall at . ann at -> ShowS)
           -> HolesAnn ann ki codes f ix
           -> ShowS
-holesShow _ f (Hole a x)       = ('`':) . f a . showString (show x) 
-holesShow _ f (HOpq a k)       = f a . showString (show k)
+holesShow _ f (Hole a x)       = ('`':) . f a . showString (showHO x) 
+holesShow _ f (HOpq a k)       = f a . showString (showHO k)
 holesShow p f h@(HPeel a c rest)
   = showParen (needParens h) $ showString cname
                              . f a
@@ -394,11 +394,11 @@
     needParens _               = True
 
 instance {-# OVERLAPPABLE #-} (HasDatatypeInfo ki fam codes , ShowHO ki , ShowHO f , ShowHO ann)
-    => Show (HolesAnn ann ki codes f ix) where
-  show h = holesShow (Proxy :: Proxy fam) showsAnn h ""
+    => ShowHO (HolesAnn ann ki codes f) where
+  showHO h = holesShow (Proxy :: Proxy fam) showsAnn h ""
     where
       showsAnn ann = showString "{"
-                   . showString (show ann)
+                   . showString (showHO ann)
                    . showString "}"
 
 instance {-# OVERLAPPING #-} (HasDatatypeInfo ki fam codes , ShowHO ki , ShowHO f)
diff --git a/src/Generics/MRSOP/Opaque.hs b/src/Generics/MRSOP/Opaque.hs
--- a/src/Generics/MRSOP/Opaque.hs
+++ b/src/Generics/MRSOP/Opaque.hs
@@ -14,6 +14,7 @@
 module Generics.MRSOP.Opaque where
 
 import Data.Type.Equality
+import Generics.MRSOP.Util
 
 -- * Opaque Types
 --
@@ -48,7 +49,7 @@
   SChar    :: Char    -> Singl 'KChar
   SString  :: String  -> Singl 'KString
 
-deriving instance Eq   (Singl k)
+deriving instance Eq (Singl k)
 
 instance Show (Singl k) where
  show (SInt      a) = show a 
@@ -62,6 +63,12 @@
 -- |Equality over singletons
 eqSingl :: Singl k -> Singl k -> Bool
 eqSingl = (==)
+
+instance EqHO Singl where
+  eqHO = eqSingl
+
+instance ShowHO Singl where
+  showHO = show
 
 instance TestEquality Singl where
   testEquality (SInt _) (SInt _)         = Just Refl
diff --git a/src/Generics/MRSOP/Util.hs b/src/Generics/MRSOP/Util.hs
--- a/src/Generics/MRSOP/Util.hs
+++ b/src/Generics/MRSOP/Util.hs
@@ -1,5 +1,4 @@
 {-# LANGUAGE TypeSynonymInstances  #-}
-{-# LANGUAGE QuantifiedConstraints #-}
 {-# LANGUAGE ConstraintKinds       #-}
 {-# LANGUAGE GADTs                 #-}
 {-# LANGUAGE TypeFamilies          #-}
@@ -37,7 +36,7 @@
   , Lkup , Idx , El(..) , getElSNat , into
 
     -- * Higher-order Eq and Show
-  , EqHO , ShowHO
+  , EqHO(..) , ShowHO(..)
   ) where
 
 import Data.Proxy
@@ -187,19 +186,66 @@
 type L3 xs ys zs    = (IsList xs, IsList ys, IsList zs) 
 type L4 xs ys zs as = (IsList xs, IsList ys, IsList zs, IsList as) 
 
--- |Constraint synonym replacing the old @EqHO@ hack.
--- @since 2.2.0
-type EqHO   f = forall x . Eq   (f x)
+-- |Higher order , poly kinded, version of 'Eq'
+-- @since 2.3.0
+class EqHO (f :: ki -> *) where
+  eqHO :: forall k . f k -> f k -> Bool
 
--- |Constraint synonym replacing the old @ShowHO@ hack.
--- @since 2.2.0
-type ShowHO f = forall x . Show (f x)
+instance Eq a => EqHO (Const a) where
+  eqHO (Const a) (Const b) = a == b
 
-instance (EqHO f , EqHO g) => Eq ((f :*: g) x) where
-  (fx :*: gx) == (fy :*: gy) = fx == fy && gx == gy
+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) => Eq (Sum f g x) where
-  (InL x) == (InL y) = x == y
-  (InR x) == (InR y) = x == y
-  _       == _       = False
+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, poly kinded, version of 'Show'; We provide
+-- the same 'showsPrec' mechanism. The documentation of "Text.Show"
+-- has a good example of the correct usage of 'showsPrec':
+--
+-- > 
+-- > infixr 5 :^:
+-- > data Tree a =  Leaf a  |  Tree a :^: Tree a
+-- >
+-- > instance (Show a) => Show (Tree a) where
+-- >   showsPrec d (Leaf m) = showParen (d > app_prec) $
+-- >        showString "Leaf " . showsPrec (app_prec+1) m
+-- >     where app_prec = 10
+-- > 
+-- >   showsPrec d (u :^: v) = showParen (d > up_prec) $
+-- >        showsPrec (up_prec+1) u .
+-- >        showString " :^: "      .
+-- >        showsPrec (up_prec+1) v
+-- >     where up_prec = 5
+--
+-- @since 2.3.0
+class ShowHO (f :: ki -> *) where
+  showHO      :: forall k . f k -> String
+  showsPrecHO :: forall k . Int -> f k -> ShowS
+  {-# MINIMAL showHO | showsPrecHO #-}
+
+  showHO fx          = showsPrecHO 0 fx ""
+  showsPrecHO _ fx s = showHO fx ++ s
+
+instance Show a => ShowHO (Const a) where
+  showsPrecHO d (Const a) = showParen (d > app_prec) $
+      showString "Const " . showsPrec (app_prec + 1) a
+    where app_prec = 10
+
+instance (ShowHO f , ShowHO g) => ShowHO (Product f g) where
+  showsPrecHO d (Pair x y) = showParen (d > app_prec) $
+      showString "Pair " . showsPrecHO (app_prec+1) x
+                         . showString " "
+                         . showsPrecHO (app_prec+1) y
+    where app_prec = 10
+
+instance (ShowHO f , ShowHO g) => ShowHO (Sum f g) where
+  showsPrecHO d (InL fx) = showParen (d > app_prec) $
+      showString "InL " . showsPrecHO (app_prec + 1) fx
+    where app_prec = 10
+  showsPrecHO d (InR gx) = showParen (d > app_prec) $
+      showString "InR " . showsPrecHO (app_prec + 1) gx
+    where app_prec = 10