Type level equality test

type-level-equality-test.hs

type family Delete (t :: Tree) (n :: Nat) :: Tree where
  Delete 'Empty _        = 'Empty
  Delete ('Node l c r) n = Delete' (Compare n c) ('Node l c r) n

type family Delete' (ord :: Ordering) (t :: Tree) (n :: Nat) :: Tree where
  Delete' 'LT ('Node l c r) n = 'Node (Delete l n) c r
  Delete' 'GT ('Node l c r) n = 'Node l c (Delete r n)
  Delete' 'EQ ('Node l c 'Empty) n = l
  Delete' 'EQ ('Node l c r) n = Constr l (Smallest r)

type family Constr (l :: Tree) (r :: (Nat, Tree)) :: Tree where
  Constr l '(c, r) = 'Node l c r

type family Smallest (t :: Tree) :: (Nat, Tree) where
  Smallest ('Node 'Empty c r) = '(c, r)
  Smallest ('Node l c r) = Smallest' (Smallest l) c r

type family Smallest' (l :: (Nat, Tree)) (c :: Nat) (r:: Tree) :: (Nat, Tree) where
  Smallest' '(min, l) c r = '(min, 'Node l c r)

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

data (x :: Tree) :~: (y :: Tree) where
  Refl :: x :~: x

deleteTest0 :: Delete 'Empty 'Z :~: 'Empty
deleteTest0 = Refl

deleteTest1 :: Delete (Insert 'Empty 'Z) 'Z :~: 'Empty
deleteTest1 = Refl

deleteTest2 :: Insert (Insert 'Empty 'Z) 'Z :~: Insert 'Empty 'Z
deleteTest2 = Refl

deleteTest3
   :: Insert (Insert 'Empty 'Z) ('S 'Z)
  :~: 'Node 'Empty 'Z ('Node 'Empty ('S 'Z) 'Empty)
deleteTest3 = Refl