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 401055D5 for ; Mon, 6 Apr 2020 15:05:37 +0000 (UTC) X-IronPort-AV: E=Sophos;i="5.72,351,1580770800"; d="scan'208";a="444078946" Received: from sympa.inria.fr ([193.51.193.213]) by mail2-relais-roc.national.inria.fr with ESMTP; 06 Apr 2020 17:05:35 +0200 Received: by sympa.inria.fr (Postfix, from userid 20132) id EC0B47F485; Mon, 6 Apr 2020 17:05:35 +0200 (CEST) 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 65F367F345 for ; Mon, 6 Apr 2020 17:05:31 +0200 (CEST) Authentication-Results: mail2-smtp-roc.national.inria.fr; spf=None smtp.pra=oleg@okmij.org; spf=Pass smtp.mailfrom=oleg@okmij.org; spf=None smtp.helo=postmaster@mail1.g3.pair.com IronPort-PHdr: =?us-ascii?q?9a23=3ADGtKgRablGji+UzIipm7QFL/LSx+4OfEezUN459i?= =?us-ascii?q?sYplN5qZoMy8bnLW6fgltlLVR4KTs6sC17OL9fm7EjNeqdbZ6TZeKcAKD0dEwe?= =?us-ascii?q?wt3CUeQ+e9QXXhK/DrayFoVO9jb3RCu0+BDE5OBczlbEfTqHDhpRQbGxH4KBYn?= =?us-ascii?q?br+tQt2agMu4zf299IPOaAtUmjW9falyLBKrpgnNq8Uam4RvJrsxxxfTv3dFde?= =?us-ascii?q?tayGFpKFmOmxrw+tq88IRs/ihNtP8t7dJMXbn/c68lUbFWETMqPnw668HsqRTN?= =?us-ascii?q?VxaE6GEGUmURnBpIAgzF4w//U5zsrCb0tfdz1TeDM8HuQr86RTqt76FwSB/1ky?= =?us-ascii?q?gHLCI28HvWisNrkq1Wpg+qqgFlzI7VZIGVM+d+fr/YcNgHS2dNQtpdWipcCY66?= =?us-ascii?q?coABDfcOPfxAoofzp1UAswawCwqjC+zz1zBHiGT73bEm3+k7DQ3KwBYtE8wIvX?= =?us-ascii?q?/JrNv1LqASUeWtwafRyTXMcfxW0ir65YjPdhAuv/6MUKl3ccrSzEkvFgHFgk+X?= =?us-ascii?q?qYz/MDOYz+IAuHWY4ep4Te+iim8qpxt/rzWr3MshhJPFip8Ixl3L7Sl13Yc4KN?= =?us-ascii?q?OiREN0ZdOoCoVcuzyEO4dsX88vQX1ktSAnwbMco5G7ZjIFyJE/yh7fdfOHd4+I?= =?us-ascii?q?7wrmVOmLIDd4gG9pdKiwhxu860Sg0vfzVsiu0FpQsiVFldzMumgM1xzV9MeHVu?= =?us-ascii?q?Nw80ag1DqV2Q3e7vtILE4umabGNpIszaY8lp8JvkTCGi/2ll/2jKiTdkg8/eio?= =?us-ascii?q?7/roYrr9q5+bNI90jwD+MqY0lsy4G+Q4PRACX3KH9uSkyL3j4Ur5Ta1WgfIsl6?= =?us-ascii?q?nZtInWJcAapq6iHw9YyZ0j6ha6Dze+ytsUh3gHLFRfeBKGlYflIV/OIOqrRcu4?= =?us-ascii?q?1l+llTMuw/HdIpXgBI/MJz7NiuTPZ7F4vmlYxQV7mddb6p18DbIEIfC1XVX+4o?= =?us-ascii?q?+LRiQlOhC5lr60QO520ZkTDDrWXv2pdZjKuFrN3doBZvGWbdZM6jH+Lvknofn0?= =?us-ascii?q?gi1hwAJPTeySxZISLUuAMLFmLkGeOCu+h94AFT5MsVF4VOXrkhuJVjsBPy/jDZ?= =?us-ascii?q?J53SkyDcedNamGQ4mshLKb2yLiR89RZWVHCBaLC3i6Log=3D?= X-IronPort-Anti-Spam-Filtered: true X-IronPort-Anti-Spam-Result: =?us-ascii?q?A0BwAwDwQ4teh3IDJ0JmHgELHIVlATGNR?= =?us-ascii?q?oV7nVgKAQMBDC0CBAEBhw8cBwEENBMCEAEBBQEBAQIBAgMEARMBAQEKCwkIKYV?= =?us-ascii?q?pgjsig0ETgTSEAoJ8AbFCM4pxgTiMMw4MgUBAgRGLYIIsBJhplzt6gkcEgheVA?= =?us-ascii?q?ymEZZcdi0CgRIFpgXlNMAiDJU8YDY4pDgmONDIBgTeOUwEB?= X-IPAS-Result: =?us-ascii?q?A0BwAwDwQ4teh3IDJ0JmHgELHIVlATGNRoV7nVgKAQMBDC0?= =?us-ascii?q?CBAEBhw8cBwEENBMCEAEBBQEBAQIBAgMEARMBAQEKCwkIKYVpgjsig0ETgTSEA?= =?us-ascii?q?oJ8AbFCM4pxgTiMMw4MgUBAgRGLYIIsBJhplzt6gkcEgheVAymEZZcdi0CgRIF?= =?us-ascii?q?pgXlNMAiDJU8YDY4pDgmONDIBgTeOUwEB?= X-IronPort-AV: E=Sophos;i="5.72,351,1580770800"; d="scan'208";a="444078930" X-MGA-submission: =?us-ascii?q?MDH+lh81NmihOyq5JDmOdawUeLWWqoRtivF1F3?= =?us-ascii?q?f54v9mff+noAIiGkpWa5dJdImNnIY7Pfwd8oHln+RBWJCRIqByv+G3kZ?= =?us-ascii?q?JMYgK3raKIceYiWRtFvV/zeiYDcMz2YN2IPeExtk9H8ge6Y0tLZaoaFQ?= =?us-ascii?q?A/d0K0rmDa+fahP+Q/BLjhMQ=3D=3D?= Received: from mail1.g3.pair.com ([66.39.3.114]) by mail2-smtp-roc.national.inria.fr with ESMTP/TLS/DHE-RSA-AES256-GCM-SHA384; 06 Apr 2020 17:05:30 +0200 Received: from mail1.g3.pair.com (localhost [127.0.0.1]) by mail1.g3.pair.com (Postfix) with ESMTP id 532B53FB3D4; Mon, 6 Apr 2020 11:05:28 -0400 (EDT) Received: from Melchior.localnet (170.212.49.163.rev.vmobile.jp [163.49.212.170]) (using TLSv1.2 with cipher ECDHE-RSA-AES256-GCM-SHA384 (256/256 bits)) (No client certificate requested) by mail1.g3.pair.com (Postfix) with ESMTPSA id 81410584B84; Mon, 6 Apr 2020 11:05:27 -0400 (EDT) Date: Tue, 7 Apr 2020 00:08:49 +0900 From: Oleg To: caml-list@inria.fr Message-ID: <20200406150849.GA5980@Melchior.localnet> Mail-Followup-To: Oleg , caml-list@inria.fr MIME-Version: 1.0 Content-Type: text/plain; charset=us-ascii Content-Disposition: inline User-Agent: Mutt/1.10.1 (2018-07-13) Subject: [Caml-list] That dreaded `a type variable cannot be deduced' GADT error Reply-To: Oleg X-Loop: caml-list@inria.fr X-Sequence: 18088 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: The following seemingly reasonable declaration (* The type of the initializer *) type 'a init = (* Essentially let-insertion. The initializing expression may be stateful *) | Ilet : 'a code -> 'a code init (* Mutable state with the given initial value *) | Iref : 'a code -> 'a ref code init is, however, not accepted by OCaml 4.07, because Error: In this definition, a type variable cannot be deduced from the type parameters. 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 = sig type +'a code val seq: unit code -> 'a code -> 'a code ... end Here, I really want to keep 'a code fully abstract. The odd thing is that there is a simple albeit ugly workaround: type ('a,'b) eq = Refl : ('a,'a) eq (* The type of the initializer *) type 'a init = (* Essentially let-insertion. The initializing expression may be stateful *) | Ilet : 'a code -> 'a code init (* Mutable state with the given initial value Eq is a hack: without it, OCaml complains that it can't figure out the type of 'a: because 'a code is abstract *) | Iref : 'a code * ('a ref code,'b) eq -> 'b init Now, instead of pattern-matching on Iref x I have to pattern-match on Iref (x,Refl). 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. 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? 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? 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, all appearance of a type variable 'a are in the context like 'a t where t is an abstract type 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.