diff --git a/pringletons.cabal b/pringletons.cabal
--- a/pringletons.cabal
+++ b/pringletons.cabal
@@ -1,5 +1,5 @@
 name:                pringletons
-version:             0.3
+version:             0.4
 synopsis:            Classes and data structures complementing the singletons library
 description:         Please see README.md
 homepage:            https://github.com/andrewthad/pringletons
@@ -18,10 +18,10 @@
     Data.Singletons.Map
     Data.Singletons.Class
     Data.Case.Enumerate
-  build-depends:       
-      base >= 4.7 && < 5
+  build-depends:
+      base >= 4.9 && < 5
     , hashable
-    , singletons
+    , singletons >= 2.2 && < 2.3
     , aeson
     , text
     , vector
diff --git a/src/Data/Case/Enumerate.hs b/src/Data/Case/Enumerate.hs
--- a/src/Data/Case/Enumerate.hs
+++ b/src/Data/Case/Enumerate.hs
@@ -1,4 +1,4 @@
-module Data.Case.Enumerate 
+module Data.Case.Enumerate
   ( enumerateConstructors
   ) where
 
@@ -19,7 +19,7 @@
 
 enumerateConstructors :: Name -> Name -> Exp -> Q Exp
 enumerateConstructors vname name expr = do
-  TyConI (DataD _ _ _ ctors _) <- reify name
+  TyConI (DataD _ _ _ _ ctors _) <- reify name
   matches <- forM ctors $ \(NormalC cname args) -> case args of
     [] -> return $ Match (ConP (sketchyNameSingletonize cname) []) (NormalB expr) []
     _ -> fail "constConstructors2: empty data constructor required"
@@ -27,6 +27,6 @@
 
 sketchyNameSingletonize :: Name -> Name
 sketchyNameSingletonize = id
-  . mkName . ('S':) . reverse 
+  . mkName . ('S':) . reverse
   . takeWhile (/= '.') . reverse . show
 
