Пересвязываем do обозначения для индексированных монад

Я следил за работой Конора МакБрайда «Стрелы безумного счастья Кляйсли», и я разместил свою реализацию его кода здесь . Вкратце, он определяет следующие типы и классы:

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

Затем он определяет два типа привязок, последний из которых использует (:=) для ограничения начального индекса:

-- 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

Последнее связывание прекрасно работает для повторного связывания нотации do для использования индексированных монад с расширением RebindableSyntax, используя следующие соответствующие определения для return и fail:

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

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

... но проблема в том, что я не могу заставить работать прежнюю привязку (т.е. (?>=)). Вместо этого я попытался определить (>>=) и return:

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

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

Затем я создал тип данных, который гарантированно будет содержать определенный индекс:

data Unit a where
    Unit :: Unit ()

Но когда я пытаюсь Пересвязать нотацию do, используя новые определения для (>>=) и return, она не работает, как показано в следующем примере:

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

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

test1 проверки типов, но test2 не, что странно, так как я думал, что все, что сделал RebindableSyntax, было позволено do обозначения desugar test2 - test1, так что если test1 проверяет тип, то почему нет test2? Я получаю следующую ошибку:

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 }

Ошибка сохраняется даже тогда, когда я использую явный синтаксис forall вместо оператора типа :->.

Теперь я знаю, что есть еще одна проблема с использованием «демонической привязки», которая заключается в том, что вы не можете определить (>>), но я все еще хотел посмотреть, как далеко я смогу пойти с этим. Кто-нибудь может объяснить, почему я не могу заставить GHC десугарировать «демоническое связывание», даже когда оно обычно проверяет тип?