Это действительно невозможно, по крайней мере, в общем случае, когда m может быть произвольной монадой.
Предположим, что монада m является продолжением монады (- -> r) -> r. (Я опускаю оболочку newtype для ясности).
Тогда вам нужен способ конвертации (a -> b) -> b в (a -> (b -> r) -> r) -> (b -> r) -> r. Другими словами, вам нужен термин полиморф c типа
t :: ((a -> b) -> b) -> (a -> (b -> r) -> r) -> (b -> r) -> r
Мы докажем, что t не может существовать из-за противоречия. Предположим, что такой t существует. Мы можем специализировать его, выбрав r~a и b~Void (пустой тип).
t :: ((a -> Void) -> Void) -> (a -> (Void -> a) -> a) -> (Void -> a) -> a
Теперь вспомним, что у нас есть (всего!) Функция absurd :: Void -> a (по сути, absurd x = case x of {}). Затем мы получим
\ x -> t x (\y _ -> y) absurd
:: ((a -> Void) -> Void) -> a
По изоморфизму Карри-Говарда следующее будет логической тавтологией в интуиции c logi c:
((A -> False) -> False) -> A
Но приведенная выше формула имеет вид Not (Not A) -> A, т. Е. Исключение двойного отрицания, которое, как известно, невозможно доказать в интуиции c logi c. Следовательно, мы получаем противоречие, и мы должны заключить, что нет термина t этого типа.
Обратите внимание, что t может существовать для других монад m.