>>579
> [U >: Int](U)U ⊇ (Int)Int が成り立つか、という話になります(Uはメソッド
> 適用までインスタンス化されない点が重要です)。で、おそらくおわかりかと思う
> のですが、これは成り立ちません(リスコフの置換原則を思い出してください)。

なるほど。齟齬の原因が判った。

(a) [U >: Int] (U)U で表現可能な関数型の集合には(Int)Intを含む
(b) [U >: Int] (U)U で表現可能な関数型の集合には(Int)Intを受理しないものがある
は両方とも真。
俺は(a)を指して [U >: Int] (U)U ⊇ (Int)Int が成り立つと言っているのだが、
◆CgacaMDhSQさんは(b)を指して [U >: Int] (U)U ⊇ (Int)Int が
成り立たないと書いているらしい。つまり、[U >: Int] (U)U は (Int)Int の
Liskov substituion principleにおけるsubtypeではないことを書いているのだろう。

それには異論無し。
俺ならtype orderを表す時は⊇でなく≧を使うので、混乱した。申し訳ない。

齟齬が生じた原因は、想定した型推論のアプローチの違いだろう。

俺が想定していたのは、Cartesian Product Algorithm (CPA)のような、解候補集合の
うち制約充足解を選び出すconstraint-based analysisの方。だから、解は多数の
型の集合の中から制約で1つに絞れればいい。なので、(a)でＯＫという立場。

◆CgacaMDhSQさんはprincipal typeをunification-basedで求めたいので、
（ひとつの）解候補が無矛盾かどうかが興味の対象だと推測する。
だから、(b)なのでダメという立場。（正しい？）

ちなみに、constraint-based analysisアプローチは、
Demand-Driven Analysis with Goal Pruning (DDP)の提案者が
現在Scalaに適用チャレンジ中とのこと。
それ以上は知らないので、詳しい人がいたら教えてほしい。