単一化で人間の気持ちが失われるんだ！というサビシイ話

OCaml 演習とかやってひぃひぃ言っている人対象ですぅ。わからない人にはわかるように書いていませんから、「さっぱりわからない」とか呟く前にスルー推奨です

type t = int list list list

let x : t = [[[1]]]
let y = x @ x

をコンパイルすると、 x は t だが y の型は int list list list とレポートされる。これが残念だって話。だって明らかに t でしょ？
これはもちろん単一化アルゴリズムの気持ちになれば明らかに、明らかではないのだが…

それに、じゃあ x @ x の型が t としてレポートされるべきかというと、そうではないわな。

type kg = float
type m = float (* メーテル *)
let bmi (w : kg) (h : m) = w /. (h *. h)

としたときに bmi の戻り値が kg (もしくは m) になっていて欲しいですかあなたは？

あなたが単一化アルゴリズムの気持ちになれているかどうかは、

let z = [x] @ [x]

の型が int list list list list ではなく t list としてレポートできるのは何故か、で、なぜそれは bmi の例とちがっておかしさがないか、考えるといいですぅ。

どーしてもこれが嫌なら、

type t = Foo of int list list list

として別の型にせにゃならん、がもちろん (@) はそのままでは使えなくなる。

はっ！今気づいた。ようするに、あれだ。 (@) : 'a list -> 'a list -> 'a list は 'a は全部同じことを保証しているが、三つの 'a list が同じであることを保証していない。（いや、同じ型だよ、でも bmi の例と同じく、人間の気持ち的には同じ意味じゃないかもしれないよね？) だから、人間の気持ちを導入してやればよろしい:

let (@!) : ('a list as 'b) -> 'b -> 'b = (@)
let y = x @! x

はいできました。 y の型は t になるよ。

ようするに、機械の体は人間の気持ちを推論してくれないのだ。メーテル、サビシイね、と鉄郎は思った。