ML系言語は型推論が得意なので基本的には型を書かなくてもコードを書けますが、状況によっては型注釈が必要になります。代表的なML系言語3つ（SML, OCaml, Haskell）について、それぞれ型注釈が必要になる（型注釈がないとコンパイルが通らない）ケースを挙げてみます。
なお、ここでは型システムのみに注目し、評価戦略はどうでもいいので、Haskellも「ML系言語」に含めています。
また、MLのモジュール／ファンクター周りは扱いません。コア言語のみを対象にします。
SML
SMLで型注釈をなくすとコンパイルが通らなくなるのは、例えば以下の例です：
- 組み込み演算子やリテラルのアドホックなオーバーロード
- レコードを受け取る関数
リテラルの例：
val x: IntInf.int = 12345678901234567890123;
(* 型注釈を剥ぐとダメ： val x = 12345678901234567890123; *)
演算子オーバーロードの例：
fun add (x : word) y = x + y;
(* 型注釈を剥ぐとダメ： fun add x y = x + y; *)
(* 型注釈がない場合は add の型は int -> int -> int になる *)
add 0w123 0w456;
レコードの例：
fun getFoo (r : {foo : 'a}) = #foo r;
(* 型注釈を剥ぐとダメ： fun proj r = #foo r; *)
print (getFoo {foo = "hoge"});
レコードの例に関しては、レコード多相があれば主要型がつけられるのでまだどうにかなりそうです。SML#なら型注釈なしでも多分大丈夫ではないでしょうか（試してない）。
OCaml
OCamlにはGADTsや多相再帰があるので、これらを使う状況では型注釈が必要です。そのほか、状況は違いますがSMLと似たようなアドホックなオーバーロードがあります。
- GADTs
- 多相再帰
- フォーマット文字列
- レコードフィールドやコンストラクターのオーバーロード
GADTsの例：
type 'a t =
| Int : int -> int t
| Bool : bool -> bool t
(* f の型注釈がないとコンパイルが通らない *)
let f : type a. a t -> int -> bool = fun t y -> match t with
| Int x -> y >= 2
| Bool x -> x
;;
多相再帰の例：
type 'a fuga =
| Leaf of 'a
| Nested of 'a list fuga
(* depth の型注釈がないとコンパイルが通らない *)
let rec depth: 'a. 'a fuga -> int = function
| Leaf _ -> 0
| Nested y -> 1 + depth y
;;
print_int (depth (Nested (Nested (Nested (Leaf [[[0]]])))));;
print_newline ();;
フォーマット文字列の例：
(* s の型注釈を消すとコンパイルできない *)
let s : (string -> string, unit, string) format = "Goodbye %s!\n";;
print_string (Format.sprintf s "world");;
レコードフィールドやコンストラクターの例：
type hoge = { foo : string; bar : int }
type piyo = { foo : int; bar : string }
let baz (x : hoge) = x.foo;; (* 型注釈がないと piyo -> int になる *)
print_string (baz { foo = "Hello world!" ; bar = 42 });;
type nyan =
| A
| B
type piyo =
| A
| C
(* f の型注釈を消すとコンパイルできない *)
let f : nyan -> string = function
| A -> "yes"
| B -> "no"
;;
Haskell
Haskellには（GHC拡張抜きでも）多相再帰があるので、その場合は当然型注釈が必要です。一方、SMLにあったようなアドホックなオーバーロードに関しては、型クラスがあるので、型推論しやすく（主要型がつくように）なっています。しかし、型クラスによって型の曖昧さが問題になるケースが起こります。
Haskellで型注釈が必要になる状況を挙げてみます。
- 多相再帰
- 型クラスの曖昧性
- monomorphism restriction
- GHC拡張を含めると、GADTsやRankNTypesやImpredicativeTypesなど
多相再帰の例
data Foo a = Leaf a
| Nested (Foo [a])
depth :: Foo a -> Int -- この型注釈がないとコンパイルエラー（多相再帰）
depth (Leaf _) = 0
depth (Nested t) = 1 + depth t
main = print (depth (Nested (Nested (Nested (Leaf [[[0]]])))))
型クラスが曖昧になる例
型クラス周りで注釈がないとエラーになるのは、以下のような状況です。
main = print (minBound :: ()) -- 型注釈がないとコンパイルエラー
なお、Haskellに限らず、他のML系言語でも型が曖昧になる状況は起こり得ます。例えば、以下のSMLコードにおいて x の型は曖昧なままです（しかし、コンパイルや実行は問題なくできます）。
(fn f => "foo") (fn x => x)
なので、「型が曖昧になる」のが問題というよりは、「型クラスのインスタンスが曖昧になる」のが問題である、と言った方が正確だと思います。
ちなみに、型クラスのインスタンスが曖昧になる状況であってもdefaulting規則があればコンパイルを通せます。上記の print minBound の例も、GHCiのように ExtendedDefaultRules 拡張が有効な状況ではコンパイル・実行できてしまいます。もちろん、実行時に意図した結果になるとは限りません。
Monomorphism restriction
Monomorphism restrictionは理論的な制約というよりは、言語デザインによる制約です。GHC拡張 NoMonomorphismRestriction をつけると無効にできます。
Monomorphism restrictionのせいで型注釈が必要な例：
f :: Show a => a -> String -- この型注釈がないとコンパイルエラー
f = show
main = do
print (f ())
print (f "")
さて、そもそもなぜ monomorphism restriction なんてものがあるのでしょうか。そのために次のコードを考えてみます。
-- 10000番目の素数を計算する
-- prime10000 :: Int
-- prime10000 :: (Integral a, Enum a) => a
prime10000 = naiveSieve [2..] !! 9999
where
-- エラトステネスの篩じゃないやつ。
-- ちなみに、だめぽラボの「Haskellで戦う競技プログラミング」では、
-- エラトステネスの篩とこのアルゴリズムの計算量の違いについて軽く考察しているので、
-- 持っている方は読んでみてください（持ってないのにこの話目的でわざわざ買うほどではないです）
naiveSieve (p:ps) = p : naiveSieve [q | q <- ps, q `rem` p /= 0]
printInt :: Int -> IO ()
printInt = print
main = do
printInt prime10000
print prime10000
このコードをmonomorphism restrictionあり、monomorphism restrictionなしの状況でそれぞれコンパイル・実行して実行時間を計ってみます。
$ stack ghc -- -O2 monorest.hs
[1 of 1] Compiling Main ( monorest.hs, monorest.o )
Linking monorest ...
$ time ./monorest
104729
104729
real 0m2.026s
user 0m1.884s
sys 0m0.035s
$ stack ghc -- -O2 -XNoMonomorphismRestriction monorest.hs
[1 of 1] Compiling Main ( monorest.hs, monorest.o ) [flags changed]
Linking monorest ...
$ time ./monorest
104729
104729
real 0m4.862s
user 0m4.614s
sys 0m0.066s
**Monomorphism restrictionが無効だと、実行時間が2倍以上になりました。**理由を考えてみましょう。
- Monomorphism restrictionが有効な場合
prime10000 の型は単相的で、 printInt に渡しているために Int となります。その後の print に渡す際も、 Int として使用されます。
print prime10000 では先に計算した prime10000 :: Int の値が使い回されるので prime10000 は1回しか計算されません。
- Monomorphism restrictionが無効な場合
prime10000 の型は prime10000 :: (Integral a, Enum a) => a となります。printInt に渡す際は a = Int となり、 print に渡す際はdefaultingにより a = Integer になります。
というわけで「10000番目の素数の計算」は printInt (prime10000 :: Int) と print (prime10000 :: Integer) で2回行われることになります。
こういう風に、monomorphism restrictionがないと変数の値が不必要に多相的になって、プログラマーの意図しない再計算が発生する可能性があります。
ちなみに、型クラスが関係しなければmonomorphism restrictionは必要ありません。
emptyList = [] -- monomorphism restriction の対象にはならない
main = do
print (emptyList :: [Char])
print (emptyList :: [Int])
GHC拡張有効時
GHC拡張を考慮すると GADTs やら RankNTypes やらがあるので、当然、型注釈が必要になります。
GADTsの例：
data Foo a where
Int :: Int -> Foo Int
Bool :: Bool -> Foo Bool
-- どちらかの型注釈がないとエラー
-- f :: Foo a -> a -> Bool
-- f :: Foo a -> Int -> Bool
f (Int x) y = y >= 2
f (Bool x) y = x
まとめ
その辺の言語の型推論の仕様を比較するときはこの記事の内容を踏まえた上で発言しましょう。実用的な言語には例外（アドホックな規則）がつきものです。