Version française
Home     About     Download     Resources     Contact us    
Browse thread
type unsoundness with constraints and polymorphic variants
[ Home ] [ Index: by date | by threads ]
[ Search: ]

[ 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 ()