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 4018F7EE51 for ; Tue, 30 Apr 2013 10:02:48 +0200 (CEST) Received-SPF: None (mail2-smtp-roc.national.inria.fr: no sender authenticity information available from domain of alain@frisch.fr) identity=pra; client-ip=193.252.23.211; receiver=mail2-smtp-roc.national.inria.fr; envelope-from="alain@frisch.fr"; x-sender="alain@frisch.fr"; x-conformance=sidf_compatible Received-SPF: None (mail2-smtp-roc.national.inria.fr: no sender authenticity information available from domain of alain@frisch.fr) identity=mailfrom; client-ip=193.252.23.211; receiver=mail2-smtp-roc.national.inria.fr; envelope-from="alain@frisch.fr"; x-sender="alain@frisch.fr"; x-conformance=sidf_compatible Received-SPF: None (mail2-smtp-roc.national.inria.fr: no sender authenticity information available from domain of postmaster@msa.smtpout.orange.fr) identity=helo; client-ip=193.252.23.211; receiver=mail2-smtp-roc.national.inria.fr; envelope-from="alain@frisch.fr"; x-sender="postmaster@msa.smtpout.orange.fr"; x-conformance=sidf_compatible X-IronPort-Anti-Spam-Filtered: true X-IronPort-Anti-Spam-Result: AssBAKd5f1HB/BfTlGdsb2JhbABSDoMwvlaBGA4BAQEBCQsJCRQDJYIfAQEFOEABEAsYCRYPCQMCAQIBRQYNAQUCAQEXh3+wT45ajWiBMgeDTwOXHoYTjWlBgXE X-IPAS-Result: AssBAKd5f1HB/BfTlGdsb2JhbABSDoMwvlaBGA4BAQEBCQsJCRQDJYIfAQEFOEABEAsYCRYPCQMCAQIBRQYNAQUCAQEXh3+wT45ajWiBMgeDTwOXHoYTjWlBgXE X-IronPort-AV: E=Sophos;i="4.87,580,1363129200"; d="scan'208";a="15449258" Received: from msa02.smtpout.orange.fr (HELO msa.smtpout.orange.fr) ([193.252.23.211]) by mail2-smtp-roc.national.inria.fr with ESMTP; 30 Apr 2013 10:02:47 +0200 Received: from [192.168.1.106] ([86.195.153.11]) by mwinf5d57 with ME id W82n1l0090F12tA0382nVw; Tue, 30 Apr 2013 10:02:47 +0200 Message-ID: <517F7AA7.1020108@frisch.fr> Date: Tue, 30 Apr 2013 10:02:47 +0200 From: Alain Frisch User-Agent: Mozilla/5.0 (X11; Linux i686 on x86_64; rv:21.0) Gecko/20100101 Thunderbird/21.0 MIME-Version: 1.0 To: Jacques Garrigue CC: OCaML List Mailing 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> <517F6BB9.4070703@frisch.fr> In-Reply-To: Content-Type: text/plain; charset=windows-1252; format=flowed Content-Transfer-Encoding: 7bit Subject: Re: [Caml-list] Request for feedback: A problem with injectivity and GADTs On 04/30/2013 09:56 AM, Jacques Garrigue wrote: > On 2013/04/30, at 15:59, Alain Frisch wrote: > >> It's reassuring to see that the conservative solution (not assuming injectivity of user defined abstract types) does not seem too bad for now, even if not very satisfying. >> >> I'm only concerned with: >> >>> 3) The problem I describe in my first mail. I.e. when defining a type, >>> if you use type variables appearing in constrained type parameters, >>> you need the type constructors leading to the type variables to be >>> injective. This is PR#5985, and it is only fixed in branches/non-vanishing. >> >> Do you think that fixing this unsoundness (without injectivity annotations) would lead to reject existing programs? > > Potentially yes. > But I don't know how it is in practice for code existing now. > Hence my question. Apart from GADTs, does your patch address the unsoundness with type constraints? Alain