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 F24C87ED99 for ; Wed, 27 May 2015 17:22:17 +0200 (CEST) Received-SPF: None (mail2-smtp-roc.national.inria.fr: no sender authenticity information available from domain of joris@giovannangeli.fr) identity=pra; client-ip=217.70.183.197; receiver=mail2-smtp-roc.national.inria.fr; envelope-from="joris@giovannangeli.fr"; x-sender="joris@giovannangeli.fr"; x-conformance=sidf_compatible Received-SPF: None (mail2-smtp-roc.national.inria.fr: no sender authenticity information available from domain of joris@giovannangeli.fr) identity=mailfrom; client-ip=217.70.183.197; receiver=mail2-smtp-roc.national.inria.fr; envelope-from="joris@giovannangeli.fr"; x-sender="joris@giovannangeli.fr"; x-conformance=sidf_compatible Received-SPF: None (mail2-smtp-roc.national.inria.fr: no sender authenticity information available from domain of postmaster@relay5-d.mail.gandi.net) identity=helo; client-ip=217.70.183.197; receiver=mail2-smtp-roc.national.inria.fr; envelope-from="joris@giovannangeli.fr"; x-sender="postmaster@relay5-d.mail.gandi.net"; x-conformance=sidf_compatible X-IronPort-Anti-Spam-Filtered: true X-IronPort-Anti-Spam-Result: A0DjAgDb4GVVnMW3RtlchEiDGcYcAoE9PBABAQEBAQEBEQEBAQEBBg0JCSEuQQWDXQEBAwEjVQYLCxoCBRYLAgIJAwIBAgFFEwgBAYghDK0ApB4BCyCBIYoZhQwWglKBRQWfQIZPi16DVwKBBIEFghSCM4EBAQEB X-IPAS-Result: A0DjAgDb4GVVnMW3RtlchEiDGcYcAoE9PBABAQEBAQEBEQEBAQEBBg0JCSEuQQWDXQEBAwEjVQYLCxoCBRYLAgIJAwIBAgFFEwgBAYghDK0ApB4BCyCBIYoZhQwWglKBRQWfQIZPi16DVwKBBIEFghSCM4EBAQEB X-IronPort-AV: E=Sophos;i="5.13,506,1427752800"; d="scan'208";a="155535826" Received: from relay5-d.mail.gandi.net ([217.70.183.197]) by mail2-smtp-roc.national.inria.fr with ESMTP/TLS/ADH-AES256-SHA; 27 May 2015 17:22:17 +0200 Received: from mfilter22-d.gandi.net (mfilter22-d.gandi.net [217.70.178.150]) by relay5-d.mail.gandi.net (Postfix) with ESMTP id 5981841C087 for ; Wed, 27 May 2015 17:22:17 +0200 (CEST) X-Virus-Scanned: Debian amavisd-new at mfilter22-d.gandi.net Received: from relay5-d.mail.gandi.net ([217.70.183.197]) by mfilter22-d.gandi.net (mfilter22-d.gandi.net [10.0.15.180]) (amavisd-new, port 10024) with ESMTP id yYfCCiJiynf9 for ; Wed, 27 May 2015 17:22:05 +0200 (CEST) X-Originating-IP: 194.254.61.44 Received: from [172.28.134.176] (roam-nat-fw-prg-194-254-61-44.net.univ-paris-diderot.fr [194.254.61.44]) (Authenticated sender: joris@giovannangeli.fr) by relay5-d.mail.gandi.net (Postfix) with ESMTPSA id 560C541C07D for ; Wed, 27 May 2015 17:22:05 +0200 (CEST) Message-ID: <5565E11B.7010300@giovannangeli.fr> Date: Wed, 27 May 2015 17:22:03 +0200 From: Joris Giovannangeli User-Agent: Mozilla/5.0 (X11; Linux x86_64; rv:31.0) Gecko/20100101 Thunderbird/31.6.0 MIME-Version: 1.0 To: caml-list@inria.fr References: <5565DD11.6080608@giovannangeli.fr> In-Reply-To: Content-Type: text/plain; charset=utf-8 Content-Transfer-Encoding: 7bit Subject: Re: [Caml-list] Matching exhausitvity with GADT and modules > 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