> 1. В ML'ях хотя бы было такое свойство: программа либо вообще не
> компилируется, либо имеет одну главную типизацию, из которой все остальные выводятся
> как частные случаи. Классы типов рушат это свойство, и программа может
> перестать работать (но продолжать компилироваться), если стереть аннотации типов.

Не. Классы типов, если нормально написаны, это свойство практически не рушат. Кроме того, я совершенно не уверен, что отсутствие аннотаций типов вот так уж и хорошо. См. исходники компилятора Ocaml'а - там же без поллитра вообще не разберёшься.

> 2. типа
> ну ладно, пусть так

Ну да, примерно так.

> 3. я не про exceptions, я про то, что программа не компилируется
> из-за неправильных типов, но ошибка выдается не там, где она есть,
> а где-то глубоко внутри функции, которая сама-то правильная, но типы явно
> не прописаны.

Это я описал практический приём отладки вот таких проблем. В Хаскеле ставится заглушка undefined, дальше компилируется. В ocaml'е вместо неё можно ставить failwith "unimplemented"; кроме того, ставятся аннотации типов там, где нужно. После этого всё сводится, а главное - работает.