Re: [Caml-list] GADT existential escape

["Daniel Bünzli" <daniel.buenzli@erratique.ch>]

Thanks Jerem{y,ie} for the answers !  

Now I'm naively trying to backport this using exceptions — I'm conservative and old fashioned. But I'm failing to type this Eq value, any hints maybe ?  

module W : sig
  type 'a t
  val w : 'a t
end = struct
  type 'a t = unit
  let w = ()
end

module type W = sig
  type t
  exception E of t W.t
end

type 'a witness = (module W with type t = 'a)

let witness () (type s) =
  let module M = struct
    type t = s
    exception E of t W.t
  end
  in
  (module M : W with type t = s)

type ('a, 'b) eq = Eq : ('a, 'a) eq

let eq (type r) (type s) (r : r witness) (s : s witness)
  : (r, s) eq option
  =
  let module R = (val r : W with type t = r) in
  let module S = (val s : W with type t = s) in
  match R.E W.w with
  | S.E _ -> Some Eq (* Compiler screams here. *)
  | _ -> None



N.B. As it stands this is slightly less efficient than using open variants, since you'd have to allocate an exn value for checking equality.  

Best,

Daniel