Ошибки типов с экзистенциальными типами в Haskell

Я борюсь с экзистенциальными типами в своей программе. Мне кажется, что я пытаюсь сделать что-то очень разумное, но я не могу пройти проверку типов: (

У меня есть тип данных, который как бы имитирует монаду

data M o = R o | forall o1. B (o1 -> M o) (M o1)

Теперь я создаю для него Context, подобный описанному в статье Haskell Wiki о Zipper, однако для простоты я использую функцию вместо структуры данных -

type C o1 o2 = M o1 -> M o2

Теперь, когда я пытаюсь написать функцию, которая разбивает значение данных на его контекст и подзначение, проверка типов выдает ошибку -

ctx :: M o -> (M o1 -> M o, M o1)
ctx (B f m) = (B f, m) -- Doesn't typecheck

Ошибка -

Couldn't match type `o2' with `o1'
  `o2' is a rigid type variable bound by
       a pattern with constructor
         B :: forall o o1. (o1 -> M o) -> M o1 -> M o,
       in an equation for `ctx'
       at delme1.hs:6:6
  `o1' is a rigid type variable bound by
       the type signature for ctx :: M o -> (M o1 -> M o, M o1)
       at delme1.hs:6:1
Expected type: M o2
  Actual type: M o1
In the expression: m
In the expression: (B f, m)

Однако, я могу обойти ее следующим образом -

ctx (B f m) = let (c,m') = ctx m in ((B f) . c, m') -- OK

Почему второе определение проверяется, а первое нет?

Также, если я пытаюсь преобразовать ctx в полную функцию, проверяя R, я снова получаю ошибку типовой проверки -

ctx (R o) = (id, R o) -- Doesn't typecheck

Ошибка -

Couldn't match type `o' with `o1'
  `o' is a rigid type variable bound by
      the type signature for ctx :: M o -> (M o1 -> M o, M o1)
      at delme1.hs:7:1
  `o1' is a rigid type variable bound by
       the type signature for ctx :: M o -> (M o1 -> M o, M o1)
       at delme1.hs:7:1
In the first argument of `R', namely `o'
In the expression: R o
In the expression: (id, R o)

Как я могу обойти эту ошибку?

Любая помощь приветствуется!