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

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

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 "demonic bind"
(?>=) :: (IMonad m) => m a i -> (a :-> m b) -> m b i
(?>=) = flip bind

-- Conor McBride "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 отказаться от "демонической привязки", даже если он обычно будет проверять тип?

Ответ 1