[Caml-list] That dreaded `a type variable cannot be deduced' GADT error

[Caml-list] That dreaded `a type variable cannot be deduced' GADT error

[Oleg]

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.

Re: [Caml-list] That dreaded `a type variable cannot be deduced' GADT error

[Jacques Garrigue]

Hi Oleg,

That’s an interesting workaround.
But I’m 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’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 <oleg@okmij.org> wrote:
> 
> 
> 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.
>