caml-list - the Caml user's mailing list
 help / color / mirror / Atom feed
From: Oleg <oleg@okmij.org>
To: caml-list@inria.fr
Subject: [Caml-list] That dreaded `a type variable cannot be deduced' GADT error
Date: Tue, 7 Apr 2020 00:08:49 +0900	[thread overview]
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.


             reply	other threads:[~2020-04-06 15:05 UTC|newest]

Thread overview: 2+ messages / expand[flat|nested]  mbox.gz  Atom feed  top
2020-04-06 15:08 Oleg [this message]
2020-04-08  9:44 ` Jacques Garrigue

Reply instructions:

You may reply publicly 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 \
    --to=oleg@okmij.org \
    --cc=caml-list@inria.fr \
    /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
Be sure your reply has a Subject: header at the top and a blank line before the message body.
This is a public inbox, see mirroring instructions
for how to clone and mirror all data and code used for this inbox;
as well as URLs for NNTP newsgroup(s).