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 CCD597F94F for ; Sun, 29 Jun 2014 16:49:32 +0200 (CEST) Received-SPF: None (mail3-smtp-sop.national.inria.fr: no sender authenticity information available from domain of gregoire.henry@ocamlpro.com) identity=pra; client-ip=194.254.61.138; receiver=mail3-smtp-sop.national.inria.fr; envelope-from="gregoire.henry@ocamlpro.com"; x-sender="gregoire.henry@ocamlpro.com"; x-conformance=sidf_compatible Received-SPF: None (mail3-smtp-sop.national.inria.fr: no sender authenticity information available from domain of gregoire.henry@ocamlpro.com) identity=mailfrom; client-ip=194.254.61.138; receiver=mail3-smtp-sop.national.inria.fr; envelope-from="gregoire.henry@ocamlpro.com"; x-sender="gregoire.henry@ocamlpro.com"; x-conformance=sidf_compatible Received-SPF: None (mail3-smtp-sop.national.inria.fr: no sender authenticity information available from domain of postmaster@korolev.univ-paris7.fr) identity=helo; client-ip=194.254.61.138; receiver=mail3-smtp-sop.national.inria.fr; envelope-from="gregoire.henry@ocamlpro.com"; x-sender="postmaster@korolev.univ-paris7.fr"; x-conformance=sidf_compatible X-IronPort-Anti-Spam-Filtered: true X-IronPort-Anti-Spam-Result: AlYBALkmsFPC/j2KnGdsb2JhbABagmnHGAGBCBYPAQEBAQEGDQkJFCiEBAEFJwsBRhALIRMHCw8tGwaIVgPGEReOVDMHgy2BFgWaXQGVfYFE X-IPAS-Result: AlYBALkmsFPC/j2KnGdsb2JhbABagmnHGAGBCBYPAQEBAQEGDQkJFCiEBAEFJwsBRhALIRMHCw8tGwaIVgPGEReOVDMHgy2BFgWaXQGVfYFE X-IronPort-AV: E=Sophos;i="5.01,570,1400018400"; d="scan'208";a="69453391" Received: from korolev.univ-paris7.fr ([194.254.61.138]) by mail3-smtp-sop.national.inria.fr with ESMTP/TLS/DHE-RSA-AES256-SHA; 29 Jun 2014 16:49:32 +0200 Received: from potemkin.univ-paris7.fr (potemkin.univ-paris7.fr [IPv6:2001:660:3301:8000::1:1]) by korolev.univ-paris7.fr (8.14.4/8.14.4/relay1/46573) with ESMTP id s5TEnVrL029533 (version=TLSv1/SSLv3 cipher=DHE-RSA-AES256-GCM-SHA384 bits=256 verify=NO); Sun, 29 Jun 2014 16:49:31 +0200 Received: from mailhub.math.univ-paris-diderot.fr (mailhub.math.univ-paris-diderot.fr [81.194.30.253]) by potemkin.univ-paris7.fr (8.14.4/8.14.4/relay2/46573) with ESMTP id s5TEnVHZ025799; Sun, 29 Jun 2014 16:49:31 +0200 Received: from mailhub.math.univ-paris-diderot.fr (localhost [127.0.0.1]) by mailhub.math.univ-paris-diderot.fr (Postfix) with ESMTP id F40F62B826F; Sun, 29 Jun 2014 16:49:30 +0200 (CEST) X-Virus-Scanned: amavisd-new at math.univ-paris-diderot.fr Received: from mailhub.math.univ-paris-diderot.fr ([127.0.0.1]) by mailhub.math.univ-paris-diderot.fr (mailhub.math.univ-paris-diderot.fr [127.0.0.1]) (amavisd-new, port 10023) with ESMTP id 8yvL23o_bmY5; Sun, 29 Jun 2014 16:49:30 +0200 (CEST) Received: from melquiades.lan (81-64-137-19.rev.numericable.fr [81.64.137.19]) (Authenticated sender: henry) by mailhub.math.univ-paris-diderot.fr (Postfix) with ESMTPSA id 0471A2B825E; Sun, 29 Jun 2014 16:49:29 +0200 (CEST) Received: from greg by melquiades.lan with local (Exim 4.82_1-5b7a7c0-XX) (envelope-from ) id 1X1GQ5-0000QV-FY; Sun, 29 Jun 2014 16:49:29 +0200 Date: Sun, 29 Jun 2014 16:49:29 +0200 From: =?iso-8859-1?Q?Gr=E9goire?= Henry To: Nicolas Trangez Cc: Caml-list Message-ID: <20140629144929.GB32483@mlqds.hnr.gr> References: <1403996132.26873.18.camel@chi.nicolast.be> MIME-Version: 1.0 Content-Type: text/plain; charset=iso-8859-1 Content-Disposition: inline Content-Transfer-Encoding: 8bit In-Reply-To: <1403996132.26873.18.camel@chi.nicolast.be> X-Greylist: Sender IP whitelisted, not delayed by milter-greylist-4.2.7 (korolev.univ-paris7.fr [IPv6:2001:660:3301:8000::1:2]); Sun, 29 Jun 2014 16:49:31 +0200 (CEST) X-Greylist: Sender IP whitelisted, not delayed by milter-greylist-4.2.7 (potemkin.univ-paris7.fr [194.254.61.141]); Sun, 29 Jun 2014 16:49:31 +0200 (CEST) X-Miltered: at korolev with ID 53B0277B.000 by Joe's j-chkmail (http : // j-chkmail dot ensmp dot fr)! X-Miltered: at potemkin with ID 53B0277B.000 by Joe's j-chkmail (http : // j-chkmail dot ensmp dot fr)! X-j-chkmail-Enveloppe: 53B0277B.000 from potemkin.univ-paris7.fr/potemkin.univ-paris7.fr/null/potemkin.univ-paris7.fr/ X-j-chkmail-Enveloppe: 53B0277B.000 from mailhub.math.univ-paris-diderot.fr/mailhub.math.univ-paris-diderot.fr/null/mailhub.math.univ-paris-diderot.fr/ X-j-chkmail-Score: MSGID : 53B0277B.000 on korolev.univ-paris7.fr : j-chkmail score : . : R=. U=. O=. B=0.000 -> S=0.000 X-j-chkmail-Score: MSGID : 53B0277B.000 on potemkin.univ-paris7.fr : j-chkmail score : . : R=. U=. O=. B=0.000 -> S=0.000 X-j-chkmail-Status: Ham X-j-chkmail-Status: Ham Subject: Re: [Caml-list] Strange interaction between recursive modules, GADT exhaustiveness checking and type-checking? Hi, I believe the presence of recursive module has nothing to do with this particular warning. But, in general, the exhaustiveness-check can't assume that two abstract types are distinct, as they may be equal in some other typing context. In your code example, there is no such typing context. But, for instance, imagine the following program: module rec W : sig type a type b type (_, _) t = | AA : (a, a) t | AB : (a, b) t | BB : (b, b) t type 'a w = | W : ('a, 'b) W.t * 'b -> 'a w val x : a w end = struct type a = unit type b = unit type (_, _) t = | AA : (a, a) t | AB : (a, b) t | BB : (b, b) t type 'a w = | W : ('a, 'b) W.t * 'b -> 'a w let x : a w = W (BB, ()) end open W type s = | A of a | B of b let f : a w -> s = function | W (AA, a) -> A a | W (AB, b) -> B b (* Warning *) let _ = f x (* Match_failure *) In general, it is rather difficult to decide if there exists a typing context where two abstract types may be considered as equal. And even more complex with separate compilation. As a consequence, while testing the exhaustiveness of a pattern-matching, the type-checker has to assume that 'W.a' and 'W.b' might be equal. let f3 : a w -> s = function | W (AA, a) -> A a | W (AB, b) -> B b | W (BB, b) -> B b In particular, while type-checking the third branch of [f3], the type-checker assumes that 'W.a = W.b'. This is safe, as the existence of a value 'W (BB, b)' of type 'a w' can be seen as a proof of this equality: in the typing context where the value was built, the two types have to be equals. Your first example is a particular case where we could assume that 'W.a' and 'W.b' are distinct. They are 'fully abstract types', they have no inhabitants. They were introduced in current typing context (and not imported from the signature of another module) and we known they are distinct. HTH, Grégoire