From mboxrd@z Thu Jan 1 00:00:00 1970 Return-Path: Received: from mail3-relais-sop.national.inria.fr (mail3-relais-sop.national.inria.fr [192.134.164.104]) by sympa.inria.fr (Postfix) with ESMTPS id 5CE2E7EF10 for ; Wed, 25 Feb 2015 11:38:46 +0100 (CET) Received-SPF: None (mail3-smtp-sop.national.inria.fr: no sender authenticity information available from domain of yallop@gmail.com) identity=pra; client-ip=209.85.216.44; receiver=mail3-smtp-sop.national.inria.fr; envelope-from="yallop@gmail.com"; x-sender="yallop@gmail.com"; x-conformance=sidf_compatible Received-SPF: Pass (mail3-smtp-sop.national.inria.fr: domain of yallop@gmail.com designates 209.85.216.44 as permitted sender) identity=mailfrom; client-ip=209.85.216.44; receiver=mail3-smtp-sop.national.inria.fr; envelope-from="yallop@gmail.com"; x-sender="yallop@gmail.com"; x-conformance=sidf_compatible; x-record-type="v=spf1" Received-SPF: None (mail3-smtp-sop.national.inria.fr: no sender authenticity information available from domain of postmaster@mail-qa0-f44.google.com) identity=helo; client-ip=209.85.216.44; receiver=mail3-smtp-sop.national.inria.fr; envelope-from="yallop@gmail.com"; x-sender="postmaster@mail-qa0-f44.google.com"; x-conformance=sidf_compatible X-IronPort-Anti-Spam-Filtered: true X-IronPort-Anti-Spam-Result: A0BtAQB3pe1UlSzYVdFbhCQMBIMExX0BCQKBGgdDAQEBAQEBEAEBAQEHDQkJEjCEEAEBBBIRHQEbHQEDDAYFCw0CAiYCAiEBAREBBQEcBhMih3gBAxGvED4xiy6Ba4J3jkIKGScNVIRdAQEBAQEFAQEBAQEBFgEFDoETiXKCRIIqB4JogUMFlVGCCYFGjTSEPRIjgQwJhBA+MYJDAQEB X-IPAS-Result: A0BtAQB3pe1UlSzYVdFbhCQMBIMExX0BCQKBGgdDAQEBAQEBEAEBAQEHDQkJEjCEEAEBBBIRHQEbHQEDDAYFCw0CAiYCAiEBAREBBQEcBhMih3gBAxGvED4xiy6Ba4J3jkIKGScNVIRdAQEBAQEFAQEBAQEBFgEFDoETiXKCRIIqB4JogUMFlVGCCYFGjTSEPRIjgQwJhBA+MYJDAQEB X-IronPort-AV: E=Sophos;i="5.09,643,1418079600"; d="scan'208";a="101262053" Received: from mail-qa0-f44.google.com ([209.85.216.44]) by mail3-smtp-sop.national.inria.fr with ESMTP/TLS/RC4-SHA; 25 Feb 2015 11:38:45 +0100 Received: by mail-qa0-f44.google.com with SMTP id n8so2037695qaq.3 for ; Wed, 25 Feb 2015 02:38:44 -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=s+rBEBTg00CWzzSIOLNQRSGqZGV2NUiMYmdltk0Oh44=; b=qnXLD8PnhPgHkgAzWBH9T5dUxF88IZ87llp6fknhuJglHMs2zMuwg6w/uxLtvkfmd3 agsIYlJFspDchflvTOJwGz7FkgtqXJgCt6eJkUAz5N/FXvD2O1lM2emU/J9KYQrw2xx0 ZQNNqj9m+Y4//IaX+7j4pJcRFeoDJS+0R0RJ3ePpiZYIXx1A1azR9Dz53jyQOMFBGPYB HTnnoHmZkLFN4/gpjQ0ml9ob2ZQev2ZYeBOLawGPILK5E3+C4eoXsvQx8gAy6IgiAfZt 51XQQA9/UrHUjv/bdb6fJrhVlsgOK0QN7k1ZAPs8QuaJo1yDvSN7I3nrHY7k7JlUxrSZ FWMA== MIME-Version: 1.0 X-Received: by 10.140.34.36 with SMTP id k33mr5400213qgk.66.1424860724447; Wed, 25 Feb 2015 02:38:44 -0800 (PST) Received: by 10.229.160.11 with HTTP; Wed, 25 Feb 2015 02:38:44 -0800 (PST) In-Reply-To: References: Date: Wed, 25 Feb 2015 10:38:44 +0000 Message-ID: From: Jeremy Yallop To: Martin DeMello Cc: OCaml List Content-Type: text/plain; charset=UTF-8 Subject: Re: [Caml-list] "this ground coercion is not principal" 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.