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 3EFAB801CD for ; Fri, 18 Aug 2017 17:34:04 +0200 (CEST) Authentication-Results: mail2-smtp-roc.national.inria.fr; spf=None smtp.pra=gabriel.scherer@gmail.com; spf=Pass smtp.mailfrom=gabriel.scherer@gmail.com; spf=None smtp.helo=postmaster@mail-qk0-f182.google.com Received-SPF: None (mail2-smtp-roc.national.inria.fr: no sender authenticity information available from domain of gabriel.scherer@gmail.com) identity=pra; client-ip=209.85.220.182; receiver=mail2-smtp-roc.national.inria.fr; envelope-from="gabriel.scherer@gmail.com"; x-sender="gabriel.scherer@gmail.com"; x-conformance=sidf_compatible Received-SPF: Pass (mail2-smtp-roc.national.inria.fr: domain of gabriel.scherer@gmail.com designates 209.85.220.182 as permitted sender) identity=mailfrom; client-ip=209.85.220.182; receiver=mail2-smtp-roc.national.inria.fr; envelope-from="gabriel.scherer@gmail.com"; x-sender="gabriel.scherer@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-qk0-f182.google.com) identity=helo; client-ip=209.85.220.182; receiver=mail2-smtp-roc.national.inria.fr; envelope-from="gabriel.scherer@gmail.com"; x-sender="postmaster@mail-qk0-f182.google.com"; x-conformance=sidf_compatible IronPort-PHdr: =?us-ascii?q?9a23=3AAwyN9BTcU0rvrmi/leIFKavFztpsv+yvbD5Q0YIu?= =?us-ascii?q?jvd0So/mwa64ZBCN2/xhgRfzUJnB7Loc0qyN7PCmBDRIyK3CmU5BWaQEbwUCh8?= =?us-ascii?q?QSkl5oK+++Imq/EsTXaTcnFt9JTl5v8iLzG0FUHMHjew+a+SXqvnYkIQjkLQd+?= =?us-ascii?q?OsjyH4fTiYz3i7HzqNXvZFBhgDetbKI6ARqxtwLP/p0fhYZybKE3zgqPrlNHfu?= =?us-ascii?q?1XwSVjIlfFzDjm4cLl05dp6SVdv7oa/M5NS6jgN/A3RLZCDTkidXs+5MDxuAPr?= =?us-ascii?q?Qg6G539aWWITxEkbSzPZ5Q33C8+i+hDxsfBwjXXLMA=3D=3D?= X-IronPort-Anti-Spam-Filtered: true X-IronPort-Anti-Spam-Result: =?us-ascii?q?A0A3AQCgCJdZf7bcVdFdFgQBAQEBAgEBA?= =?us-ascii?q?QEIAQEBARQBAQEBAQEBAQEBAQcBAQEBAYNUP4ECEweeHoFugkaVaCyFFwICAoN?= =?us-ascii?q?lB0MUAQEBAQEBAQEBAQESAQEJCwsIJjGCMwUDBB6CPAECAQIjHQEbEgsBAwwGB?= =?us-ascii?q?QsDCgICCR0CAiEBAREBBQEKEgYTEooFAQMVEKAXP4wLggQFARyDCQWDYQoZJwM?= =?us-ascii?q?KVoNKAQEBAQEBAQMBAQEBAQEaAgYSeYIdggKBTIFjgyeCV4IcgxOCYQWIGQyXb?= =?us-ascii?q?DyCKIUsh3iEdoIQWYkDhnKKW4FciB4VH4EVNoErMiEkXhqEboIUPjYBAYh2gT8?= =?us-ascii?q?BAQE?= X-IPAS-Result: =?us-ascii?q?A0A3AQCgCJdZf7bcVdFdFgQBAQEBAgEBAQEIAQEBARQBAQE?= =?us-ascii?q?BAQEBAQEBAQcBAQEBAYNUP4ECEweeHoFugkaVaCyFFwICAoNlB0MUAQEBAQEBA?= =?us-ascii?q?QEBAQESAQEJCwsIJjGCMwUDBB6CPAECAQIjHQEbEgsBAwwGBQsDCgICCR0CAiE?= =?us-ascii?q?BAREBBQEKEgYTEooFAQMVEKAXP4wLggQFARyDCQWDYQoZJwMKVoNKAQEBAQEBA?= =?us-ascii?q?QMBAQEBAQEaAgYSeYIdggKBTIFjgyeCV4IcgxOCYQWIGQyXbDyCKIUsh3iEdoI?= =?us-ascii?q?QWYkDhnKKW4FciB4VH4EVNoErMiEkXhqEboIUPjYBAYh2gT8BAQE?= X-IronPort-AV: E=Sophos;i="5.41,393,1498514400"; d="scan'208";a="287526533" Received: from mail-qk0-f182.google.com ([209.85.220.182]) by mail2-smtp-roc.national.inria.fr with ESMTP/TLS/AES128-GCM-SHA256; 18 Aug 2017 17:34:03 +0200 Received: by mail-qk0-f182.google.com with SMTP id u139so54696328qka.1 for ; Fri, 18 Aug 2017 08:34:03 -0700 (PDT) DKIM-Signature: v=1; a=rsa-sha256; c=relaxed/relaxed; d=gmail.com; s=20161025; h=mime-version:in-reply-to:references:from:date:message-id:subject:to :cc:content-transfer-encoding; bh=ULXF9tV3c2eJGTjMMDH4eUcxvd+w350JPAB9czx4+O8=; b=Hf41Iu5KwgLTYSa4FQIOFToye39NP77/mwvScSr6ZxjHJZGY/36N6KWBUfSdVosDhM nqCfTIwEfhf7EBs1K3ERz1CYMRANjj79l1OFsCV3MWZqNBvg1LBEgkXCCZY8U3WYZA10 w1sxByA3bOWpF1GN1AbN0CbPvel31pfCCiVTl22J1XmhDXtU1QrhrHI+x6LUIw4vMdHS NOFw9eMZNUNprL9L+cZs5DdTmZ7T1aTtbV8NoQ4gjxmqnGiH24S41L/Z7JD+Zjngk1Bm LipAzpviYs6Tjf9ZfTIACABDCSICGLY0sFpePLJdLEALBb0gjvCm/ibcgN4n3weB/AVQ AajA== X-Google-DKIM-Signature: v=1; a=rsa-sha256; c=relaxed/relaxed; d=1e100.net; s=20161025; h=x-gm-message-state:mime-version:in-reply-to:references:from:date :message-id:subject:to:cc:content-transfer-encoding; bh=ULXF9tV3c2eJGTjMMDH4eUcxvd+w350JPAB9czx4+O8=; b=E869yEUh8TlfehttG4ZogYiow8o61pvj4GJ/0hPzf3EsofclZ7geBgFswacdINbQHy FJMFQjCvGvzijz2ACKnt4WfKIrR40cNpyurOlH8XHkHkDjDUOS3CIX6J8Nmk5bgVvH+0 mTdpuxAYbSfrzvBfx1IhhTwMTtzX+V6Z8Lrrs6+I1/Mfp2HUKlfR2yzYdZP9HjIId9/N eAdaP2ujtzuoVifAxoDA6MhTCUuCNF9vsCYAuFrkqzNwMA9VYTZ12iwcOi1X+C62lQkp UkxrKnmFVUjAzy0H8n8Qnbv+Xl5pUGmgFAj/M++TgXYKArRglv6qiWNcy1Li4Dl+UOT+ DkZg== X-Gm-Message-State: AHYfb5g6yn862FqAbZ5SCwzgq0i4kLXOqOJ1DbEzi3KedC8sHdc7nqfQ Yg2R9A6Tl/BBHDSxRSlcM2ULDI97eg== X-Received: by 10.55.67.136 with SMTP id q130mr12205929qka.185.1503070441861; Fri, 18 Aug 2017 08:34:01 -0700 (PDT) MIME-Version: 1.0 Received: by 10.12.184.148 with HTTP; Fri, 18 Aug 2017 08:33:21 -0700 (PDT) In-Reply-To: References: From: Gabriel Scherer Date: Fri, 18 Aug 2017 17:33:21 +0200 Message-ID: To: Alexey Egorov Cc: caml users Content-Type: text/plain; charset="UTF-8" Content-Transfer-Encoding: quoted-printable Subject: Re: [Caml-list] strange type error with -principal If you want to understand the details of GADT type inference, there is a paper about it whose introduction remains at an informal level and will get you a good picture: Ambivalent Types for Principal Type Inference with GADTs Jacques Garrigue and Didier R=C3=A9my, 2013 http://gallium.inria.fr/~remy/gadts/Garrigue-Remy:gadts@aplas2013.pdf The problem you had, however, is not about the mechanics describe in this paper which are relatively clear and robust, but how they interact with propagation of user annotations (which is a more ad-hoc part of the type-checker). The GADT type inference described in this paper clearly flags your pattern-matching code as requiring an annotation in the clause, and the question/issue is whether it gets pushed there or not by the independent annotation-propagation mechanism. On Fri, Aug 18, 2017 at 5:23 PM, Alexey Egorov wrot= e: > Thanks for explanation! > Every problem I've had with GADTs was solved placing an annotation in > the right place... > > 2017-08-18 19:36 GMT+05:00 Gabriel Scherer : >> These errors on "ambiguous" types come from GADT type checking, which >> requires annotations in certain places (-principal is more picky about >> requiring more annotations; instead sometimes the type-checker makes >> guesses). >> >> Currently the syntactic forms >> let : =3D in >> and >> let : =3D in >> are not desugared in the same way. The first is turned into >> let =3D ( : ) in >> and the second into >> let ( : ) =3D in >> >> In the first case (let ), the body of the definition gets the >> annotation. This is required, in your code, for this body to compile und= er >> -principal. In the second case (let ), the body does not get the >> annotation, so type-checking fails (under -principal). >> >> You can fix it yourself by adding the annotation on the right-hand-side >> directly >> >> let (op, idx) =3D (begin match ... end : int op * int) >> >> in fact it suffices to write (op : int op), 2 in the second clause's >> right-hand-side. >> >> I don't know whether (let : =3D in ) could >> instead be desugared into >> (let ( : : ) in ), which would a= lso >> fix the issue. The specifics of how type information is propagated in the >> type-checker is a delicate design aspect of the type-checker which may s= till >> evolve in the future. >> >> If you wonder what the error message means, you should read the GADT sec= tion >> in the Reference Manual, and in particular the "type inference" subsecti= on >> (but it depends on the text before it): >> http://caml.inria.fr/pub/docs/manual-ocaml-4.05/extn.html#sec236 >> >> The problem is that within the Op clause, we know the type equality (a = =3D >> int), but this is not true outside the clause; so when a value that has = both >> types (a op) and (int op) is returned by the clause, the type-checker ca= nnot >> know which type to give to the outside (a op, or int op?), and it needs = an >> explicit annotation to not make an arbitrary (non-principal) choice. >> >> On Fri, Aug 18, 2017 at 4:09 PM, Alexey Egorov >> wrote: >>> >>> Hello, >>> >>> I'm getting very confusing error when compiling with -principal: >>> >>> > Error: This expression has type int op >>> > but an expression was expected of type 'a >>> > This instance of int is ambiguous: >>> > it would escape the scope of its equation >>> >>> What is the "instance of int"? >>> >>> Here is the code - https://pastebin.com/T74haahx >>> I'm mostly confused by the fact that changing pattern from (op, idx) >>> to simple value binding eliminates this error. >>> >>> Thanks! >>> >>> -- >>> Caml-list mailing list. Subscription management and archives: >>> https://sympa.inria.fr/sympa/arc/caml-list >>> Beginner's list: http://groups.yahoo.com/group/ocaml_beginners >>> Bug reports: http://caml.inria.fr/bin/caml-bugs >> >>