--------------------------------------------------------------------------------
--                                                                            --
--  Sum and Only are used to define towers of types                           --
--                                                                            --
-------------------------------------------------------------------------------- 
-- Sum class

infix 5 <+> 

class Sum sum where
  inl :: x -> sum x y
  inr :: y -> sum x y
  (<+>) :: (x -> z) -> (y -> z) -> sum x y -> z
 
-- Only class

class Only only where
  only :: u -> only u
  ylno :: only u -> u

-- SUM data

data SUM x y = L x | R y

instance Sum SUM where
  inl = L
  inr = R
  f <+> g = \s -> case s of 
                   L x -> f x 
                   R y -> g y

-- ONLY type (avoids overlaps)

type ONLY u = u in

 oNLY :: u -> ONLY u , 
 yLNO :: ONLY u -> u 
 
oNLY = id
yLNO = id

instance Only ONLY where
  only = oNLY
  ylno = yLNO

-- Write instances

instance (Write x, Write y, Sum sum) => Write (sum x y) where
  write = write <+> write

instance (Write u, Only only) => Write (only u) where
  write = write . ylno

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