Этот вопрос к чему относится — нужна ли статическая типизация, или к проблемам вывода типов?
Проблема вывода типов, как и проблема автоматического доказательства, очевидно, сложна и упирается в теорему Геделя и разрешимость. Но я и не говорил, что вывод типов — это вообще хорошо и нужно.
Вывод типов — это когда программист написал хрень, а компилятор разбирается. Очевидно, он не всегда может разобраться, это нормально (даже по теоретическим причинам). Если компилятор не смог вывести тип, так как либо столкнулся с фундаментальной теоретической проблемой, либо слишком сложно, либо задача в принципе подразумевает полиморфизм времени исполнения, тут два варианта, конечно: предложить программисту указать типы явно, то есть разобраться самому с тем, что он написал, либо молча подставить динамический тип, который, кстати, является статическим вариантным типом.
Динамическая типизация — это частный случай статической, с одним вариантным типом.
Мне кажется странным по умолчанию использовать динамическую типизацию, так как это, по меньшей мере, неэффективно. Лучше уж по умолчанию использовать статическую, а если проблемы — делать fallback к динамической.
Про нужность вывода типов: программист, написавший код, что-то все равно имеет в виду, какой-то тип, иначе что это за бессмыслица, это же не "непонятно какие" манипуляции над "непонятно чем"? Так чтобы не путать коллег, читающих код, почему бы не указать явно, что ты имел в виду? Что за игра в прятки? Если машина в твоем коде не может разобраться, то что должен делать твой коллега?
