When is double coercion useful?

Question

I came across the following compilation post in OCaml:

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

This happened in a rather complicated source code, but here is MNWE:

 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) 

You can compile this example with ocamlfind ocamlc -c -package eliom.server -thread test.ml with Eliom 6 installed.

The error is in the last line, where the OCaml compiler complains that f_link cannot be converted to tfull type.

Can someone explain to me why you cannot directly force f_link to tfull , but you can indirectly use its tfull , using tphrasing as an average step?

Any pointer to the type theory behind it would also be welcome.

Answer 1

The general coercion operator, also known as double match, has the form

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

The <subtype> type can sometimes be omitted, in which case it is called one coercion. Therefore, in your case, the correct enforcement should look like this:

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

where f_link_type is the type of the f_link function.

The reason this can happen is described in the manual :

The former statement sometimes cannot force the expression expr from type typ1 to type typ2, even if type typ1 is a subtype of type typ2: in the current implementation, it only extends two levels of the abbreviation type containing objects and / or polymorphic variants, preserving only recursion when it is explicit in class type (for objects). As an exception to the above algorithm, if both the alleged type of the expression and the type are terrestrial (i.e., do not contain type variables), the first operator behaves like the last, taking the proposed type of expression as typ1. In case of failure with the former operator, the latter should be used.

Let me try to bring it to simpler words. Coercion is possible only if both the domain and the code are known. However, in many cases, you can apply a heuristic that will infer the domain from the codename and the current type of expression. This heuristic works if the type of expression is based on the earth, has no recursions and some other restrictions. In principle, if the domain type does not have a unique most general type, we need to list all possible generalizations and check all possible combinations.