From: Oleg <firstname.lastname@example.org> To: email@example.com Subject: [Caml-list] That dreaded `a type variable cannot be deduced' GADT error Date: Tue, 7 Apr 2020 00:08:49 +0900 Message-ID: <20200406150849.GA5980@Melchior.localnet> (raw) 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.
next reply index Thread overview: 2+ messages / expand[flat|nested] mbox.gz Atom feed top 2020-04-06 15:05 Oleg [this message] 2020-04-08 9:47 ` Jacques Garrigue
Reply instructions: You may reply publically to this message via plain-text email using any one of the following methods: * Save the following mbox file, import it into your mail client, and reply-to-all from there: mbox Avoid top-posting and favor interleaved quoting: https://en.wikipedia.org/wiki/Posting_style#Interleaved_style * Reply using the --to, --cc, and --in-reply-to switches of git-send-email(1): git send-email \ --in-reply-to=20200406150849.GA5980@Melchior.localnet \ --firstname.lastname@example.org \ --email@example.com \ /path/to/YOUR_REPLY https://kernel.org/pub/software/scm/git/docs/git-send-email.html * If your mail client supports setting the In-Reply-To header via mailto: links, try the mailto: link
caml-list - the Caml user's mailing list Archives are clonable: git clone --mirror https://inbox.ocaml.org/caml-list AGPL code for this site: git clone https://public-inbox.org/ public-inbox