>>370 >>372

(fn (id : 'a -> 'a) => (id 123, id "abc")
では上記全体で'aは同一だが
let id : 'a -> 'a = fn x => x in (id 123, id "abc") end;;
では、id 123 での 'a と id "abc" での 'a は別物。

これは別に奇妙な事でも何でもなくて、
letが局所定義のための表現式だということさえわかっていれば
fun id x:'a = x ;;
(id 123, id "abc")
がエラーにならないのと同様に
エラーとなるべきではないことぐらい簡単にわかるはず。
で、これのどこがMLの型推論の不完全さを示してるわけ？

あと、>>372は
>意味的には
なんて言ってるけど、どういう意味で「意味的には」なわけ？
一方は局所変数の束縛、もう一方はラムダ束縛。全然違うじゃん。