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 1A7947EE51 for ; Tue, 30 Apr 2013 07:45:10 +0200 (CEST) Received-SPF: None (mail3-smtp-sop.national.inria.fr: no sender authenticity information available from domain of garrigue@math.nagoya-u.ac.jp) identity=pra; client-ip=133.6.130.5; receiver=mail3-smtp-sop.national.inria.fr; envelope-from="garrigue@math.nagoya-u.ac.jp"; x-sender="garrigue@math.nagoya-u.ac.jp"; x-conformance=sidf_compatible Received-SPF: None (mail3-smtp-sop.national.inria.fr: no sender authenticity information available from domain of garrigue@math.nagoya-u.ac.jp) identity=mailfrom; client-ip=133.6.130.5; receiver=mail3-smtp-sop.national.inria.fr; envelope-from="garrigue@math.nagoya-u.ac.jp"; x-sender="garrigue@math.nagoya-u.ac.jp"; x-conformance=sidf_compatible Received-SPF: None (mail3-smtp-sop.national.inria.fr: no sender authenticity information available from domain of postmaster@mailhost.math.nagoya-u.ac.jp) identity=helo; client-ip=133.6.130.5; receiver=mail3-smtp-sop.national.inria.fr; envelope-from="garrigue@math.nagoya-u.ac.jp"; x-sender="postmaster@mailhost.math.nagoya-u.ac.jp"; x-conformance=sidf_compatible X-IronPort-Anti-Spam-Filtered: true X-IronPort-Anti-Spam-Result: AgUFAHVZf1GFBoIFdGdsb2JhbABSgz2+V4EfDgEMFQg8gh8BAQQBQwE3AwsLNBJXBhMbh3UFDa0CgzKBEgKGBoc1B45nOoJuYYkTjg6BJpMk X-IPAS-Result: AgUFAHVZf1GFBoIFdGdsb2JhbABSgz2+V4EfDgEMFQg8gh8BAQQBQwE3AwsLNBJXBhMbh3UFDa0CgzKBEgKGBoc1B45nOoJuYYkTjg6BJpMk X-IronPort-AV: E=Sophos;i="4.87,579,1363129200"; d="scan'208";a="12690851" Received: from rabbit.math.nagoya-u.ac.jp (HELO mailhost.math.nagoya-u.ac.jp) ([133.6.130.5]) by mail3-smtp-sop.national.inria.fr with ESMTP; 30 Apr 2013 07:45:07 +0200 Received: from mailhost.math.nagoya-u.ac.jp (localhost [127.0.0.1]) by mailhost.math.nagoya-u.ac.jp (Postfix) with ESMTP id E8D1762E4 for ; Tue, 30 Apr 2013 14:45:04 +0900 (JST) Received: from mailhost.math.nagoya-u.ac.jp (localhost [127.0.0.1]) by mailhost.math.nagoya-u.ac.jp (Postfix) with ESMTP id 3D45C250C for ; Tue, 30 Apr 2013 14:45:04 +0900 (JST) DomainKey-Signature: h=Received:Content-Type:Mime-Version:Subject:From:In-Reply-To:Date:Content-Transfer-Encoding:Message-Id:References:To:X-Mailer; b=; c=nofws; d=math.nagoya-u.ac.jp; q=; s=alpha Received: from tet.garrigue.jp (58x158x128x157.ap58.ftth.ucom.ne.jp [58.158.128.157]) by mailhost.math.nagoya-u.ac.jp (Postfix) with ESMTPSA id 298002504 for ; Tue, 30 Apr 2013 14:45:04 +0900 (JST) Content-Type: text/plain; charset=windows-1252 Mime-Version: 1.0 (Mac OS X Mail 6.3 \(1503\)) From: Jacques Garrigue In-Reply-To: <1EA5B7CE-C0C3-4113-9F8F-C4C3BC888D49@math.nagoya-u.ac.jp> Date: Tue, 30 Apr 2013 14:45:03 +0900 Content-Transfer-Encoding: quoted-printable Message-Id: <0BC2A384-6D0F-49F2-BD68-5C840BA0888A@math.nagoya-u.ac.jp> References: <00C57DF0-C6F0-4EDE-8607-2155F3A17146@math.nagoya-u.ac.jp> <517E2818.5040506@frisch.fr> <1EA5B7CE-C0C3-4113-9F8F-C4C3BC888D49@math.nagoya-u.ac.jp> To: OCaML List Mailing X-Mailer: Apple Mail (2.1503) Subject: Re: [Caml-list] Request for feedback: A problem with injectivity and GADTs I have now committed in trunk a fix to PR#5985. You can use it to test whether your codebase runs into problems. You can either obtain it from subversion directly svn checkout http://caml.inria.fr/svn/ocaml/trunk or use opam to do it for you. I checked that at least Core itself compiles without problems. Again, if you run into problems, you can try branches/non-vanishing, which allows you to annotate some abstract types are injective. Jacques Garrigue On 2013/04/29, at 19:52, Jacques Garrigue wr= ote: > Dear Camlers, >=20 > First, let me reiterate my request for feedback: >=20 > What I want to know is whether anybody is using GADTs in a way that > would be broken if we disallow type variables under abstract types > (other than the predefined ones) in the return type of GADTs. > I.e., for instance defining a type witness type involving such abstract t= ypes. >=20 > This is really the question I want you all to answer. >=20 > If this is not the case, we can safely prohibit that at this point, and t= ake > our time to think about the solution.