Противоречивость Хиндли-Милнера с Y-комбинатором

[MekhrubonT]

Y-комбинатор нетипизируем в HM, но авторы допустили забили на этот факт и дали тип \forall y. (y->y)->y. Этот факт делает систему HM неразрешимой, то есть из контекста Y можно доказать утверждение Bottom.

Y |- Y : \forall y. (y -> y) -> y (Тавт)              |- Id: \forall x. x -> x (Легко доказать)
Y |- Y : (a -> a) -> a (Сужение типа)                 |- Id: a -> a (Сужение типа)
                                     Y |- (Y Id) : a (Аппликация)
                                     Y |- (Y Id) : \forall a. a (Навешивание квантора) 

HM противоречив.

[artemohanjanyan]

Разве это не "противоречивостью" называется?

[artemohanjanyan]

Ещё мне кажется, что идейно это связано с парадоксом Карри, any thoughts?