From mboxrd@z Thu Jan  1 00:00:00 1970
Return-Path: <garrigue@math.nagoya-u.ac.jp>
X-Spam-Checker-Version: SpamAssassin 3.1.3 (2006-06-01) on yquem.inria.fr
X-Spam-Level: 
X-Spam-Status: No, score=0.4 required=5.0 tests=AWL,DNS_FROM_RFC_ABUSE 
	autolearn=disabled version=3.1.3
X-Original-To: caml-list@yquem.inria.fr
Delivered-To: caml-list@yquem.inria.fr
Received: from mail2-relais-roc.national.inria.fr (mail2-relais-roc.national.inria.fr [192.134.164.83])
	by yquem.inria.fr (Postfix) with ESMTP id 9522BBC6B
	for <caml-list@yquem.inria.fr>; Tue, 12 Feb 2008 05:22:34 +0100 (CET)
X-IronPort-Anti-Spam-Filtered: true
X-IronPort-Anti-Spam-Result: AgAAALitsEfAXQImh2dsb2JhbACQPQEBAQgKKZoM
X-IronPort-AV: E=Sophos;i="4.25,337,1199660400"; 
   d="scan'208";a="7207447"
Received: from discorde.inria.fr ([192.93.2.38])
  by mail2-smtp-roc.national.inria.fr with ESMTP; 12 Feb 2008 05:22:34 +0100
Received: from mail1-relais-roc.national.inria.fr (mail1-relais-roc.national.inria.fr [192.134.164.82])
	by discorde.inria.fr (8.13.6/8.13.6) with ESMTP id m1C4MVOR013198
	(version=TLSv1/SSLv3 cipher=RC4-SHA bits=128 verify=OK)
	for <caml-list@inria.fr>; Tue, 12 Feb 2008 05:22:34 +0100
X-IronPort-Anti-Spam-Filtered: true
X-IronPort-Anti-Spam-Result: Ao8CALitsEeCNhAB/2dsb2JhbACrBw
X-IronPort-AV: E=Sophos;i="4.25,337,1199660400"; 
   d="scan'208";a="7951358"
Received: from kurims.kurims.kyoto-u.ac.jp ([130.54.16.1])
  by mail1-smtp-roc.national.inria.fr with ESMTP; 12 Feb 2008 05:22:32 +0100
Received: from localhost (orion [130.54.16.5])
	by kurims.kurims.kyoto-u.ac.jp (8.13.8/8.13.8) with ESMTP id m1C4MSFT008174;
	Tue, 12 Feb 2008 13:22:29 +0900 (JST)
Date: Tue, 12 Feb 2008 13:22:25 +0900 (JST)
Message-Id: <20080212.132225.27792058.garrigue@math.nagoya-u.ac.jp>
To: sweeks@janestcapital.com
Cc: caml-list@inria.fr
Subject: Re: [Caml-list] type unsoundness with constraints and polymorphic
 variants
From: Jacques Garrigue <garrigue@math.nagoya-u.ac.jp>
In-Reply-To: <18352.43565.401296.820373@nyc-qws-r03.delacy.com>
References: <18352.43565.401296.820373@nyc-qws-r03.delacy.com>
X-Mailer: Mew version 4.2 on Emacs 22.1 / Mule 5.0 (SAKAKI)
Mime-Version: 1.0
Content-Type: Text/Plain; charset=us-ascii
Content-Transfer-Encoding: 7bit
X-Miltered: at discorde with ID 47B11F07.000 by Joe's j-chkmail (http://j-chkmail . ensmp . fr)!
X-Spam: no; 0.00; variants:01 ocaml:01 segfault:01 runtime:01 read-only:01 bug:01 segfault:01 sig:01 val:01 struct:01 bug:01 sig:01 val:01 struct:01 cvs:01 

From: "Stephen Weeks" <sweeks@janestcapital.com>
> We've hit a type unsoundness in OCaml that can easily cause a segfault
> at runtime.  It came up in some code that uses phantom types to
> express whether or not a structure can be mutated and the identity
> functions to convert from a read-write object to a read-only view.
> 
> 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.
> 
> -----------------------------------------------------------------------------
> type 'a t = 'a constraint 'a = [< `X | `Y of unit -> unit ]
> 
> module M : sig
>   val f : 'a t -> [ `Y of unit -> unit ] t
> end = struct
>   let f x = x
> end
> 
> let () =
>   match M.f `X with
>   | `X -> ()  (* line 11 *)
>   | `Y f -> f ()

Thanks for the report. It's so clearly a bug that it's strange it was
not found earlier :-(
A shorter version (without constraints) is:

  module M : sig val f : [< `A | `B] -> [`A] end = struct let f x = x end

This is now fixed in CVS, and should go in 3.10.2.

Cheers,

Jacques Garrigue

BTW, there is a bug tracking system...