31437 sjanssen {-# 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 3374442041 #haskell