Re: [Caml-list] type unsoundness with constraints and polymorphic variants

[Jacques Garrigue <garrigue@math.nagoya-u.ac.jp>]

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...