using indexed Monads to make illegal DAGs underrepresentable

Dag.hs

{-# LANGUAGE FlexibleInstances, GADTs, MultiParamTypeClasses, RebindableSyntax #-}

import Data.Maybe
import Prelude (IO, putStrLn, ($), id, (.), fst, snd)


data Void

data Dag where
  Dag :: Dag' a -> Dag

data Dag' a where
  Nil  :: Dag' Void
  Cons :: [a] -> Dag' a -> Dag' (Maybe a)


class IxMonad m where
  return :: a -> m i i a
  (>>=)  :: m i j a -> (a -> m j k b) -> m i k b

newtype StateIx i j a = StateIx
  { runStateIx :: i -> (j, a) }

instance IxMonad StateIx where
  return a = StateIx $ \i -> (i, a)
  sija >>= cc = StateIx $ \i
    -> let (j, a) = runStateIx sija i
    in runStateIx (cc a) j

execStateIx :: StateIx i j a -> i -> j
execStateIx sija = fst . runStateIx sija


class Weaken i j where
  weaken :: i -> j

instance {-# OVERLAPPING #-} Weaken (Maybe i) (Maybe i) where
  weaken = id

instance Weaken i j => Weaken i (Maybe j) where
  weaken = Just . weaken


edgeTo :: Weaken i j => i -> j
edgeTo = weaken

vertex :: [i] -> StateIx (Dag' i)
                         (Dag' (Maybe i))
                         (Maybe i)
vertex edges = StateIx $ \dag'
  -> (Cons edges dag', Nothing)

dag :: StateIx (Dag' Void)
               (Dag' j)
               ()
    -> Dag
dag body = Dag (execStateIx body Nil)


infixr 0 `Cons`

example :: Dag
example = dag $ do
  e <- vertex []
  d <- vertex [edgeTo e]
  x <- vertex [edgeTo d]
  b <- vertex [edgeTo d]
  a <- vertex [edgeTo b, edgeTo x]
  return ()

@gelisam, Could I please have your thoughts on the following code.
https://gist.github.com/adithyaov/f87b5b496fd88ef91cfe438dfaf3a955
Do you think it solves the same purpose, but in a simpler manner?
Of course, the representation of the DAG is unsafe but one needn't export its constructors.
Vertices here are encoded by natural numbers.