From mboxrd@z Thu Jan 1 00:00:00 1970 Return-Path: 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 B845B7EE7E for ; Wed, 27 May 2015 17:37:01 +0200 (CEST) Received-SPF: None (mail2-smtp-roc.national.inria.fr: no sender authenticity information available from domain of yjuglaret@gmail.com) identity=pra; client-ip=209.85.212.169; receiver=mail2-smtp-roc.national.inria.fr; envelope-from="yjuglaret@gmail.com"; x-sender="yjuglaret@gmail.com"; x-conformance=sidf_compatible Received-SPF: Pass (mail2-smtp-roc.national.inria.fr: domain of yjuglaret@gmail.com designates 209.85.212.169 as permitted sender) identity=mailfrom; client-ip=209.85.212.169; receiver=mail2-smtp-roc.national.inria.fr; envelope-from="yjuglaret@gmail.com"; x-sender="yjuglaret@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-wi0-f169.google.com) identity=helo; client-ip=209.85.212.169; receiver=mail2-smtp-roc.national.inria.fr; envelope-from="yjuglaret@gmail.com"; x-sender="postmaster@mail-wi0-f169.google.com"; x-conformance=sidf_compatible X-IronPort-Anti-Spam-Filtered: true X-IronPort-Anti-Spam-Result: A0BfAQBA5GVVlKnUVdFcg2Regx/AJYV3AoE9PBABAQEBAQEBEQEBAQEHCwsJHzCEIwEBBBIRDwEFCAEbHAIDDAYFCw8CBRYLAgIJAwIBAgEREQEFARwTCAEBFweHdQEDEgUIoFs+MYs+gWuCeZlyChknDVeEGgEBAQcBAQEBARcBBQ6BE4oZhQwWglKBRQEElz2GWoEpPoYRIYc3hAaCDzWBFYEEgQWCFG2CRwEBAQ X-IPAS-Result: A0BfAQBA5GVVlKnUVdFcg2Regx/AJYV3AoE9PBABAQEBAQEBEQEBAQEHCwsJHzCEIwEBBBIRDwEFCAEbHAIDDAYFCw8CBRYLAgIJAwIBAgEREQEFARwTCAEBFweHdQEDEgUIoFs+MYs+gWuCeZlyChknDVeEGgEBAQcBAQEBARcBBQ6BE4oZhQwWglKBRQEElz2GWoEpPoYRIYc3hAaCDzWBFYEEgQWCFG2CRwEBAQ X-IronPort-AV: E=Sophos;i="5.13,506,1427752800"; d="scan'208";a="155538368" Received: from mail-wi0-f169.google.com ([209.85.212.169]) by mail2-smtp-roc.national.inria.fr with ESMTP/TLS/RC4-SHA; 27 May 2015 17:37:01 +0200 Received: by wifw1 with SMTP id w1so27508448wif.0 for ; Wed, 27 May 2015 08:37:01 -0700 (PDT) DKIM-Signature: v=1; a=rsa-sha256; c=relaxed/relaxed; d=gmail.com; s=20120113; h=message-id:date:from:user-agent:mime-version:to:subject:references :in-reply-to:content-type:content-transfer-encoding; bh=n1uaKZBjP/AXYYibQcOPgHF9cDAvUW30sj9o/ByZlxs=; b=Ja3lExbnlZQCFHXY5qkuYy5NepkS6Y+bo5LykuUE9ietwSVhTeiOr2qahirskEqsCi +hwWRWz+b4xdLgX6AHOdLYWhwiZV08YTH5VZxTgb/u+4BS7frRjBBIX3vRUI4UWjMzVi 2ez/NSIMcBBUmiBv6vjXzLZPje+eLLgbL+gMvikLJjbrXvYoEUovD47pLPaLZmkw8S/Z MGxrt232Gxcp0t0ihV1CcdrO19qngGvcCjXoaMBzUZuMJBvwqbomT3gS811h0fwsFwqU sgV8YAwZAHAjbzA+IS+oz3nC/lNP1zVg1ZHOfqF0w00jmGd9ZrUHJDBvc3hIpEXKPkgN 5mUw== X-Received: by 10.194.187.170 with SMTP id ft10mr60318115wjc.26.1432741021295; Wed, 27 May 2015 08:37:01 -0700 (PDT) Received: from [128.93.44.112] (diffie.rocq.inria.fr. [128.93.44.112]) by mx.google.com with ESMTPSA id x10sm27448041wjf.45.2015.05.27.08.37.00 for (version=TLSv1 cipher=ECDHE-RSA-RC4-SHA bits=128/128); Wed, 27 May 2015 08:37:00 -0700 (PDT) Message-ID: <5565E49B.9090209@gmail.com> Date: Wed, 27 May 2015 17:36:59 +0200 From: Yannis Juglaret User-Agent: Mozilla/5.0 (X11; Linux x86_64; rv:24.0) Gecko/20100101 Thunderbird/24.2.0 MIME-Version: 1.0 To: caml-list@inria.fr References: <5565DD11.6080608@giovannangeli.fr> <5565E11B.7010300@giovannangeli.fr> In-Reply-To: <5565E11B.7010300@giovannangeli.fr> Content-Type: text/plain; charset=UTF-8; format=flowed Content-Transfer-Encoding: 8bit Subject: Re: [Caml-list] Matching exhausitvity with GADT and modules Hi, Removing this warning is not a good solution, because this warning may be relevant the day you update your GADT. As far as I know, you should always be using concrete types. Read for example: . This is a question to the list: is there any good reason for allowing abstract types in module implementations, and not just in module signatures -- where they can actually be used to abstract types? -- Yannis Le 27/05/2015 17:22, Joris Giovannangeli a écrit : > >> This is a common problem that has annoyed me as well. The issue is that >> B sees foo and bar as abstract types, so cannot be sure they are >> different, so cannot be sure that a value of type foo gadt can't be >> constructed with Bar. If you add explicit constructors for both >> currently-empty types, then their inequality will be exposed and your >> pattern match should work. > > That's a nice workaround in the case where foo and bar and phantom types > indeed. Just adding a dummy constructor. In case they are real abstract > type, someone advised me to disable the exhaustivity warning locally > with [@@warning "-8"] code annotation, which is a bit more hack-ish. > > Thanks > >