From mboxrd@z Thu Jan 1 00:00:00 1970 Return-Path: X-Original-To: caml-list@sympa.inria.fr Delivered-To: caml-list@sympa.inria.fr Received: from mail2-relais-roc.national.inria.fr (mail2-relais-roc.national.inria.fr [192.134.164.83]) by sympa.inria.fr (Postfix) with ESMTPS id ED9BF7EF10 for ; Wed, 25 Feb 2015 22:35:50 +0100 (CET) Received-SPF: None (mail2-smtp-roc.national.inria.fr: no sender authenticity information available from domain of martindemello@gmail.com) identity=pra; client-ip=209.85.160.182; receiver=mail2-smtp-roc.national.inria.fr; envelope-from="martindemello@gmail.com"; x-sender="martindemello@gmail.com"; x-conformance=sidf_compatible Received-SPF: Pass (mail2-smtp-roc.national.inria.fr: domain of martindemello@gmail.com designates 209.85.160.182 as permitted sender) identity=mailfrom; client-ip=209.85.160.182; receiver=mail2-smtp-roc.national.inria.fr; envelope-from="martindemello@gmail.com"; x-sender="martindemello@gmail.com"; x-conformance=sidf_compatible; x-record-type="v=spf1" Received-SPF: None (mail2-smtp-roc.national.inria.fr: no sender authenticity information available from domain of postmaster@mail-yk0-f182.google.com) identity=helo; client-ip=209.85.160.182; receiver=mail2-smtp-roc.national.inria.fr; envelope-from="martindemello@gmail.com"; x-sender="postmaster@mail-yk0-f182.google.com"; x-conformance=sidf_compatible X-IronPort-Anti-Spam-Filtered: true X-IronPort-Anti-Spam-Result: A0CjAgDGPu5UlLagVdFbhCIMBIMFxgsCgSMHQwEBAQEBARABAQEBBwsLCRIwhBABAQQSER0BGx0BAwwGBQsNAgImAgIhAQERAQUBHAYTIod4AQMRsE0+MYsugWuCd444ChknDVSEZAEBAQEBBQEBAQEBARYBBQ6BE4lygkSCKgeCaIFDBYpOiwSCCYFGjTeEPRIjgQwJhDEdMYJDAQEB X-IPAS-Result: A0CjAgDGPu5UlLagVdFbhCIMBIMFxgsCgSMHQwEBAQEBARABAQEBBwsLCRIwhBABAQQSER0BGx0BAwwGBQsNAgImAgIhAQERAQUBHAYTIod4AQMRsE0+MYsugWuCd444ChknDVSEZAEBAQEBBQEBAQEBARYBBQ6BE4lygkSCKgeCaIFDBYpOiwSCCYFGjTeEPRIjgQwJhDEdMYJDAQEB X-IronPort-AV: E=Sophos;i="5.09,647,1418079600"; d="scan'208";a="123409930" Received: from mail-yk0-f182.google.com ([209.85.160.182]) by mail2-smtp-roc.national.inria.fr with ESMTP/TLS/RC4-SHA; 25 Feb 2015 22:35:50 +0100 Received: by ykp9 with SMTP id 9so2198389ykp.10 for ; Wed, 25 Feb 2015 13:35:49 -0800 (PST) DKIM-Signature: v=1; a=rsa-sha256; c=relaxed/relaxed; d=gmail.com; s=20120113; h=mime-version:in-reply-to:references:date:message-id:subject:from:to :cc:content-type; bh=w5xm9Afwc41DxCDi26VaEZCjZ1FVsuUWHFPHjVy2zBM=; b=JCcC8UefwAQRC6FfaNZB8NKmv/cqiuWJ2tB6tUHPiNCdGgdEp3j39QwPewsN5yOl01 yNMWgbxNr9M9K6lxulXibBvDkVMH67/Q1tASV71Rsd79qYKXRSOebK7H8km195ZIsk9D uR2ZibCckeEVQPNlgQe4xpU3cWPMroiCTBksbNuz5UbdSEeX4zwelOXWI+SW2wB7JEwc 8AzrRpRZkJzdBWWEc1zJMx80768/aZSxm+PxV29QuBUbcamNhxAJEllXIefMoVcwY2XQ 5zJSxqtCqg7k4ft+OQ2Jp/1/1wa4BDvvWl7c6T5m4ryEzP+IJ76IVWBcW2unrsCdesAh sc5g== MIME-Version: 1.0 X-Received: by 10.170.75.2 with SMTP id r2mr4402609ykr.79.1424900148932; Wed, 25 Feb 2015 13:35:48 -0800 (PST) Received: by 10.170.149.65 with HTTP; Wed, 25 Feb 2015 13:35:48 -0800 (PST) In-Reply-To: References: Date: Wed, 25 Feb 2015 13:35:48 -0800 Message-ID: From: Martin DeMello To: Jeremy Yallop Cc: OCaml List Content-Type: text/plain; charset=UTF-8 Subject: Re: [Caml-list] "this ground coercion is not principal" 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 wrote: > On 25 February 2015 at 04:47, Martin DeMello 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.