deniok

Если говорить очень грубо, то здесь возникает система неравенств на типы, в отличие от обычного Хиндли-Милнера, где мы имеем дело с системой уравнений. В последнем случае мы дальше делаем унификацию по Робинсону и все чики. А для неравенств дело дрянь. Джо Уэллс показал, что эта задача с помощью специальной тета-редукции сводится к SUP (Semiunification Problem), которая неразрешима. То есть ручками, конечно, можно терм перебирать, но важно понимать, что, даже составив правильную систему неравенств, мы не имеем универсального механизма решения.