Ваш вопрос не совсем корректен, потому что набор "всех случаев" не совсем четко определен.
Например, вы упоминаете полиморфные типы c более высокого ранга как случай, когда вывод типа Хиндли-Милнера не всегда может вывести правильный тип, что верно, за исключением того, что существуют языки, такие как Standard ML и Haskell, которые используют вывод типа Хиндли-Милнера и не имеют полиморфы высшего ранга c типов. Фактически, алгоритмы Хиндли-Милнера do работают во всех случаях, охватываемых системой типов Хиндли-Милнера; то есть система Хиндли-Милнера допускает именно те типы, которые могут быть выведены с помощью алгоритмов вывода типов Хиндли-Милнера, и поэтому явные аннотации типов никогда не требуются в этой системе.
Конечно, в реальных языках, использующих Хиндли-Милнер обычно расширяет систему различными способами по прагматическим c причинам, и некоторые из этих расширений приводят к случаям, которые алгоритм не охватывает. (Например, Standard ML имеет некоторые встроенные перегруженные идентификаторы, такие как + : real * real -> real и + : int * int -> int, что означает, что программистам иногда нужно использовать явные аннотации типов для выбора правильной перегрузки.) Но это решение проекта не необходимость; и я замечаю, что вы, во всяком случае, не упоминаете никаких языков реального мира в своем вопросе.
Но из вашего вопроса вы, похоже, хотите, чтобы хотя бы все Хиндли-Милнера плюс выше полиморфный тип c. Это означает, что вы хотите по крайней мере все Система F , лямбда-исчисление полиморфизма c. И вывод типа в Системе F, как известно, неразрешим. Это означает, что ответом на ваш вопрос является «нет»: ни один алгоритм вывода типов не может вывести правильные типы для всех случаев, которые вам нужны.