deniok

Я, всё-таки, чего-то не понимаю.
Из терма мы можем извлечь информацию об арности каждой переменной.

ww - понятно, что арность w ≥1, и первый аргумент рекурсивного типа (избавляемся от рекурсии, заявляя, что там forall)
обозначим это, для краткости, звёздочкой, как с кайндами:
w :: * → wr (w-result)
ww :: wr

v yy yz - арность v ≥2, арность y ≥1 и первый аргумент рекурсивный:
y :: * → yr
yy :: yr
yz :: yr
v :: yr → yr → vr
v(yy)(yz) :: vr

\a.\b.a :: a → b → a — старый добрый const

x xv v — арность x ≥2,
x :: * → v → xr
xv :: v → xr
x xv v :: xr

const x (x xv v)
:t a = :t x
:t b = :t x xv v
обозначим тип результата :t сr = :t x = * → v → vr

(v yy yz) (\x.const...) (\w.ww)
:t vr = (* → v → vr) → (* → wr)

:t v = yr → yr → ((* → v → vr) → (* → wr))
возникла рекурсия более затейливого вида, а мы возьмём да и изведём её через forall:
:t v = yr → yr → (* → * → vr) → * → wr

чтобы в звёздочках не путаться, восстановим forall'ы
:t v = forall v. forall x. forall w. yr → yr → (x → v → vr) → w → wr

Что-то, чем больше стрелок, тем сильнее глаза разбегаются, и у меня сейчас нет сил додумать, что там в итоге получается...
ghci на мои жалкие попытки пишет что-то вида "y is rigid type..." (там, где идёт сопоставление с forall y.y)

Это и есть то самое место спотыкания системы F?