From mboxrd@z Thu Jan 1 00:00:00 1970 Received: from mail4-relais-sop.national.inria.fr (mail4-relais-sop.national.inria.fr [192.134.164.105]) by walapai.inria.fr (8.13.6/8.13.6) with ESMTP id pBDJFrod027522 for ; Tue, 13 Dec 2011 20:15:53 +0100 X-IronPort-Anti-Spam-Filtered: true X-IronPort-Anti-Spam-Result: AtAEAAmk505ii1vQaWdsb2JhbAA2DZpkkF0NCQsHGSKBbQUBAQQBCyAVAQIVIQEBAwsGBUYvAQ4BBhIGiA8CpGoKgmGEYIkwAQYKAYtYBIgwjEiFRipIiC6DXQ X-IronPort-AV: E=Sophos;i="4.71,347,1320620400"; d="scan'208";a="123242002" Received: from nm15-vm0.bullet.mail.sp2.yahoo.com ([98.139.91.208]) by mail4-smtp-sop.national.inria.fr with SMTP; 13 Dec 2011 20:15:47 +0100 Received: from [98.139.91.61] by nm15.bullet.mail.sp2.yahoo.com with NNFMP; 13 Dec 2011 19:15:45 -0000 Received: from [98.139.91.37] by tm1.bullet.mail.sp2.yahoo.com with NNFMP; 13 Dec 2011 19:15:45 -0000 Received: from [127.0.0.1] by omp1037.mail.sp2.yahoo.com with NNFMP; 13 Dec 2011 19:15:45 -0000 X-Yahoo-Newman-Property: ymail-3 X-Yahoo-Newman-Id: 719972.98972.bm@omp1037.mail.sp2.yahoo.com Received: (qmail 4186 invoked by uid 60001); 13 Dec 2011 19:15:45 -0000 DKIM-Signature: v=1; a=rsa-sha256; c=relaxed/relaxed; d=yahoo.com; s=s1024; t=1323803745; bh=pw0ZBJ1OgBHJinHQF3eX5NgIOptsqj9lzghOZQFwCRw=; h=X-YMail-OSG:Received:X-Mailer:References:Message-ID:Date:From:Reply-To:Subject:To:Cc:In-Reply-To:MIME-Version:Content-Type:Content-Transfer-Encoding; b=vqy7BJSAJSmtRSGN5oNa++6L1U77vTv7WzYz8ANf41CPdsIxE8M/ij9/n2e348OUruywz+pTpvpvGlkCefcTf1zEpud4hKYcztNUb8a4g0XC9HmpAQiHs7RZcs51s/QMOjTn6/Nx9VQZfeCOaPhu0qABg+px+xB3B7Fv7HI9slw= DomainKey-Signature: a=rsa-sha1; q=dns; c=nofws; s=s1024; d=yahoo.com; h=X-YMail-OSG:Received:X-Mailer:References:Message-ID:Date:From:Reply-To:Subject:To:Cc:In-Reply-To:MIME-Version:Content-Type:Content-Transfer-Encoding; b=YgfbDv48FhGm0TSfSJUVblSZLQgJkfN2itesE/yY8prBRm3Ym6LPUFjhaqZRrmPVrP8fwfC0EC2kIxEGGwT4XAAggs4zDlmEeEsiflIhw3781miDqmlGqqeVX0BTns8zI77ODhHAvMSFQUC5iMRKTWbY6rlu2cAk9vtBtJVfvJU=; X-YMail-OSG: MBMcugAVM1neKiJCzfmC_bgS0GBFd9WZsD.bvNx3XP0Lgg8 9FcvOLfyUX1HlXzS6q7Jlwepjgc5c2xd_JpLzZ4B9VgOFWFmORxNRnaqlxEL 8FnXWgOPk3eWFQoIFw7wS.bz6eOjuBciUNCLb75a5OLrixTTir8ADrRzWM4t x8V2fuJvQdBSpTVpk4X_691jZoVoJTdwvStAoZYvRLG11teVySjmPNDULhi. cSvrb4W.OpW2RMGVo1PzldcKt2uK1edNOj3d.wH4Hmz1dLJbzl6mP8G98QaW g9u_yR7EIJM_S382_bo4m889LmLuEWryMwLzR6j7BEYGxWQp9xJr4vBcN8eC Autt9Gw7Ezz8yXB9X30ZeblMoURDItt9kqZN6cBue1Jz87XqiAu6GUMY_Hrk cVrBQ1DMrHHCbnvkB7WtPXP4QFDKxYLSWJxmdWEjDkixwp.AUnl7pSktmFDG yXVMmY1JsGaxUPUKVOY8QbcxGtQFh7zg- Received: from [195.23.39.232] by web111502.mail.gq1.yahoo.com via HTTP; Tue, 13 Dec 2011 11:15:45 PST X-Mailer: YahooMailWebService/0.8.115.331698 References: <1323786905.94413.YahooMailNeo@web111503.mail.gq1.yahoo.com> Message-ID: <1323803745.3632.YahooMailNeo@web111502.mail.gq1.yahoo.com> Date: Tue, 13 Dec 2011 11:15:45 -0800 (PST) From: Dario Teixeira Reply-To: Dario Teixeira To: Jacques Le Normand Cc: caml In-Reply-To: MIME-Version: 1.0 Content-Type: text/plain; charset=iso-8859-1 Content-Transfer-Encoding: 8bit X-MIME-Autoconverted: from quoted-printable to 8bit by walapai.inria.fr id pBDJFrod027522 Subject: Re: [Caml-list] PV-GADTs Hi, > The way GADTs are handled is that local constraints are generated when > patterns are typed and then those constraints are used in the body of > the associated clause. To generate the constraints, we need to > propagate typing information. From my understanding, we can't do this > with polymorphic variants because it would change the typing > algorithm. In other words, with polymorphic variants the type of the > pattern is infered independently of the context. > > From my understanding, Jacques Garrigue has good reasons to reject > propagation in such a case. Personally, I'd like to see a flag, say > -unsafepropagation, to let people use polymorphic variants and GADTs > at their own risk, knowing that the behaviour of the typing algorithm > may not satisfy some expected theoretical properties. Thanks for the clarification.  Mind you, my question did not stem from any actual need for PV-GADTS; it was pure curiosity... Cheers, Dario