diff --git a/ChangeLog.md b/ChangeLog.md
--- a/ChangeLog.md
+++ b/ChangeLog.md
@@ -1,7 +1,11 @@
 # Changelog for type-sets
 
+## 0.1.1.0 --- 2019-08-11
+
+- Added `Type.RBSet` for a red-black-tree-backed set (thanks to @danidiaz)
+
 ## 0.1.0.0 --- 2019-08-07
 
-Initial release!
+- Initial release!
 
 ## Unreleased changes
diff --git a/README.md b/README.md
--- a/README.md
+++ b/README.md
@@ -1,7 +1,7 @@
 # type-sets
 
 [![Build Status](https://api.travis-ci.org/isovector/type-sets.svg?branch=master)](https://travis-ci.org/isovector/type-sets)
-[![Hackage](https://img.shields.io/hackage/v/cmptype.svg?logo=haskell&label=cmptype)](https://hackage.haskell.org/package/cmptype)
+[![Hackage](https://img.shields.io/hackage/v/type-sets.svg?logo=haskell&label=type-sets)](https://hackage.haskell.org/package/type-sets)
 
 
 ## Dedication
@@ -31,7 +31,7 @@
 test1 = id  -- Bool is a member :)
 
 test2 :: Proxy (Member Char MySet) -> Proxy 'False
-test2 = id  -- False is not a member :(
+test2 = id  -- Char is not a member :(
 ```
 
 See the `Type.Set` module for more operations.
diff --git a/src/Type/RBSet.hs b/src/Type/RBSet.hs
new file mode 100644
--- /dev/null
+++ b/src/Type/RBSet.hs
@@ -0,0 +1,583 @@
+{-# LANGUAGE DataKinds             #-}
+{-# LANGUAGE PolyKinds             #-}
+{-# LANGUAGE TypeFamilies          #-}
+{-# LANGUAGE TypeOperators         #-}
+{-# LANGUAGE UndecidableInstances  #-}
+{-# LANGUAGE MultiParamTypeClasses #-}
+{-# LANGUAGE FlexibleInstances     #-}
+
+-- | See <https://www.cs.kent.ac.uk/people/staff/smk/redblack/rb.html here> for
+-- the original term-level code by Stefan Kahrs.
+--
+-- @since 0.1.1.0
+module Type.RBSet
+  ( -- * Core type
+    TypeSet (..)
+  , Empty
+    -- * Set operations
+  , Member
+  , Insertable(Insert)
+  , InsertAll
+  , FromList
+  , Removable(Remove)
+  , Merge
+  ) where
+
+import Type.Compare
+import GHC.TypeLits
+
+-- | The color of a node.
+data Color = R
+           | B
+    deriving (Show,Eq)
+
+-- | A Red-Black tree.
+--
+-- @since 0.1.1.0
+data TypeSet a = E
+               | N Color (TypeSet a) a (TypeSet a)
+    deriving (Show,Eq)
+
+-- | A map without entries.
+type Empty = E
+
+--
+--
+-- Insertion
+
+{- | Insert a list of type level key / value pairs into a type-level map.
+-}
+type family InsertAll (es :: [k]) (t :: TypeSet k) :: TypeSet k where
+    InsertAll '[] t = t
+    InsertAll ( v ': es ) t = Insert v (InsertAll es t)
+
+{- | Build a type-level map out of a list of type level key / value pairs.
+-}
+type FromList (es :: [k]) = InsertAll es Empty
+
+{- | The associated type family 'Insert' produces the resulting map.
+
+ -}
+class Insertable (k :: ki) (t :: TypeSet ki) where
+    type Insert k t :: TypeSet ki
+
+-- insert x s =
+--  T B a z b
+--  where
+--  T _ a z b = ins s
+instance (InsertableHelper1 k t, Insert1 k t ~ inserted, CanMakeBlack inserted) => Insertable k t where
+    type Insert k t = MakeBlack (Insert1 k t)
+
+class CanMakeBlack (t :: TypeSet ki) where
+    type MakeBlack t :: TypeSet ki
+
+instance CanMakeBlack (N color left k right) where
+    type MakeBlack (N color left k right) = N B left k right
+
+instance CanMakeBlack E where
+    type MakeBlack E = E
+
+class InsertableHelper1 (k :: ki)
+                        (t :: TypeSet ki) where
+    type Insert1 k t :: TypeSet ki
+
+instance InsertableHelper1 k E where
+    type Insert1 k E = N R E k E
+
+instance (CmpType k k' ~ ordering,
+          InsertableHelper2 ordering k color left k' right
+         )
+         => InsertableHelper1 k (N color left k' right) where
+    -- FIXME possible duplicate work with CmpType: both in constraint and in associated type family.
+    -- Is that bad? How to avoid it?
+    type Insert1 k (N color left k' right) = Insert2 (CmpType k k') k color left k' right
+
+class InsertableHelper2 (ordering :: Ordering)
+                        (k :: ki)
+                        (color :: Color)
+                        (left :: TypeSet ki)
+                        (k' :: ki)
+                        (right :: TypeSet ki) where
+    type Insert2 ordering k color left k' right :: TypeSet ki
+
+--  ins s@(T B a y b)
+--      | x<y = balance (ins a) y b
+instance (InsertableHelper1 k left, Insert1 k left ~ inserted,
+          Balanceable inserted k' right
+         )
+         => InsertableHelper2 LT k B left k' right where
+    type Insert2              LT k B left k' right = Balance (Insert1 k left) k' right
+
+--  ins s@(T B a y b)
+--      | x<y = balance (ins a) y b
+instance (InsertableHelper1 k left, Insert1 k left ~ inserted,
+          Balanceable inserted k' right
+         )
+         => InsertableHelper2 LT k R left k' right where
+    type Insert2              LT k R left k' right = N R (Insert1 k left) k' right
+
+
+instance InsertableHelper2 EQ k color left k right where
+    type Insert2           EQ k color left k right = N color left k right
+
+--  ins s@(T B a y b)
+--      | ...
+--      | x>y = balance a y (ins b)
+instance (InsertableHelper1 k right, Insert1 k right ~ inserted,
+          Balanceable left  k' inserted
+         )
+         => InsertableHelper2 GT k B left k' right where
+    type Insert2              GT k B left k' right = Balance left  k' (Insert1 k right)
+
+--  ins s@(T R a y b)
+--      | ...
+--      | x>y = T R a y (ins b)
+instance (InsertableHelper1 k right, Insert1 k right ~ inserted,
+          Balanceable left  k' inserted
+         )
+         => InsertableHelper2 GT k R left k' right where
+    type Insert2              GT k R left k' right = N R left k' (Insert1 k right)
+
+data BalanceAction = BalanceSpecial
+                   | BalanceLL
+                   | BalanceLR
+                   | BalanceRL
+                   | BalanceRR
+                   | DoNotBalance
+                   deriving Show
+
+type family ShouldBalance (left :: TypeSet ki) (right :: TypeSet ki) :: BalanceAction where
+    ShouldBalance (N R _ _ _) (N R _ _ _) = BalanceSpecial
+    ShouldBalance (N R (N R _ _ _) _ _) _ = BalanceLL
+    ShouldBalance (N R _ _ (N R _ _ _)) _ = BalanceLR
+    ShouldBalance _ (N R (N R _ _ _) _ _) = BalanceRL
+    ShouldBalance _ (N R _ _ (N R _ _ _)) = BalanceRR
+    ShouldBalance _ _                     = DoNotBalance
+
+class Balanceable (left :: TypeSet ki) (k :: ki) (right :: TypeSet ki) where
+    type Balance left k right :: TypeSet ki
+
+instance (ShouldBalance left right ~ action,
+          BalanceableHelper action left k right
+         )
+         => Balanceable left k right where
+    -- FIXME possible duplicate work with ShouldBalance: both in constraint and in associated type family.
+    -- Is that bad? How to avoid it?
+    type Balance left k right = Balance' (ShouldBalance left right) left k right
+
+class BalanceableHelper (action :: BalanceAction)
+                        (left :: TypeSet ki)
+                        (k :: ki)
+                        (right :: TypeSet ki) where
+    type Balance' action left k right :: TypeSet ki
+
+-- balance (T R a x b) y (T R c z d) = T R (T B a x b) y (T B c z d)
+instance BalanceableHelper BalanceSpecial (N R left1 k1 right1) kx (N R left2 k2 right2) where
+    type Balance'          BalanceSpecial (N R left1 k1 right1) kx (N R left2 k2 right2) =
+                                      N R (N B left1 k1 right1) kx (N B left2 k2 right2)
+
+-- balance (T R (T R a x b) y c) z d = T R (T B a x b) y (T B c z d)
+instance BalanceableHelper BalanceLL (N R (N R a k1 b) k2 c) k3 d where
+    type Balance'          BalanceLL (N R (N R a k1 b) k2 c) k3 d =
+                                 N R (N B a k1 b) k2 (N B c k3 d)
+
+-- balance (T R a x (T R b y c)) z d = T R (T B a x b) y (T B c z d)
+instance BalanceableHelper BalanceLR (N R a k1 (N R b k2 c)) k3 d where
+    type Balance'          BalanceLR (N R a k1 (N R b k2 c)) k3 d =
+                                 N R (N B a k1 b) k2 (N B c k3 d)
+
+-- balance a x (T R (T R b y c) z d) = T R (T B a x b) y (T B c z d)
+instance BalanceableHelper BalanceRL a k1 (N R (N R b k2 c) k3 d) where
+    type Balance'          BalanceRL a k1 (N R (N R b k2 c) k3 d) =
+                                 N R (N B a k1 b) k2 (N B c k3 d)
+
+
+-- balance a x (T R b y (T R c z d)) = T R (T B a x b) y (T B c z d)
+instance BalanceableHelper BalanceRR a k1(N R b k2 (N R c k3 d)) where
+    type Balance'          BalanceRR a k1(N R b k2 (N R c k3 d)) =
+                                 N R (N B a k1 b) k2 (N B c k3 d)
+
+-- balance a x b = T B a x b
+instance BalanceableHelper DoNotBalance a k b where
+    type Balance'          DoNotBalance a k b = N B a k b
+
+
+--- Member
+---
+---
+------------------------------------------------------------------------------
+-- | /O(log n)/. Determine membership in the 'TypeSet.'
+type family Member (t :: k) (bst :: TypeSet k)  :: Bool where
+  Member t 'E = 'False
+  Member t ('N _ lbst a rbst) = MemberImpl (CmpType t a) t lbst rbst
+
+type family MemberImpl (ord :: Ordering)
+                       (t :: k)
+                       (lbst :: TypeSet k)
+                       (rbst :: TypeSet k) :: Bool where
+  MemberImpl 'EQ t lbst rbst = 'True
+  MemberImpl 'LT t lbst rbst = Member t lbst
+  MemberImpl 'GT t lbst rbst = Member t rbst
+
+------------------------------------------------------------------------------
+-- | /O(m log n)/ for @Merge m n@; put your smaller set on the left side. Merge
+-- two 'TypeSet's together.
+type family Merge (small :: TypeSet k) (big :: TypeSet k) :: TypeSet k where
+  Merge Empty big   = big
+  Merge small Empty = small
+  Merge ('N _ lbst a rbst) big = Merge rbst (Merge lbst (Insert a big))
+
+
+--
+--
+--
+-- deletion
+--
+--
+--
+
+type family DiscriminateBalL (l :: TypeSet ki) (r :: TypeSet ki) :: Bool where
+    DiscriminateBalL (N R _ _ _) _ = False
+    DiscriminateBalL _           _ = True
+
+class BalanceableL (l :: TypeSet ki) (k :: ki) (r :: TypeSet ki) where
+    type BalL l k r :: TypeSet ki
+
+class BalanceableHelperL (b :: Bool) (l :: TypeSet ki) (k :: ki) (r :: TypeSet ki) where
+    type BalL' b l k r :: TypeSet ki
+
+instance (DiscriminateBalL l r ~ b, BalanceableHelperL b l k r) => BalanceableL l k r where
+    type BalL l k r = BalL' (DiscriminateBalL l r) l k r
+
+-- balleft :: RB a -> a -> RB a -> RB a
+-- balleft (T R a x b) y c = T R (T B a x b) y c
+instance BalanceableHelperL False (N R left1 k1 right1) k2 right2 where
+    type BalL'              False (N R left1 k1 right1) k2 right2 =
+                             (N R (N B left1 k1 right1) k2 right2)
+
+-- balleft bl x (T B a y b) = balance bl x (T R a y b)
+-- the @(N B in the call to balance tree is misleading, as it is ingored...
+instance (N R t2 z t3 ~ g, BalanceableHelper (ShouldBalance t1 g) t1 y g) =>
+    BalanceableHelperL True t1 y (N B t2 z t3) where
+    type BalL'         True t1 y (N B t2 z t3)
+                 =  Balance t1 y (N R t2 z t3)
+
+-- balleft bl x (T R (T B a y b) z c) = T R (T B bl x a) y (balance b z (sub1 c))
+instance (N R l k r ~ g, BalanceableHelper    (ShouldBalance t3 g) t3 z g) =>
+    BalanceableHelperL True t1 y (N R (N B t2 u t3) z (N B l k r)) where
+    type BalL'         True t1 y (N R (N B t2 u t3) z (N B l k r)) =
+                             N R (N B t1 y t2) u (Balance t3 z (N R l k r))
+
+
+-- balright :: RB a -> a -> RB a -> RB a
+-- balright a x (T R b y c) = T R a x (T B b y c)
+-- balright (T B a x b) y bl = balance (T R a x b) y bl
+-- balright (T R a x (T B b y c)) z bl = T R (balance (sub1 a) x b) y (T B c z bl)
+type family DiscriminateBalR (l :: TypeSet ki) (r :: TypeSet ki) :: Bool where
+    DiscriminateBalR _ (N R _ _ _) = False
+    DiscriminateBalR _ _           = True
+
+class BalanceableR (l :: TypeSet ki) (k :: ki) (r :: TypeSet ki) where
+    type BalR l k r :: TypeSet ki
+
+class BalanceableHelperR (b :: Bool) (l :: TypeSet ki) (k :: ki) (r :: TypeSet ki) where
+    type BalR' b l k r :: TypeSet ki
+
+instance (DiscriminateBalR l r ~ b, BalanceableHelperR b l k r) => BalanceableR l k r where
+    type BalR l k r = BalR' (DiscriminateBalR l r) l k r
+
+-- balright :: RB a -> a -> RB a -> RB a
+-- balright a x (T R b y c) = T R a x (T B b y c)
+instance BalanceableHelperR False right2 k2 (N R left1 k1 right1) where
+    type BalR'              False right2 k2 (N R left1 k1 right1) =
+                                  (N R right2 k2 (N B left1 k1 right1))
+
+-- balright (T B a x b) y bl = balance (T R a x b) y bl
+instance (N R t2 z t3 ~ g, ShouldBalance g t1 ~ shouldbalance, BalanceableHelper shouldbalance g y t1) =>
+    BalanceableHelperR True (N B t2 z t3) y t1 where
+    type BalR'         True (N B t2 z t3) y t1
+             =  Balance (N R t2 z t3) y t1
+
+-- balright (T R a x (T B b y c)) z bl = T R (balance (sub1 a) x b) y (T B c z bl)
+instance (N R t2 u t3 ~ g, ShouldBalance g l ~ shouldbalance, BalanceableHelper shouldbalance g z l) =>
+    BalanceableHelperR True (N R (N B t2 u t3) z (N B l k r)) y t1 where
+    type BalR'         True (N R (N B t2 u t3) z (N B l k r)) y t1 =
+                             N R (Balance (N R t2 u t3) z l) k (N B r y t1)
+-- app :: RB a -> RB a -> RB a
+-- app E x = x
+-- app x E = x
+-- app (T R a x b) (T R c y d) =
+--  case app b c of
+--      T R b' z c' -> T R(T R a x b') z (T R c' y d)
+--      bc -> T R a x (T R bc y d)
+-- app (T B a x b) (T B c y d) =
+--  case app b c of
+--      T R b' z c' -> T R(T B a x b') z (T B c' y d)
+--      bc -> balleft a x (T B bc y d)
+-- app a (T R b x c) = T R (app a b) x c
+-- app (T R a x b) c = T R a x (app b c)
+
+
+class Fuseable (l :: TypeSet ki) (r :: TypeSet ki) where
+    type Fuse l r :: TypeSet ki
+
+instance Fuseable E E where
+    type Fuse E E = E
+
+-- app E x = x
+instance Fuseable E (N color left k right) where
+    type Fuse E (N color left k right) = N color left k right
+
+-- app x E = x
+instance Fuseable (N color left k right) E where
+    type Fuse (N color left k right) E = N color left k right
+
+-- app a (T R b x c) = T R (app a b) x c
+instance Fuseable (N B left1 k1 right1) left2
+    => Fuseable (N B left1 k1 right1) (N R left2 k2 right2) where
+    type Fuse   (N B left1 k1 right1) (N R left2 k2 right2) = N R (Fuse (N B left1 k1 right1) left2) k2 right2
+
+
+-- app (T R a x b) c = T R a x (app b c)
+instance Fuseable right1 (N B left2 k2 right2)
+    => Fuseable (N R left1 k1 right1) (N B left2 k2 right2) where
+    type Fuse   (N R left1 k1 right1) (N B left2 k2 right2) = N R left1 k1 (Fuse right1 (N B left2 k2 right2))
+
+
+-- app (T R a x b) (T R c y d) =
+instance (Fuseable right1 left2, Fuse right1 left2 ~ fused, FuseableHelper1 fused (N R left1 k1 right1) (N R left2 k2 right2))
+    => Fuseable (N R left1 k1 right1) (N R left2 k2 right2) where
+    type Fuse   (N R left1 k1 right1) (N R left2 k2 right2) = Fuse1 (Fuse right1 left2) (N R left1 k1 right1) (N R left2 k2 right2)
+
+class FuseableHelper1 (fused :: TypeSet ki) (l :: TypeSet ki) (r :: TypeSet ki) where
+    type Fuse1 fused l r :: TypeSet ki
+
+-- app (T R a x b) (T R c y d) =
+--  case app b c of
+--      T R b' z c' -> T R (T R a x b') z (T R c' y d)
+-- FIXME: The Fuseable constraint is repeated from avobe :(
+instance (Fuseable right1 left2, Fuse right1 left2 ~ N R s1 z s2)
+    => FuseableHelper1 (N R s1 z s2) (N R left1 k1 right1) (N R left2 k2 right2) where
+    type Fuse1         (N R s1 z s2) (N R left1 k1 right1) (N R left2 k2 right2) = N R (N R left1 k1 s1) z (N R s2 k2 right2)
+
+
+-- app (T R a x b) (T R c y d) =
+--  case app b c of
+--      ...
+--      bc -> T R a x (T R bc y d)
+-- FIXME: The Fuseable constraint is repeated from above :(
+instance (Fuseable right1 left2, Fuse right1 left2 ~ N B s1 z s2)
+    => FuseableHelper1 (N B s1 z s2) (N R left1 k1 right1) (N R left2 k2 right2) where
+    type Fuse1         (N B s1 z s2) (N R left1 k1 right1) (N R left2 k2 right2) = N R left1 k1 (N R (N B s1 z s2) k2 right2)
+
+-- app (T R a x b) (T R c y d) =
+--  case app b c of
+--      ...
+--      bc -> T R a x (T R bc y d)
+instance FuseableHelper1 E (N R left1 k1 E) (N R E k2 right2) where
+    type Fuse1           E (N R left1 k1 E) (N R E k2 right2) = N R left1 k1 (N R E k2 right2)
+
+-- app (T B a x b) (T B c y d) =
+instance (Fuseable right1 left2, Fuse right1 left2 ~ fused, FuseableHelper2 fused (N B left1 k1 right1) (N B left2 k2 right2))
+    => Fuseable (N B left1 k1 right1) (N B left2 k2 right2) where
+    type Fuse   (N B left1 k1 right1) (N B left2 k2 right2) = Fuse2 (Fuse right1 left2) (N B left1 k1 right1) (N B left2 k2 right2)
+
+-- could FuseableHelper1 and FuseableHelper2 be, well... fused?
+class FuseableHelper2 (fused :: TypeSet ki) (l :: TypeSet ki) (r :: TypeSet ki) where
+    type Fuse2 fused l r :: TypeSet ki
+
+-- app (T B a x b) (T B c y d) =
+--  case app b c of
+--      T R b' z c' -> T R (T B a x b') z (T B c' y d)
+instance (Fuseable right1 left2, Fuse right1 left2 ~ N R s1 z s2)
+    => FuseableHelper2 (N R s1 z s2) (N B left1 k1 right1) (N B left2 k2 right2) where
+    type Fuse2         (N R s1 z s2) (N B left1 k1 right1) (N B left2 k2 right2) = N R (N B left1 k1 s1) z (N B s2 k2 right2)
+
+-- app (T B a x b) (T B c y d) =
+--  case app b c of
+--      ...
+--      bc -> balleft a x (T B bc y d)
+instance (Fuseable right1 left2, Fuse right1 left2 ~ N B s1 z s2, BalanceableL left1 k1 (N B (N B s1 z s2) k2 right2))
+    => FuseableHelper2 (N B s1 z s2) (N B left1 k1 right1) (N B left2 k2 right2) where
+    type Fuse2         (N B s1 z s2) (N B left1 k1 right1) (N B left2 k2 right2) = BalL left1 k1 (N B (N B s1 z s2) k2 right2)
+
+-- app (T B a x b) (T B c y d) =
+--  case app b c of
+--      ...
+--      bc -> balleft a x (T B bc y d)
+instance (BalanceableL left1 k1 (N B E k2 right2))
+    => FuseableHelper2 E (N B left1 k1 E) (N B E k2 right2) where
+    type Fuse2         E (N B left1 k1 E) (N B E k2 right2) = BalL left1 k1 (N B E k2 right2)
+
+
+--  del E = E
+--  del (T _ a y b)
+--      | x<y = delformLeft a y b
+--      | x>y = delformRight a y b
+--      | otherwise = app a b
+class Delable (k :: ki) (t :: TypeSet ki) where
+    type Del k t :: TypeSet ki
+
+--  delformLeft a@(T B _ _ _) y b = balleft (del a) y b
+--  delformLeft a y b = T R (del a) y b
+--  In the term-level code, the k to delete is already on the environment.
+class DelableL (k :: ki) (l :: TypeSet ki) (kx :: ki)  (r :: TypeSet ki) where
+    type DelL k l kx r :: TypeSet ki
+
+--  delformLeft a@(T B _ _ _) y b = balleft (del a) y b
+instance (N B leftz kz rightz ~ g, Delable k g, Del k g ~ deleted, BalanceableL deleted kx right)
+    => DelableL k (N B leftz kz rightz) kx right where
+    type DelL   k (N B leftz kz rightz) kx right = BalL (Del k (N B leftz kz rightz)) kx right
+
+--  delformLeft a y b = T R (del a) y b
+instance (Delable k (N R leftz kz rightz))
+    => DelableL k (N R leftz kz rightz) kx right where
+    type DelL   k (N R leftz kz rightz) kx right = N R (Del k (N R leftz kz rightz)) kx right
+
+--  delformLeft a y b = T R (del a) y b
+instance DelableL k E kx right where
+    type DelL     k E kx right = N R E kx right
+
+--  delformRight a y b@(T B _ _ _) = balright a y (del b)
+--  delformRight a y b = T R a y (del b)
+class DelableR (k :: ki) (l :: TypeSet ki) (kx :: ki) (r :: TypeSet ki) where
+    type DelR k l kx r :: TypeSet ki
+
+--  delformRight a y b@(T B _ _ _) = balright a y (del b)
+instance (N B leftz kz rightz ~ g, Delable k g, Del k g ~ deleted, BalanceableR left kx deleted)
+    => DelableR k left kx (N B leftz kz rightz) where
+    type DelR   k left kx (N B leftz kz rightz) = BalR left kx (Del k (N B leftz kz rightz))
+
+
+--  delformRight a y b = T R a y (del b)
+instance (Delable k (N R leftz kz rightz))
+    => DelableR k left kx (N R leftz kz rightz) where
+    type   DelR k left kx (N R leftz kz rightz) = N R left kx (Del k (N R leftz kz rightz))
+
+--  delformRight a y b = T R a y (del b)
+instance DelableR k left kx E where
+    type DelR     k left kx E = N R left kx E
+
+--  del E = E
+instance Delable k E where
+    type Del     k E = E
+
+-- the color is discarded
+--  del (T _ a y b)
+--      | x<y = delformLeft a y b
+--      | x>y = delformRight a y b
+--      | otherwise = app a b
+instance (CmpType kx k ~ ordering, DelableHelper ordering k left kx right) => Delable k (N color left kx right) where
+    type Del k (N color left kx right) = Del' (CmpType kx k) k left kx right
+
+class DelableHelper (ordering :: Ordering) (k :: ki) (l :: TypeSet ki) (kx :: ki) (r :: TypeSet ki) where
+    type Del' ordering k l kx r :: TypeSet ki
+
+--      | x<y = delformLeft a y b
+instance DelableL k left kx right => DelableHelper GT k left kx right where
+    type Del'                                      GT k left kx right = DelL k left kx right
+
+--      | otherwise = app a b
+instance Fuseable left right => DelableHelper EQ k left k right where
+    type Del'                                 EQ k left k right = Fuse left right
+
+--      | x>y = delformRight a y b
+instance DelableR k left kx right => DelableHelper LT k left kx right where
+    type Del'                                      LT k left kx right = DelR k left kx right
+
+{- | The associated type family 'Remove' produces the resulting map.
+
+ -}
+class Removable (k :: ki) (t :: TypeSet ki) where
+    type Remove k t :: TypeSet ki
+
+instance (Delable k t, Del k t ~ deleted, CanMakeBlack deleted) => Removable k t where
+    type Remove k t = MakeBlack (Del k t)
+
+
+
+-- The original term-level code, taken from:
+-- https://www.cs.kent.ac.uk/people/staff/smk/redblack/rb.html
+--
+-- {- Version 1, 'untyped' -}
+-- data Color = R | B deriving Show
+-- data RB a = E | T Color (RB a) a (RB a) deriving Show
+--
+-- {- Insertion and membership test as by Okasaki -}
+-- insert :: Ord a => a -> RB a -> RB a
+-- insert x s =
+--  T B a z b
+--  where
+--  T _ a z b = ins s
+--  ins E = T R E x E
+--  ins s@(T B a y b)
+--      | x<y = balance (ins a) y b
+--      | x>y = balance a y (ins b)
+--      | otherwise = s
+--  ins s@(T R a y b)
+--      | x<y = T R (ins a) y b
+--      | x>y = T R a y (ins b)
+--      | otherwise = s
+--
+--
+-- {- balance: first equation is new,
+--    to make it work with a weaker invariant -}
+-- balance :: RB a -> a -> RB a -> RB a
+-- balance (T R a x b) y (T R c z d) = T R (T B a x b) y (T B c z d)
+-- balance (T R (T R a x b) y c) z d = T R (T B a x b) y (T B c z d)
+-- balance (T R a x (T R b y c)) z d = T R (T B a x b) y (T B c z d)
+-- balance a x (T R b y (T R c z d)) = T R (T B a x b) y (T B c z d)
+-- balance a x (T R (T R b y c) z d) = T R (T B a x b) y (T B c z d)
+-- balance a x b = T B a x b
+--
+-- member :: Ord a => a -> RB a -> Bool
+-- member x E = False
+-- member x (T _ a y b)
+--  | x<y = member x a
+--  | x>y = member x b
+--  | otherwise = True
+--
+-- {- deletion a la SMK -}
+-- delete :: Ord a => a -> RB a -> RB a
+-- delete x t =
+--  case del t of {T _ a y b -> T B a y b; _ -> E}
+--  where
+--  del E = E
+--  del (T _ a y b)
+--      | x<y = delformLeft a y b
+--      | x>y = delformRight a y b
+--             | otherwise = app a b
+--  delformLeft a@(T B _ _ _) y b = balleft (del a) y b
+--  delformLeft a y b = T R (del a) y b
+--
+--  delformRight a y b@(T B _ _ _) = balright a y (del b)
+--  delformRight a y b = T R a y (del b)
+--
+-- balleft :: RB a -> a -> RB a -> RB a
+-- balleft (T R a x b) y c = T R (T B a x b) y c
+-- balleft bl x (T B a y b) = balance bl x (T R a y b)
+-- balleft bl x (T R (T B a y b) z c) = T R (T B bl x a) y (balance b z (sub1 c))
+--
+-- balright :: RB a -> a -> RB a -> RB a
+-- balright a x (T R b y c) = T R a x (T B b y c)
+-- balright (T B a x b) y bl = balance (T R a x b) y bl
+-- balright (T R a x (T B b y c)) z bl = T R (balance (sub1 a) x b) y (T B c z bl)
+--
+-- sub1 :: RB a -> RB a
+-- sub1 (T B a x b) = T R a x b
+-- sub1 _ = error "invariance violation"
+--
+-- app :: RB a -> RB a -> RB a
+-- app E x = x
+-- app x E = x
+-- app (T R a x b) (T R c y d) =
+--  case app b c of
+--      T R b' z c' -> T R (T R a x b') z (T R c' y d)
+--      bc -> T R a x (T R bc y d)
+-- app (T B a x b) (T B c y d) =
+--  case app b c of
+--      T R b' z c' -> T R(T B a x b') z (T B c' y d)
+--      bc -> balleft a x (T B bc y d)
+-- app a (T R b x c) = T R (app a b) x c
+-- app (T R a x b) c = T R a x (app b c)
+
diff --git a/test/Spec.hs b/test/Spec.hs
--- a/test/Spec.hs
+++ b/test/Spec.hs
@@ -1,10 +1,13 @@
 {-# LANGUAGE DataKinds #-}
 
 {-# OPTIONS_GHC -fplugin=Type.Compare.Plugin      #-}
-{-# OPTIONS_GHC -fconstraint-solver-iterations=10 #-}
+{-# OPTIONS_GHC -fconstraint-solver-iterations=0  #-} -- with iterations=10, bit sets fail in the RB tests :(
 
 import Data.Proxy
+import Data.Functor.Identity
+import Data.Functor.Const
 import Type.Set
+import qualified Type.RBSet as RB
 
 type MySet = Insert Bool (Insert String (Insert (Maybe Int) 'Empty))
 
@@ -13,6 +16,198 @@
 
 test2 :: Proxy (Member Char MySet) -> Proxy 'False
 test2 = id  -- False is not a member :(
+
+-- RB tests
+--
+--
+type MyRBSet = RB.FromList '[
+                              Bool
+                            , String
+                            , String
+                            , String
+                            , Maybe Int
+                            , Maybe Char
+                            , Char
+                            , Either Int Int
+                            , Either Int Int
+                            , Either Int Int
+                            , Either Char Int
+                            , Either Bool Int
+                            , Maybe Bool
+                            , Identity Int
+                            , Identity Char
+                            , Identity Bool
+                            , Either Int (Identity Int)
+                            , Either Int (Identity Char)
+                            , Either Int (Identity Bool)
+                            , Either Char (Identity Int)
+                            , Either Char (Identity Char)
+                            , Either Char (Identity Bool)
+                            , Either Bool (Identity Int)
+                            , Either Bool (Identity Char)
+                            , Either Bool (Identity Bool)
+                            ]
+
+type MyReducedRBSet = RB.Remove Bool
+                    ( RB.Remove String
+                    ( RB.Remove (Either Int Int)
+                    ( RB.Remove (Either Char Int)
+                    ( RB.Remove (Either Bool (Identity Int))
+                    ( RB.Remove (Either Bool (Identity Char))
+                    ( RB.Remove (Either Bool (Identity Bool))
+                      MyRBSet))))))
+
+type MyReducedToEmptyRBSet =
+                      RB.Remove (Maybe Int)
+                    ( RB.Remove (Maybe Char)
+                    ( RB.Remove Char
+                    ( RB.Remove (Either Bool Int)
+                    ( RB.Remove (Maybe Bool)
+                    ( RB.Remove (Identity Int)
+                    ( RB.Remove (Identity Char)
+                    ( RB.Remove (Identity Bool)
+                    ( RB.Remove (Either Int (Identity Int))
+                    ( RB.Remove (Either Int (Identity Char))
+                    ( RB.Remove (Either Int (Identity Bool))
+                    ( RB.Remove (Either Char (Identity Int))
+                    ( RB.Remove (Either Char (Identity Char))
+                    ( RB.Remove (Either Char (Identity Bool))
+                      MyReducedRBSet)))))))))))))
+
+type MyMergedRBSet = RB.Merge (RB.FromList '[Const Int Bool,
+                                             Const Int Char,
+                                             Const Int String])
+                              MyReducedRBSet
+
+testRB1 :: Proxy (RB.Member (Bool) MyRBSet) -> Proxy 'True
+testRB1 = id
+testRB2 :: Proxy (RB.Member (String) MyRBSet) -> Proxy 'True
+testRB2 = id
+testRB3 :: Proxy (RB.Member (Maybe Int) MyRBSet) -> Proxy 'True
+testRB3 = id
+testRB4 :: Proxy (RB.Member (Maybe Char) MyRBSet) -> Proxy 'True
+testRB4 = id
+testRB5 :: Proxy (RB.Member (Char) MyRBSet) -> Proxy 'True
+testRB5 = id
+testRB6 :: Proxy (RB.Member (Either Int Int) MyRBSet) -> Proxy 'True
+testRB6 = id
+testRB7 :: Proxy (RB.Member (Either Char Int) MyRBSet) -> Proxy 'True
+testRB7 = id
+testRB8 :: Proxy (RB.Member (Either Bool Int) MyRBSet) -> Proxy 'True
+testRB8 = id
+testRB9 :: Proxy (RB.Member (Maybe Bool) MyRBSet) -> Proxy 'True
+testRB9 = id
+testRB10 :: Proxy (RB.Member (Identity Int) MyRBSet) -> Proxy 'True
+testRB10 = id
+testRB11 :: Proxy (RB.Member (Identity Char) MyRBSet) -> Proxy 'True
+testRB11 = id
+testRB12 :: Proxy (RB.Member (Identity Bool) MyRBSet) -> Proxy 'True
+testRB12 = id
+testRB13 :: Proxy (RB.Member (Either Int (Identity Int)) MyRBSet) -> Proxy 'True
+testRB13 = id
+testRB14 :: Proxy (RB.Member (Either Int (Identity Char)) MyRBSet) -> Proxy 'True
+testRB14 = id
+testRB15 :: Proxy (RB.Member (Either Int (Identity Bool)) MyRBSet) -> Proxy 'True
+testRB15 = id
+testRB16 :: Proxy (RB.Member (Either Char (Identity Int)) MyRBSet) -> Proxy 'True
+testRB16 = id
+testRB17 :: Proxy (RB.Member (Either Char (Identity Char)) MyRBSet) -> Proxy 'True
+testRB17 = id
+testRB18 :: Proxy (RB.Member (Either Char (Identity Bool)) MyRBSet) -> Proxy 'True
+testRB18 = id
+testRB19 :: Proxy (RB.Member (Either Bool (Identity Int)) MyRBSet) -> Proxy 'True
+testRB19 = id
+testRB20 :: Proxy (RB.Member (Either Bool (Identity Char)) MyRBSet) -> Proxy 'True
+testRB20 = id
+testRB21 :: Proxy (RB.Member (Either Bool (Identity Bool)) MyRBSet) -> Proxy 'True
+testRB21 = id
+
+testRB102 :: Proxy (RB.Member Float MyRBSet) -> Proxy 'False
+testRB102 = id  -- False is not a member :(
+
+--
+-- Test MyReducedRBSet
+testRB201 :: Proxy (RB.Member (Bool) MyReducedRBSet) -> Proxy 'False
+testRB201 = id
+testRB202 :: Proxy (RB.Member (String) MyReducedRBSet) -> Proxy 'False
+testRB202 = id
+testRB203 :: Proxy (RB.Member (Either Int Int) MyReducedRBSet) -> Proxy 'False
+testRB203 = id
+testRB204 :: Proxy (RB.Member (Either Char Int) MyReducedRBSet) -> Proxy 'False
+testRB204 = id
+testRB205 :: Proxy (RB.Member (Either Bool (Identity Int)) MyReducedRBSet) -> Proxy 'False
+testRB205 = id
+testRB206 :: Proxy (RB.Member (Either Bool (Identity Char)) MyReducedRBSet) -> Proxy 'False
+testRB206 = id
+testRB207 :: Proxy (RB.Member (Either Bool (Identity Bool)) MyReducedRBSet) -> Proxy 'False
+testRB207 = id
+
+-- the rest remain
+testRB303 :: Proxy (RB.Member (Maybe Int) MyReducedRBSet) -> Proxy 'True
+testRB303 = id
+testRB304 :: Proxy (RB.Member (Maybe Char) MyReducedRBSet) -> Proxy 'True
+testRB304 = id
+testRB305 :: Proxy (RB.Member (Char) MyReducedRBSet) -> Proxy 'True
+testRB305 = id
+testRB308 :: Proxy (RB.Member (Either Bool Int) MyReducedRBSet) -> Proxy 'True
+testRB308 = id
+testRB309 :: Proxy (RB.Member (Maybe Bool) MyReducedRBSet) -> Proxy 'True
+testRB309 = id
+testRB310 :: Proxy (RB.Member (Identity Int) MyReducedRBSet) -> Proxy 'True
+testRB310 = id
+testRB311 :: Proxy (RB.Member (Identity Char) MyReducedRBSet) -> Proxy 'True
+testRB311 = id
+testRB312 :: Proxy (RB.Member (Identity Bool) MyReducedRBSet) -> Proxy 'True
+testRB312 = id
+testRB313 :: Proxy (RB.Member (Either Int (Identity Int)) MyReducedRBSet) -> Proxy 'True
+testRB313 = id
+testRB314 :: Proxy (RB.Member (Either Int (Identity Char)) MyReducedRBSet) -> Proxy 'True
+testRB314 = id
+testRB315 :: Proxy (RB.Member (Either Int (Identity Bool)) MyReducedRBSet) -> Proxy 'True
+testRB315 = id
+testRB316 :: Proxy (RB.Member (Either Char (Identity Int)) MyReducedRBSet) -> Proxy 'True
+testRB316 = id
+testRB317 :: Proxy (RB.Member (Either Char (Identity Char)) MyReducedRBSet) -> Proxy 'True
+testRB317 = id
+testRB318 :: Proxy (RB.Member (Either Char (Identity Bool)) MyReducedRBSet) -> Proxy 'True
+testRB318 = id
+
+-- Tests for MyMergedRBSet
+testRB400 :: Proxy (RB.Member (Const Int Bool) MyMergedRBSet) -> Proxy 'True
+testRB400 = id
+testRB401 :: Proxy (RB.Member (Const Int Char) MyMergedRBSet) -> Proxy 'True
+testRB401 = id
+testRB402 :: Proxy (RB.Member (Const Int String) MyMergedRBSet) -> Proxy 'True
+testRB402 = id
+
+testRB403 :: Proxy (RB.Member (Maybe Int) MyMergedRBSet) -> Proxy 'True
+testRB403 = id
+testRB404 :: Proxy (RB.Member (Maybe Char) MyMergedRBSet) -> Proxy 'True
+testRB404 = id
+testRB405 :: Proxy (RB.Member (Char) MyMergedRBSet) -> Proxy 'True
+testRB405 = id
+testRB408 :: Proxy (RB.Member (Either Bool Int) MyMergedRBSet) -> Proxy 'True
+testRB408 = id
+testRB409 :: Proxy (RB.Member (Maybe Bool) MyMergedRBSet) -> Proxy 'True
+testRB409 = id
+testRB410 :: Proxy (RB.Member (Identity Int) MyMergedRBSet) -> Proxy 'True
+testRB410 = id
+testRB411 :: Proxy (RB.Member (Identity Char) MyMergedRBSet) -> Proxy 'True
+testRB411 = id
+testRB412 :: Proxy (RB.Member (Identity Bool) MyMergedRBSet) -> Proxy 'True
+testRB412 = id
+testRB413 :: Proxy (RB.Member (Either Int (Identity Int)) MyMergedRBSet) -> Proxy 'True
+testRB413 = id
+testRB414 :: Proxy (RB.Member (Either Int (Identity Char)) MyMergedRBSet) -> Proxy 'True
+testRB414 = id
+testRB415 :: Proxy (RB.Member (Either Int (Identity Bool)) MyMergedRBSet) -> Proxy 'True
+testRB415 = id
+testRB416 :: Proxy (RB.Member (Either Char (Identity Int)) MyMergedRBSet) -> Proxy 'True
+testRB416 = id
+testRB417 :: Proxy (RB.Member (Either Char (Identity Char)) MyMergedRBSet) -> Proxy 'True
+testRB417 = id
+testRB418 :: Proxy (RB.Member (Either Char (Identity Bool)) MyMergedRBSet) -> Proxy 'True
+testRB418 = id
 
 main :: IO ()
 main = putStrLn "It compiled!"
diff --git a/type-sets.cabal b/type-sets.cabal
--- a/type-sets.cabal
+++ b/type-sets.cabal
@@ -4,10 +4,10 @@
 --
 -- see: https://github.com/sol/hpack
 --
--- hash: 60b368d526cc5cac3b6dd1535ea9d63df46fe48ac16f522464490b53a71a034b
+-- hash: b462ce7243b616ca6d6a73fd65f8ead37c671611e51cbcd0c759f4cf55154214
 
 name:           type-sets
-version:        0.1.0.0
+version:        0.1.1.0
 synopsis:       Type-level sets
 description:    Please see the README on GitHub at <https://github.com/isovector/type-sets#readme>
 category:       Type
@@ -29,6 +29,7 @@
 
 library
   exposed-modules:
+      Type.RBSet
       Type.Set
       Type.Set.Variant
   other-modules:
@@ -37,7 +38,7 @@
       src
   build-depends:
       base >=4.7 && <5
-    , cmptype >=0.1.0.0 && <0.2
+    , cmptype >=0.1.0.0 && <=0.3.0.0
   default-language: Haskell2010
 
 test-suite type-sets-test
@@ -50,6 +51,6 @@
   ghc-options: -threaded -rtsopts -with-rtsopts=-N
   build-depends:
       base >=4.7 && <5
-    , cmptype >=0.1.0.0 && <0.2
+    , cmptype >=0.1.0.0 && <=0.3.0.0
     , type-sets
   default-language: Haskell2010