Browse thread
type unsoundness with constraints and polymorphic variants
[
Home
]
[ Index:
by date
|
by threads
]
[ Message by date: previous | next ] [ Message in thread: previous | next ] [ Thread: previous | next ]
[ Message by date: previous | next ] [ Message in thread: previous | next ] [ Thread: previous | next ]
| Date: | -- (:) |
| From: | Jacques Garrigue <garrigue@m...> |
| Subject: | Re: [Caml-list] type unsoundness with constraints and polymorphic variants |
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...