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 mail2-relais-roc.national.inria.fr (mail2-relais-roc.national.inria.fr [192.134.164.83]) by sympa.inria.fr (Postfix) with ESMTPS id BC7C47EE51 for ; Sat, 4 May 2013 09:09:47 +0200 (CEST) Received-SPF: None (mail2-smtp-roc.national.inria.fr: no sender authenticity information available from domain of gabriel.scherer@gmail.com) identity=pra; client-ip=209.85.214.43; receiver=mail2-smtp-roc.national.inria.fr; envelope-from="gabriel.scherer@gmail.com"; x-sender="gabriel.scherer@gmail.com"; x-conformance=sidf_compatible Received-SPF: Pass (mail2-smtp-roc.national.inria.fr: domain of gabriel.scherer@gmail.com designates 209.85.214.43 as permitted sender) identity=mailfrom; client-ip=209.85.214.43; receiver=mail2-smtp-roc.national.inria.fr; envelope-from="gabriel.scherer@gmail.com"; x-sender="gabriel.scherer@gmail.com"; x-conformance=sidf_compatible; x-record-type="v=spf1" Received-SPF: None (mail2-smtp-roc.national.inria.fr: no sender authenticity information available from domain of postmaster@mail-bk0-f43.google.com) identity=helo; client-ip=209.85.214.43; receiver=mail2-smtp-roc.national.inria.fr; envelope-from="gabriel.scherer@gmail.com"; x-sender="postmaster@mail-bk0-f43.google.com"; x-conformance=sidf_compatible X-IronPort-Anti-Spam-Filtered: true X-IronPort-Anti-Spam-Result: AkICAGuzhFHRVdYrjWdsb2JhbABQDoMwrSSSG3QIFg4BAQEBBwsLCRIGJIIfAQEEAScZARsSCwEDAQsGBQsNDSEiAREBBQEKEgYTEodnAQMJBgylAIw7gn6EMwoZJwMKWIcqAQUMjnIzB4NTA5csgSaOJxYpg3RBOg X-IPAS-Result: AkICAGuzhFHRVdYrjWdsb2JhbABQDoMwrSSSG3QIFg4BAQEBBwsLCRIGJIIfAQEEAScZARsSCwEDAQsGBQsNDSEiAREBBQEKEgYTEodnAQMJBgylAIw7gn6EMwoZJwMKWIcqAQUMjnIzB4NTA5csgSaOJxYpg3RBOg X-IronPort-AV: E=Sophos;i="4.87,610,1363129200"; d="scan'208";a="16018180" Received: from mail-bk0-f43.google.com ([209.85.214.43]) by mail2-smtp-roc.national.inria.fr with ESMTP/TLS/RC4-SHA; 04 May 2013 09:09:47 +0200 Received: by mail-bk0-f43.google.com with SMTP id jm19so972830bkc.16 for ; Sat, 04 May 2013 00:09:46 -0700 (PDT) DKIM-Signature: v=1; a=rsa-sha256; c=relaxed/relaxed; d=gmail.com; s=20120113; h=x-received:mime-version:in-reply-to:references:from:date:message-id :subject:to:cc:content-type:content-transfer-encoding; bh=4mWQyT6Oq0+r3Aqzq248F6T4W0WPYpa/CMxKHrNu0RU=; b=dr113RXTAsjIHXyVgniKLJD/SjDs7J93o+xn4j7cGQE2VDrZpkUztwyDEJrPGmNhjM fSTmn7yaHq54lGkT/IvrGKPe7W/nND0g5WBzTNxQ8+xfsbm0NKCWaDW7lSnYCbmEVo0f clKpkIvcTaSMe2vLbwrHaAGNTofxirmdyC0jT+Q16j9HHHQ160weN2Sn3GMrKSBZ6qLX ROAubNLBsaE8xsfsGD19/IFXe7RIFTXHuxKNHZWewdfsKnZVbMCRoxGOh7CyhbInv3L4 j8cvZ+gxTNlG77IttJlAqpCnbPh1b5S7t1CAPpGOjeAdscK+VrZocYGI7eF19aMzW/PB uvTg== X-Received: by 10.205.118.203 with SMTP id fr11mr4698413bkc.103.1367651386653; Sat, 04 May 2013 00:09:46 -0700 (PDT) MIME-Version: 1.0 Received: by 10.205.83.144 with HTTP; Sat, 4 May 2013 00:09:06 -0700 (PDT) In-Reply-To: <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> <44ACA8B7-8DCC-4948-8D8A-7C7A7FB0B4AF@math.nagoya-u.ac.jp> From: Gabriel Scherer Date: Sat, 4 May 2013 09:09:06 +0200 Message-ID: To: Jacques Garrigue Cc: OCaML List Mailing Content-Type: text/plain; charset=windows-1252 Content-Transfer-Encoding: quoted-printable Subject: Re: [Caml-list] Request for feedback: A problem with injectivity and GADTs > 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. If I understand correctly, you are saying that this "constraint", in absence of injectivity, could be handled semantically like GADTs with non-injective equations, that is as quantifying locally on a ("true") existential variable? Handling existential variables (in fact local type constructors) attached to GADT constructors is well-understood as they have clear introduction sites and scopes, exactly where their constructor is matched. When you say that checking the "constraint" case is painful, is it related to the fact that there is no such corresponding term-level marker? On Sat, May 4, 2013 at 8:46 AM, Jacques Garrigue wrote: > On 2013/04/30, at 14:45, Jacques Garrigue = wrote: > >> 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. >> >> I checked that at least Core itself compiles without problems. > > Ironically, I have just found that lablgtk2 does not compile with the fix= ed version. > lablgtk2 does not use GADTs, but it uses constrained type parameters in c= lasses. > > 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 > -- > Caml-list mailing list. Subscription management and archives: > https://sympa.inria.fr/sympa/arc/caml-list > Beginner's list: http://groups.yahoo.com/group/ocaml_beginners > Bug reports: http://caml.inria.fr/bin/caml-bugs