x = mon (1,(0,(0,()))) :: Polynomial Integer (Natural,(Natural,(Natural,())))
y = mon (0,(1,(0,()))) :: Polynomial Integer (Natural,(Natural,(Natural,())))
z = mon (0,(0,(1,()))) :: Polynomial Integer (Natural,(Natural,(Natural,())))

data VARS m t where
  VARZ :: VARS m ()
  VARS :: (Ord n, Show n, Monoid n) => String -> VARS m n -> VARS m (m,n)

xyz = VARS "x" $ VARS "y" $ VARS "z" $ VARZ
e123 = VARS "e1" $ VARS "e2" $ VARS "e3" $ VARZ

data EXISTS_VARS_AND_LOOKUP m where
  WITNESS :: (Show t, Ord t, Monoid t) => t -> VARS m t -> (String -> Maybe (MonoidRing m t)) -> EXISTS_VARS_AND_LOOKUP m

declare_variables :: [String] -> EXISTS_VARS_AND_LOOKUP Natural
declare_variables [] = WITNESS () VARZ (\_ -> Nothing)
declare_variables (x:xs) = case declare_variables xs of
  WITNESS t v f -> WITNESS (0,t) (VARS x v) (\x' -> if x == x'
                                                    then Just (mon (1,t))
                                                    else fmap sup (f x'))
    where
      sup :: Ord t => Polynomial Integer t -> MonoidRing Integer (Natural,t)
      sup = fromCoefficientList . map (\(x,k) -> ((0,x),k)) . coefficientList