Re: [Caml-list] "this ground coercion is not principal"

[Jeremy Yallop <yallop@gmail.com>]

On 25 February 2015 at 04:47, Martin DeMello <martindemello@gmail.com> wrote:
> What does this warning mean?

[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:

  (1) 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))

Jeremy.