A merge sort implementation in Haskell's type system

TypeSort.hs

{-# LANGUAGE NoImplicitPrelude, UndecidableInstances, FlexibleInstances, FunctionalDependencies, UnicodeSyntax, TypeOperators, FlexibleContexts #-}
module TypeSort where

data T
data F

class (Either b l r) o | b l r → o
instance (Either T l r) l
instance (Either F l r) r

data Nil
data x ::: xs
infixr 5 :::

class (a <= b) o | a b → o

class (Merge ls rs) xs | ls rs → xs
instance (Merge Nil rs) rs
instance (Merge ls Nil) ls
instance ( (l <= r) b
         , (Merge ls (r:::rs)) ls'
         , (Merge (l:::ls) rs) rs'
         , (Either b (l:::ls') (r:::rs')) os
         ) => (Merge (l:::ls) (r:::rs)) os

class (Split xs) ls rs | xs → ls rs
instance (Split Nil) Nil Nil
instance (Split (l:::Nil)) (l:::Nil) Nil
instance ( (Split xs) ls rs
         ) => (Split (l:::r:::xs)) (l:::ls) (r:::rs)

class (MergeSort xs) os | xs → os
instance (MergeSort Nil) Nil
instance (MergeSort (a:::Nil)) (a:::Nil)
instance ( (Split (a:::b:::xs)) ls rs
         , (MergeSort ls) ls'
         , (MergeSort rs) rs'
         , (Merge ls' rs') os
         ) => (MergeSort (a:::b:::xs)) os

data A
data B
data C
data D
instance (A <= A) T; instance (B <= A) F; instance (C <= A) F; instance (D <= A) F
instance (A <= B) T; instance (B <= B) T; instance (C <= B) F; instance (D <= B) F
instance (A <= C) T; instance (B <= C) T; instance (C <= C) T; instance (D <= C) F
instance (A <= D) T; instance (B <= D) T; instance (C <= D) T; instance (D <= D) T

-- I know no better way to typecheck than this.
a :: (MergeSort
      (A:::B:::A:::D:::C:::A:::D:::B:::Nil)
      (A:::A:::A:::B:::B:::C:::D:::D:::Nil)
     ) => T; a' :: T
a = a; a' = a