From mboxrd@z Thu Jan 1 00:00:00 1970 Return-Path: Received: from mail2-relais-roc.national.inria.fr (mail2-relais-roc.national.inria.fr [192.134.164.83]) by c5ff346549e7 (Postfix) with ESMTPS id CC3915D4 for ; Wed, 8 Apr 2020 09:47:44 +0000 (UTC) X-IronPort-AV: E=Sophos;i="5.72,357,1580770800"; d="scan'208";a="444361514" Received: from sympa.inria.fr ([193.51.193.213]) by mail2-relais-roc.national.inria.fr with ESMTP; 08 Apr 2020 11:47:43 +0200 Received: by sympa.inria.fr (Postfix, from userid 20132) id B723F7F486; Wed, 8 Apr 2020 11:47:43 +0200 (CEST) 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 21E517F449 for ; Wed, 8 Apr 2020 11:45:12 +0200 (CEST) Authentication-Results: mail3-smtp-sop.national.inria.fr; spf=None smtp.pra=jacques.garrigue@gmail.com; spf=Pass smtp.mailfrom=jacques.garrigue@gmail.com; spf=None smtp.helo=postmaster@mail-wr1-f68.google.com IronPort-PHdr: =?us-ascii?q?9a23=3AZNn4QBEyEttf5w8XhC9uR51GYnF86YWxBRYc798d?= =?us-ascii?q?s5kLTJ75p82wAkXT6L1XgUPTWs2DsrQf1LqQ7viocFdDyKjCmUhKSIZLWR4BhJ?= =?us-ascii?q?detC0bK+nBN3fGKuX3ZTcxBsVIWQwt1Xi6NU9IBJS2PAWK8TWapAQfERTnNAdz?= =?us-ascii?q?Ov+9WsuL15z2hKiO/Mj0ZwhHzBm8er52PRKo5VHWssQZqYxhL6czjBzTrS0bVf?= =?us-ascii?q?5RwDZKLFmKghvnrui55oRi/Dld86Yj/sVZTKjhOasxV6ZZAykrG28w7czv8xLE?= =?us-ascii?q?SF3ctTMnTmwKn08QUED+5xbgU8K063Oi77sv6GyhJcTzCIsMd3Gn5qZvRgXvjX?= =?us-ascii?q?5eZTE8+WDTzMd3ifAC+U7zl1lE24fRJbqtGr9mZKqEJIEVQGNAWoBaUCkTWtrh?= =?us-ascii?q?PbtKNPIIOKNjl6e4p1YKqkHjVwylBeeq1SURw3Gojes11OMuFQyA1wslTYoD?= X-IronPort-Anti-Spam-Filtered: true X-IronPort-Anti-Spam-Result: =?us-ascii?q?A0DhAQDEnI1eZ0TdVdFmHAEBAQEBBwEBE?= =?us-ascii?q?QEEBAEBgXuCKWwDUlyEHI8AgWwlg3CHBpBTCgEDAQoBAR8QBAEBhEQCggccBwE?= =?us-ascii?q?ENBMCEAEBBQEBAQIBAgMEARMLCwsGKYVfDII7BQEjAQaDBgEBAQMSEQQZARsdA?= =?us-ascii?q?QMMBgULDQICJgICIxEBBQEcBhMbB4MEAYJKAQMuBAujX4EEPYsofxYFAReDAAW?= =?us-ascii?q?EZQoZJw1iA4EzAgEGCQEIfCqMMw+BTD+BEScMEIJNPoJnAoFlgxIygiwEsDZ6B?= =?us-ascii?q?4JAfASGdY9AFgePLhKMSItEjSCPS4M4AgQCBAUCBg8jgUaBeU0jUCoBBoI4PhI?= =?us-ascii?q?YDZEiDBeDUIpXPzOOAIFSAQE?= X-IPAS-Result: =?us-ascii?q?A0DhAQDEnI1eZ0TdVdFmHAEBAQEBBwEBEQEEBAEBgXuCKWw?= =?us-ascii?q?DUlyEHI8AgWwlg3CHBpBTCgEDAQoBAR8QBAEBhEQCggccBwEENBMCEAEBBQEBA?= =?us-ascii?q?QIBAgMEARMLCwsGKYVfDII7BQEjAQaDBgEBAQMSEQQZARsdAQMMBgULDQICJgI?= =?us-ascii?q?CIxEBBQEcBhMbB4MEAYJKAQMuBAujX4EEPYsofxYFAReDAAWEZQoZJw1iA4EzA?= =?us-ascii?q?gEGCQEIfCqMMw+BTD+BEScMEIJNPoJnAoFlgxIygiwEsDZ6B4JAfASGdY9AFge?= =?us-ascii?q?PLhKMSItEjSCPS4M4AgQCBAUCBg8jgUaBeU0jUCoBBoI4PhIYDZEiDBeDUIpXP?= =?us-ascii?q?zOOAIFSAQE?= X-IronPort-AV: E=Sophos;i="5.72,357,1580770800"; d="scan'208";a="345340481" X-MGA-submission: =?us-ascii?q?MDF9aIM6gmNOm1oSh4Lz1mXlbfZpEaTNUMjTHf?= =?us-ascii?q?L5VaGYzA3hcj7pA0UZVQiHB4/6fncKeNf/JqkAfPGzEhDdZsYXUQbDqy?= =?us-ascii?q?2lFSIzyKQuw8f3RY9koNqUBkUDAkZXD/9pUYAwK/4PBV4/FrOXUr3Fbk?= =?us-ascii?q?M4wHe6LQkaWQLn0aE2hKsDOA=3D=3D?= Received: from mail-wr1-f68.google.com ([209.85.221.68]) by mail3-smtp-sop.national.inria.fr with ESMTP/TLS/AES256-GCM-SHA384; 08 Apr 2020 11:44:44 +0200 Received: by mail-wr1-f68.google.com with SMTP id a25so7082814wrd.0 for ; Wed, 08 Apr 2020 02:44:44 -0700 (PDT) DKIM-Signature: v=1; a=rsa-sha256; c=relaxed/relaxed; d=gmail.com; s=20161025; h=from:mime-version:subject:in-reply-to:date:cc :content-transfer-encoding:message-id:references:to; bh=2AR5diKwo3wsYFneSCb2LtMJe0Wg7w8tEmimORU/t8g=; b=VbEqz5qGm+LxGezTu4nrOxOdb7dGfDjXmhOIW9YDwmvgm6uC4WlTIwRqvLNZRc8WWv PluVcEJuV+v9iU2FA/Flm+EfETeaFcFDkHz3DIxXLSQX7AzddvbdUTqalY4Z8HJZbqkO kIYYqxyQpqw0dHIetW9zbPuXw8/iT6wS4QeO2T/wyb1EEnHYcDhcBExQXEocamx2qG4P /k6rqOl+xD6n+8kJ4YU6Arb/XGzD2K1865kSrbTlxxqkJ1ubpUQkLuZfNrA5Iki1qnSn BpFinFdyaP8o6Hrrp1jp7NFMGogLgV4XdaxBygu6GcPetyQDoj0u4fOS/jck37lvhr6P iVWw== X-Google-DKIM-Signature: v=1; a=rsa-sha256; c=relaxed/relaxed; d=1e100.net; s=20161025; h=x-gm-message-state:from:mime-version:subject:in-reply-to:date:cc :content-transfer-encoding:message-id:references:to; bh=2AR5diKwo3wsYFneSCb2LtMJe0Wg7w8tEmimORU/t8g=; b=iWNrECrrLaeFYRXOwDFS1l1Kj2ViJ3akq9D48BqGDMu0e8cDZcU8fv+kOn2SFabEbD p1x+fx2ljdu9kD8DVvg102ZN0N62uKo04f385JdNeBIZJa45e+2SOdNJw32dsClOLlL0 b3HivziGDEp13OO7MSCSTn2/Nm1jPUchTMl84sUnhie5ctiXudkbsGHBFG1Htf6TdBgg a2sA6VQdmfKYv3ZS5pf1lqu8bZ5e67bv9fk4pWxdCKAmop2HbYLcWNr4466q3RPl++2T kOt8IsR30seiX23GTT2doh9dudAVgwZpBs1shL1Ci7RCqwBYwjiQplggX+MIfibKZ/3Q cwFA== X-Gm-Message-State: AGi0PuaKTCiRR2pehNZZ6AC2UDk3IYYY5Lk+cJ8Boa9dZYpe0Rq2B0fy u793WqqvrCKqM54TZW2891pSmRfs0o8= X-Google-Smtp-Source: APiQypL4ARXgFd4duSy7RZ9gEePzhlPXOmcMkpsFCpyVPIbOcmm2Zhq5uT+lvqMsggQp9m7VcBhIMA== X-Received: by 2002:adf:80af:: with SMTP id 44mr7740623wrl.241.1586339083987; Wed, 08 Apr 2020 02:44:43 -0700 (PDT) Received: from [192.168.0.21] (ip-111.net-89-2-185.rev.numericable.fr. [89.2.185.111]) by smtp.gmail.com with ESMTPSA id z11sm19739888wrv.58.2020.04.08.02.44.43 (version=TLS1_2 cipher=ECDHE-RSA-AES128-GCM-SHA256 bits=128/128); Wed, 08 Apr 2020 02:44:43 -0700 (PDT) From: Jacques Garrigue X-Google-Original-From: Jacques Garrigue Content-Type: text/plain; charset=utf-8 Mime-Version: 1.0 (Mac OS X Mail 13.0 \(3608.60.0.2.5\)) In-Reply-To: <20200406150849.GA5980@Melchior.localnet> Date: Wed, 8 Apr 2020 11:44:42 +0200 Cc: Mailing List OCaml Content-Transfer-Encoding: quoted-printable Message-Id: References: <20200406150849.GA5980@Melchior.localnet> To: Oleg Kiselyov X-Mailer: Apple Mail (2.3608.60.0.2.5) X-Validation-by: jacques.garrigue@gmail.com Subject: Re: [Caml-list] That dreaded `a type variable cannot be deduced' GADT error Reply-To: Jacques Garrigue X-Loop: caml-list@inria.fr X-Sequence: 18097 Errors-to: caml-list-owner@inria.fr Precedence: list Precedence: bulk Sender: caml-list-request@inria.fr X-no-archive: yes List-Id: List-Archive: List-Help: List-Owner: List-Post: List-Subscribe: List-Unsubscribe: Hi Oleg, That=E2=80=99s an interesting workaround. But I=E2=80=99m not sure doing this transformation silently would be the = right solution, as the behavior is going to be different. I.e., you have forced the definition to be accepted, but it doesn=E2=80=99= t change the problem that the type constructor code is not recognized as = injective. I have a proposal for nominal abstract types, which aims at solving this = problem: https://github.com/ocaml/RFCs/pull/4 Could we discuss possible solutions there? Jacques On 6 Apr 2020, at 17:08, Oleg wrote: >=20 >=20 > The following seemingly reasonable declaration=20 >=20 > (* The type of the initializer *) > type 'a init =3D > (* Essentially let-insertion. The initializing expression may be = stateful *) > | Ilet : 'a code -> 'a code init > (* Mutable state with the given initial value *) =20 > | Iref : 'a code -> 'a ref code init >=20 > is, however, not accepted by OCaml 4.07, because >=20 > Error: In this definition, a type variable cannot be deduced > from the type parameters. >=20 > The cause is that the type 'a code is abstract. In many cases, the > error can be gotten rid of by making the offending type more concrete, > so OCaml can see the uses of the type parameters in the type > declaration. However, this workaround does not apply here since 'a > code is provided by MetaOCaml (incidentally, it is defined without any > magic, as a private type -- not even abstract type -- and I really > wish it to stay this way). Mainly, I envisage the use of the above 'a > init declaration in the code that is parameterized by the > basic generator -- a module of the signature > module type Code =3D sig > type +'a code > val seq: unit code -> 'a code -> 'a code > ... > end > Here, I really want to keep 'a code fully abstract. >=20 > The odd thing is that there is a simple albeit ugly workaround: >=20 > type ('a,'b) eq =3D Refl : ('a,'a) eq >=20 > (* The type of the initializer *) > type 'a init =3D > (* Essentially let-insertion. The initializing expression may be = stateful *) > | Ilet : 'a code -> 'a code init > (* Mutable state with the given initial value=20 > Eq is a hack: without it, OCaml complains that it can't figure out = the > type of 'a: because 'a code is abstract > *) =20 > | Iref : 'a code * ('a ref code,'b) eq -> 'b init >=20 > Now, instead of pattern-matching on Iref x I have to pattern-match on > Iref (x,Refl). >=20 > This workaround is rather general: at least all strictly-positive = GADTs > can always be represented as an existential and the eq GADT, if I > remember correctly.=20 >=20 > My question is hence: given the existence of such a general workaround > that works for many GADT definitions, could some future version of > OCaml possibly apply this workaround automatically and transparently? >=20 > The reason for the `a type variable cannot be deduced' error is > soundness, which may be lost otherwise in edge cases. In the cases the > workaround applies (which are many, it seems), no soundness is lost, > right? >=20 > P.S. The error message itself is rather puzzling and always startles > me. It takes me a couple of seconds to remember what is this all > about. Perhaps the error message might say that, for example, >=20 > all appearance of a type variable 'a are in the context like 'a t = where t > is an abstract type >=20 > Incidentally, I remember that on IBM S\360, all diagnostic messages > started with a unique code (which is a three-letter identifier for a > program/subsystem followed by a number). For example, > IEE311I DJ PARAMETER MISSING > The code can be used to look up a detailed description and discussion > of the message in a special set of manuals. This convention was quite > handy; too bad it is forgotten. >=20