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 4ACEA81792 for ; Thu, 4 Jul 2013 10:14:10 +0200 (CEST) Received-SPF: None (mail3-smtp-sop.national.inria.fr: no sender authenticity information available from domain of alain@frisch.fr) identity=pra; client-ip=193.252.23.211; receiver=mail3-smtp-sop.national.inria.fr; envelope-from="alain@frisch.fr"; x-sender="alain@frisch.fr"; x-conformance=sidf_compatible Received-SPF: None (mail3-smtp-sop.national.inria.fr: no sender authenticity information available from domain of alain@frisch.fr) identity=mailfrom; client-ip=193.252.23.211; receiver=mail3-smtp-sop.national.inria.fr; envelope-from="alain@frisch.fr"; x-sender="alain@frisch.fr"; x-conformance=sidf_compatible Received-SPF: None (mail3-smtp-sop.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=mail3-smtp-sop.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: AsEAAPkt1VHB/BfTlGdsb2JhbABaDoMuvhSCc4EbDgEBAQEJCwkJFAMlgiMBAQQBMgEFQQULCxgJJQ8CRgYNAQcBAYgFCrl0j2sHg20Dl0mGIY13QA X-IPAS-Result: AsEAAPkt1VHB/BfTlGdsb2JhbABaDoMuvhSCc4EbDgEBAQEJCwkJFAMlgiMBAQQBMgEFQQULCxgJJQ8CRgYNAQcBAYgFCrl0j2sHg20Dl0mGIY13QA X-IronPort-AV: E=Sophos;i="4.87,993,1363129200"; d="scan'208";a="19965726" Received: from msa02.smtpout.orange.fr (HELO msa.smtpout.orange.fr) ([193.252.23.211]) by mail3-smtp-sop.national.inria.fr with ESMTP; 04 Jul 2013 10:14:09 +0200 Received: from [192.168.1.111] ([92.151.124.168]) by mwinf5d38 with ME id w8E91l0033e6krg038E9KX; Thu, 04 Jul 2013 10:14:09 +0200 Message-ID: <51D52ED1.30808@frisch.fr> Date: Thu, 04 Jul 2013 10:14:09 +0200 From: Alain Frisch User-Agent: Mozilla/5.0 (X11; Linux i686 on x86_64; rv:22.0) Gecko/20100101 Thunderbird/22.0 MIME-Version: 1.0 To: Jacques Garrigue CC: OCaML List Mailing References: <00C57DF0-C6F0-4EDE-8607-2155F3A17146@math.nagoya-u.ac.jp> <51D19680.4060609@frisch.fr> <3BB0E3A0-455F-40D0-AA97-621AB7D24E4B@math.nagoya-u.ac.jp> <51D44C85.3040308@frisch.fr> <4AA00D93-1FD9-4E5B-9960-959BA835E8E5@math.nagoya-u.ac.jp> In-Reply-To: <4AA00D93-1FD9-4E5B-9960-959BA835E8E5@math.nagoya-u.ac.jp> Content-Type: text/plain; charset=windows-1252; format=flowed Content-Transfer-Encoding: 8bit Subject: Re: [Caml-list] Request for feedback: A problem with injectivity and GADTs On 07/04/2013 03:00 AM, Jacques Garrigue wrote: > In theory, it would be OK to assume that all pattern-matchings may contain GADT type constructors. > The only real problem is with let's: if they contain GADTs, we must use the code for pattern-matching, which doesn't handle unused definition warnings in the same way… Having all non recursive let's go through this code would have a high impact on warnings. If this is the only problem with the direct approach (not depending on backtracking), maybe the treatment of warnings can be parametrized to behave as expected? > If unused definition warnings could be separated from type checking this would be much easier. Maybe I'm wrong, but it seems to me that achieving the same behavior would require to duplicate of lot of the "data-flow" logic in the type-checker, thus increasing the global complexity (and the risk to have diverging behaviors). Alain