Dependently typed red-black tree in Haskell, part 3

We left off with the basic GADTs defined to capture a red-black tree, but we had no way to insert or delete values. To implement these operations, I will use zippers via some auxiliary GADTs (I have heard of another pattern, lenses, that, from what I can tell, solve a similar problem to zippers, though I don't yet understand lenses. If lenses, or something else, could solve this problem more elegantly, I'd appreciate any references).

Zippers bread crumbs allow us to move up and down the tree to manipulate the state deep inside the tree.

type RB a n = Either (Red a n) (Black a n)

type RBCrumb a n = Either (RedCrumb a n) (BlackCrumb a (S n))

data RedCrumb a n where
  RootCrumb :: RedCrumb a n
  RedCrumb :: a -> (Black a n) -> (BlackCrumb a (S n)) -> RedCrumb a n

data BlackCrumb a n where
  BlackCrumb :: a -> (RB a n) -> (RBCrumb a (S n)) -> BlackCrumb a (S n)

type RBZip a n = Either (RedZip a n) (BlackZip a n)

data RedZip a n where
  RedZip :: a -> (Black a n) -> (Black a n) -> (BlackCrumb a (S n)) -> RedZip a n

data BlackZip a n where
  LeafZip :: (RBCrumb a n) -> BlackZip a Z
  Black2Zip :: a -> (Black a n) -> (Black a n) -> (RBCrumb a (S n)) -> BlackZip a (S n)
  Black3Zip :: a -> (Red a n) -> (Black a n) -> (RBCrumb a (S n)) -> BlackZip a (S n)
  Black4Zip :: a -> (Red a n) -> (Red a n) -> (RBCrumb a (S n)) -> BlackZip a (S n)

The zipper mirrors the structure of the tree, with the added "crumb" that acts like the parent pointer in an imperative implementation. The crumb is somewhat dual to the tree: there is no leaf crumb since you can never be below a leaf; instead, we have a red "root" crumb, with no associated value, that lies above the root element of the tree.
A couple auxiliary functions for converting nodes into zippers.

toBlackZip :: Black a n -> RBCrumb a n -> BlackZip a n
toBlackZip Leaf c = LeafZip $ c
toBlackZip (Black2 v l r) c = Black2Zip v l r c
toBlackZip (Black3 v l r) c = Black3Zip v l r c
toBlackZip (Black4 v l r) c = Black4Zip v l r c

toRedZip :: Red a n -> BlackCrumb a (S n) -> RedZip a n
toRedZip (Red v l r) c = RedZip v l r c

Next step is functions to find the leaf where a new value would fit in. Nothing to exciting, most interesting part was seeing the type checker catch my bugs.

findLeafB :: (Ord a) => a -> BlackZip a n -> BlackZip a Z
findLeafB u z@(LeafZip c) = z
findLeafB u (Black2Zip v l r c)
  | u < v     = findLeafB u $ toBlackZip l (Right $ BlackCrumb v (Right r) c)
  | otherwise = findLeafB u $ toBlackZip r (Right $ BlackCrumb v (Right l) c)
findLeafB u (Black3Zip v l r c)
  | u < v     = findLeafR u . toRedZip l $ BlackCrumb v (Right r) c
  | otherwise = findLeafB u $ toBlackZip r (Right $ BlackCrumb v (Left l) c)
findLeafB u (Black4Zip v l r c)
  | u < v     = findLeafR u . toRedZip l $ BlackCrumb v (Left r) c
  | otherwise = findLeafR u $ toRedZip r $ BlackCrumb v (Left r) c

findLeafR :: (Ord a) => a -> RedZip a n -> BlackZip a Z
findLeafR u (RedZip v l r c)
  | u < v     = findLeafB u $ toBlackZip l (Left $ RedCrumb v r c)
  | otherwise = findLeafB u $ toBlackZip r (Left $ RedCrumb v l c)

Now, to insert the new value, we replace the leaf zipper with a red zipper containing the new value

inject :: a -> BlackZip a Z -> RedZip a Z
inject v (LeafZip c) = RedZip v Leaf Leaf c

But this won't type-check! The parent of a red node must be black (which is enforced by the type system), while the parent of a black node, like a leaf, can be either red or black. To handle this, I will need to augment the red zipper to allow some illegal, transient states. However, since these extra states are not part of the node GADTs, it is still impossible to construct an illegal tree!