When is double coercion useful?

Question

I stumbled upon the following compilation message in OCaml:

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

It happened in a fairly complicated source code, but here is a 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 happens on the last line, where the OCaml compiler complains that f_link can not be converted to type tfull.

Can someone explain to me why it is not possible to coerce f_link to tfull directly, but it is possible to coerce it to tfull indirectly using tphrasing as a mid step?

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

Answer 1

The general coercion operator, also known as a double coersion, has a form

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

The <subtype> type can be sometimes omitted, in that case it is called a single coercion. So in your case, the correct coercion should look like this:

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

where f_link_type is a type of the f_link function.

The reason why it may fail is described in the manual:

The former operator will sometimes fail to coerce an expression expr from a type typ1 to a type typ2 even if type typ1 is a subtype of type typ2: in the current implementation it only expands two levels of type abbreviations containing objects and/or polymorphic variants, keeping only recursion when it is explicit in the class type (for objects). As an exception to the above algorithm, if both the inferred type of expr and typ are ground (i.e. do not contain type variables), the former operator behaves as the latter one, taking the inferred type of expr as typ1. In case of failure with the former operator, the latter one should be used.

Let me try to put it into more simple terms. The coercion is only possible if both a domain and a codomain are known. However, in many cases, you can apply a heuristic that will infer the domain from the codomain and current type of expression. This heuristic works if the type of expression is ground, has no recursions, and some other restrictions. Basically, if the domain type has no unique most general type we need to enumerate all possible generalizations and check every possible combination.