Re: [Caml-list] Error: In this definition, a type variable cannot be deduced from the type parameters

[Jacques Garrigue <garrigue@math.nagoya-u.ac.jp>]

On 2014/02/23 02:54, Goswin von Brederlow wrote:

> Hi,
> 
> I'm stuck trying to solve this error:
> 
>    Error: In this definition, a type variable cannot be deduced
>           from the type parameters.
> 
> The error happens when I use the "type 'a node = InnerNode.t" from the
> comment and disapears when I box it in a constructor as shown below.
> 
> Can anyone explain what is missing that makes the extra constructor
> necessary?
> 
> MfG
> 	Goswin
> 
> PS: needs and must work with ocaml 4.01.

Actually it seems that you have already found the solution:
if a type variable appears in the return type of a gadt, and is used
in the body, injectivity under invariance must be guaranteed for this return type.
This is the famous PR#5985.
Injectivity is broken if the type variable can disappear by expanding
any abbreviation in the type, such as node in your case.
By making node a nominal type, you prevented that.
Note that using a private abbreviation would not be sufficient here,
as a private abbreviation can be used to hide a normal abbreviation.

If you dislike the change in internal representation for node,
you can also define a separate type for the gadt parameter.
Except in very specific cases, there is no strong reason for the
gadt parameter type and the concrete type to coincide.

	Jacques