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.
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 typetyp1
to a typetyp2
even if typetyp1
is a subtype of typetyp2
: 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 ofexpr
andtyp
are ground (i.e. do not contain type variables), the former operator behaves as the latter one, taking the inferred type ofexpr
astyp1
. 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.
If you love us? You can donate to us via Paypal or buy me a coffee so we can maintain and grow! Thank you!
Donate Us With