Могу ли я реализовать гетерогенный список, основанный на экзистенциале с кодировкой Черча и типами Rank-N?

Question

В моей попытке понять экзистенциальные типы, я прочитал, что кодирования Черча вместе с расширением Rank-N-types будет достаточно, чтобы кодировать их в Haskell без экзистенциального количественного определения. Я нашел этот простой пример:

type Obj = forall y. (forall x. (Show x) => x -> y) -> y

obj :: Obj
obj f = f "hello"

app :: Obj -> String
app obj = obj (\x -> show x)

В Haskell Wiki я наткнулся на следующий пример гетерогенного списка, основанного на экзистенциальном типе:

data Obj = forall a. (Show a) => Obj a

xs :: [Obj]
xs = [Obj 1, Obj "foo", Obj 'c']

doShow :: [Obj] -> String
doShow [] = ""
doShow ((Obj x):xs) = show x ++ doShow xs

Теперь я попытался выразить эту реализацию с помощью Church и потерпел неудачу с ошибкой недопустимого полиморфного типа:

type Obj = forall y. (forall x. (Show x) => x -> y) -> y 

obj1 :: Obj 
obj1 f = f 1 

obj2 :: Obj 
obj2 f = f "foo" 

obj3 :: Obj 
obj3 f = f 'c' 

xs :: [Obj] 
xs = [obj1, obj2, obj3]

doShow :: [Obj] -> String 
doShow [] = "" 
doShow (obj:xs) = obj (\x -> show x ++ doShow xs)

Я думаю, что этот перевод довольно схематичен и просто неверен. Правильно ли, что экзистенциальные типы могут быть закодированы с помощью Church/Rank-N? Как это сделано правильно?