diff --git a/src/Data/Singletons/Class.hs b/src/Data/Singletons/Class.hs
--- a/src/Data/Singletons/Class.hs
+++ b/src/Data/Singletons/Class.hs
@@ -1,13 +1,17 @@
 {-# LANGUAGE FlexibleContexts #-}
+{-# LANGUAGE TypeInType #-}
+{-# LANGUAGE UndecidableInstances #-}
 
-module Data.Singletons.Class 
-  ( 
+module Data.Singletons.Class
+  (
   -- * Singleton Classes
   -- $singletonClasses
     EqSing1(..)
   , EqSing2(..)
   , OrdSing1(..)
   , OrdSing2(..)
+  , ShowSing2(..)
+  , ReadSing2(..)
   , HashableSing1(..)
   , HashableSing2(..)
   , ToJSONSing1(..)
@@ -53,7 +57,10 @@
 import Data.Singletons.Decide
 import Data.Text (Text)
 import Data.Functor.Identity
-import Text.Read (readMaybe)
+import Text.Read.Lex (Lexeme(Ident))
+import Text.Read (readMaybe,readPrec,ReadPrec,lexP,parens)
+import Text.ParserCombinators.ReadPrec (readPrec_to_S, prec, step)
+import Text.Show (showChar, showString, showParen)
 import qualified Data.Text as Text
 import qualified Data.Aeson as Aeson
 import qualified Data.Aeson.Types as Aeson
@@ -63,10 +70,11 @@
 import Control.Arrow (first)
 import qualified Data.Vector as Vector
 import Data.Function ((&))
+import Data.Kind (Type)
 
 {- $singletonClasses
- 
- These are singleton variants of the commonly used classes from @base@, 
+
+ These are singleton variants of the commonly used classes from @base@,
  @hashable@, and @aeson@. These variants work on higher-kinded types instead
  of on ground types. For example, if you wrote the following:
 
@@ -87,9 +95,9 @@
  >     SMyChar -> a == b
  >     SMyBool -> a == b
 
- For our example @MyValue@ type, the @EqSing1@ instance is trivial. We simply 
+ For our example @MyValue@ type, the @EqSing1@ instance is trivial. We simply
  pattern match on the singleton and then do the same thing in each case. This
- kind of pattern matching ends up happening any time our universe 
+ kind of pattern matching ends up happening any time our universe
  interpreter maps to types that all have @Eq@ instances. Since writing this
  out is tedious, we can instead use a template haskell function provided in
  the @Data.Case.Enumerate@ module:
@@ -113,6 +121,12 @@
 class EqSing2 f => OrdSing2 f where
   compareSing2 :: Sing a -> Sing b -> f a b -> f a b -> Ordering
 
+class ShowSing2 f where
+  showsPrecSing2 :: Int -> Sing a -> Sing b -> f a b -> ShowS
+
+class ReadSing2 f where
+  readPrecSing2 :: Sing a -> Sing b -> ReadPrec (f a b)
+
 class HashableSing1 f where
   hashWithSaltSing1 :: Sing a -> Int -> f a -> Int
 
@@ -132,14 +146,14 @@
   parseJSONSing2 :: Sing a -> Sing b -> Aeson.Value -> Aeson.Parser (f a b)
 
 {- $kindClasses
- 
- These are kind classes. They express that something is true for all 
+
+ These are kind classes. They express that something is true for all
  singletons of a particular kind. Note that these are different from the
  kind classes provided in the @singletons@ library itself. The methods
  in those classes ('SOrd','SEnum',etc.) work entirely on singletons. Here,
  the methods also work with normal data types.
 
- Notice that classes like @EqKind@ and @OrdKind@ have been omitted from 
+ Notice that classes like @EqKind@ and @OrdKind@ have been omitted from
  this library. The reason is that that functions that would be provided by
  these can be trivially recovered by demoting the results of methods in 'SEq'
  and 'SOrd'.
@@ -148,90 +162,114 @@
  singleton and using the corresponding method from the normal typeclass.
 -}
 
-class (kproxy ~ 'KProxy) => ShowKind (kproxy :: KProxy a) where
-  showsPrecKind :: Int -> Sing (x :: a) -> ShowS
-  default showsPrecKind :: (SingKind kproxy, Show (DemoteRep kproxy)) => Int -> Sing (x :: a) -> ShowS
+class ShowKind k where
+  showsPrecKind :: Int -> Sing (x :: k) -> ShowS
+  default showsPrecKind :: (SingKind k, Show (DemoteRep k)) => Int -> Sing (x :: k) -> ShowS
   showsPrecKind i s xs = showsPrec i (fromSing s) xs
 
-class (kproxy ~ 'KProxy) => ReadKind (kproxy :: KProxy a) where
-  readsPrecKind :: Int -> ReadS (SomeSing kproxy)
-  default readsPrecKind :: (SingKind kproxy, Read (DemoteRep kproxy)) => Int -> ReadS (SomeSing kproxy)
-  readsPrecKind i s = map (first toSing) (readsPrec i s)
+class ReadKind k where
+  readPrecKind :: ReadPrec (SomeSing k)
+  default readPrecKind :: (SingKind k, Read (DemoteRep k)) => ReadPrec (SomeSing k)
+  readPrecKind = fmap toSing readPrec
+  -- readsPrecKind :: Int -> ReadS (SomeSing kproxy)
+  -- default readsPrecKind :: (SingKind kproxy, Read (DemoteRep kproxy)) => Int -> ReadS (SomeSing kproxy)
+  -- readsPrecKind i s = map (first toSing) (readsPrec i s)
 
-class (kproxy ~ 'KProxy) => HashableKind (kproxy :: KProxy a) where
-  hashWithSaltKind :: Int -> Sing (x :: a) -> Int
-  default hashWithSaltKind :: (SingKind kproxy, Hashable (DemoteRep kproxy)) => Int -> Sing (x :: a) -> Int
+class HashableKind k where
+  hashWithSaltKind :: Int -> Sing (x :: k) -> Int
+  default hashWithSaltKind :: (SingKind k, Hashable (DemoteRep k)) => Int -> Sing (x :: k) -> Int
   hashWithSaltKind i s = hashWithSalt i (fromSing s)
 
-class (kproxy ~ 'KProxy) => ToJSONKind (kproxy :: KProxy a) where
-  toJSONKind :: Sing (x :: a) -> Aeson.Value
-  default toJSONKind :: ShowKind kproxy => Sing (x :: a) -> Aeson.Value
+class ToJSONKind k where
+  toJSONKind :: Sing (x :: k) -> Aeson.Value
+  default toJSONKind :: ShowKind k => Sing (x :: k) -> Aeson.Value
   toJSONKind s = Aeson.String (Text.pack (showKind s))
 
-class (kproxy ~ 'KProxy) => FromJSONKind (kproxy :: KProxy a) where
-  parseJSONKind :: Aeson.Value -> Aeson.Parser (SomeSing kproxy)
+class FromJSONKind k where
+  parseJSONKind :: Aeson.Value -> Aeson.Parser (SomeSing k)
+  default parseJSONKind :: ReadKind k => Aeson.Value -> Aeson.Parser (SomeSing k)
+  parseJSONKind (Aeson.String t) = let s = Text.unpack t in
+    case readMaybeKind s of
+      Nothing -> fail ("Could not parse singleton from: " ++ s)
+      Just a -> return a
 
-class (kproxy ~ 'KProxy) => ToJSONKeyKind (kproxy :: KProxy a) where
-  toJSONKeyKind :: Sing (x :: a) -> Text
-  default toJSONKeyKind :: ShowKind kproxy => Sing (x :: a) -> Text
+class ToJSONKeyKind k where
+  toJSONKeyKind :: Sing (x :: k) -> Text
+  default toJSONKeyKind :: ShowKind k => Sing (x :: k) -> Text
   toJSONKeyKind s = Text.pack (showKind s)
 
-class (kproxy ~ 'KProxy) => FromJSONKeyKind (kproxy :: KProxy a) where
-  parseJSONKeyKind :: Text -> Aeson.Parser (SomeSing kproxy)
-  default parseJSONKeyKind :: ReadKind kproxy => Text -> Aeson.Parser (SomeSing kproxy)
-  parseJSONKeyKind t = let s = Text.unpack t in 
+class FromJSONKeyKind k where
+  parseJSONKeyKind :: Text -> Aeson.Parser (SomeSing k)
+  default parseJSONKeyKind :: ReadKind k => Text -> Aeson.Parser (SomeSing k)
+  parseJSONKeyKind t = let s = Text.unpack t in
     case readMaybeKind s of
-      Nothing -> fail ("Could not parse key " ++ s)
+      Nothing -> fail ("Could not parse key: " ++ s)
       Just a -> return a
 
 ------------------------
 -- Data Types
 ------------------------
-newtype Applied1 (f :: TyFun k * -> *) (a :: k) =
+newtype Applied1 (f :: TyFun k Type -> Type) (a :: k) =
   Applied1 { getApplied1 :: Apply f a }
 
-newtype Applied2 (f :: TyFun k (TyFun j * -> *) -> *) (a :: k) (b :: j) =
+-- These all require FlexibleContexts. I do not like this,
+-- but having these instances is important. There is probably
+-- a way to get them without using that extension, but it
+-- will require more work.
+deriving instance Eq (Apply f a) => Eq (Applied1 f a)
+deriving instance Ord (Apply f a) => Ord (Applied1 f a)
+deriving instance Read (Apply f a) => Read (Applied1 f a)
+deriving instance Show (Apply f a) => Show (Applied1 f a)
+deriving instance Hashable (Apply f a) => Hashable (Applied1 f a)
+deriving instance ToJSON (Apply f a) => ToJSON (Applied1 f a)
+deriving instance FromJSON (Apply f a) => FromJSON (Applied1 f a)
+
+newtype Applied2 (f :: TyFun k (TyFun j Type -> Type) -> Type) (a :: k) (b :: j) =
   Applied2 { getApplied2 :: Apply (Apply f a) b }
 
-newtype Applied3 (f :: TyFun k (TyFun j (TyFun l * -> *) -> *) -> *) (a :: k) (b :: j) (c :: l) =
+newtype Applied3 (f :: TyFun k (TyFun j (TyFun l Type -> Type) -> Type) -> Type) (a :: k) (b :: j) (c :: l) =
   Applied3 { getApplied3 :: Apply (Apply (Apply f a) b) c }
 
-data SingWith1 (kproxy :: KProxy k) (f :: k -> *) (a :: k) where
-  SingWith1 :: Sing a -> f a -> SingWith1 'KProxy f a
+data SingWith1 k (f :: k -> Type) (a :: k) where
+  SingWith1 :: Sing a -> f a -> SingWith1 k f a
 
-data SomeSingWith1 (kproxy :: KProxy k) (f :: k -> *) where
-  SomeSingWith1 :: Sing a -> f a -> SomeSingWith1 'KProxy f
+data SomeSingWith1 (k :: Type) (f :: k -> Type) where
+  SomeSingWith1 :: forall (a :: k) (f :: k -> Type).
+    Sing a -> f a -> SomeSingWith1 k f
 
-type SomeSingWith1' = SomeSingWith1 'KProxy
+type family SomeSingWith1' (f :: k -> Type) :: Type where
+  SomeSingWith1' (f :: k -> Type) = SomeSingWith1 k f
 
-data SomeSingWith2 (kproxy1 :: KProxy k) (kproxy2 :: KProxy j) (f :: k -> j -> *) where
-  SomeSingWith2 :: Sing a -> Sing b -> f a b -> SomeSingWith2 'KProxy 'KProxy f
+data SomeSingWith2 (k :: Type) (j :: Type) (f :: k -> j -> Type) where
+  SomeSingWith2 :: forall (a :: k) (b :: j) (f :: k -> j -> Type).
+    Sing a -> Sing b -> f a b -> SomeSingWith2 k j f
 
-type SomeSingWith2' = SomeSingWith2 'KProxy 'KProxy
+type family SomeSingWith2' (f :: k -> j -> Type) :: Type where
+  SomeSingWith2' (f :: k -> j -> Type) = SomeSingWith2 k j f
 
 {- $appliedClasses
- 
+
  These are additional classes used to provide instances for 'Applied1'.
  If you have a defunctionalized typeclass that provides produces types
  in the category hask, you can use this. Instances will often look like
  this:
 
  > data Thing = ...
- > type family ToType (x :: Thing) :: * where ...
+ > type family ToType (x :: Thing) :: Type where ...
  > instance EqApplied1 ToTypeSym0 where
  >   eqApplied1 _ x (Applied a) (Applied b) = $(enumerateConstructors 'x ''Thing =<< [|a == b|])
 
 -}
-class EqApplied1 (f :: TyFun k * -> *) where
+class EqApplied1 (f :: TyFun k Type -> Type) where
   eqApplied1 :: proxy f -> Sing a -> Apply f a -> Apply f a -> Bool
 
-class HashableApplied1 (f :: TyFun k * -> *) where
+class HashableApplied1 (f :: TyFun k Type -> Type) where
   hashWithSaltApplied1 :: proxy f -> Sing a -> Int -> Apply f a -> Int
 
-class ToJSONApplied1 (f :: TyFun k * -> *) where
+class ToJSONApplied1 (f :: TyFun k Type -> Type) where
   toJSONApplied1 :: proxy f -> Sing a -> Apply f a -> Aeson.Value
 
-class FromJSONApplied1 (f :: TyFun k * -> *) where
+class FromJSONApplied1 (f :: TyFun k Type -> Type) where
   parseJSONApplied1 :: proxy f -> Sing a -> Aeson.Value -> Aeson.Parser (Apply f a)
 
 
@@ -252,16 +290,41 @@
   hashWithSaltSing1 s i (Applied1 a) = hashWithSaltApplied1 (Proxy :: Proxy f) s i a
 
 instance (EqSing1 f, SDecide kproxy) => Eq (SomeSingWith1 kproxy f) where
-  SomeSingWith1 s1 v1 == SomeSingWith1 s2 v2 = 
+  SomeSingWith1 s1 v1 == SomeSingWith1 s2 v2 =
     case testEquality s1 s2 of
       Nothing -> False
       Just Refl -> eqSing1 s1 v1 v2
 
+instance (ShowKind kproxy1, ShowKind kproxy2, ShowSing2 f) => Show (SomeSingWith2 kproxy1 kproxy2 f) where
+  showsPrec i (SomeSingWith2 s1 s2 f) =
+    showString "SomeSingWith2 " . showParen True
+      ( showsPrecKind 11 s1
+      . showChar ' '
+      . showsPrecKind 11 s2
+      . showChar ' '
+      . showsPrecSing2 11 s1 s2 f
+      )
+
+instance (ReadKind k, ReadKind j, ReadSing2 f) => Read (SomeSingWith2 k j f) where
+  readPrec = parens $ prec 10 $ do
+    Ident "SomeSingWith2" <- lexP
+    SomeSing s1 <- step readPrecKind
+    SomeSing s2 <- step readPrecKind
+    f <- step (readPrecSing2 s1 s2)
+    return (SomeSingWith2 s1 s2 f)
+
+
+instance (SDecide kproxy1, SDecide kproxy2, EqSing2 f) => Eq (SomeSingWith2 kproxy1 kproxy2 f) where
+  SomeSingWith2 s1 s2 a == SomeSingWith2 t1 t2 b = fromMaybe False $ do
+    Refl <- testEquality s1 t1
+    Refl <- testEquality s2 t2
+    return $ eqSing2 s1 s2 a b
+
 instance (ToJSONKind kproxy1, ToJSONKind kproxy2, ToJSONSing2 f) => ToJSON (SomeSingWith2 kproxy1 kproxy2 f) where
-  toJSON (SomeSingWith2 s1 s2 v) = 
+  toJSON (SomeSingWith2 s1 s2 v) =
     toJSON [toJSONKind s1, toJSONKind s2, toJSONSing2 s1 s2 v]
 
-instance (FromJSONKind kproxy1, FromJSONKind kproxy2, FromJSONSing2 f) => FromJSON (SomeSingWith2 kproxy1 kproxy2 f) where
+instance (FromJSONKind k, FromJSONKind j, FromJSONSing2 f) => FromJSON (SomeSingWith2 k j f) where
   parseJSON (Aeson.Array xs) = case Vector.toList xs of
     [v1,v2,v] -> do
       SomeSing s1 <- parseJSONKind v1
@@ -271,23 +334,26 @@
     _ -> fail "SomeSingWith2: expected Array of three elements"
   parseJSON _ = mempty
 
-instance (HashableKind kproxy1, HashableSing1 f) => Hashable (SomeSingWith1 kproxy1 f) where
+instance (HashableKind k, HashableSing1 f) => Hashable (SomeSingWith1 k f) where
   hashWithSalt i (SomeSingWith1 s v) = i
-    & flip hashWithSaltKind s 
+    & flip hashWithSaltKind s
     & flip (hashWithSaltSing1 s) v
 
-showKind :: forall (kproxy :: KProxy k) (a :: k). ShowKind kproxy => Sing a -> String
+showKind :: forall (a :: k). ShowKind k => Sing a -> String
 showKind x = showsPrecKind 0 x ""
 
+readsPrecKind :: ReadKind kproxy => Int -> ReadS (SomeSing kproxy)
+readsPrecKind = readPrec_to_S readPrecKind
+
 readMaybeKind :: ReadKind kproxy => String -> Maybe (SomeSing kproxy)
-readMaybeKind s = listToMaybe 
-  $ mapMaybe (\(a,x) -> if null x then Just a else Nothing) 
+readMaybeKind s = listToMaybe
+  $ mapMaybe (\(a,x) -> if null x then Just a else Nothing)
   $ readsPrecKind 0 s
 
 -- | Helper function to demote an equality check. It would be nice if
 --   this could be added as an 'Eq' instance for 'SomeSing', but it
 --   would required collapsing a lot of the modules in 'singletons'
---   to prevent cyclic imports. Or it could be provided as an orphan 
+--   to prevent cyclic imports. Or it could be provided as an orphan
 --   instance.
 eqSome :: SEq kproxy => SomeSing kproxy -> SomeSing kproxy -> Bool
 eqSome (SomeSing a) (SomeSing b) = fromSing (a %:== b)
diff --git a/src/Data/Singletons/Map.hs b/src/Data/Singletons/Map.hs
--- a/src/Data/Singletons/Map.hs
+++ b/src/Data/Singletons/Map.hs
@@ -1,5 +1,7 @@
+{-# LANGUAGE TypeInType #-}
+
 {-| This is a dependent version of the @Data.Map@ module from @containers@.
- 
+
     This module was largely copied from the @dependent-map@ package.
 -}
 module Data.Singletons.Map where
@@ -18,38 +20,41 @@
 import Data.Text (Text)
 import Data.Hashable
 import Data.Vinyl.Core (Rec(..))
+import Data.Kind (Type)
 
-data SingMap (kproxy :: KProxy j) (f :: j -> *) where
-    Tip :: SingMap kproxy f
+data SingMap (k :: Type) (f :: k -> Type) where
+    Tip :: SingMap k f
     Bin :: {- sz    -} !Int
         -> {- key   -} !(Sing v)
         -> {- value -} !(f v)
-        -> {- left  -} !(SingMap kproxy f)
-        -> {- right -} !(SingMap kproxy f)
-        -> SingMap kproxy f
+        -> {- left  -} !(SingMap k f)
+        -> {- right -} !(SingMap k f)
+        -> SingMap k f
 
-type SingMap' = SingMap 'KProxy
+type family SingMap' (f :: k -> Type) :: Type where
+  SingMap' (f :: k -> Type) = SingMap k f
 
-instance (SEq kproxy, SDecide kproxy, EqSing1 f) => Eq (SingMap kproxy f) where
+
+instance (SEq k, SDecide k, EqSing1 f) => Eq (SingMap k f) where
   t1 == t2 = (size t1 == size t2) && (toAscList t1 == toAscList t2)
 
-instance (HashableKind kproxy, HashableSing1 f) => Hashable (SingMap kproxy f) where
+instance (HashableKind k, HashableSing1 f) => Hashable (SingMap k f) where
   hashWithSalt i m = hashWithSalt i (toAscList m)
 
-instance (ToJSONKeyKind kproxy, ToJSONSing1 f) => ToJSON (SingMap kproxy f) where
+instance (ToJSONKeyKind k, ToJSONSing1 f) => ToJSON (SingMap k f) where
   toJSON = Object . foldrWithKey (\s f -> HashMap.insert (toJSONKeyKind s) (toJSONSing1 s f)) HashMap.empty
 
-instance (SOrd kproxy, SDecide kproxy, FromJSONKeyKind kproxy, FromJSONSing1 f) => FromJSON (SingMap kproxy f) where
-  parseJSON = withObject "SingMap kproxy a" $ fmap fromList . mapM parseSingWith . HashMap.toList
-    where 
-    parseSingWith :: (Text,Value) -> Parser (SomeSingWith1 kproxy f)
+instance (SOrd k, SDecide k, FromJSONKeyKind k, FromJSONSing1 f) => FromJSON (SingMap k f) where
+  parseJSON = withObject "SingMap k a" $ fmap fromList . mapM parseSingWith . HashMap.toList
+    where
+    parseSingWith :: (Text,Value) -> Parser (SomeSingWith1 k f)
     parseSingWith (t,v) = do
-      SomeSing s :: SomeSing kproxy  <- parseJSONKeyKind t
+      SomeSing s :: SomeSing k  <- parseJSONKeyKind t
       pv <- parseJSONSing1 s v
       return (SomeSingWith1 s pv)
-      
 
 
+
 {--------------------------------------------------------------------
   Construction
 --------------------------------------------------------------------}
@@ -58,14 +63,14 @@
 --
 -- > empty      == fromList []
 -- > size empty == 0
-empty :: SingMap kproxy f
+empty :: SingMap k f
 empty = Tip
 
 -- | /O(1)/. A map with a single element.
 --
 -- > singleton 1 'a'        == fromList [(1, 'a')]
 -- > size (singleton 1 'a') == 1
-singleton :: Sing v -> f v -> SingMap kproxy f
+singleton :: Sing v -> f v -> SingMap k f
 singleton k x = Bin 1 k x Tip Tip
 
 {--------------------------------------------------------------------
@@ -73,12 +78,12 @@
 --------------------------------------------------------------------}
 
 -- | /O(1)/. Is the map empty?
-null :: SingMap kproxy f -> Bool
+null :: SingMap k f -> Bool
 null Tip    = True
 null Bin{}  = False
 
 -- | /O(1)/. The number of elements in the map.
-size :: SingMap kproxy f -> Int
+size :: SingMap k f -> Int
 size Tip                = 0
 size (Bin n _ _ _ _)    = n
 
@@ -86,12 +91,12 @@
 --
 -- The function will return the corresponding value as @('Just' value)@,
 -- or 'Nothing' if the key isn't in the map.
-lookup :: forall kproxy f v. (SOrd kproxy, SDecide kproxy) => Sing v -> SingMap kproxy f -> Maybe (f v)
+lookup :: forall k f v. (SOrd k, SDecide k) => Sing v -> SingMap k f -> Maybe (f v)
 lookup k = k `seq` go
   where
-  go :: SingMap kproxy f -> Maybe (f v)
+  go :: SingMap k f -> Maybe (f v)
   go Tip = Nothing
-  go (Bin _ kx x l r) = 
+  go (Bin _ kx x l r) =
     case sCompare k kx of
       SLT -> go l
       SGT -> go r
@@ -99,10 +104,10 @@
         Nothing -> error "lookup: inconsistent SOrd and SDecide instances"
         Just Refl -> Just x
 
-lookupAssoc :: forall kproxy f v. (SOrd kproxy, SDecide kproxy) => SomeSing kproxy -> SingMap kproxy f -> Maybe (SomeSingWith1 kproxy f)
+lookupAssoc :: forall k f v. (SOrd k, SDecide k) => SomeSing k -> SingMap k f -> Maybe (SomeSingWith1 k f)
 lookupAssoc (SomeSing k) = k `seq` go
   where
-  go :: SingMap kproxy f -> Maybe (SomeSingWith1 kproxy f)
+  go :: SingMap k f -> Maybe (SomeSingWith1 k f)
   go Tip = Nothing
   go (Bin _ kx x l r) =
     case sCompare k kx of
@@ -115,7 +120,7 @@
   Utility functions that maintain the balance properties of the tree.
   All constructors assume that all values in [l] < [k] and all values
   in [r] > [k], and that [l] and [r] are valid trees.
-  
+
   In order of sophistication:
     [Bin sz k x l r]  The type constructor.
     [bin k x l r]     Maintains the correct size, assumes that both [l]
@@ -123,7 +128,7 @@
     [balance k x l r] Restores the balance and size.
                       Assumes that the original tree was balanced and
                       that [l] or [r] has changed by at most one element.
-    [combine k x l r] Restores balance and size. 
+    [combine k x l r] Restores balance and size.
 
   Furthermore, we can construct a new tree from two trees. Both operations
   assume that all values in [l] < all values in [r] and that [l] and [r]
@@ -133,17 +138,17 @@
     [merge l r]       Merges two trees and restores balance.
 
   Note: in contrast to Adam's paper, we use (<=) comparisons instead
-  of (<) comparisons in [combine], [merge] and [balance]. 
-  Quickcheck (on [difference]) showed that this was necessary in order 
-  to maintain the invariants. It is quite unsatisfactory that I haven't 
-  been able to find out why this is actually the case! Fortunately, it 
+  of (<) comparisons in [combine], [merge] and [balance].
+  Quickcheck (on [difference]) showed that this was necessary in order
+  to maintain the invariants. It is quite unsatisfactory that I haven't
+  been able to find out why this is actually the case! Fortunately, it
   doesn't hurt to be a bit more conservative.
 --------------------------------------------------------------------}
 
 {--------------------------------------------------------------------
   Combine
 --------------------------------------------------------------------}
-combine :: (SOrd kproxy, SDecide kproxy) => Sing v -> f v -> SingMap kproxy f -> SingMap kproxy f -> SingMap kproxy f
+combine :: (SOrd k, SDecide k) => Sing v -> f v -> SingMap k f -> SingMap k f -> SingMap k f
 combine kx x Tip r  = insertMin kx x r
 combine kx x l Tip  = insertMax kx x l
 combine kx x l@(Bin sizeL ky y ly ry) r@(Bin sizeR kz z lz rz)
@@ -153,23 +158,23 @@
 
 
 -- insertMin and insertMax don't perform potentially expensive comparisons.
-insertMax,insertMin :: Sing v -> f v -> SingMap kproxy f -> SingMap kproxy f
+insertMax,insertMin :: Sing v -> f v -> SingMap k f -> SingMap k f
 insertMax kx x t
   = case t of
       Tip -> singleton kx x
       Bin _ ky y l r
           -> balance ky y l (insertMax kx x r)
-             
+
 insertMin kx x t
   = case t of
       Tip -> singleton kx x
       Bin _ ky y l r
           -> balance ky y (insertMin kx x l) r
-             
+
 {--------------------------------------------------------------------
   [merge l r]: merges two trees.
 --------------------------------------------------------------------}
-merge :: SOrd kproxy => SingMap kproxy f -> SingMap kproxy f -> SingMap kproxy f
+merge :: SOrd k => SingMap k f -> SingMap k f -> SingMap k f
 merge Tip r   = r
 merge l Tip   = l
 merge l@(Bin sizeL kx x lx rx) r@(Bin sizeR ky y ly ry)
@@ -181,20 +186,20 @@
   [glue l r]: glues two trees together.
   Assumes that [l] and [r] are already balanced with respect to each other.
 --------------------------------------------------------------------}
-glue :: (kproxy ~ 'KProxy) => SingMap kproxy f -> SingMap kproxy f -> SingMap kproxy f
+glue ::  SingMap k f -> SingMap k f -> SingMap k f
 glue Tip r = r
 glue l Tip = l
-glue l r   
+glue l r
   | size l > size r = case deleteFindMax l of (SomeSingWith1 km m,l') -> balance km m l' r
   | otherwise       = case deleteFindMin r of (SomeSingWith1 km m,r') -> balance km m l r'
 
 -- | /O(log n)/. Delete and find the minimal element.
 --
--- > deleteFindMin (fromList [(5,"a"), (3,"b"), (10,"c")]) == ((3,"b"), fromList[(5,"a"), (10,"c")]) 
+-- > deleteFindMin (fromList [(5,"a"), (3,"b"), (10,"c")]) == ((3,"b"), fromList[(5,"a"), (10,"c")])
 -- > deleteFindMin                                            Error: can not return the minimal element of an empty map
 
-deleteFindMin :: (kproxy ~ 'KProxy) => SingMap kproxy f -> (SomeSingWith1 kproxy f, SingMap kproxy f)
-deleteFindMin t 
+deleteFindMin ::  SingMap k f -> (SomeSingWith1 k f, SingMap k f)
+deleteFindMin t
   = case t of
       Bin _ k x Tip r -> (SomeSingWith1 k x ,r)
       Bin _ k x l r   -> let (km,l') = deleteFindMin l in (km,balance k x l' r)
@@ -205,7 +210,7 @@
 -- > deleteFindMax (fromList [(5,"a"), (3,"b"), (10,"c")]) == ((10,"c"), fromList [(3,"b"), (5,"a")])
 -- > deleteFindMax empty                                      Error: can not return the maximal element of an empty map
 
-deleteFindMax :: (kproxy ~ 'KProxy) => SingMap kproxy f -> (SomeSingWith1 kproxy f, SingMap kproxy f)
+deleteFindMax ::  SingMap k f -> (SomeSingWith1 k f, SingMap k f)
 deleteFindMax t
   = case t of
       Bin _ k x l Tip -> (SomeSingWith1 k x,l)
@@ -229,7 +234,7 @@
   Note that:
   - [delta] should be larger than 4.646 with a [ratio] of 2.
   - [delta] should be larger than 3.745 with a [ratio] of 1.534.
-  
+
   - A lower [delta] leads to a more 'perfectly' balanced tree.
   - A higher [delta] performs less rebalancing.
 
@@ -247,7 +252,7 @@
 delta = 4
 ratio = 2
 
-balance :: Sing v -> f v -> SingMap kproxy f -> SingMap kproxy f -> SingMap kproxy f
+balance :: Sing v -> f v -> SingMap k f -> SingMap k f -> SingMap k f
 balance k x l r
   | sizeL + sizeR <= 1    = Bin sizeX k x l r
   | sizeR >= delta*sizeL  = rotateL k x l r
@@ -259,26 +264,26 @@
     sizeX = sizeL + sizeR + 1
 
 -- rotate
-rotateL :: Sing v -> f v -> SingMap kproxy f -> SingMap kproxy f -> SingMap kproxy f
+rotateL :: Sing v -> f v -> SingMap k f -> SingMap k f -> SingMap k f
 rotateL k x l r@(Bin _ _ _ ly ry)
   | size ly < ratio*size ry = singleL k x l r
   | otherwise               = doubleL k x l r
 rotateL _ _ _ Tip = error "rotateL Tip"
 
-rotateR :: Sing v -> f v -> SingMap kproxy f -> SingMap kproxy f -> SingMap kproxy f
+rotateR :: Sing v -> f v -> SingMap k f -> SingMap k f -> SingMap k f
 rotateR k x l@(Bin _ _ _ ly ry) r
   | size ry < ratio*size ly = singleR k x l r
   | otherwise               = doubleR k x l r
 rotateR _ _ Tip _ = error "rotateR Tip"
 
 -- basic rotations
-singleL, singleR :: Sing v -> f v -> SingMap kproxy f -> SingMap kproxy f -> SingMap kproxy f
+singleL, singleR :: Sing v -> f v -> SingMap k f -> SingMap k f -> SingMap k f
 singleL k1 x1 t1 (Bin _ k2 x2 t2 t3)  = bin k2 x2 (bin k1 x1 t1 t2) t3
 singleL _ _ _ Tip = error "singleL Tip"
 singleR k1 x1 (Bin _ k2 x2 t1 t2) t3  = bin k2 x2 t1 (bin k1 x1 t2 t3)
 singleR _ _ Tip _ = error "singleR Tip"
 
-doubleL, doubleR :: Sing v -> f v -> SingMap kproxy f -> SingMap kproxy f -> SingMap kproxy f
+doubleL, doubleR :: Sing v -> f v -> SingMap k f -> SingMap k f -> SingMap k f
 doubleL k1 x1 t1 (Bin _ k2 x2 (Bin _ k3 x3 t2 t3) t4) = bin k3 x3 (bin k1 x1 t1 t2) (bin k2 x2 t3 t4)
 doubleL _ _ _ _ = error "doubleL"
 doubleR k1 x1 (Bin _ k2 x2 t1 (Bin _ k3 x3 t2 t3)) t4 = bin k3 x3 (bin k2 x2 t1 t2) (bin k1 x1 t3 t4)
@@ -287,7 +292,7 @@
 {--------------------------------------------------------------------
   The bin constructor maintains the size of the tree
 --------------------------------------------------------------------}
-bin :: Sing v -> f v -> SingMap kproxy f -> SingMap kproxy f -> SingMap kproxy f
+bin :: Sing v -> f v -> SingMap k f -> SingMap k f -> SingMap k f
 bin k x l r
   = Bin (size l + size r + 1) k x l r
 
@@ -313,7 +318,7 @@
   values between the range [lo] to [hi]. The returned tree is either
   empty or the key of the root is between @lo@ and @hi@.
 --------------------------------------------------------------------}
-trim :: SOrd kproxy => (SomeSing kproxy -> Ordering) -> (SomeSing kproxy -> Ordering) -> SingMap kproxy f -> SingMap kproxy f
+trim :: SOrd k => (SomeSing k -> Ordering) -> (SomeSing k -> Ordering) -> SingMap k f -> SingMap k f
 trim _     _     Tip = Tip
 trim cmplo cmphi t@(Bin _ kx _ l r)
   = case cmplo (SomeSing kx) of
@@ -321,8 +326,8 @@
               GT -> t
               _  -> trim cmplo cmphi l
       _  -> trim cmplo cmphi r
-              
-trimLookupLo :: (SOrd kproxy, SDecide kproxy) => SomeSing kproxy -> (SomeSing kproxy -> Ordering) -> SingMap kproxy f -> (Maybe (SomeSingWith1 kproxy f), SingMap kproxy f)
+
+trimLookupLo :: (SOrd k, SDecide k) => SomeSing k -> (SomeSing k -> Ordering) -> SingMap k f -> (Maybe (SomeSingWith1 k f), SingMap k f)
 trimLookupLo _  _     Tip = (Nothing,Tip)
 trimLookupLo lo cmphi t@(Bin _ kx x l r)
   = case compareSome lo (SomeSing kx) of
@@ -337,7 +342,7 @@
   [filterGt k t] filter all keys >[k] from tree [t]
   [filterLt k t] filter all keys <[k] from tree [t]
 --------------------------------------------------------------------}
-filterGt :: (SOrd kproxy, SDecide kproxy) => (SomeSing kproxy -> Ordering) -> SingMap kproxy f -> SingMap kproxy f
+filterGt :: (SOrd k, SDecide k) => (SomeSing k -> Ordering) -> SingMap k f -> SingMap k f
 filterGt cmp = go
   where
     go Tip              = Tip
@@ -346,7 +351,7 @@
               GT -> go r
               EQ -> r
 
-filterLt :: (SOrd kproxy, SDecide kproxy) => (SomeSing kproxy -> Ordering) -> SingMap kproxy f -> SingMap kproxy f
+filterLt :: (SOrd k, SDecide k) => (SomeSing k -> Ordering) -> SingMap k f -> SingMap k f
 filterLt cmp = go
   where
     go Tip              = Tip
@@ -372,11 +377,11 @@
 -- > fromList [(5,'a'), (3,'b')] ! 1    Error: element not in the map
 -- > fromList [(5,'a'), (3,'b')] ! 5 == 'a'
 
-(!) :: (SOrd kproxy, SDecide kproxy) => SingMap kproxy f -> Sing v -> f v
+(!) :: (SOrd k, SDecide k) => SingMap k f -> Sing v -> f v
 (!) m k    = find k m
 
 -- | Same as 'difference'.
-(\\) :: (SOrd kproxy, SDecide kproxy) => SingMap kproxy f -> SingMap kproxy f -> SingMap kproxy f
+(\\) :: (SOrd k, SDecide k) => SingMap k f -> SingMap k f -> SingMap k f
 m1 \\ m2 = difference m1 m2
 
 {--------------------------------------------------------------------
@@ -384,17 +389,17 @@
 --------------------------------------------------------------------}
 
 -- | /O(log n)/. Is the key a member of the map? See also 'notMember'.
-member :: forall (kproxy :: KProxy k) f (v :: k). (SOrd kproxy, SDecide kproxy) => Sing v -> SingMap kproxy f -> Bool
+member :: forall k f (v :: k). (SOrd k, SDecide k) => Sing v -> SingMap k f -> Bool
 member k = isJust . lookup k
 
 -- | /O(log n)/. Is the key not a member of the map? See also 'member'.
-notMember :: forall (kproxy :: KProxy k) f (v :: k). (SOrd kproxy, SDecide kproxy) => Sing v -> SingMap kproxy f -> Bool
+notMember :: forall k f (v :: k). (SOrd k, SDecide k) => Sing v -> SingMap k f -> Bool
 notMember k m = not (member k m)
 
 -- | /O(log n)/. Find the value at a key.
 -- Calls 'error' when the element can not be found.
 -- Consider using 'lookup' when elements may not be present.
-find :: (SOrd kproxy, SDecide kproxy) => Sing v -> SingMap kproxy f -> f v
+find :: (SOrd k, SDecide k) => Sing v -> SingMap k f -> f v
 find k m = case lookup k m of
     Nothing -> error "SingMap.find: element not in the map"
     Just v  -> v
@@ -402,7 +407,7 @@
 -- | /O(log n)/. The expression @('findWithDefault' def k map)@ returns
 -- the value at key @k@ or returns default value @def@
 -- when the key is not in the map.
-findWithDefault :: (SOrd kproxy, SDecide kproxy) => f v -> Sing v -> SingMap kproxy f -> f v
+findWithDefault :: (SOrd k, SDecide k) => f v -> Sing v -> SingMap k f -> f v
 findWithDefault def k m = case lookup k m of
     Nothing -> def
     Just v  -> v
@@ -415,10 +420,10 @@
 -- If the key is already present in the map, the associated value is
 -- replaced with the supplied value. 'insert' is equivalent to
 -- @'insertWith' 'const'@.
-insert :: forall kproxy f v. (SOrd kproxy, SDecide kproxy) => Sing v -> f v -> SingMap kproxy f -> SingMap kproxy f
+insert :: forall k f v. (SOrd k, SDecide k) => Sing v -> f v -> SingMap k f -> SingMap k f
 insert kx x = kx `seq` go
     where
-        go :: SingMap kproxy f -> SingMap kproxy f
+        go :: SingMap k f -> SingMap k f
         go Tip = singleton kx x
         go (Bin sz ky y l r) = case sCompare kx ky of
             SLT -> balance ky y (go l) r
@@ -426,28 +431,28 @@
             SEQ -> Bin sz kx x l r
 
 -- | /O(log n)/. Insert with a function, combining new value and old value.
--- @'insertWith' f key value mp@ 
+-- @'insertWith' f key value mp@
 -- will insert the entry @key :=> value@ into @mp@ if key does
 -- not exist in the map. If the key does exist, the function will
 -- insert the entry @key :=> f new_value old_value@.
-insertWith :: (SOrd kproxy, SDecide kproxy) => (f v -> f v -> f v) -> Sing v -> f v -> SingMap kproxy f -> SingMap kproxy f
+insertWith :: (SOrd k, SDecide k) => (f v -> f v -> f v) -> Sing v -> f v -> SingMap k f -> SingMap k f
 insertWith f = insertWithKey (\_ x' y' -> f x' y')
 
 -- | Same as 'insertWith', but the combining function is applied strictly.
 -- This is often the most desirable behavior.
-insertWith' :: (SOrd kproxy, SDecide kproxy) => (f v -> f v -> f v) -> Sing v -> f v -> SingMap kproxy f -> SingMap kproxy f
+insertWith' :: (SOrd k, SDecide k) => (f v -> f v -> f v) -> Sing v -> f v -> SingMap k f -> SingMap k f
 insertWith' f = insertWithKey' (\_ x' y' -> f x' y')
 
 -- | /O(log n)/. Insert with a function, combining key, new value and old value.
--- @'insertWithKey' f key value mp@ 
+-- @'insertWithKey' f key value mp@
 -- will insert the entry @key :=> value@ into @mp@ if key does
 -- not exist in the map. If the key does exist, the function will
 -- insert the entry @key :=> f key new_value old_value@.
 -- Note that the key passed to f is the same key passed to 'insertWithKey'.
-insertWithKey :: forall kproxy f v. (SOrd kproxy, SDecide kproxy) => (Sing v -> f v -> f v -> f v) -> Sing v -> f v -> SingMap kproxy f -> SingMap kproxy f
+insertWithKey :: forall k f v. (SOrd k, SDecide k) => (Sing v -> f v -> f v -> f v) -> Sing v -> f v -> SingMap k f -> SingMap k f
 insertWithKey f kx x = kx `seq` go
   where
-    go :: SingMap kproxy f -> SingMap kproxy f
+    go :: SingMap k f -> SingMap k f
     go Tip = singleton kx x
     go (Bin sy ky y l r) =
         case sCompare kx ky of
@@ -456,10 +461,10 @@
             SEQ -> unifyOnCompareEQ kx ky (Bin sy kx (f kx x y) l r)
 
 -- | Same as 'insertWithKey', but the combining function is applied strictly.
-insertWithKey' :: forall kproxy f v. (SOrd kproxy, SDecide kproxy) => (Sing v -> f v -> f v -> f v) -> Sing v -> f v -> SingMap kproxy f -> SingMap kproxy f
+insertWithKey' :: forall k f v. (SOrd k, SDecide k) => (Sing v -> f v -> f v -> f v) -> Sing v -> f v -> SingMap k f -> SingMap k f
 insertWithKey' f kx x = kx `seq` go
   where
-    go :: SingMap kproxy f -> SingMap kproxy f
+    go :: SingMap k f -> SingMap k f
     go Tip = singleton kx $! x
     go (Bin sy ky y l r) =
         case sCompare kx ky of
@@ -471,11 +476,11 @@
 -- The expression (@'insertLookupWithKey' f k x map@)
 -- is a pair where the first element is equal to (@'lookup' k map@)
 -- and the second element equal to (@'insertWithKey' f k x map@).
-insertLookupWithKey :: forall kproxy f v. (SOrd kproxy, SDecide kproxy) => (Sing v -> f v -> f v -> f v) -> Sing v -> f v -> SingMap kproxy f
-                    -> (Maybe (f v), SingMap kproxy f)
+insertLookupWithKey :: forall k f v. (SOrd k, SDecide k) => (Sing v -> f v -> f v -> f v) -> Sing v -> f v -> SingMap k f
+                    -> (Maybe (f v), SingMap k f)
 insertLookupWithKey f kx x = kx `seq` go
   where
-    go :: SingMap kproxy f -> (Maybe (f v), SingMap kproxy f)
+    go :: SingMap k f -> (Maybe (f v), SingMap k f)
     go Tip = (Nothing, singleton kx x)
     go (Bin sy ky y l r) =
         case sCompare kx ky of
@@ -486,11 +491,11 @@
             SEQ -> unifyOnCompareEQ kx ky (Just y, Bin sy kx (f kx x y) l r)
 
 -- | /O(log n)/. A strict version of 'insertLookupWithKey'.
-insertLookupWithKey' :: forall kproxy f v. (SOrd kproxy, SDecide kproxy) => (Sing v -> f v -> f v -> f v) -> Sing v -> f v -> SingMap kproxy f
-                     -> (Maybe (f v), SingMap kproxy f)
+insertLookupWithKey' :: forall k f v. (SOrd k, SDecide k) => (Sing v -> f v -> f v -> f v) -> Sing v -> f v -> SingMap k f
+                     -> (Maybe (f v), SingMap k f)
 insertLookupWithKey' f kx x = kx `seq` go
   where
-    go :: SingMap kproxy f -> (Maybe (f v), SingMap kproxy f)
+    go :: SingMap k f -> (Maybe (f v), SingMap k f)
     go Tip = x `seq` (Nothing, singleton kx x)
     go (Bin sy ky y l r) =
         case sCompare kx ky of
@@ -507,10 +512,10 @@
 
 -- | /O(log n)/. Delete a key and its value from the map. When the key is not
 -- a member of the map, the original map is returned.
-delete :: forall (kproxy :: KProxy k) f (v :: k). (SOrd kproxy, SDecide kproxy) => Sing v -> SingMap kproxy f -> SingMap kproxy f
+delete :: forall k f (v :: k). (SOrd k, SDecide k) => Sing v -> SingMap k f -> SingMap k f
 delete k = k `seq` go
   where
-    go :: SingMap kproxy f -> SingMap kproxy f
+    go :: SingMap k f -> SingMap k f
     go Tip = Tip
     go (Bin _ kx x l r) =
         case sCompare k kx of
@@ -521,28 +526,28 @@
 -- | /O(log n)/. Update a value at a specific key with the result of the provided function.
 -- When the key is not
 -- a member of the map, the original map is returned.
-adjust :: (SOrd kproxy, SDecide kproxy) => (f v -> f v) -> Sing v -> SingMap kproxy f -> SingMap kproxy f
+adjust :: (SOrd k, SDecide k) => (f v -> f v) -> Sing v -> SingMap k f -> SingMap k f
 adjust f = adjustWithKey (\_ x -> f x)
 
 -- | /O(log n)/. Adjust a value at a specific key. When the key is not
 -- a member of the map, the original map is returned.
-adjustWithKey :: (SOrd kproxy, SDecide kproxy) => (Sing v -> f v -> f v) -> Sing v -> SingMap kproxy f -> SingMap kproxy f
+adjustWithKey :: (SOrd k, SDecide k) => (Sing v -> f v -> f v) -> Sing v -> SingMap k f -> SingMap k f
 adjustWithKey f = updateWithKey (\k' x' -> Just (f k' x'))
 
 -- | /O(log n)/. The expression (@'update' f k map@) updates the value @x@
 -- at @k@ (if it is in the map). If (@f x@) is 'Nothing', the element is
 -- deleted. If it is (@'Just' y@), the key @k@ is bound to the new value @y@.
-update :: (SOrd kproxy, SDecide kproxy) => (f v -> Maybe (f v)) -> Sing v -> SingMap kproxy f -> SingMap kproxy f
+update :: (SOrd k, SDecide k) => (f v -> Maybe (f v)) -> Sing v -> SingMap k f -> SingMap k f
 update f = updateWithKey (\_ x -> f x)
 
 -- | /O(log n)/. The expression (@'updateWithKey' f k map@) updates the
 -- value @x@ at @k@ (if it is in the map). If (@f k x@) is 'Nothing',
 -- the element is deleted. If it is (@'Just' y@), the key @k@ is bound
 -- to the new value @y@.
-updateWithKey :: forall kproxy f v. (SOrd kproxy, SDecide kproxy) => (Sing v -> f v -> Maybe (f v)) -> Sing v -> SingMap kproxy f -> SingMap kproxy f
+updateWithKey :: forall k f v. (SOrd k, SDecide k) => (Sing v -> f v -> Maybe (f v)) -> Sing v -> SingMap k f -> SingMap k f
 updateWithKey f k = k `seq` go
   where
-    go :: SingMap kproxy f -> SingMap kproxy f
+    go :: SingMap k f -> SingMap k f
     go Tip = Tip
     go (Bin sx kx x l r) =
         case sCompare k kx of
@@ -554,16 +559,16 @@
 
 -- | /O(log n)/. Lookup and update. See also 'updateWithKey'.
 -- The function returns changed value, if it is updated.
--- Returns the original key value if the map entry is deleted. 
-updateLookupWithKey :: forall kproxy f v. (SOrd kproxy, SDecide kproxy) => (Sing v -> f v -> Maybe (f v)) -> Sing v -> SingMap kproxy f -> (Maybe (f v), SingMap kproxy f)
+-- Returns the original key value if the map entry is deleted.
+updateLookupWithKey :: forall k f v. (SOrd k, SDecide k) => (Sing v -> f v -> Maybe (f v)) -> Sing v -> SingMap k f -> (Maybe (f v), SingMap k f)
 updateLookupWithKey f k = k `seq` go
  where
-   go :: SingMap kproxy f -> (Maybe (f v), SingMap kproxy f)
+   go :: SingMap k f -> (Maybe (f v), SingMap k f)
    go Tip = (Nothing,Tip)
    go (Bin sx kx x l r) =
           case sCompare k kx of
                SLT -> let (found,l') = go l in (found,balance kx x l' r)
-               SGT -> let (found,r') = go r in (found,balance kx x l r') 
+               SGT -> let (found,r') = go r in (found,balance kx x l r')
                SEQ -> unifyOnCompareEQ k kx $ case f kx x of
                        Just x' -> (Just x',Bin sx kx x' l r)
                        Nothing -> (Just x,glue l r)
@@ -571,10 +576,10 @@
 -- | /O(log n)/. The expression (@'alter' f k map@) alters the value @x@ at @k@, or absence thereof.
 -- 'alter' can be used to insert, delete, or update a value in a 'Map'.
 -- In short : @'lookup' k ('alter' f k m) = f ('lookup' k m)@.
-alter :: forall kproxy f v. (SOrd kproxy, SDecide kproxy) => (Maybe (f v) -> Maybe (f v)) -> Sing v -> SingMap kproxy f -> SingMap kproxy f
+alter :: forall k f v. (SOrd k, SDecide k) => (Maybe (f v) -> Maybe (f v)) -> Sing v -> SingMap k f -> SingMap k f
 alter f k = k `seq` go
   where
-    go :: SingMap kproxy f -> SingMap kproxy f
+    go :: SingMap k f -> SingMap k f
     go Tip = case f Nothing of
                Nothing -> Tip
                Just x  -> singleton k x
@@ -593,7 +598,7 @@
 -- | /O(log n)/. Return the /index/ of a key. The index is a number from
 -- /0/ up to, but not including, the 'size' of the map. Calls 'error' when
 -- the key is not a 'member' of the map.
-findIndex :: forall (kproxy :: KProxy k) f (v :: k). (SOrd kproxy, SDecide kproxy) => Sing v -> SingMap kproxy f -> Int
+findIndex :: forall k f (v :: k). (SOrd k, SDecide k) => Sing v -> SingMap k f -> Int
 findIndex k t
   = case lookupIndex k t of
       Nothing  -> error "Map.findIndex: element is not in the map"
@@ -601,20 +606,20 @@
 
 -- | /O(log n)/. Lookup the /index/ of a key. The index is a number from
 -- /0/ up to, but not including, the 'size' of the map.
-lookupIndex :: forall (kproxy :: KProxy k) f (v :: k). (SOrd kproxy, SDecide kproxy) => Sing v -> SingMap kproxy f -> Maybe Int
+lookupIndex :: forall k f (v :: k). (SOrd k, SDecide k) => Sing v -> SingMap k f -> Maybe Int
 lookupIndex k = k `seq` go 0
   where
-    go :: Int -> SingMap kproxy f -> Maybe Int
+    go :: Int -> SingMap k f -> Maybe Int
     go !idx Tip  = idx `seq` Nothing
     go !idx (Bin _ kx _ l r)
       = case sCompare k kx of
           SLT -> go idx l
-          SGT -> go (idx + size l + 1) r 
+          SGT -> go (idx + size l + 1) r
           SEQ -> Just (idx + size l)
 
 -- | /O(log n)/. Retrieve an element by /index/. Calls 'error' when an
 -- invalid index is used.
-elemAt :: (kproxy ~ 'KProxy) => Int -> SingMap kproxy f -> SomeSingWith1 kproxy f
+elemAt ::  Int -> SingMap k f -> SomeSingWith1 k f
 elemAt _ Tip = error "Map.elemAt: index out of range"
 elemAt i (Bin _ kx x l r)
   = case compare i sizeL of
@@ -626,7 +631,7 @@
 
 -- | /O(log n)/. Update the element at /index/. Calls 'error' when an
 -- invalid index is used.
-updateAt :: (kproxy ~ 'KProxy) => (forall v. Sing v -> f v -> Maybe (f v)) -> Int -> SingMap kproxy f -> SingMap kproxy f
+updateAt ::  (forall v. Sing v -> f v -> Maybe (f v)) -> Int -> SingMap k f -> SingMap k f
 updateAt f i0 t = i0 `seq` go i0 t
  where
     go _ Tip  = error "Map.updateAt: index out of range"
@@ -636,12 +641,12 @@
       EQ -> case f kx x of
               Just x' -> Bin sx kx x' l r
               Nothing -> glue l r
-      where 
+      where
         sizeL = size l
 
 -- | /O(log n)/. Delete the element at /index/.
 -- Defined as (@'deleteAt' i map = 'updateAt' (\k x -> 'Nothing') i map@).
-deleteAt :: (kproxy ~ 'KProxy) => Int -> SingMap kproxy f -> SingMap kproxy f
+deleteAt ::  Int -> SingMap k f -> SingMap k f
 deleteAt i m
   = updateAt (\_ _ -> Nothing) i m
 
@@ -651,31 +656,31 @@
 --------------------------------------------------------------------}
 
 -- | /O(log n)/. The minimal key of the map. Calls 'error' is the map is empty.
-findMin :: (kproxy ~ 'KProxy) => SingMap kproxy f -> SomeSingWith1 kproxy f
+findMin ::  SingMap k f -> SomeSingWith1 k f
 findMin (Bin _ kx x Tip _)  = SomeSingWith1 kx x
 findMin (Bin _ _  _ l _)    = findMin l
 findMin Tip                 = error "Map.findMin: empty map has no minimal element"
 
 -- | /O(log n)/. The maximal key of the map. Calls 'error' is the map is empty.
-findMax :: (kproxy ~ 'KProxy) => SingMap kproxy f -> SomeSingWith1 kproxy f
+findMax ::  SingMap k f -> SomeSingWith1 k f
 findMax (Bin _ kx x _ Tip)  = SomeSingWith1 kx x
 findMax (Bin _ _  _ _ r)    = findMax r
 findMax Tip                 = error "Map.findMax: empty map has no maximal element"
 
 -- | /O(log n)/. Delete the minimal key. Returns an empty map if the map is empty.
-deleteMin :: (kproxy ~ 'KProxy) => SingMap kproxy f -> SingMap kproxy f
+deleteMin ::  SingMap k f -> SingMap k f
 deleteMin (Bin _ _  _ Tip r)  = r
 deleteMin (Bin _ kx x l r)    = balance kx x (deleteMin l) r
 deleteMin Tip                 = Tip
 
 -- | /O(log n)/. Delete the maximal key. Returns an empty map if the map is empty.
-deleteMax :: (kproxy ~ 'KProxy) => SingMap kproxy f -> SingMap kproxy f
+deleteMax ::  SingMap k f -> SingMap k f
 deleteMax (Bin _ _  _ l Tip)  = l
 deleteMax (Bin _ kx x l r)    = balance kx x l (deleteMax r)
 deleteMax Tip                 = Tip
 
 -- | /O(log n)/. Update the value at the minimal key.
-updateMinWithKey :: (forall v. Sing v -> f v -> Maybe (f v)) -> SingMap kproxy f -> SingMap kproxy f
+updateMinWithKey :: (forall v. Sing v -> f v -> Maybe (f v)) -> SingMap k f -> SingMap k f
 updateMinWithKey f = go
  where
     go (Bin sx kx x Tip r) = case f kx x of
@@ -685,7 +690,7 @@
     go Tip                 = Tip
 
 -- | /O(log n)/. Update the value at the maximal key.
-updateMaxWithKey :: (forall v. Sing v -> f v -> Maybe (f v)) -> SingMap kproxy f -> SingMap kproxy f
+updateMaxWithKey :: (forall v. Sing v -> f v -> Maybe (f v)) -> SingMap k f -> SingMap k f
 updateMaxWithKey f = go
  where
     go (Bin sx kx x l Tip) = case f kx x of
@@ -696,53 +701,53 @@
 
 -- | /O(log n)/. Retrieves the minimal (key :=> value) entry of the map, and
 -- the map stripped of that element, or 'Nothing' if passed an empty map.
-minViewWithKey :: (kproxy ~ 'KProxy) => SingMap kproxy f -> Maybe (SomeSingWith1 kproxy f, SingMap kproxy f)
+minViewWithKey ::  SingMap k f -> Maybe (SomeSingWith1 k f, SingMap k f)
 minViewWithKey Tip = Nothing
 minViewWithKey x   = Just (deleteFindMin x)
 
 -- | /O(log n)/. Retrieves the maximal (key :=> value) entry of the map, and
 -- the map stripped of that element, or 'Nothing' if passed an empty map.
-maxViewWithKey :: (kproxy ~ 'KProxy) => SingMap kproxy f -> Maybe (SomeSingWith1 kproxy f, SingMap kproxy f)
+maxViewWithKey ::  SingMap k f -> Maybe (SomeSingWith1 k f, SingMap k f)
 maxViewWithKey Tip = Nothing
 maxViewWithKey x   = Just (deleteFindMax x)
 
 {--------------------------------------------------------------------
-  Union. 
+  Union.
 --------------------------------------------------------------------}
 
 -- | The union of a list of maps:
 --   (@'unions' == 'Prelude.foldl' 'union' 'empty'@).
-unions :: (SOrd kproxy, SDecide kproxy) => [SingMap kproxy f] -> SingMap kproxy f
+unions :: (SOrd k, SDecide k) => [SingMap k f] -> SingMap k f
 unions ts
   = foldlStrict union empty ts
 
 -- | The union of a list of maps, with a combining operation:
 --   (@'unionsWithKey' f == 'Prelude.foldl' ('unionWithKey' f) 'empty'@).
-unionsWithKey :: (SOrd kproxy, SDecide kproxy) => (forall v. Sing v -> f v -> f v -> f v) -> [SingMap kproxy f] -> SingMap kproxy f
+unionsWithKey :: (SOrd k, SDecide k) => (forall v. Sing v -> f v -> f v -> f v) -> [SingMap k f] -> SingMap k f
 unionsWithKey f ts
   = foldlStrict (unionWithKey f) empty ts
 
 -- | /O(n+m)/.
--- The expression (@'union' t1 t2@) takes the left-biased union of @t1@ and @t2@. 
+-- The expression (@'union' t1 t2@) takes the left-biased union of @t1@ and @t2@.
 -- It prefers @t1@ when duplicate keys are encountered,
 -- i.e. (@'union' == 'unionWith' 'const'@).
 -- The implementation uses the efficient /hedge-union/ algorithm.
 -- Hedge-union is more efficient on (bigset \``union`\` smallset).
-union :: (SOrd kproxy, SDecide kproxy) => SingMap kproxy f -> SingMap kproxy f -> SingMap kproxy f
+union :: (SOrd k, SDecide k) => SingMap k f -> SingMap k f -> SingMap k f
 union Tip t2  = t2
 union t1 Tip  = t1
 union t1 t2 = hedgeUnionL (const LT) (const GT) t1 t2
 
 -- left-biased hedge union
-hedgeUnionL :: (SOrd kproxy, SDecide kproxy)
-            => (SomeSing kproxy -> Ordering) -> (SomeSing kproxy -> Ordering) -> SingMap kproxy f -> SingMap kproxy f
-            -> SingMap kproxy f
+hedgeUnionL :: (SOrd k, SDecide k)
+            => (SomeSing k -> Ordering) -> (SomeSing k -> Ordering) -> SingMap k f -> SingMap k f
+            -> SingMap k f
 hedgeUnionL _     _     t1 Tip
   = t1
 hedgeUnionL cmplo cmphi Tip (Bin _ kx x l r)
   = combine kx x (filterGt cmplo l) (filterLt cmphi r)
 hedgeUnionL cmplo cmphi (Bin _ kx x l r) t2
-  = combine kx x (hedgeUnionL cmplo cmpkx l (trim cmplo cmpkx t2)) 
+  = combine kx x (hedgeUnionL cmplo cmpkx l (trim cmplo cmpkx t2))
               (hedgeUnionL cmpkx cmphi r (trim cmpkx cmphi t2))
   where
     cmpkx k  = compareSome (SomeSing kx) k
@@ -754,22 +759,22 @@
 -- | /O(n+m)/.
 -- Union with a combining function. The implementation uses the efficient /hedge-union/ algorithm.
 -- Hedge-union is more efficient on (bigset \``union`\` smallset).
-unionWithKey :: (SOrd kproxy, SDecide kproxy) => (forall v. Sing v -> f v -> f v -> f v) -> SingMap kproxy f -> SingMap kproxy f -> SingMap kproxy f
+unionWithKey :: (SOrd k, SDecide k) => (forall v. Sing v -> f v -> f v -> f v) -> SingMap k f -> SingMap k f -> SingMap k f
 unionWithKey _ Tip t2  = t2
 unionWithKey _ t1 Tip  = t1
 unionWithKey f t1 t2 = hedgeUnionWithKey f (const LT) (const GT) t1 t2
 
-hedgeUnionWithKey :: forall kproxy f. (SOrd kproxy, SDecide kproxy)
+hedgeUnionWithKey :: forall k f. (SOrd k, SDecide k)
                   => (forall v. Sing v -> f v -> f v -> f v)
-                  -> (SomeSing kproxy -> Ordering) -> (SomeSing kproxy -> Ordering)
-                  -> SingMap kproxy f -> SingMap kproxy f
-                  -> SingMap kproxy f
+                  -> (SomeSing k -> Ordering) -> (SomeSing k -> Ordering)
+                  -> SingMap k f -> SingMap k f
+                  -> SingMap k f
 hedgeUnionWithKey _ _     _     t1 Tip
   = t1
 hedgeUnionWithKey _ cmplo cmphi Tip (Bin _ kx x l r)
   = combine kx x (filterGt cmplo l) (filterLt cmphi r)
 hedgeUnionWithKey f cmplo cmphi (Bin _ (kx :: Sing tx) x l r) t2
-  = combine kx newx (hedgeUnionWithKey f cmplo cmpkx l lt) 
+  = combine kx newx (hedgeUnionWithKey f cmplo cmpkx l lt)
                  (hedgeUnionWithKey f cmpkx cmphi r gt)
   where
     cmpkx k     = compareSome (SomeSing kx) k
@@ -786,50 +791,50 @@
   Difference
 --------------------------------------------------------------------}
 
--- | /O(n+m)/. Difference of two maps. 
+-- | /O(n+m)/. Difference of two maps.
 -- Return elements of the first map not existing in the second map.
 -- The implementation uses an efficient /hedge/ algorithm comparable with /hedge-union/.
-difference :: (SOrd kproxy, SDecide kproxy) => SingMap kproxy f -> SingMap kproxy g -> SingMap kproxy f
+difference :: (SOrd k, SDecide k) => SingMap k f -> SingMap k g -> SingMap k f
 difference Tip _   = Tip
 difference t1 Tip  = t1
 difference t1 t2   = hedgeDiff (const LT) (const GT) t1 t2
 
-hedgeDiff :: (SOrd kproxy, SDecide kproxy)
-          => (SomeSing kproxy -> Ordering) -> (SomeSing kproxy -> Ordering) -> SingMap kproxy f -> SingMap kproxy g
-          -> SingMap kproxy f
+hedgeDiff :: (SOrd k, SDecide k)
+          => (SomeSing k -> Ordering) -> (SomeSing k -> Ordering) -> SingMap k f -> SingMap k g
+          -> SingMap k f
 hedgeDiff _     _     Tip _
   = Tip
-hedgeDiff cmplo cmphi (Bin _ kx x l r) Tip 
+hedgeDiff cmplo cmphi (Bin _ kx x l r) Tip
   = combine kx x (filterGt cmplo l) (filterLt cmphi r)
-hedgeDiff cmplo cmphi t (Bin _ kx _ l r) 
-  = merge (hedgeDiff cmplo cmpkx (trim cmplo cmpkx t) l) 
+hedgeDiff cmplo cmphi t (Bin _ kx _ l r)
+  = merge (hedgeDiff cmplo cmpkx (trim cmplo cmpkx t) l)
           (hedgeDiff cmpkx cmphi (trim cmpkx cmphi t) r)
   where
-    cmpkx k = compareSome (SomeSing kx) k   
+    cmpkx k = compareSome (SomeSing kx) k
 
 -- | /O(n+m)/. Difference with a combining function. When two equal keys are
 -- encountered, the combining function is applied to the key and both values.
 -- If it returns 'Nothing', the element is discarded (proper set difference). If
--- it returns (@'Just' y@), the element is updated with a new value @y@. 
+-- it returns (@'Just' y@), the element is updated with a new value @y@.
 -- The implementation uses an efficient /hedge/ algorithm comparable with /hedge-union/.
-differenceWithKey :: (SOrd kproxy, SDecide kproxy) => (forall v. Sing v -> f v -> g v -> Maybe (f v)) -> SingMap kproxy f -> SingMap kproxy g -> SingMap kproxy f
+differenceWithKey :: (SOrd k, SDecide k) => (forall v. Sing v -> f v -> g v -> Maybe (f v)) -> SingMap k f -> SingMap k g -> SingMap k f
 differenceWithKey _ Tip _   = Tip
 differenceWithKey _ t1 Tip  = t1
 differenceWithKey f t1 t2   = hedgeDiffWithKey f (const LT) (const GT) t1 t2
 
-hedgeDiffWithKey :: (SOrd kproxy, SDecide kproxy)
+hedgeDiffWithKey :: (SOrd k, SDecide k)
                  => (forall v. Sing v -> f v -> g v -> Maybe (f v))
-                 -> (SomeSing kproxy -> Ordering) -> (SomeSing kproxy -> Ordering)
-                 -> SingMap kproxy f -> SingMap kproxy g
-                 -> SingMap kproxy f
+                 -> (SomeSing k -> Ordering) -> (SomeSing k -> Ordering)
+                 -> SingMap k f -> SingMap k g
+                 -> SingMap k f
 hedgeDiffWithKey _ _     _     Tip _
   = Tip
 hedgeDiffWithKey _ cmplo cmphi (Bin _ kx x l r) Tip
   = combine kx x (filterGt cmplo l) (filterLt cmphi r)
-hedgeDiffWithKey f cmplo cmphi t (Bin _ kx x l r) 
+hedgeDiffWithKey f cmplo cmphi t (Bin _ kx x l r)
   = case found of
       Nothing -> merge tl tr
-      Just (SomeSingWith1 ky y) -> 
+      Just (SomeSingWith1 ky y) ->
         case kx %:== ky of
           SFalse -> error "SingMap.difference: inconsistent SEq instance"
           STrue -> unifyOnEq kx ky $
@@ -837,7 +842,7 @@
               Nothing -> merge tl tr
               Just z  -> combine ky z tl tr
   where
-    cmpkx k     = compareSome (SomeSing kx) k   
+    cmpkx k     = compareSome (SomeSing kx) k
     lt          = trim cmplo cmpkx t
     (found,gt)  = trimLookupLo (SomeSing kx) cmphi t
     tl          = hedgeDiffWithKey f cmplo cmpkx lt l
@@ -852,13 +857,13 @@
 -- | /O(n+m)/. Intersection of two maps.
 -- Return data in the first map for the keys existing in both maps.
 -- (@'intersection' m1 m2 == 'intersectionWith' 'const' m1 m2@).
-intersection :: (SOrd kproxy, SDecide kproxy) => SingMap kproxy f -> SingMap kproxy f -> SingMap kproxy f
+intersection :: (SOrd k, SDecide k) => SingMap k f -> SingMap k f -> SingMap k f
 intersection m1 m2
   = intersectionWithKey (\_ x _ -> x) m1 m2
 
 -- | /O(n+m)/. Intersection with a combining function.
 -- Intersection is more efficient on (bigset \``intersection`\` smallset).
-intersectionWithKey :: (SOrd kproxy, SDecide kproxy) => (forall v. Sing v -> f v -> g v -> h v) -> SingMap kproxy f -> SingMap kproxy g -> SingMap kproxy h
+intersectionWithKey :: (SOrd k, SDecide k) => (forall v. Sing v -> f v -> g v -> h v) -> SingMap k f -> SingMap k g -> SingMap k h
 intersectionWithKey _ Tip _ = Tip
 intersectionWithKey _ _ Tip = Tip
 intersectionWithKey f t1@(Bin s1 k1 x1 l1 r1) t2@(Bin s2 k2 x2 l2 r2) =
@@ -884,19 +889,19 @@
 -- --------------------------------------------------------------------}
 -- -- | /O(n+m)/.
 -- -- This function is defined as (@'isSubmapOf' = 'isSubmapOfBy' 'eqTagged')@).
--- isSubmapOf :: ((SOrd kproxy, SDecide kproxy) EqTag k f) => SingMap kproxy f -> SingMap kproxy f -> Bool
+-- isSubmapOf :: ((SOrd k, SDecide k) EqTag k f) => SingMap k f -> SingMap k f -> Bool
 -- isSubmapOf m1 m2 = isSubmapOfBy eqTagged m1 m2
--- 
+--
 -- {- | /O(n+m)/.
 --  The expression (@'isSubmapOfBy' f t1 t2@) returns 'True' if
 --  all keys in @t1@ are in tree @t2@, and when @f@ returns 'True' when
 --  applied to their respective keys and values.
 -- -}
--- isSubmapOfBy :: (SOrd kproxy, SDecide kproxy) => (forall v. Sing v -> Sing v -> f v -> g v -> Bool) -> SingMap kproxy f -> SingMap kproxy g -> Bool
+-- isSubmapOfBy :: (SOrd k, SDecide k) => (forall v. Sing v -> Sing v -> f v -> g v -> Bool) -> SingMap k f -> SingMap k g -> Bool
 -- isSubmapOfBy f t1 t2
 --   = (size t1 <= size t2) && (submap' f t1 t2)
--- 
--- submap' :: (SOrd kproxy, SDecide kproxy) => (forall v. Sing v -> Sing v -> f v -> g v -> Bool) -> SingMap kproxy f -> SingMap kproxy g -> Bool
+--
+-- submap' :: (SOrd k, SDecide k) => (forall v. Sing v -> Sing v -> f v -> g v -> Bool) -> SingMap k f -> SingMap k g -> Bool
 -- submap' _ Tip _ = True
 -- submap' _ _ Tip = False
 -- submap' f (Bin _ kx x l r) t
@@ -905,20 +910,20 @@
 --       Just (ky, y)  -> f kx ky x y && submap' f l lt && submap' f r gt
 --   where
 --     (lt,found,gt) = splitLookupWithKey kx t
--- 
--- -- | /O(n+m)/. Is this a proper submap? (ie. a submap but not equal). 
+--
+-- -- | /O(n+m)/. Is this a proper submap? (ie. a submap but not equal).
 -- -- Defined as (@'isProperSubmapOf' = 'isProperSubmapOfBy' 'eqTagged'@).
--- isProperSubmapOf :: ((SOrd kproxy, SDecide kproxy) EqTag k f) => SingMap kproxy f -> SingMap kproxy f -> Bool
+-- isProperSubmapOf :: ((SOrd k, SDecide k) EqTag k f) => SingMap k f -> SingMap k f -> Bool
 -- isProperSubmapOf m1 m2
 --   = isProperSubmapOfBy eqTagged m1 m2
--- 
+--
 -- {- | /O(n+m)/. Is this a proper submap? (ie. a submap but not equal).
 --  The expression (@'isProperSubmapOfBy' f m1 m2@) returns 'True' when
 --  @m1@ and @m2@ are not equal,
 --  all keys in @m1@ are in @m2@, and when @f@ returns 'True' when
---  applied to their respective keys and values. 
+--  applied to their respective keys and values.
 -- -}
--- isProperSubmapOfBy :: (SOrd kproxy, SDecide kproxy) => (forall v. Sing v -> Sing v -> f v -> g v -> Bool) -> SingMap kproxy f -> SingMap kproxy g -> Bool
+-- isProperSubmapOfBy :: (SOrd k, SDecide k) => (forall v. Sing v -> Sing v -> f v -> g v -> Bool) -> SingMap k f -> SingMap k g -> Bool
 -- isProperSubmapOfBy f t1 t2
 --   = (size t1 < size t2) && (submap' f t1 t2)
 
@@ -927,7 +932,7 @@
 --------------------------------------------------------------------}
 
 -- | /O(n)/. Filter all keys\/values that satisfy the predicate.
-filterWithKey :: (SOrd kproxy, SDecide kproxy) => (forall v. Sing v -> f v -> Bool) -> SingMap kproxy f -> SingMap kproxy f
+filterWithKey :: (SOrd k, SDecide k) => (forall v. Sing v -> f v -> Bool) -> SingMap k f -> SingMap k f
 filterWithKey p = go
   where
     go Tip = Tip
@@ -938,7 +943,7 @@
 -- | /O(n)/. Partition the map according to a predicate. The first
 -- map contains all elements that satisfy the predicate, the second all
 -- elements that fail the predicate. See also 'split'.
-partitionWithKey :: (SOrd kproxy, SDecide kproxy) => (forall v. Sing v -> f v -> Bool) -> SingMap kproxy f -> (SingMap kproxy f, SingMap kproxy f)
+partitionWithKey :: (SOrd k, SDecide k) => (forall v. Sing v -> f v -> Bool) -> SingMap k f -> (SingMap k f, SingMap k f)
 partitionWithKey _ Tip = (Tip,Tip)
 partitionWithKey p (Bin _ kx x l r)
   | p kx x    = (combine kx x l1 r1,merge l2 r2)
@@ -948,7 +953,7 @@
     (r1,r2) = partitionWithKey p r
 
 -- | /O(n)/. Map keys\/values and collect the 'Just' results.
-mapMaybeWithKey :: (SOrd kproxy, SDecide kproxy) => (forall v. Sing v -> f v -> Maybe (g v)) -> SingMap kproxy f -> SingMap kproxy g
+mapMaybeWithKey :: (SOrd k, SDecide k) => (forall v. Sing v -> f v -> Maybe (g v)) -> SingMap k f -> SingMap k g
 mapMaybeWithKey f = go
   where
     go Tip = Tip
@@ -957,8 +962,8 @@
         Nothing -> merge (go l) (go r)
 
 -- | /O(n)/. Map keys\/values and separate the 'Left' and 'Right' results.
-mapEitherWithKey :: (SOrd kproxy, SDecide kproxy) =>
-  (forall v. Sing v -> f v -> Either (g v) (h v)) -> SingMap kproxy f -> (SingMap kproxy g, SingMap kproxy h)
+mapEitherWithKey :: (SOrd k, SDecide k) =>
+  (forall v. Sing v -> f v -> Either (g v) (h v)) -> SingMap k f -> (SingMap k g, SingMap k h)
 mapEitherWithKey _ Tip = (Tip, Tip)
 mapEitherWithKey f (Bin _ kx x l r) = case f kx x of
   Left y  -> (combine kx y l1 r1, merge l2 r2)
@@ -972,7 +977,7 @@
 --------------------------------------------------------------------}
 
 -- | /O(n)/. Map a function over all values in the map.
-mapWithKey :: (forall v. Sing v -> f v -> g v) -> SingMap kproxy f -> SingMap kproxy g
+mapWithKey :: (forall v. Sing v -> f v -> g v) -> SingMap k f -> SingMap k g
 mapWithKey f = go
   where
     go Tip = Tip
@@ -980,7 +985,7 @@
 
 -- | /O(n)/. The function 'mapAccumLWithKey' threads an accumulating
 -- argument throught the map in ascending order of keys.
-mapAccumLWithKey :: (forall v. a -> Sing v -> f v -> (a, g v)) -> a -> SingMap kproxy f -> (a, SingMap kproxy g)
+mapAccumLWithKey :: (forall v. a -> Sing v -> f v -> (a, g v)) -> a -> SingMap k f -> (a, SingMap k g)
 mapAccumLWithKey f = go
   where
     go a Tip               = (a,Tip)
@@ -992,7 +997,7 @@
 
 -- | /O(n)/. The function 'mapAccumRWithKey' threads an accumulating
 -- argument through the map in descending order of keys.
-mapAccumRWithKey :: (forall v. a -> Sing v -> f v -> (a, g v)) -> a -> SingMap kproxy f -> (a, SingMap kproxy g)
+mapAccumRWithKey :: (forall v. a -> Sing v -> f v -> (a, g v)) -> a -> SingMap k f -> (a, SingMap k g)
 mapAccumRWithKey f = go
   where
     go a Tip = (a,Tip)
@@ -1002,20 +1007,20 @@
                      (a3,l') = go a2 l
                  in (a3,Bin sx kx x' l' r')
 
--- TODO: Maybe fix mapKeysWith. I don't think this function is 
+-- TODO: Maybe fix mapKeysWith. I don't think this function is
 -- actually meaningful with singletons though.
 -- | /O(n*log n)/.
 -- @'mapKeysWith' c f s@ is the map obtained by applying @f@ to each key of @s@.
--- 
+--
 -- The size of the result may be smaller if @f@ maps two or more distinct
 -- keys to the same new key.  In this case the associated values will be
 -- combined using @c@.
--- mapKeysWith :: (SOrd kproxy2, SDecide kproxy2) => (forall v. Sing v -> f v -> f v -> f v) -> (forall v. Sing v -> Sing v) -> SingMap kproxy1 f -> SingMap kproxy2 f
+-- mapKeysWith :: (SOrd k2, SDecide k2) => (forall v. Sing v -> f v -> f v -> f v) -> (forall v. Sing v -> Sing v) -> SingMap k1 f -> SingMap k2 f
 -- mapKeysWith c f = fromListWithKey c . map fFirst . toList
 --     where fFirst (SomeSingWith1 x y) = (SomeSingWith1 (f x) y)
 
 
--- TODO: Maybe fix mapKeysMonotonic. I don't think this function is 
+-- TODO: Maybe fix mapKeysMonotonic. I don't think this function is
 -- actually meaningful with singletons though.
 --
 -- | /O(n)/.
@@ -1024,20 +1029,20 @@
 -- That is, for any values @x@ and @y@, if @x@ < @y@ then @f x@ < @f y@.
 -- /The precondition is not checked./
 -- Semi-formally, we have:
--- 
--- > and [x < y ==> f x < f y | x <- ls, y <- ls] 
+--
+-- > and [x < y ==> f x < f y | x <- ls, y <- ls]
 -- >                     ==> mapKeysMonotonic f s == mapKeys f s
 -- >     where ls = keys s
 --
 -- This means that @f@ maps distinct original keys to distinct resulting keys.
 -- This function has better performance than 'mapKeys'.
--- mapKeysMonotonic :: forall (kproxy1 :: KProxy k) kproxy2 f. (forall (v :: k). Sing v -> Sing v) -> SingMap kproxy1 f -> SingMap kproxy2 f
+-- mapKeysMonotonic :: forall (k1 :: KProxy k) k2 f. (forall (v :: k). Sing v -> Sing v) -> SingMap k1 f -> SingMap k2 f
 -- mapKeysMonotonic _ Tip = Tip
 -- mapKeysMonotonic f (Bin sz k x l r) =
 --     Bin sz (f k) x (mapKeysMonotonic f l) (mapKeysMonotonic f r)
 
 {--------------------------------------------------------------------
-  Folds  
+  Folds
 --------------------------------------------------------------------}
 
 -- | /O(n)/. Fold the keys and values in the map, such that
@@ -1045,13 +1050,13 @@
 --
 -- This is identical to 'foldrWithKey', and you should use that one instead of
 -- this one.  This name is kept for backward compatibility.
-foldWithKey :: (forall v. Sing v -> f v -> b -> b) -> b -> SingMap kproxy f -> b
+foldWithKey :: (forall v. Sing v -> f v -> b -> b) -> b -> SingMap k f -> b
 foldWithKey = foldrWithKey
 {-# DEPRECATED foldWithKey "Use foldrWithKey instead" #-}
 
 -- | /O(n)/. Post-order fold.  The function will be applied from the lowest
 -- value to the highest.
-foldrWithKey :: (forall v. Sing v -> f v -> b -> b) -> b -> SingMap kproxy f -> b
+foldrWithKey :: (forall v. Sing v -> f v -> b -> b) -> b -> SingMap k f -> b
 foldrWithKey f = go
   where
     go z Tip              = z
@@ -1059,7 +1064,7 @@
 
 -- | /O(n)/. Pre-order fold.  The function will be applied from the highest
 -- value to the lowest.
-foldlWithKey :: (forall v. b -> Sing v -> f v -> b) -> b -> SingMap kproxy f -> b
+foldlWithKey :: (forall v. b -> Sing v -> f v -> b) -> b -> SingMap k f -> b
 foldlWithKey f = go
   where
     go z Tip              = z
@@ -1067,7 +1072,7 @@
 
 {-
 -- | /O(n)/. A strict version of 'foldlWithKey'.
-foldlWithKey' :: (b -> k -> a -> b) -> b -> SingMap kproxy -> b
+foldlWithKey' :: (b -> k -> a -> b) -> b -> SingMap k -> b
 foldlWithKey' f = go
   where
     go z Tip              = z
@@ -1075,7 +1080,7 @@
 -}
 
 {--------------------------------------------------------------------
-  List variations 
+  List variations
 --------------------------------------------------------------------}
 
 -- | /O(n)/. Return all keys of the map in ascending order.
@@ -1083,68 +1088,68 @@
 -- > keys (fromList [(5,"a"), (3,"b")]) == [3,5]
 -- > keys empty == []
 
-keys :: (kproxy ~ 'KProxy) => SingMap kproxy f -> [SomeSing kproxy]
+keys ::  SingMap k f -> [SomeSing k]
 keys m
   = [SomeSing k | (SomeSingWith1 k _) <- assocs m]
 
 -- | /O(n)/. Return all key\/value pairs in the map in ascending key order.
-assocs :: (kproxy ~ 'KProxy) => SingMap kproxy f -> [SomeSingWith1 kproxy f]
+assocs ::  SingMap k f -> [SomeSingWith1 k f]
 assocs m
   = toList m
 
 {--------------------------------------------------------------------
-  Lists 
+  Lists
   use [foldlStrict] to reduce demand on the control-stack
 --------------------------------------------------------------------}
 
 -- | /O(n*log n)/. Build a map from a list of key\/value pairs. See also 'fromAscList'.
 -- If the list contains more than one value for the same key, the last value
 -- for the key is retained.
-fromList :: (SOrd kproxy, SDecide kproxy) => [SomeSingWith1 kproxy f] -> SingMap kproxy f
-fromList xs       
+fromList :: (SOrd k, SDecide k) => [SomeSingWith1 k f] -> SingMap k f
+fromList xs
   = foldlStrict ins empty xs
   where
-    ins :: (SOrd kproxy, SDecide kproxy) => SingMap kproxy f -> SomeSingWith1 kproxy f -> SingMap kproxy f
+    ins :: (SOrd k, SDecide k) => SingMap k f -> SomeSingWith1 k f -> SingMap k f
     ins t (SomeSingWith1 k x) = insert k x t
 
 -- | /O(n*log n)/. Build a map from a list of key\/value pairs with a combining function. See also 'fromAscListWithKey'.
-fromListWithKey :: (SOrd kproxy, SDecide kproxy) => (forall v. Sing v -> f v -> f v -> f v) -> [SomeSingWith1 kproxy f] -> SingMap kproxy f
-fromListWithKey f xs 
+fromListWithKey :: (SOrd k, SDecide k) => (forall v. Sing v -> f v -> f v -> f v) -> [SomeSingWith1 k f] -> SingMap k f
+fromListWithKey f xs
   = foldlStrict (ins f) empty xs
   where
-    ins :: (SOrd kproxy, SDecide kproxy) => (forall v. Sing v -> f v -> f v -> f v) -> SingMap kproxy f -> SomeSingWith1 kproxy f -> SingMap kproxy f
+    ins :: (SOrd k, SDecide k) => (forall v. Sing v -> f v -> f v -> f v) -> SingMap k f -> SomeSingWith1 k f -> SingMap k f
     ins f t (SomeSingWith1 k x) = insertWithKey f k x t
 
 -- | /O(n)/. Convert to a list of key\/value pairs.
-toList :: (kproxy ~ 'KProxy) => SingMap kproxy f -> [SomeSingWith1 kproxy f]
+toList ::  SingMap k f -> [SomeSingWith1 k f]
 toList t      = toAscList t
 
 -- | /O(n)/. Convert to an ascending list.
-toAscList :: (kproxy ~ 'KProxy) => SingMap kproxy f -> [SomeSingWith1 kproxy f]
+toAscList ::  SingMap k f -> [SomeSingWith1 k f]
 toAscList t   = foldrWithKey (\k x xs -> (SomeSingWith1 k x):xs) [] t
 
 -- | /O(n)/. Convert to a descending list.
-toDescList :: (kproxy ~ 'KProxy) => SingMap kproxy f -> [SomeSingWith1 kproxy f]
+toDescList :: SingMap k f -> [SomeSingWith1 k f]
 toDescList t  = foldlWithKey (\xs k x -> (SomeSingWith1 k x):xs) [] t
 
 {--------------------------------------------------------------------
   Building trees from ascending/descending lists can be done in linear time.
-  
-  Note that if [xs] is ascending that: 
+
+  Note that if [xs] is ascending that:
     fromAscList xs       == fromList xs
     fromAscListWith f xs == fromListWith f xs
 --------------------------------------------------------------------}
 
 -- | /O(n)/. Build a map from an ascending list in linear time.
 -- /The precondition (input list is ascending) is not checked./
-fromAscList :: (SEq kproxy, SDecide kproxy) => [SomeSingWith1 kproxy f] -> SingMap kproxy f
+fromAscList :: (SEq k, SDecide k) => [SomeSingWith1 k f] -> SingMap k f
 fromAscList xs
   = fromAscListWithKey (\_ x _ -> x) xs
 
 -- | /O(n)/. Build a map from an ascending list in linear time with a
 -- combining function for equal keys.
 -- /The precondition (input list is ascending) is not checked./
-fromAscListWithKey :: (SEq kproxy, SDecide kproxy) => (forall v. Sing v -> f v -> f v -> f v) -> [SomeSingWith1 kproxy f] -> SingMap kproxy f 
+fromAscListWithKey :: (SEq k, SDecide k) => (forall v. Sing v -> f v -> f v -> f v) -> [SomeSingWith1 k f] -> SingMap k f
 fromAscListWithKey f xs
   = fromDistinctAscList (combineEq f xs)
   where
@@ -1155,7 +1160,7 @@
         [x]    -> [x]
         (x:xx) -> combineEq' f x xx
 
-  combineEq' :: (SEq kproxy, SDecide kproxy) => (forall v. Sing v -> f v -> f v -> f v) -> SomeSingWith1 kproxy f -> [SomeSingWith1 kproxy f] -> [SomeSingWith1 kproxy f]
+  combineEq' :: (SEq k, SDecide k) => (forall v. Sing v -> f v -> f v -> f v) -> SomeSingWith1 k f -> [SomeSingWith1 k f] -> [SomeSingWith1 k f]
   combineEq' f z [] = [z]
   combineEq' f z@(SomeSingWith1 kz zz) (x@(SomeSingWith1 kx xx):xs') =
     case kx %:== kz of
@@ -1165,17 +1170,17 @@
 
 -- | /O(n)/. Build a map from an ascending list of distinct elements in linear time.
 -- /The precondition is not checked./
-fromDistinctAscList :: [SomeSingWith1 kproxy f] -> SingMap kproxy f
+fromDistinctAscList :: [SomeSingWith1 k f] -> SingMap k f
 fromDistinctAscList xs
   = build const (length xs) xs
   where
     -- 1) use continutations so that we use heap space instead of stack space.
-    -- 2) special case for n==5 to build bushier trees. 
-    
-    build :: (SingMap kproxy f -> [SomeSingWith1 kproxy f] -> b) -> Int -> [SomeSingWith1 kproxy f] -> b
+    -- 2) special case for n==5 to build bushier trees.
+
+    build :: (SingMap k f -> [SomeSingWith1 k f] -> b) -> Int -> [SomeSingWith1 k f] -> b
     build c 0 xs'  = c Tip xs'
     build c 5 xs'  = case xs' of
-                       ((SomeSingWith1 k1 x1):(SomeSingWith1 k2 x2):(SomeSingWith1 k3 x3):(SomeSingWith1 k4 x4):(SomeSingWith1 k5 x5):xx) 
+                       ((SomeSingWith1 k1 x1):(SomeSingWith1 k2 x2):(SomeSingWith1 k3 x3):(SomeSingWith1 k4 x4):(SomeSingWith1 k5 x5):xx)
                             -> c (bin k4 x4 (bin k2 x2 (singleton k1 x1) (singleton k3 x3)) (singleton k5 x5)) xx
                        _ -> error "fromDistinctAscList build"
     build c n xs'  = seq nr $ build (buildR nr c) nl xs'
@@ -1183,14 +1188,14 @@
                      nl = n `div` 2
                      nr = n - nl - 1
 
-    buildR :: Int -> (SingMap kproxy f -> [SomeSingWith1 kproxy f] -> b) -> SingMap kproxy f -> [SomeSingWith1 kproxy f] -> b
+    buildR :: Int -> (SingMap k f -> [SomeSingWith1 k f] -> b) -> SingMap k f -> [SomeSingWith1 k f] -> b
     buildR n c l (SomeSingWith1 k x : ys) = build (buildB l k x c) n ys
     buildR _ _ _ []           = error "fromDistinctAscList buildR []"
-    
-    buildB :: SingMap kproxy f -> Sing v -> f v -> (SingMap kproxy f -> a -> b) -> SingMap kproxy f -> a -> b
+
+    buildB :: SingMap k f -> Sing v -> f v -> (SingMap k f -> a -> b) -> SingMap k f -> a -> b
     buildB l k x c r zs       = c (bin k x l r) zs
-                      
 
+
 {--------------------------------------------------------------------
   Split
 --------------------------------------------------------------------}
@@ -1198,10 +1203,10 @@
 -- | /O(log n)/. The expression (@'split' k map@) is a pair @(map1,map2)@ where
 -- the keys in @map1@ are smaller than @k@ and the keys in @map2@ larger than @k@.
 -- Any key equal to @k@ is found in neither @map1@ nor @map2@.
-split :: forall (kproxy :: KProxy k) f (v :: k). (SOrd kproxy, SDecide kproxy) => Sing v -> SingMap kproxy f -> (SingMap kproxy f, SingMap kproxy f)
+split :: forall k f (v :: k). (SOrd k, SDecide k) => Sing v -> SingMap k f -> (SingMap k f, SingMap k f)
 split k = go
   where
-    go :: SingMap kproxy f -> (SingMap kproxy f, SingMap kproxy f)
+    go :: SingMap k f -> (SingMap k f, SingMap k f)
     go Tip              = (Tip, Tip)
     go (Bin _ kx x l r) = case sCompare k kx of
       SLT -> let (lt,gt) = go l in (lt,combine kx x gt r)
@@ -1210,10 +1215,10 @@
 
 -- | /O(log n)/. The expression (@'splitLookup' k map@) splits a map just
 -- like 'split' but also returns @'lookup' k map@.
-splitLookup :: forall kproxy f v. (SOrd kproxy, SDecide kproxy) => Sing v -> SingMap kproxy f -> (SingMap kproxy f, Maybe (f v), SingMap kproxy f)
+splitLookup :: forall k f v. (SOrd k, SDecide k) => Sing v -> SingMap k f -> (SingMap k f, Maybe (f v), SingMap k f)
 splitLookup k = go
   where
-    go :: SingMap kproxy f -> (SingMap kproxy f, Maybe (f v), SingMap kproxy f)
+    go :: SingMap k f -> (SingMap k f, Maybe (f v), SingMap k f)
     go Tip              = (Tip,Nothing,Tip)
     go (Bin _ kx x l r) = case sCompare k kx of
       SLT -> let (lt,z,gt) = go l in (lt,z,combine kx x gt r)
@@ -1221,10 +1226,10 @@
       SEQ -> unifyOnCompareEQ k kx (l,Just x,r)
 
 -- | /O(log n)/.
-splitLookupWithKey :: forall kproxy f v. (SOrd kproxy, SDecide kproxy) => Sing v -> SingMap kproxy f -> (SingMap kproxy f, Maybe (Sing v, f v), SingMap kproxy f)
+splitLookupWithKey :: forall k f v. (SOrd k, SDecide k) => Sing v -> SingMap k f -> (SingMap k f, Maybe (Sing v, f v), SingMap k f)
 splitLookupWithKey k = go
   where
-    go :: SingMap kproxy f -> (SingMap kproxy f, Maybe (Sing v, f v), SingMap kproxy f)
+    go :: SingMap k f -> (SingMap k f, Maybe (Sing v, f v), SingMap k f)
     go Tip              = (Tip,Nothing,Tip)
     go (Bin _ kx x l r) = case sCompare k kx of
       SLT -> let (lt,z,gt) = go l in (lt,z,combine kx x gt r)
@@ -1233,18 +1238,18 @@
 
 -- TODO: Enable Eq and Ord instances
 {--------------------------------------------------------------------
-  Eq converts the tree to a list. In a lazy setting, this 
-  actually seems one of the faster methods to compare two trees 
+  Eq converts the tree to a list. In a lazy setting, this
+  actually seems one of the faster methods to compare two trees
   and it is certainly the simplest :-)
 --------------------------------------------------------------------}
--- instance EqSing1 f => Eq (SingMap kproxy f) where
+-- instance EqSing1 f => Eq (SingMap k f) where
 --   t1 == t2  = (size t1 == size t2) && (toAscList t1 == toAscList t2)
 
 {--------------------------------------------------------------------
-  Ord 
+  Ord
 --------------------------------------------------------------------}
 
--- instance OrdTag k f => Ord (SingMap kproxy f) where
+-- instance OrdTag k f => Ord (SingMap k f) where
 --     compare m1 m2 = compare (toAscList m1) (toAscList m2)
 
 -- TODO: Figure out show to recreate a Read instance
@@ -1252,27 +1257,27 @@
   Read
 --------------------------------------------------------------------}
 
--- instance ((SOrd kproxy, SDecide kproxy) ReadTag k f) => Read (SingMap kproxy f) where
+-- instance ((SOrd k, SDecide k) ReadTag k f) => Read (SingMap k f) where
 --   readPrec = parens $ prec 10 $ do
 --     Ident "fromList" <- lexP
 --     xs <- readPrec
 --     return (fromList xs)
--- 
+--
 --   readListPrec = readListPrecDefault
 
 -- TODO: Figure out show to recreate a Show instance
 {--------------------------------------------------------------------
   Show
 --------------------------------------------------------------------}
--- instance ShowTag k f => Show (SingMap kproxy f) where
+-- instance ShowTag k f => Show (SingMap k f) where
 --     showsPrec p m = showParen (p>10)
 --         ( showString "fromList "
 --         . showsPrec 11 (toList m)
 --         )
--- 
+--
 -- -- | /O(n)/. Show the tree that implements the map. The tree is shown
 -- -- in a compressed, hanging format. See 'showTreeWith'.
--- showTree :: ShowTag k f => SingMap kproxy f -> String
+-- showTree :: ShowTag k f => SingMap k f -> String
 -- showTree m
 --   = showTreeWith showElem True False m
 --   where
@@ -1285,17 +1290,17 @@
  'True', a /hanging/ tree is shown otherwise a rotated tree is shown. If
  @wide@ is 'True', an extra wide version is shown.
 -}
-showTreeWith :: (forall v. Sing v -> f v -> String) -> Bool -> Bool -> SingMap kproxy f -> String
+showTreeWith :: (forall v. Sing v -> f v -> String) -> Bool -> Bool -> SingMap k f -> String
 showTreeWith showelem hang wide t
   | hang      = (showsTreeHang showelem wide [] t) ""
   | otherwise = (showsTree showelem wide [] [] t) ""
 
-showsTree :: (forall v. Sing v -> f v -> String) -> Bool -> [String] -> [String] -> SingMap kproxy f -> ShowS
+showsTree :: (forall v. Sing v -> f v -> String) -> Bool -> [String] -> [String] -> SingMap k f -> ShowS
 showsTree showelem wide lbars rbars t
   = case t of
       Tip -> showsBars lbars . showString "|\n"
       Bin _ kx x Tip Tip
-          -> showsBars lbars . showString (showelem kx x) . showString "\n" 
+          -> showsBars lbars . showString (showelem kx x) . showString "\n"
       Bin _ kx x l r
           -> showsTree showelem wide (withBar rbars) (withEmpty rbars) r .
              showWide wide rbars .
@@ -1303,22 +1308,22 @@
              showWide wide lbars .
              showsTree showelem wide (withEmpty lbars) (withBar lbars) l
 
-showsTreeHang :: (forall v. Sing v -> f v -> String) -> Bool -> [String] -> SingMap kproxy f -> ShowS
+showsTreeHang :: (forall v. Sing v -> f v -> String) -> Bool -> [String] -> SingMap k f -> ShowS
 showsTreeHang showelem wide bars t
   = case t of
-      Tip -> showsBars bars . showString "|\n" 
+      Tip -> showsBars bars . showString "|\n"
       Bin _ kx x Tip Tip
-          -> showsBars bars . showString (showelem kx x) . showString "\n" 
+          -> showsBars bars . showString (showelem kx x) . showString "\n"
       Bin _ kx x l r
-          -> showsBars bars . showString (showelem kx x) . showString "\n" . 
+          -> showsBars bars . showString (showelem kx x) . showString "\n" .
              showWide wide bars .
              showsTreeHang showelem wide (withBar bars) l .
              showWide wide bars .
              showsTreeHang showelem wide (withEmpty bars) r
 
 showWide :: Bool -> [String] -> String -> String
-showWide wide bars 
-  | wide      = showString (concat (reverse bars)) . showString "|\n" 
+showWide wide bars
+  | wide      = showString (concat (reverse bars)) . showString "|\n"
   | otherwise = id
 
 showsBars :: [String] -> ShowS
@@ -1339,32 +1344,32 @@
 --------------------------------------------------------------------}
 
 -- | /O(n)/. Test if the internal map structure is valid.
-valid :: (SOrd kproxy, SDecide kproxy) => SingMap kproxy f -> Bool
+valid :: (SOrd k, SDecide k) => SingMap k f -> Bool
 valid t
   = balanced t && ordered t && validsize t
 
-ordered :: (SOrd kproxy, SDecide kproxy) => SingMap kproxy f -> Bool
+ordered :: (SOrd k, SDecide k) => SingMap k f -> Bool
 ordered t
   = bounded (const True) (const True) t
   where
-    bounded :: (SOrd kproxy, SDecide kproxy) => (SomeSing kproxy -> Bool) -> (SomeSing kproxy -> Bool) -> SingMap kproxy f -> Bool
+    bounded :: (SOrd k, SDecide k) => (SomeSing k -> Bool) -> (SomeSing k -> Bool) -> SingMap k f -> Bool
     bounded lo hi t'
       = case t' of
           Tip              -> True
-          Bin _ kx _ l r  -> (lo (SomeSing kx)) 
-                          && (hi (SomeSing kx)) 
-                          && bounded lo (`ltSome` SomeSing kx) l 
+          Bin _ kx _ l r  -> (lo (SomeSing kx))
+                          && (hi (SomeSing kx))
+                          && bounded lo (`ltSome` SomeSing kx) l
                           && bounded (`gtSome` SomeSing kx) hi r
 
 -- | Exported only for "Debug.QuickCheck"
-balanced :: SingMap kproxy f -> Bool
+balanced :: SingMap k f -> Bool
 balanced t
   = case t of
       Tip            -> True
       Bin _ _ _ l r  -> (size l + size r <= 1 || (size l <= delta*size r && size r <= delta*size l)) &&
                         balanced l && balanced r
 
-validsize :: SingMap kproxy f -> Bool
+validsize :: SingMap k f -> Bool
 validsize t
   = (realsize t == Just (size t))
   where
@@ -1384,22 +1389,22 @@
     go z (x:xs) = z `seq` go (f z x) xs
 
 
-ltSome :: SOrd kproxy => SomeSing kproxy -> SomeSing kproxy -> Bool
+ltSome :: SOrd k => SomeSing k -> SomeSing k -> Bool
 ltSome (SomeSing a) (SomeSing b) = fromSing (a %:< b)
 
-gtSome :: SOrd kproxy => SomeSing kproxy -> SomeSing kproxy -> Bool
+gtSome :: SOrd k => SomeSing k -> SomeSing k -> Bool
 gtSome (SomeSing a) (SomeSing b) = fromSing (a %:> b)
 
-unifyOnCompareEQ :: forall (kproxy :: KProxy k) (a :: k) (b :: k) x. 
-  (SDecide kproxy, Compare a b ~ 'EQ)
+unifyOnCompareEQ :: forall k (a :: k) (b :: k) x.
+  (SDecide k, Compare a b ~ 'EQ)
   => Sing a -> Sing b -> (a ~ b => x) -> x
 unifyOnCompareEQ a b x =
   case testEquality a b of
     Nothing -> error "unifyOnCompareEQ: inconsistent SOrd and SDecide instances"
     Just Refl -> x
 
-unifyOnEq :: forall (kproxy :: KProxy k) (a :: k) (b :: k) x. 
-  (SDecide kproxy, (a :== b) ~ 'True)
+unifyOnEq :: forall k (a :: k) (b :: k) x.
+  (SDecide k, (a :== b) ~ 'True)
   => Sing a -> Sing b -> (a ~ b => x) -> x
 unifyOnEq a b x =
   case testEquality a b of
@@ -1409,10 +1414,10 @@
 ---------------------
 -- Record Helpers
 ---------------------
-fromRec :: (SOrd kproxy, SDecide kproxy) => Rec (SingWith1 kproxy f) rs -> SingMap kproxy f
+fromRec :: (SOrd k, SDecide k) => Rec (SingWith1 k f) rs -> SingMap k f
 fromRec r = insertRec r empty
 
-insertRec :: (SOrd kproxy, SDecide kproxy) => Rec (SingWith1 kproxy f) rs -> SingMap kproxy f -> SingMap kproxy f
+insertRec :: (SOrd k, SDecide k) => Rec (SingWith1 k f) rs -> SingMap k f -> SingMap k f
 insertRec RNil m = m
 insertRec (SingWith1 s v :& rs) m = insert s v (insertRec rs m)