Rebinding do notation for indexed monads

I was following Conor McBride's "Kleisli arrows of outrageous fortune" paper and I've posted my implementation of his code here. Briefly, he defines the following types and classes:

type a :-> b = forall i . a i -> b i

class IFunctor f where imap :: (a :-> b) -> (f a :-> f b)

class (IFunctor m) => IMonad m where
    skip :: a :-> m a
    bind :: (a :-> m b) -> (m a :-> m b)

data (a := i) j where
    V :: a -> (a := i) i

Then he defines two types of binds, the latter of which uses (:=) to restrict the initial index:

-- Conor McBride's "demonic bind"
(?>=) :: (IMonad m) => m a i -> (a :-> m b) -> m b i
(?>=) = flip bind

-- Conor McBride's "angelic bind"   
(>>=) :: (IMonad m) => m (a := j) i -> (a -> m b j) -> m b i
m >>= f = bind (\(V a) -> f a) m

The latter bind works perfectly fine for rebinding do notation to use indexed monads with the RebindableSyntax extension, using the following corresponding definitions for return and fail:

return :: (IMonad m) => a -> m (a := i) i
return = skip . V

fail :: String -> m a i
fail = error

... but the problem is that I cannot get the former bind (i.e. (?>=)) to work. I tried instead defining (>>=) and return to be:

(>>=) :: (IMonad m) => m a i -> (a :-> m b) -> m b i
(>>=) = (?>=)

return :: (IMonad m) => a :-> m a
return = skip

Then I created a data type guaranteed to inhabit a specific index:

data Unit a where
    Unit :: Unit ()

But when I try to rebind do notation using the new definitions for (>>=) and return, it does not work, as demonstrated in the following example:

-- Without do notation
test1 = skip Unit >>= \Unit -> skip Unit

-- With do notation
test2 = do
    Unit <- skip Unit
    skip Unit

test1 type-checks, but test2 does not, which is weird, since I thought all that RebindableSyntax did was let do notation desugar test2 to test1, so if test1 type-checks, then why does not test2? The error I get is:

Couldn't match expected type `t0 -> t1'
            with actual type `a0 :-> m0 b0'
Expected type: m0 a0 i0 -> (t0 -> t1) -> m Unit ()
  Actual type: m0 a0 i0 -> (a0 :-> m0 b0) -> m0 b0 i0
In a stmt of a 'do' block: Unit <- skip Unit
In the expression:
  do { Unit <- skip Unit;
       skip Unit }

The error remains even when I use the explicit forall syntax instead of the :-> type operator.

Now, I know there is another problem with using the "demonic bind", which is that you can't define (>>), but I still wanted to see how far I could go with it. Can anybody explain why I cannot get GHC to desugar the "demonic bind", even when it would normally type-check?