オーバーロードが解決されるルール？

どうもこんばんは。G'Camlの路上販売を試みたものの巨大資本の前に敗れ去り、港*1で海を眺めているYTです。

型レの発表内容について、id:camlspotterさんに補足いただきました。ありがたや。
Obj.magic(またはassert false)を使わないで済む構造など、非常に参考になります。

で、型レでlimitationsとして、次のようなis_same_typeの各引数に同じ型を与えた場合、int -> intは'b -> 'cにもマッチするためオーバーロードが解決されずtrue_tが得られないみたいな話をしたのでした。

val is_same_type: [| 'a -> 'a -> true_t | 'b -> 'c -> false_t |]

それに対して、このような反論？がなされてます。

さて、型が同じかどうか判定できないのではないかという話があったけれども、これは、マァ出来る、という主張をしておきたい
(中略)
これは GCaml の変態的 overload resolution priority のおかげ。Overload resolution しなくちゃいけないけど、複数のケースがマッチするときは、先に宣言された方を勝手に GCaml が選んでくれる。正直キモいが、便利な時もある。とういう訳で、型が同じかどうか、というか、 unifiable かどうかは、GCaml では expansive let による auto overload resolution を使えば可能、ということです:

確かに上が優先というのはk.inabaさんの資料の内容とも一致します。
しかし現実にis_same_typeはオーバーロードが解決されない。例示されたTComp.compareと、is_same_typeの何が違うのかイマイチわからなかったので、色々実験してみました。

# module TypeLevel:
    sig
      type ('a, 'b) cons
      type nil
    end =
  struct
    type ('a, 'b) cons = unit
    type nil = unit
  end;;
module TypeLevel : sig type ('a, 'b) cons type nil end
# open TypeLevel;;
# type true_t = (nil, nil) cons;;
type true_t = (TypeLevel.nil, TypeLevel.nil) TypeLevel.cons
# type false_t = nil;;
type false_t = TypeLevel.nil
(* 型レで上手くいかないと言った形 *)
# let is_same_type = generic
                     | : 'a -> 'a -> true_t => fun _ _ -> assert false
                     | : 'b -> 'c -> false_t => fun _ _ -> assert false;;
val is_same_type : [| 'a -> 'a -> true_t | 'b -> 'c -> false_t |] = <generic>
# lazy (is_same_type 1 2);;
- : { int -> int -> 'd < [| 'a -> 'a -> true_t | 'b -> 'c -> false_t |] } =>
      'd lazy_t
= <generic>
(* refを付けてみた *)
# let is_same_type2 = generic
                    | : 'a -> 'a -> true_t ref => fun _ _ -> assert false
                    | : 'b -> 'c -> false_t ref => fun _ _ -> assert false;;
val is_same_type2 : [| 'a -> 'a -> true_t ref | 'b -> 'c -> false_t ref |] =
  <generic>
# lazy (is_same_type2 1 2);;
- : true_t ref lazy_t = <lazy>
(* listを付けてみた *)
# let is_same_type3 = generic
                    | : 'a -> 'a -> true_t list => fun _ _ -> assert false
                    | : 'b -> 'c -> false_t list => fun _ _ -> assert false;;
val is_same_type3 : [| 'a -> 'a -> true_t list | 'b -> 'c -> false_t list |] =
  <generic>
# lazy (is_same_type3 1 2);;
- : { int -> int -> 'd list < [| 'a -> 'a -> true_t list
                               | 'b -> 'c -> false_t list |] } =>
      'd list lazy_t
= <generic>
(* 抽象型を付けてみた *)
# module T: sig type 'a t end = struct type 'a t = unit end;;
module T : sig type 'a t end
# let is_same_type4 = generic
                    | : 'a -> 'a -> true_t T.t => fun _ _ -> assert false
                    | : 'b -> 'c -> false_t T.t => fun _ _ -> assert false;;
val is_same_type4 : [| 'a -> 'a -> true_t T.t | 'b -> 'c -> false_t T.t |] =
  <generic>
# lazy (is_same_type4 1 2);;
- : true_t T.t lazy_t = <lazy>

結果、生の型とlistはオーバーロードが解決されない。ref(レコード)と抽象型はオーバーロードが解決される。
例示されたTComp.compareは、全体を抽象型tでラップ(と言うのでしょうか。抽象型tの型パラメータとしている)しているためオーバーロードが解決されるようです。
……なんだこれはああああ。
結論、よくわかりませんが抽象型の型パラメータにすることで上優先ルールが働き型の同値判定は可能。Lokiに追いつく道が開けましたバンザイ。

*1:G'CamlのMacPorts用野良Portfile書きましたのでよろしければご利用ください。