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 E6C8D7ED1D for ; Tue, 13 Oct 2015 08:06:40 +0200 (CEST) IronPort-PHdr: 9a23:diDthx0ce7LT4XC9smDT+DRfVm0co7zxezQtwd8ZsekWK/ad9pjvdHbS+e9qxAeQG96Lt7QU0aGM7fmocFdDyKjCmUhKSIZLWR4BhJdetC0bK+nBN3fGKuX3ZTcxBsVIWQwt1Xi6NU9IBJS2PAWK8TWM5DIfUi/yKRBybrysXNWC04LnjavopcSbSj4LrQT+SIs6FA+xowTVu5teqqpZAYF19CH0pGBVcf9d32JiKAHbtR/94sCt4MwrqHwI6LoJvvRNWqTifqk+UacQTHF/azh0t4XXskzqRweG4n8VUi0tmxRGAgTE6hyyCp77viL+suN9njKTM8P3QbEyVByt6q5qTFnjjyJRZBAj92SCsdB9gqtd6DKmoxBy2YvdZprdYOFic63Ue/sESGFdWdxfXiZbA4inKYAICrxSbq5js4Dhqg5W/lOFDg62Cbaqk2cQiw== Authentication-Results: mail2-smtp-roc.national.inria.fr; spf=None smtp.pra=stefan@vectorfabrics.com; spf=PermError smtp.mailfrom=stefan@vectorfabrics.com; spf=None smtp.helo=postmaster@mail-wi0-f181.google.com Received-SPF: None (mail2-smtp-roc.national.inria.fr: no sender authenticity information available from domain of stefan@vectorfabrics.com) identity=pra; client-ip=209.85.212.181; receiver=mail2-smtp-roc.national.inria.fr; envelope-from="stefan@vectorfabrics.com"; x-sender="stefan@vectorfabrics.com"; x-conformance=sidf_compatible Received-SPF: PermError (mail2-smtp-roc.national.inria.fr: cannot correctly interpret sender authenticity information from domain of stefan@vectorfabrics.com) identity=mailfrom; client-ip=209.85.212.181; receiver=mail2-smtp-roc.national.inria.fr; envelope-from="stefan@vectorfabrics.com"; x-sender="stefan@vectorfabrics.com"; x-conformance=sidf_compatible Received-SPF: None (mail2-smtp-roc.national.inria.fr: no sender authenticity information available from domain of postmaster@mail-wi0-f181.google.com) identity=helo; client-ip=209.85.212.181; receiver=mail2-smtp-roc.national.inria.fr; envelope-from="stefan@vectorfabrics.com"; x-sender="postmaster@mail-wi0-f181.google.com"; x-conformance=sidf_compatible X-IronPort-Anti-Spam-Filtered: true X-IronPort-Anti-Spam-Result: A0BaAgD+nRxWlLXUVdFdxGCDE4IKfwKBOzwQAQEBAQEBAQEQAQEBAQcLCwkfMIIfgggBAQMBEhEEUgULCxoCGA4CAjQBBQEcBjWIBAgEAZ8AgTE+MYtJk1oBAQEBAQEBAwEBAQEBAQEBGgqBGIdjgm6EWjMHgmkxgRQBBJYVjXSIKZE2NYEXOIJSHYFAh2ABAQE X-IPAS-Result: A0BaAgD+nRxWlLXUVdFdxGCDE4IKfwKBOzwQAQEBAQEBAQEQAQEBAQcLCwkfMIIfgggBAQMBEhEEUgULCxoCGA4CAjQBBQEcBjWIBAgEAZ8AgTE+MYtJk1oBAQEBAQEBAwEBAQEBAQEBGgqBGIdjgm6EWjMHgmkxgRQBBJYVjXSIKZE2NYEXOIJSHYFAh2ABAQE X-IronPort-AV: E=Sophos;i="5.17,676,1437429600"; d="scan'208";a="182462879" Received: from mail-wi0-f181.google.com ([209.85.212.181]) by mail2-smtp-roc.national.inria.fr with ESMTP/TLS/AES128-GCM-SHA256; 13 Oct 2015 08:06:40 +0200 Received: by wieq12 with SMTP id q12so14525806wie.1 for ; Mon, 12 Oct 2015 23:06:40 -0700 (PDT) X-Google-DKIM-Signature: v=1; a=rsa-sha256; c=relaxed/relaxed; d=1e100.net; s=20130820; h=x-gm-message-state:content-type:mime-version:subject:from :in-reply-to:date:cc:content-transfer-encoding:message-id:references :to; bh=UjdHwZeZq8k+eVvSjkjN0XSiIg1n3/3uMx81P13pIRo=; b=FPGOplTXivmAxOiG4D/wPEfpwdJ0Ep6c4/qNNYBgZGqCrEMAUKL2s13XvI7wRI56nb onXZBP8qcmWVq5M4k4o+wvwPcsE98H1VWXTtEvcfwFBLdJ/1mekCyFi+7jkIpTqyTV80 ALYFBzgTAFBtiN+fBERM66yfTzslOsGz11CLyrG0eYOmK45d4o8vpYtGMhnq5ssRLdI9 zyTVAZIdtbJY2jaF8U9NmhH7ARMcYwCoMWVFpLgqWcdgSbKaY9h6AhAo/C3hLzy3+R04 g/MCH+97sRqJlgDXgP1U/tefHzrICS6tVysDSHoyy6ZydoTQfDmVT+QPDsL4d91idRwI wgMQ== X-Gm-Message-State: ALoCoQkg14oovXoVd6Uv5n6TZzMqZBo73+go7e3rXq1LhAB80u7roZ/45Vg/H/8dm0WIc6dH7LG8 X-Received: by 10.194.2.5 with SMTP id 5mr6033925wjq.153.1444716400098; Mon, 12 Oct 2015 23:06:40 -0700 (PDT) Received: from kanzi.vectorfabrics.com ([85.222.242.122]) by smtp.gmail.com with ESMTPSA id r6sm21240994wia.0.2015.10.12.23.06.38 (version=TLS1 cipher=ECDHE-RSA-AES128-SHA bits=128/128); Mon, 12 Oct 2015 23:06:39 -0700 (PDT) Content-Type: text/plain; charset=utf-8 Mime-Version: 1.0 (Mac OS X Mail 9.0 \(3094\)) From: Stefan Holdermans In-Reply-To: Date: Tue, 13 Oct 2015 08:06:39 +0200 Cc: caml-list@inria.fr Content-Transfer-Encoding: quoted-printable Message-Id: References: To: Abdallah Saffidine X-Mailer: Apple Mail (2.3094) Subject: Re: [Caml-list] How to use GADTs across modules in OCaml without raising warnings? Abdallah, > gadt1.ml: >=20 > type > never >=20 > type _ t1 =3D A1 : never t1 | B1 : > bool t1 >=20 > type _ t2 =3D A2 : string t2 | B2 : > bool t2 >=20 > let get1 : bool t1 -> bool =3D function B1 -> true > let get2 : bool t2 -> bool =3D function B2 -> true > gadt2.ml: >=20 > let get1 : bool Gadt1.t1 -> bool =3D function Gadt.B1 -> true > let get2 : bool Gadt1.t2 -> bool =3D function Gadt.B2 -> true > when I compile using ocaml 4.02.3 (ocamlbuild gadt2.native), I get a warn= ing 8 about the function Gadt2.get1 not being exhaustive. I am quite puzzle= d that Gadt2.get1 raises a warning while Gadt1.get1 and Gadt2.get2 don=E2= =80=99t. I suppose that, from the perspective of =E2=80=98Gadt2', =E2=80=98Gadt1.nev= er=E2=80=99 is an abstract datatype that *could* have been implemented by = =E2=80=98Gadt1=E2=80=99 as type never =3D bool Perhaps there=E2=80=99s a design priciple emerging here? Concrete GADTs do = not mix well with abstract type arguments. Cheers, Stefan