testsuite/tests/gadt/red-black.hs

   1 {-# LANGUAGE GADTs #-}
   2
   3 module ShouldCompile where
   4
   5 -- data RBTree = forall n. Root (SubTree Black n)
   6
   7 -- Kind Colour
   8 data Red
   9 data Black
  10
  11 -- Kind Nat
  12 data Z
  13 data S a
  14
  15 data SubTree c n where
  16   Leaf :: SubTree Black Z
  17   RNode :: SubTree Black n -> Int -> SubTree Black n -> SubTree Red n
  18   BNode :: SubTree cL m   ->  Int -> SubTree cR m    -> SubTree Black (S m)
  19   Fix   :: SubTree Red n -> SubTree Black n
  20
  21
  22 ins :: Int -> SubTree c n -> SubTree c n
  23 ins n Leaf                   = (Fix (RNode Leaf n Leaf))
  24 ins n (BNode x m y) | n <= m = black (ins n x) m y
  25 ins n (BNode x m y) | n > m  = black x m (ins n y)
  26 ins n (RNode x m y) | n <= m = RNode (ins n x) m y
  27 ins n (RNode x m y) | n > m  = RNode x m (ins n y)
  28
  29 black :: SubTree c n -> Int -> SubTree d n -> SubTree Black (S n)
  30 black (RNode (Fix u) v c) w (x@(RNode _ _ _)) = Fix(RNode (blacken u) v (BNode c w x))
  31
  32 black (RNode (Fix u) v c) w (x@(BNode _ _ _)) = BNode u v (RNode c w x)
  33 black (RNode a v (Fix (RNode b u c))) w (x@(BNode _ _ _)) = BNode (RNode a v b) u (RNode c w x)
  34 black (Fix x) n (Fix y) = BNode x n y
  35 black x       n (Fix y) = BNode x n y
  36 black (Fix x) n y       = BNode x n y
  37 black x       n y       = BNode x n y
  38
  39 blacken :: SubTree Red n -> SubTree Black (S n)
  40 blacken (RNode l e r) = (BNode l e r)
  41