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 mail3-relais-sop.national.inria.fr (mail3-relais-sop.national.inria.fr [192.134.164.104]) by sympa.inria.fr (Postfix) with ESMTPS id 1721A7F02D for ; Wed, 8 Oct 2014 18:06:00 +0200 (CEST) Received-SPF: None (mail3-smtp-sop.national.inria.fr: no sender authenticity information available from domain of milanst@gmail.com) identity=pra; client-ip=209.85.213.177; receiver=mail3-smtp-sop.national.inria.fr; envelope-from="milanst@gmail.com"; x-sender="milanst@gmail.com"; x-conformance=sidf_compatible Received-SPF: Pass (mail3-smtp-sop.national.inria.fr: domain of milanst@gmail.com designates 209.85.213.177 as permitted sender) identity=mailfrom; client-ip=209.85.213.177; receiver=mail3-smtp-sop.national.inria.fr; envelope-from="milanst@gmail.com"; x-sender="milanst@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-ig0-f177.google.com) identity=helo; client-ip=209.85.213.177; receiver=mail3-smtp-sop.national.inria.fr; envelope-from="milanst@gmail.com"; x-sender="postmaster@mail-ig0-f177.google.com"; x-conformance=sidf_compatible X-IronPort-Anti-Spam-Filtered: true X-IronPort-Anti-Spam-Result: AngBAABgNVTRVdWxm2dsb2JhbABfDoNTXIMAyASHVQKBAggWAREBAQEBAQYLCwkULIQEAQEEEhEEGQEbHQEDDAYFCw0CAiYCAiIBEQEFARwGEyKIBwEDEaBbboswgXKDEIgaChknDWeGMQERAQUOgR6OZTMHgneBVAWWNYcQlBsYKYRUXCEvgkoBAQE X-IPAS-Result: AngBAABgNVTRVdWxm2dsb2JhbABfDoNTXIMAyASHVQKBAggWAREBAQEBAQYLCwkULIQEAQEEEhEEGQEbHQEDDAYFCw0CAiYCAiIBEQEFARwGEyKIBwEDEaBbboswgXKDEIgaChknDWeGMQERAQUOgR6OZTMHgneBVAWWNYcQlBsYKYRUXCEvgkoBAQE X-IronPort-AV: E=Sophos;i="5.04,678,1406584800"; d="scan'208";a="82452290" Received: from mail-ig0-f177.google.com ([209.85.213.177]) by mail3-smtp-sop.national.inria.fr with ESMTP/TLS/RC4-SHA; 08 Oct 2014 18:05:59 +0200 Received: by mail-ig0-f177.google.com with SMTP id a13so9179451igq.16 for ; Wed, 08 Oct 2014 09:05:58 -0700 (PDT) DKIM-Signature: v=1; a=rsa-sha256; c=relaxed/relaxed; d=gmail.com; s=20120113; h=mime-version:in-reply-to:references:from:date:message-id:subject:to :cc:content-type:content-transfer-encoding; bh=F/cedjbp0wuglrXSFtivVLvWtwpxoxkqfsWUG5bjS/w=; b=C+rdwlJVSyRslWnhn6CbAVsWOgrdbuEhPX0VDPxDWmXeNHmVLtMA44CrJZ9yhw7//5 I/tnP6fXHzJOx4fl41WQalh31BHmlHhzNJF2FJ063PbPZF9t/HiZr6VdnLYz6OsurNIw Fmh9+PWm0kwr9VhCNxnDfTPKidFOcyiWFZsAXAIEBS9nGRy0E4HFagBUqOE4G3Sgt8/M myvksoRS7vVuQgzIFctIDqvFKsTYJqteduj/NntSM7Evw0ZnJ+yZolhhiZEEaEfm0zmz rgbM3FZ+plaZ+nxoGhO+wgbkaDIdqDI8m7a3gX9SPrQpNnwbC3SkXeRn32jNZa2F8kbb lyTA== X-Received: by 10.50.152.35 with SMTP id uv3mr17666825igb.46.1412784358136; Wed, 08 Oct 2014 09:05:58 -0700 (PDT) MIME-Version: 1.0 Received: by 10.64.114.38 with HTTP; Wed, 8 Oct 2014 09:05:16 -0700 (PDT) In-Reply-To: <43F352EF-1F58-4CE3-8EA5-91D61EBBA751@math.nagoya-u.ac.jp> References: <43F352EF-1F58-4CE3-8EA5-91D61EBBA751@math.nagoya-u.ac.jp> From: =?UTF-8?Q?Milan_Stanojevi=C4=87?= Date: Wed, 8 Oct 2014 12:05:16 -0400 Message-ID: To: Jacques Garrigue Cc: OCaML List Mailing Content-Type: text/plain; charset=UTF-8 Content-Transfer-Encoding: quoted-printable Subject: Re: [Caml-list] constructor disambiguation for gadts Thanks for the answer. Is there any hope this might get fixed in the future? On Tue, Oct 7, 2014 at 11:29 PM, Jacques Garrigue wrote: > On 2014/10/08 01:14, Milan Stanojevi=C4=87 wrote: >> >> I was wondering what are technical difficulties that prevent >> constructor disambiguation for GADTs? >> >> I got an interesting error today, where it is clear that compiler >> knows the type but because it is GADT it is still asking me to qualify >> the constructor. >> >> Here is the simple example. >> module A : sig >> type _ t =3D >> | I : int t >> | S : string t >> end =3D struct >> type _ t =3D >> | I : int t >> | S : string t >> end >> >> let add : type a . a A.t -> a -> a -> a =3D >> fun w a1 a2 -> >> match w with >> | I -> a1 + a2 >> | S -> String.concat "" [a1; a2] >> ;; >> >> I get File "foo.ml", line 14, characters 6-7: >> Error: The GADT constructor I of type A.t must be qualified in this patt= ern. >> >> I'm not sure what extra information I'm giving to the type checker by >> qualifying the constructor. > > Typing of GADT patterns follows a slightly different path, which makes > harder to insert constructor disambiguation. > To be more precise, the type-checker first looks at the patterns, and > tries to guess whether there are some GADT constructors inside it. > If some constructors are ambiguous, it may guess wrongly that there > are none, and take the non-GADT path, to find later that it should have > taken the GADT path. > > Jacques Garrigue