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

[Jacques Garrigue <jacques.garrigue@gmail.com>]

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.
>