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

まとめ

その辺の言語の型推論の仕様を比較するときはこの記事の内容を踏まえた上で発言しましょう。実用的な言語には例外（アドホックな規則）がつきものです。