prooving invariant of balanced search trees in Haskell

the Haskell type system is very powerful compared to the industrial programming languages; a nice demonstration of this is its ability to represent and maintain the invariants of balanced search trees [AVL, red-black]; and the Haskell code is not even longer [or much messier] than the Agda version [Agda is a real dependently typed language, the most popular one currently]