二重強制はいつ便利ですか？

Question

私はOCamlの中に次のコンパイルメッセージつまずい：それはかなり複雑なソースコードで起こったが、ここではMNWEある

This simple coercion was not fully general. Consider using a double coercion. 

：

open Eliom_content.Html.D 

let f_link s = 
    let arg : Html_types.phrasing_without_interactive elt list = [pcdata "test"] in 
    [ Raw.a ~a:[a_href (uri_of_string (fun() -> "test.com"))] arg ] 

type tfull = (string -> Html_types.flow5 elt list) 
type tphrasing = (string -> Html_types.phrasing elt list) 

let a : tfull = ((f_link :> tphrasing) :> tfull) 

let b : tfull = (f_link :> tfull) 

あなたがして、ocamlfind ocamlc -c -package eliom.server -thread test.mlでこの例をコンパイルすることができますEliom 6がインストールされています。

最後の行でエラーが発生します。ここでは、f_linkをtfullに変換できないというOCamlコンパイラの不満があります。

直接tfullにf_linkを強制することはできませんなぜ誰かが私に説明しますが、半ばステップとしてtphrasingを使用して間接的にtfullにそれを強制する可能であることはできますか？

それの背後にある型理論へのポインタも歓迎されます。

Answer 1

二重coersionとして知られている一般的な強制オペレータは、<subtype>タイプその場合、それは単一の強制と呼ばれ、時にはを省略することができる形態

(<exp> : <subtype> :> <type>) 

を有しています。だからあなたの場合には、正しい強制は次のようになります。

let a : tfull = (f_link : f_link_type :> tfull) 

f_link_typeがf_link関数の型です。

それはthe manualに記載されて失敗することがあり理由：

タイプTYP1タイプのサブタイプであっても、前者オペレータが時々タイプTYP2にタイプTYP1から exprの発現を強制するために失敗します typ2：現在の実装では、 型の2つのレベルのオブジェクトおよび/または多相バリアントが含まれており、クラスタイプ（オブジェクトの場合）で明示的に再帰するだけです。 上記アルゴリズムの例外として、expr とtypの推定型の両方がグラウンド（すなわち型変数を含まない）である場合、前者の 演算子はexpr の型をtyp1とし、後者のように動作します。前者のオペレータに障害が発生した場合は、後者のオペレータ を使用する必要があります。

もっと簡単な言葉で言えばよろしいですか？強制は、ドメインとコードドメインの両方がわかっている場合にのみ可能です。ただし、多くの場合、ドメインを推論するヒューリスティックをコドモインと現在のタイプの式から適用することができます。このヒューリスティックは、式のタイプが粉砕され、再帰がなく、その他の制限がある場合に機能します。基本的に、ドメインタイプに固有の最も一般的なタイプがない場合は、すべての可能な一般化を列挙し、すべての可能な組み合わせをチェックする必要があります。