Binary trees with type-enforced balance

A Red-black tree is a binary tree which has some properties which assure that it is balanced.

The properties of the RB-Tree can be described using Haskell's type system, thus creating trees that must be balanced.

The compiler will catch any bug in the code handling them which causes the tree to not be balanced - it will not type-check.

The properties of Red-Black trees:

• Each node in the tree has a "color", either Red or Black.
• All different paths from the root of the tree all the way down have the same number of Black nodes.
• No path in the tree has two consecutive Red nodes.

This assures that the ratio between the maximum and minimum depth will be no more than two. The minimum depth will be achieved by a path of Black nodes with no Red nodes between them, while the maximum depth would have as many Red nodes possible crammed between the Black nodes - at most one Red node between each two Black ones.

In code:

{-# LANGUAGE EmptyDataDecls, ExistentialQuantification, GADTs #-}
data Zero
data Succ n

-- We use trees whose root is Black. Simply for implementation convinience.
data Tree a = forall n. Tree (BlackNode n a)
-- Node types are tagged by their subtree's Black-degree (number of Black nodes per path).
data BlackNode n a where
    __-- A degree 0 Black node must be an empty tree.
__Nil :: BlackNode Zero a
__BlackNode :: RBNode n a -> a -> RBNode n a -> BlackNode (Succ n) a
data RBNode n a
    __= ItsRed (RedNode n a)
    __| ItsBlack (BlackNode n a)
-- A Red node's children must be Black.
data RedNode n a = RedNode (BlackNode n a) a (BlackNode n a)

The types for the tree nodes are all indexed by the number of Black nodes per path / "RB-Depth".
The outward facing type, "Tree", wraps a node type using an Existential for the depth, so the depth could be any value and the user of the type would not need to care.

While the type captures the structural rules of the tree, it does not capture the conditions required by binary search trees. I suppose that might be possible in fancier languages such as Agda, and perhaps I'll give it a try :)

Complete working code for the tree, including the insert function, at github.com/yairchu/red-black-tree/blob/master/RedBlackTree.hs