From mboxrd@z Thu Jan 1 00:00:00 1970 Return-Path: X-Spam-Checker-Version: SpamAssassin 3.1.3 (2006-06-01) on yquem.inria.fr X-Spam-Level: * X-Spam-Status: No, score=1.1 required=5.0 tests=AWL,SPF_NEUTRAL autolearn=disabled version=3.1.3 X-Original-To: caml-list@yquem.inria.fr Delivered-To: caml-list@yquem.inria.fr Received: from mail4-relais-sop.national.inria.fr (mail4-relais-sop.national.inria.fr [192.134.164.105]) by yquem.inria.fr (Postfix) with ESMTP id B6D46BC6B for ; Mon, 11 Feb 2008 21:46:20 +0100 (CET) X-IronPort-Anti-Spam-Filtered: true X-IronPort-Anti-Spam-Result: AgAAAF5CsEdA6aq4mWdsb2JhbACDJI0WAQEBAQEGBAQLCBiUfIQy X-IronPort-AV: E=Sophos;i="4.25,334,1199660400"; d="scan'208";a="22489312" Received: from concorde.inria.fr ([192.93.2.39]) by mail4-smtp-sop.national.inria.fr with ESMTP; 11 Feb 2008 21:46:20 +0100 Received: from mail4-relais-sop.national.inria.fr (mail4-relais-sop.national.inria.fr [192.134.164.105]) by concorde.inria.fr (8.13.6/8.13.6) with ESMTP id m1BKkIY2022488 (version=TLSv1/SSLv3 cipher=RC4-SHA bits=128 verify=OK) for ; Mon, 11 Feb 2008 21:46:20 +0100 X-IronPort-Anti-Spam-Filtered: true X-IronPort-Anti-Spam-Result: AgAAAF5CsEdA6aq4mWdsb2JhbACDJI0WAQEBAQEGBAQLCBiUfIQy X-IronPort-AV: E=Sophos;i="4.25,334,1199660400"; d="scan'208";a="22489311" Received: from rn-out-0910.google.com ([64.233.170.184]) by mail4-smtp-sop.national.inria.fr with ESMTP; 11 Feb 2008 21:46:19 +0100 Received: by rn-out-0910.google.com with SMTP id e24so2108911rng.6 for ; Mon, 11 Feb 2008 12:46:18 -0800 (PST) DKIM-Signature: v=1; a=rsa-sha256; c=relaxed/relaxed; d=gmail.com; s=gamma; h=domainkey-signature:received:received:message-id:date:from:to:subject:cc:in-reply-to:mime-version:content-type:content-transfer-encoding:content-disposition:references; bh=maI2UoHJE0mXHBdW/yTNtLaMKg4uEDA+F53wUtE4nj0=; b=tdLC381bxP0Hx2TU8kUdhDwpp9l74M2bMAyIZdMNM0aO1RP5YFaj2x3et9+p1Z1ztFxDlwUgkmiHce7KU2rubDaaCHya6F9tzMwtZjWcIYNH2idf2mKkjXH77GCMa3rvK4qz763nxJEFhMJ8gpQ+uiz44VJflHjMK+rdAqAuix4= DomainKey-Signature: a=rsa-sha1; c=nofws; d=gmail.com; s=gamma; h=message-id:date:from:to:subject:cc:in-reply-to:mime-version:content-type:content-transfer-encoding:content-disposition:references; b=MioOF7j8cljeGC51cxJZLex+o+pWCFGVrJkAxh1XiFPLs7tY1XrvX0IzUpe3bUxQavNbFhl1rGOlqLbIJOobGD4FI/smPN3liQc931xaZTOa6XWBIDkSB+0TrMartji0JOJgoke8UG6Eeu0O7K5ioFLbRaIBe0gUNMXlMCmDfbc= Received: by 10.142.226.2 with SMTP id y2mr395276wfg.64.1202762777150; Mon, 11 Feb 2008 12:46:17 -0800 (PST) Received: by 10.142.114.8 with HTTP; Mon, 11 Feb 2008 12:46:17 -0800 (PST) Message-ID: Date: Mon, 11 Feb 2008 15:46:17 -0500 From: "Markus Mottl" To: "Stephen Weeks" Subject: Re: [Caml-list] type unsoundness with constraints and polymorphic variants Cc: caml-list@inria.fr In-Reply-To: <18352.43565.401296.820373@nyc-qws-r03.delacy.com> MIME-Version: 1.0 Content-Type: text/plain; charset=ISO-8859-1 Content-Transfer-Encoding: 7bit Content-Disposition: inline References: <18352.43565.401296.820373@nyc-qws-r03.delacy.com> X-Miltered: at concorde with ID 47B0B41A.000 by Joe's j-chkmail (http://j-chkmail . ensmp . fr)! X-Spam: no; 0.00; markus:01 mottl:01 markus:01 mottl:01 variants:01 bug:01 segfault:01 segfault:01 unification:01 ocaml:01 polymorphic:01 polymorphic:01 wrote:01 compile:01 caml-list:01 On Feb 11, 2008 3:03 PM, Stephen Weeks wrote: > Here is a distillation of the bug. If you compile this, you get a > warning about line 11 being an unused case. If you then run the > resulting executable, you get a segfault. Line 11 can obviously be deleted, the segfault still persists. The unsoundness seems to appear when the signature constraint is applied to the module. It should fail, because the identity function is clearly not a valid instance of this type, since `X can be passed to it and it would just be returned, thus violating the return type. It seems that constraints on polymorphic variables are not handled correctly during the unification of the contents of the module with its signature. Regards, Markus -- Markus Mottl http://www.ocaml.info markus.mottl@gmail.com