Ввод комбинатора Y

http://muaddibspace.blogspot.com/2008/01/type-inference-for-simply-typed-lambda.html - это краткое определение просто типизированное лямбда-исчисление в Прологе.

Это выглядит нормально, но затем он претендует на присвоение типа комбинатору Y ... тогда как в самом реальном смысле вся цель добавления типов в лямбда-исчисление состоит в том, чтобы отказаться от присвоения тип для таких вещей, как комбинатор Y.

Может ли кто-нибудь точно увидеть, где его ошибка или, что более вероятно, мое недоразумение?