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 B6F8F7EE51 for ; Sat, 4 May 2013 08:47:00 +0200 (CEST) Received-SPF: None (mail3-smtp-sop.national.inria.fr: no sender authenticity information available from domain of garrigue@math.nagoya-u.ac.jp) identity=pra; client-ip=133.6.130.5; receiver=mail3-smtp-sop.national.inria.fr; envelope-from="garrigue@math.nagoya-u.ac.jp"; x-sender="garrigue@math.nagoya-u.ac.jp"; x-conformance=sidf_compatible Received-SPF: None (mail3-smtp-sop.national.inria.fr: no sender authenticity information available from domain of garrigue@math.nagoya-u.ac.jp) identity=mailfrom; client-ip=133.6.130.5; receiver=mail3-smtp-sop.national.inria.fr; envelope-from="garrigue@math.nagoya-u.ac.jp"; x-sender="garrigue@math.nagoya-u.ac.jp"; x-conformance=sidf_compatible Received-SPF: None (mail3-smtp-sop.national.inria.fr: no sender authenticity information available from domain of postmaster@mailhost.math.nagoya-u.ac.jp) identity=helo; client-ip=133.6.130.5; receiver=mail3-smtp-sop.national.inria.fr; envelope-from="garrigue@math.nagoya-u.ac.jp"; x-sender="postmaster@mailhost.math.nagoya-u.ac.jp"; x-conformance=sidf_compatible X-IronPort-Anti-Spam-Filtered: true X-IronPort-Anti-Spam-Result: Ar0BAF6thFGFBoIFnGdsb2JhbABQgz6/PIESDgEBAQEBCBQJPIIfAQEEASccATcDCws0ElcGE4gGBQ2vd4RFAoVNhzYHjn46gnJhiRuOFIEmkyg X-IPAS-Result: Ar0BAF6thFGFBoIFnGdsb2JhbABQgz6/PIESDgEBAQEBCBQJPIIfAQEEASccATcDCws0ElcGE4gGBQ2vd4RFAoVNhzYHjn46gnJhiRuOFIEmkyg X-IronPort-AV: E=Sophos;i="4.87,609,1363129200"; d="scan'208";a="13176467" Received: from rabbit.math.nagoya-u.ac.jp (HELO mailhost.math.nagoya-u.ac.jp) ([133.6.130.5]) by mail3-smtp-sop.national.inria.fr with ESMTP; 04 May 2013 08:46:58 +0200 Received: from mailhost.math.nagoya-u.ac.jp (localhost [127.0.0.1]) by mailhost.math.nagoya-u.ac.jp (Postfix) with ESMTP id D9220638C for ; Sat, 4 May 2013 15:46:54 +0900 (JST) Received: from mailhost.math.nagoya-u.ac.jp (localhost [127.0.0.1]) by mailhost.math.nagoya-u.ac.jp (Postfix) with ESMTP id 688A2396E for ; Sat, 4 May 2013 15:46:54 +0900 (JST) DomainKey-Signature: h=Received:Content-Type:Mime-Version:Subject:From:In-Reply-To:Date:Content-Transfer-Encoding:Message-Id:References:To:X-Mailer; b=; c=nofws; d=math.nagoya-u.ac.jp; q=; s=alpha Received: from tet.garrigue.jp (58x158x128x157.ap58.ftth.ucom.ne.jp [58.158.128.157]) by mailhost.math.nagoya-u.ac.jp (Postfix) with ESMTPSA id 31B4E252A for ; Sat, 4 May 2013 15:46:54 +0900 (JST) Content-Type: text/plain; charset=windows-1252 Mime-Version: 1.0 (Mac OS X Mail 6.3 \(1503\)) From: Jacques Garrigue In-Reply-To: <0BC2A384-6D0F-49F2-BD68-5C840BA0888A@math.nagoya-u.ac.jp> Date: Sat, 4 May 2013 15:46:54 +0900 Content-Transfer-Encoding: quoted-printable Message-Id: <44ACA8B7-8DCC-4948-8D8A-7C7A7FB0B4AF@math.nagoya-u.ac.jp> References: <00C57DF0-C6F0-4EDE-8607-2155F3A17146@math.nagoya-u.ac.jp> <517E2818.5040506@frisch.fr> <1EA5B7CE-C0C3-4113-9F8F-C4C3BC888D49@math.nagoya-u.ac.jp> <0BC2A384-6D0F-49F2-BD68-5C840BA0888A@math.nagoya-u.ac.jp> To: OCaML List Mailing X-Mailer: Apple Mail (2.1503) Subject: Re: [Caml-list] Request for feedback: A problem with injectivity and GADTs On 2013/04/30, at 14:45, Jacques Garrigue wr= ote: > I have now committed in trunk a fix to PR#5985. > You can use it to test whether your codebase runs into problems. > You can either obtain it from subversion directly > svn checkout http://caml.inria.fr/svn/ocaml/trunk > or use opam to do it for you. >=20 > I checked that at least Core itself compiles without problems. Ironically, I have just found that lablgtk2 does not compile with the fixed= version. lablgtk2 does not use GADTs, but it uses constrained type parameters in cla= sses. The problem is as follows: gobject.mli: type -'a gobj gContainer.mli: class virtual ['a] item_container : object constraint 'a =3D < as_item : [>`widget] obj; .. > method add : 'a -> unit =85 end File "gContainer.mli", line 126, characters 6-665: Error: In this definition, a type variable cannot be deduced from the type parameters. It is a bit surprising, since the said variable is the row variable of the above [> `widget], and it is only referred through 'a. The reason there is an error is that the checkability requirements for the body of types and constrained type parameters differ: to allow the row variable to appear in a position potentially contravariant, we need it to know from the constraint that it appears for sure in a negative or invariant position. One way to solve this is to check that the type identified by 'a can actually be handled as a real variable (its internal variables do not occur out of it), which would solve the discrepancy. However, checking this is going to be a pain. And making gobj injective immediately solves the problem. In the midtime, the problem is fixed in the git version of lablgtk2 by pretending that gobj is a private sum type (whose contents are abstract). This also empasizes that the new restriction does not impact only GADTs: all constrained type parameters are also concerned. Jacques Garrigue=