Type error "the type variable 'a cannot be deduced from the type parameters."

Learning
1

Is there a way to type this without having to reveal the implementation of E.t ?

module E : sig
  type 'a t
  type _ Effect.t +=
  | Call : (unit -> 'a) -> 'a t Effect.t
end = struct
  type 'a t = 'a
  type _ Effect.t +=
  | Call : (unit -> 'a) -> 'a t Effect.t
end

This errors with:

File "-", lines 5-6, characters 2-40:
5 | ..type _ Effect.t +=
6 |   | Call : (unit -> 'a) -> 'a t Effect.t
Error: In the extension constructor
         type _ Stdlib.Effect.t += Call : (unit -> 'a) -> 'a t Effect.t
       the type variable 'a cannot be deduced from the type parameters.

An error which btw I’m unable to make any sense from (and the internet is mostly mute about it).

This doesn’t error but I’d really rather have that 'a t abstract.

module E : sig
  type 'a t = private 'a
  type _ Effect.t +=
  | Call : (unit -> 'a) -> 'a t Effect.t
end = struct
  type 'a t = 'a
  type _ Effect.t +=
  | Call : (unit -> 'a) -> 'a t Effect.t
end
2

You need to indicate in the signature that the type constructor 'a t is injective:

type !'a t

This is a technical condition that is required in order to successfully typecheck match on GADTs such as the one in your example (where the abstract type constructor appears in the result type of the GADT).

Cheers,
Nicolas

3

Maybe the error message would be more useful if it included the word “injective” somewhere. cc @octachron

Cheers,
Nicolas

4

For errors with weak type variables, we added something like “(see manual section X.Y.Z)” to the error message.

Now the question is if this is indeed covered in the manual.

5

I couldn’t find anything about that.

6

Here, it was suggested to expand the error message to:

>  all appearance of a type variable 'a are in the context like 'a t where t
>  is an abstract type

In the manual, we mention in section 8.1 that “injectivity annotation ! indicating that the parameter can be deduced from the whole type”, which probably needs to be expanded in order to have any hope of helping the user (and the section on injectivity below that is a bit too technical if you don’t already know the answer).

Maybe, if we can easily extract some of the types that the parameter appears in for the hint:

Error: In the extension constructor
         type _ Stdlib.Effect.t += Call : (unit -> 'a) -> 'a t Effect.t
       the type variable 'a cannot be deduced from the type parameters.
       In the type parameters or constraints, 'a only appears in contexts where it is not uniquely determined.
Hint: "'a t" does not uniquely determine 'a, because t is not injective (see manual section 8.1)

That error message also covers the example using constraints from Issue · GitHub

module F(T:sig type 'a t end) = struct
  class ['a] c x = object constraint 'a = 'b T.t val x' : 'b = x method x = x' end
end

Error: In the definition
         type 'a c = < x : 'b > constraint 'a = 'b T.t
       the type variable 'b cannot be deduced from the type parameters.
       In the type parameters or constraints, 'b only appears in contexts where it is not uniquely determined.
Hint: "'b T.t" does not uniquely determine 'b, because T.t is not injective (see manual section 8.1)

Edit: FWIW, it seems like it would be a bit of a pain to produce the hints. We probably have to handle multi-parameter types, and nested types…

7

@smuenzel thanks for your investigations. It says a lot about the current state of web search engines that searching for the error message text was unable to resurface that [caml-list] thread.

That being said while having the compiler pointing out to the chapter where you should look up things may be useful, for me the first step would be a good explanation of the error and its text at place where I expect it in the manual as a user. Here’s the places I looked:

  1. The chapter on effects.
  2. The chapter on gadts.
  3. The very well hidden section about common errors.

So while it may be nice to hack the typechecker to tell you more, I think that fundamentally the problem lies in the fact the user manual, over time, eventually lost its adjective (see also this comment).

8

my GADT tutorial has a section about this kind of errors: Dromedary and a half - GADT Tips and Tricks

it has none of the theoretical details, but it mentions the suggestion above as a possible fix. it also mentions another possible fix but not applicable to your case.

9

Thanks! Sadly searching for the error message that webpage didn’t resurface. Amusingly they now resurface this very discussion.

P.S. Typo “Alternatively, you can add a type paramter”

10

thanks, fixed the typo

yeah I tried the search too and also found this poor result. worst, i mostly had results for other languages.