>>611
> ◆CgacaMDhSQさんは(b)を指して [U >: Int] (U)U ⊇ (Int)Int が
> 成り立たないと書いているらしい。つまり、[U >: Int] (U)U は (Int)Int の
> Liskov substituion principleにおけるsubtypeではないことを書いているのだろう。はい。その通りです。
はい。それを意図していました。

> 俺ならtype orderを表す時は⊇でなく≧を使うので、混乱した。申し訳ない。
あー。なるほど。なんで、⊇使うんだろ…とか思いつつ、議論進めてたのがまずかったですね。
こちらも、その辺りについては意識を合わせておくべきでした。

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

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

正しいです。まさにprincipal typeを(unification-basedなアプローチで)求めようとすると、
Scalaの型システムだと死ねる、というのが私の言いたかったことです。

> ちなみに、constraint-based analysisアプローチは、
> Demand-Driven Analysis with Goal Pruning (DDP)の提案者が
> 現在Scalaに適用チャレンジ中とのこと。

おお。それは興味深い情報です。ちょっと調べてみます。

ところで、今更なんですが、その辺りのバックグラウンドをお持ちであったわけですし、
それを最初に明かしていただけたら、議論に齟齬が生じにくくて良かったと思います。
初学者の方が相手なのか、私などの門外漢よりも詳しい方 (:- が相手なのかによって
説明の仕方も自ずと異なってくると思いますし。