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

[Martin DeMello <martindemello@gmail.com>]

Thanks, that explained everything very nicely!

I'm still curious about where the term "ground coercion" came from,
but I understand what the warning is saying now.

martin

On Wed, Feb 25, 2015 at 2:38 AM, Jeremy Yallop <yallop@gmail.com> wrote:
> 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.