data Z = Z
data S n = S n

data (Ord a) => T a n where
    E :: T a Z
    T :: !(H l r n) -> T a l -> a -> T a r -> T a (S n)

instance (Show a) => Show (T a n) where
    show E = "E"
    show (T h l x r) =
      "(T " ++ show h ++ " " ++ show l ++ " " ++ show x ++ " " ++ show r ++ ")"

-- constraints: |l-r|<=1 and max(l,r)==n
data H l r n where
    B :: H a a a
    L :: H (S a) a (S a)
    R :: H a (S a) (S a)

instance Show (H l r n) where
    show B = "B"
    show L = "L"
    show R = "R"

-----------------------------------------------------------------------------

s :: H l r n -> H (S l) (S r) (S n)
s L = L
s B = B
s R = R

balanceL :: H l r n -> T a (S l) -> a -> T a r -> Either (T a (S n)) (T a (S (S n)))
balanceL h a x b = balanceR' (s h) a x b

balanceR :: H l r n -> T a l -> a -> T a (S r) -> Either (T a (S n)) (T a (S (S n)))
balanceR h a x b = balanceL' (s h) a x b

ins :: (Ord a) => a -> T a n -> Either (T a n) (T a (S n))
ins x E = Right (T B E x E)
ins x t@(T h l v r) =
    case x `compare` v of
    EQ -> Left t
    LT -> case ins x l of
          Left l'  -> Left (T h l' v r)
          Right l' -> balanceL h l' v r
    GT -> case ins x r of
          Left r'  -> Left (T h l v r')
          Right r' -> balanceR h l v r'

-----------------------------------------------------------------------------

balanceL' :: H (S l) r n -> T a l -> a -> T a r -> Either (T a n) (T a (S n))
balanceL' L a x b = Left  (T B a x b)
balanceL' B a x b = Right (T R a x b)
balanceL' R a x (T B b y c) = Right (T L (T R a x b) y c)
balanceL' R a x (T R b y c) = Left  (T B (T B a x b) y c)
balanceL' R a x (T L (T h b y c) z d) =
    case h of
    R -> Left (T B (T L a x b) y (T B c z d))
    B -> Left (T B (T B a x b) y (T B c z d))
    L -> Left (T B (T B a x b) y (T R c z d))

balanceR' :: H l (S r) n -> T a l -> a -> T a r -> Either (T a n) (T a (S n))
balanceR' R a x b = Left  (T B a x b)
balanceR' B a x b = Right (T L a x b)
balanceR' L (T B a x b) y c = Right (T R a x (T L b y c))
balanceR' L (T L a x b) y c = Left  (T B a x (T B b y c))
balanceR' L (T R a x (T h b y c)) z d =
    case h of
    L -> Left (T B (T B a x b) y (T R c z d))
    B -> Left (T B (T B a x b) y (T B c z d))
    R -> Left (T B (T L a x b) y (T B c z d))

removeMaxElem :: T a (S n) -> (a, Either (T a n) (T a (S n)))
removeMaxElem (T h l x E) = case h of
                            B -> (x, Left l)
                            L -> (x, Left l)
removeMaxElem (T R E x (T B E y E)) = (y, Left (T B E x E))
removeMaxElem (T h l@(T _ _ _ _) x r@(T _ _ _ _)) =
    case removeMaxElem r of
    (z, Right r') -> (z, Right (T h l x r'))
    (z, Left r')  -> (z, balanceR' h l x r')

del :: (Ord a) => a -> T a (S n) -> Either (T a n) (T a (S n))
del x t@(T h l y r) =
    case x `compare` y of
    LT -> case l of
          E -> Right t
          T _ _ _ _ -> case del x l of
                       Right l' -> Right (T h l' y r)
                       Left l'  -> balanceL' h l' y r
    EQ -> case l of
          E -> case h of
               B -> Left r
               R -> Left r
          T _ _ _ _ -> case removeMaxElem l of
                       (z, Right l') -> Right (T h l' z r)
                       (z, Left l')  -> balanceL' h l' z r
    GT -> case r of
          E -> Right t
          T _ _ _ _ -> case del x r of
                       Right r' -> Right (T h l y r')
                       Left r'  -> balanceR' h l y r'

-----------------------------------------------------------------------------

height :: T a n -> Int
height E = 0
height (T L l _ _) = 1 + height l
height (T _ _ _ r) = 1 + height r

-----------------------------------------------------------------------------

data (Ord a) => AVLSet a = forall n. AVLSet !(T a n)

instance (Show a, Ord a) => Show (AVLSet a) where
    show (AVLSet x) = show x

emptySet :: (Ord a) => AVLSet a
emptySet = AVLSet E

insert :: (Ord a) => a -> AVLSet a -> AVLSet a
insert x (AVLSet t) =
    case ins x t of
    Left u  -> AVLSet u
    Right u -> AVLSet u

delete :: (Ord a) => a -> AVLSet a -> AVLSet a
delete x s@(AVLSet t) =
    case t of
    E -> s
    T _ _ _ _ -> case del x t of
                 Left u  -> AVLSet u
                 Right u -> AVLSet u

toList :: (Ord a) => AVLSet a -> [a]
toList (AVLSet t) = f t
    where f :: forall a n. T a n -> [a]
          f E = []
          f (T _ l x r) = f l ++ [x] ++ f r

-----------------------------------------------------------------------------

test :: [Int]
test = toList $ foldl (flip insert) emptySet (reverse [1..50] ++ [51..100])

-----------------------------------------------------------------------------