content: {-# LANGUAGE GADTs #-}
  
  module ShouldCompile where
  
  -- data RBTree = forall n. Root (SubTree Black n)
  
  -- Kind Colour
  data Red
  data Black
  
  -- Kind Nat
  data Z
  data S a
  
  data SubTree c n where
    Leaf :: SubTree Black Z
    RNode :: SubTree Black n -> Int -> SubTree Black n -> SubTree Red n
    BNode :: SubTree cL m   ->  Int -> SubTree cR m    -> SubTree Black (S m)
    Fix   :: SubTree Red n -> SubTree Black n
  
  
  ins :: Int -> SubTree c n -> SubTree c n
  ins n Leaf                   = (Fix (RNode Leaf n Leaf))
  ins n (BNode x m y) | n <= m = black (ins n x) m y
  ins n (BNode x m y) | n > m  = black x m (ins n y)
  ins n (RNode x m y) | n <= m = RNode (ins n x) m y
  ins n (RNode x m y) | n > m  = RNode x m (ins n y)
  
  black :: SubTree c n -> Int -> SubTree d n -> SubTree Black (S n)
  black (RNode (Fix u) v c) w (x@(RNode _ _ _)) = Fix(RNode (blacken u) v (BNode c w x))
  
  black (RNode (Fix u) v c) w (x@(BNode _ _ _)) = BNode u v (RNode c w x)
  black (RNode a v (Fix (RNode b u c))) w (x@(BNode _ _ _)) = BNode (RNode a v b) u (RNode c w x)
  black (Fix x) n (Fix y) = BNode x n y
  black x       n (Fix y) = BNode x n y
  black (Fix x) n y       = BNode x n y
  black x       n y       = BNode x n y
  
  blacken :: SubTree Red n -> SubTree Black (S n)
  blacken (RNode l e r) = (BNode l e r)
  
  