{-# OPTIONS_GHC -fglasgow-exts -fallow-undecidable-instances #-}

newtype Succ a = Succ a
data Zero = Zero

class IfLess x y a b r | x y a b -> r
instance (IfLess x y a b r) => IfLess (Succ x) (Succ y) a b r
instance IfLess Zero (Succ y) a b a
instance IfLess (Succ x) Zero a b b
instance IfLess Zero Zero a b b

data Branch l m r = Branch l m r
data Leaf = Leaf

class Insert t x u | t x -> u
instance Insert Leaf x (Branch Leaf x Leaf)
instance (Insert l x l', Insert r x r', IfLess x m (Branch l' m r) (Branch l m r') u) => Insert (Branch l m r) x u

insert :: (Insert t x u) => t -> x -> u
insert = undefined

-- tests:
t1 :: Branch Leaf (Succ (Succ Zero)) Leaf
t1 = insert Leaf (Succ (Succ Zero))
t2 :: Branch (Branch Leaf (Succ Zero) Leaf) (Succ (Succ Zero)) Leaf
t2 = insert t1 (Succ Zero)
t3 :: Branch (Branch Leaf (Succ Zero) Leaf)
       (Succ (Succ Zero))
       (Branch Leaf (Succ (Succ (Succ (Succ Zero)))) Leaf)
t3 = insert t2 $ Succ $ Succ $ Succ $ Succ Zero
t4 :: Branch (Branch (Branch Leaf Zero Leaf) (Succ Zero) Leaf)
       (Succ (Succ Zero))
       (Branch Leaf (Succ (Succ (Succ (Succ Zero)))) Leaf)
t4 = insert t3 $ Zero
t5 :: Branch (Branch (Branch Leaf Zero Leaf) (Succ Zero) Leaf)
       (Succ (Succ Zero))
       (Branch (Branch Leaf (Succ (Succ (Succ Zero))) Leaf)
	       (Succ (Succ (Succ (Succ Zero))))
	       Leaf)
t5 = insert t4 $ Succ $ Succ $ Succ $ Zero