Здравствуйте, <Аноним>, Вы писали:

А> А что, разве не так?

Не так.

А> Вместо одной аксиомы для типа 'a -> 'b нужен набор аксиом для n-арных функций.

Нет тут никаких проблем. Вывод типов усложняется перегрузкой и приведением типов. Но к карингу это отношения не имеет. К тому же есть системы обеспечивающие вывод типов и при этих препятсвиях.