let多相と型制約と型推論
こういう（けっこう前の）記事があって面白かった：
大変面白かったのと、何故こうなるのかが微妙に理解し切れなかったのと、で少し自分でも調べてみた。
ちょっと例を簡略化すると
let f x = x in f 1, f true
は型検査を通るけど
let f x : 'a = x in f 1, f true let g (x : 'a) = x in g 1, g true
などは通らない、という話だ。
（ちなみにOCaml 4.06.1だと"Error: This expression has type bool but an expression was expected of type int"と怒られる）
'aという型「注釈」をつけた途端に型検査が通らなくなる、ように見える。
さらにいうとutopなどで
let f x = x;;
としてみるとval f : 'a -> 'a = <fun>だと言ってくる。その型と合致する注釈をつけているのに何故？
ポイントは上記の記事で@camloebaさんが言っている通り、let f x : 'a ...は型注釈ではなく型制約だという点のようだ。
つまりlet f x : 'a = ... in ...というような記述は
この
f xは'a型（パラメトリック多相）として扱ってね
という型注釈ではなく
型推論のunificationの時にとりあえず
f xには'aという型変数を振っておいてね
という型制約だということ。.mliファイルやモジュールのsignatureでval f : 'a -> 'aと指定するのとは本質的に異なる記述のようだ。
そう考えると、この制約があると
let f x : 'a = x in f 1, f true
でf 1の時点で'a = intだとunifyされて、f trueで型検査が失敗する、というのは直観的だと思う。
ではなぜこの型制約がないと型検査を通るか？
let多相と型推論についてTaPLの22.6章にこう書いてあった：
A better alternative (to allow programmers to completely omit type annotations on lambda-abstractions) is to add un-annotated abstractions to the syntax of terms and a corresponding rule to the constraint typing relation. ...
This account of un-annotated abstractions is ... more expressive, in a small but useful way: if we make copies on an un-annotated abstraction, the CT-ABS_INF (type constraint) rule will allow us to choose a different variable as the argument type of each copy. By contrast, if we regard a bare abstraction as being annotated with an invisible type variable, then making copies will yield several expressions sharing the same argument type. This difference is important for the discussion of let-polymorphism... - Benjamin Pierce, Types and Programming Languages, Chapter 22.6
そもそもlet多相を実現するためにlet x = t1 in t2という記述に対して型推論時にxに型変数を振らないでおくということらしい。ちなみに22.7章はその考えで具体的にどうlet多相を実現するかというトピック。
せっかく型推論が空気を読んで（？）letで定義される変数に型変数を振らずに解決しようとしているのに、let f x : 'a ...などとしたせいで振らざるを得なくなってしまって、その結果unificationで「int = boolになるので型検査失敗です」とエラーが出てしまう、というのが真相のようだ。
