From mboxrd@z Thu Jan 1 00:00:00 1970 Return-Path: X-Original-To: caml-list@sympa.inria.fr Delivered-To: caml-list@sympa.inria.fr Received: from mail3-relais-sop.national.inria.fr (mail3-relais-sop.national.inria.fr [192.134.164.104]) by sympa.inria.fr (Postfix) with ESMTPS id 304007FC86 for ; Thu, 19 Mar 2015 12:36:33 +0100 (CET) Received-SPF: None (mail3-smtp-sop.national.inria.fr: no sender authenticity information available from domain of daniel.buenzli@erratique.ch) identity=pra; client-ip=74.55.86.74; receiver=mail3-smtp-sop.national.inria.fr; envelope-from="daniel.buenzli@erratique.ch"; x-sender="daniel.buenzli@erratique.ch"; x-conformance=sidf_compatible Received-SPF: None (mail3-smtp-sop.national.inria.fr: no sender authenticity information available from domain of daniel.buenzli@erratique.ch) identity=mailfrom; client-ip=74.55.86.74; receiver=mail3-smtp-sop.national.inria.fr; envelope-from="daniel.buenzli@erratique.ch"; x-sender="daniel.buenzli@erratique.ch"; x-conformance=sidf_compatible Received-SPF: None (mail3-smtp-sop.national.inria.fr: no sender authenticity information available from domain of postmaster@smtp.webfaction.com) identity=helo; client-ip=74.55.86.74; receiver=mail3-smtp-sop.national.inria.fr; envelope-from="daniel.buenzli@erratique.ch"; x-sender="postmaster@smtp.webfaction.com"; x-conformance=sidf_compatible X-IronPort-Anti-Spam-Filtered: true X-IronPort-Anti-Spam-Result: A0A1AAC8swpVm0pWN0pchz/IfQKCFQEBAQEBAREBAQEBAQYLCwkULoQQAQUjBFIQCxoCJgICRxAGARqIJwSxSpt+AQEBBwEBAQEBHYEhiXaEPjMHgmgvgRYBBKEqD40lhBGDMQEBAQ X-IPAS-Result: A0A1AAC8swpVm0pWN0pchz/IfQKCFQEBAQEBAREBAQEBAQYLCwkULoQQAQUjBFIQCxoCJgICRxAGARqIJwSxSpt+AQEBBwEBAQEBHYEhiXaEPjMHgmgvgRYBBKEqD40lhBGDMQEBAQ X-IronPort-AV: E=Sophos;i="5.11,429,1422918000"; d="scan'208";a="103971788" Received: from mail6.webfaction.com (HELO smtp.webfaction.com) ([74.55.86.74]) by mail3-smtp-sop.national.inria.fr with ESMTP; 19 Mar 2015 12:36:32 +0100 Received: from [172.20.10.2] (27.233.197.178.dynamic.wless.lssmb00p-cgnat.res.cust.swisscom.ch [178.197.233.27]) by smtp.webfaction.com (Postfix) with ESMTP id 4ADAD20F3A6A; Thu, 19 Mar 2015 11:34:32 +0000 (UTC) Date: Thu, 19 Mar 2015 12:34:28 +0100 From: =?utf-8?Q?Daniel_B=C3=BCnzli?= To: Jeremy Yallop , Jeremie Dimino Cc: =?utf-8?Q?Milan_Stanojevi=C4=87?= , Caml-list Message-ID: <87E7B1EBF3144E7C844448D0F5EBB407@erratique.ch> In-Reply-To: References: <2AB388B4D07D4DDABA30298A7C890319@erratique.ch> <596DAEC11B474882835CEA10AAACE35E@erratique.ch> X-Mailer: sparrow 1.6.4 (build 1178) MIME-Version: 1.0 Content-Type: text/plain; charset="utf-8" Content-Transfer-Encoding: quoted-printable Content-Disposition: inline Subject: Re: [Caml-list] GADT existential escape Thanks Jerem{y,ie} for the answers !=20=20 Now I'm naively trying to backport this using exceptions =E2=80=94 I'm cons= ervative and old fashioned. But I'm failing to type this Eq value, any hint= s maybe ?=20=20 module W : sig type 'a t val w : 'a t end =3D struct type 'a t =3D unit let w =3D () end module type W =3D sig type t exception E of t W.t end type 'a witness =3D (module W with type t =3D 'a) let witness () (type s) =3D let module M =3D struct type t =3D s exception E of t W.t end in (module M : W with type t =3D s) type ('a, 'b) eq =3D Eq : ('a, 'a) eq let eq (type r) (type s) (r : r witness) (s : s witness) : (r, s) eq option =3D let module R =3D (val r : W with type t =3D r) in let module S =3D (val s : W with type t =3D 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.=20=20 Best, Daniel