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: | Stephen Weeks <sweeks@j...> |
| Subject: | type unsoundness with constraints and polymorphic variants |
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 ()