Что происходит с пропущенными переменными типа в ядре в церковном стиле?

Это немного эзотерично, но безумно. В ответе на другой вопрос я отметил, что в этой полностью валидной программе

poo :: String -> a -> a
poo _ = id

qoo :: (a -> a) -> String
qoo _ = ""

roo :: String -> String
roo = qoo . poo

переменная типа a не решается и не обобщается в процессе проверки roo. Интересно, что же происходит при переводе на язык ядра GHC, вариант System F в церковном стиле. Позвольте мне процитировать длинною в длину, с помощью явных lambdas типов /\ и приложений типов @.

poo :: forall a. [Char] -> a -> a
poo = /\ a -> \ s x -> id @ a

qoo :: forall a. (a -> a) -> [Char]
qoo = /\ a -> \ f -> [] @ Char

roo :: [Char] -> [Char]
roo = (.) @ [Char] @ (? -> ?) @ [Char] (qoo @ ?) (poo @ ?)

Что, черт возьми, происходит в местах ? ? Как roo становится действительным основным термином? Или мы действительно получаем загадочный пустой квантификатор, несмотря на то, что говорит типовая сигнатура?

roo :: forall a. [Char] -> [Char]
roo = /\ a -> ...

Я только что проверил, что

roo :: forall . String -> String
roo = qoo . poo

проходит нормально, что может означать, а может и нет, что эта штука печатает без лишних количественных характеристик.

Что там происходит?