what is OCaml's "ground coercion"?

Question

OCaml sometimes gives a warning "this ground coercion is not principal". I think I understand the "not principal" part (the type inference gives at least two possible types, neither of which is a subtype of the other), but I don't know what the "ground coercion" is.

I suspect the answer must involve some amount of abstract type theory, but I would much appreciate concrete examples also.

Answer 1

The answer below is from Jeremy Yallop. I cite it from the OCaml mailing list, because I failed to find an online link to the posting.

[tl;dr: the message means "The type of the expression is not known. Add type annotations for the variables in the expression."]

Background: a private type abbreviation is defined by a type alias definition with the word 'private'. For example, the following definition

type t = private int

makes t a kind of half alias for int: you can convert from type t to int, but you can't convert from int to t. Coercions are performed with the ':>' operator, so you can write things like this

let f (x : t) = (x :>  int)

to convert from the private type t to the abbreviated type int.

Now, in order to check whether the following coercion is valid

(x :> int)

the compiler needs to know the type of x. There might be several candidates: for example, with the private type abbreviation above in scope, the coercion is valid if x has type t, but do-nothing coercions are also allowed, so int is another reasonable possibility. How can the compiler choose between these alternatives to find the type of x? In the definition of f above choosing is easy: x is a function argument with an annotation, so the compiler just uses that annotation. Here's a slightly trickier case:

let g (y : t) = ()

let h x = (g x, (x :> int))

What's the type of x here? The compiler's inference algorithm checks the elements of a pair from left to right, so here's what happens:

1. Initially, when type checking for h starts, the type of x is unknown
2. The subexpression g x is checked, assigning x the type t, i.e. the type of g's argument
3. The coercion (x :> int) is checked, and determined to be correct since t can be coerced to int.

However, if the inference algorithm instead checked the elements of a pair from right to left we'd have the following sequence of steps:

Initially, when type checking for h starts, the type of x is unknown (2) The coercion (x :> int) is checked, and the compiler guesses the type of x. In the absence of other information it guesses int. (3) The subexpression g x is checked and rejected, because x has type int, not t.

Indeed, if we exchange the elements of the pair to simulate this second behaviour

let h2 x = ((x :> int), g x)

then the coercion is rejected:

let h x = ((x :> int), g x);;
                         ^
Error: This expression has type int but an expression was expected of type t

Since it's better for programs not to depend on the particular order used by the inference algorithm, the compiler emits a warning. You can address the warning by annotating the binding for x:

let h (x : t) = (g x, (x :> int))