0007565: Puzzling error message with free type variables

(0017966)
octachron (developer)
2017-06-23 16:59
edited on: 2017-06-23 17:07

To trace the origin of the 'a0 type name in error message, one can rename the universal variable 'a in the definition of the class type to:

class type t_a =
  object
    method f: 'any. 'any -> int
  end

The error message becomes then

Error: This expression has type < f : 'a -> int > but an expression was expected of type t_a The universal variable 'any would escape its scope

In other words, the type variable name `'a0` in the original error message is a type name derived from the name used in the explicitly polymorphic annotation "f:'a. …". The "0" suffix is then added to discrimate between this universal type variable "'a" and the type variable "'a" in scope at the point of the error.

I think that it could be nice to make the origin of the derivation more apparent. For instance, printing "'a(universal)" in the error message? It may also be worthwhile to add the location of the definition of the universal type variable (if possible).

(0017973)
lpw25 (developer)
2017-06-23 22:33

I think the best change in this case would be to show the expansion of t_a in the message. Then it would be clear where it came from. There is probably some case missing in printtyp.ml to handle this, but I've never really understood that code so maybe it's more complicated than that.

(0017974)
octachron (developer)
2017-06-24 03:19

Expanding the object type of t_a sounds like a good idea; and after looking at the code it seems that this is just a matter of disabling the compact mode in Printtyp.may_prepare_expansion when there is an escaping universal type variable error message laying in ambush.

(0017976)
octachron (developer)
2017-06-24 15:03

I have an implementation PR for the type expansion solution here: https://github.com/ocaml/ocaml/pull/1212 [^] .

(0019483)
octachron (developer)
2018-11-24 21:10

This issue should been fixed in OCaml 4.08 by https://github.com/ocaml/ocaml/pull/2140 [^] , which adds some context about the method type when an universal variable escapes. For instance, the error message in the reported example becomes

Error: This expression has type < f : 'a -> int >
       but an expression was expected of type t_a
       The method f has type 'a -> int, but the expected method type was
       'a0. 'a0 -> int
       The universal variable 'a0 would escape its scope

Issue History
Date Modified	Username	Field	Change
2017-06-23 16:34	sbriais	New Issue
2017-06-23 16:59	octachron	Note Added: 0017966
2017-06-23 17:02	octachron	Priority	normal => low
2017-06-23 17:02	octachron	Severity	minor => feature
2017-06-23 17:02	octachron	Status	new => confirmed
2017-06-23 17:04	octachron	Relationship added	child of 0007338
2017-06-23 17:07	octachron	Note Edited: 0017966	View Revisions
2017-06-23 22:33	lpw25	Note Added: 0017973
2017-06-24 03:19	octachron	Note Added: 0017974
2017-06-24 15:02	octachron	Assigned To	=> octachron
2017-06-24 15:02	octachron	Status	confirmed => assigned
2017-06-24 15:03	octachron	Note Added: 0017976
2018-11-24 21:10	octachron	Note Added: 0019483
2018-11-24 21:10	octachron	Status	assigned => resolved
2018-11-24 21:10	octachron	Fixed in Version	=> 4.08.0+dev
2018-11-24 21:10	octachron	Resolution	open => fixed

Notes
(0017966) octachron (developer) 2017-06-23 16:59 edited on: 2017-06-23 17:07	To trace the origin of the 'a0 type name in error message, one can rename the universal variable 'a in the definition of the class type to: class type t_a = object method f: 'any. 'any -> int end The error message becomes then Error: This expression has type < f : 'a -> int > but an expression was expected of type t_a The universal variable 'any would escape its scope In other words, the type variable name `'a0` in the original error message is a type name derived from the name used in the explicitly polymorphic annotation "f:'a. …". The "0" suffix is then added to discrimate between this universal type variable "'a" and the type variable "'a" in scope at the point of the error. I think that it could be nice to make the origin of the derivation more apparent. For instance, printing "'a(universal)" in the error message? It may also be worthwhile to add the location of the definition of the universal type variable (if possible).

(0017973) lpw25 (developer) 2017-06-23 22:33	I think the best change in this case would be to show the expansion of t_a in the message. Then it would be clear where it came from. There is probably some case missing in printtyp.ml to handle this, but I've never really understood that code so maybe it's more complicated than that.

(0017974) octachron (developer) 2017-06-24 03:19	Expanding the object type of t_a sounds like a good idea; and after looking at the code it seems that this is just a matter of disabling the compact mode in Printtyp.may_prepare_expansion when there is an escaping universal type variable error message laying in ambush.

(0017976) octachron (developer) 2017-06-24 15:03	I have an implementation PR for the type expansion solution here: https://github.com/ocaml/ocaml/pull/1212 [^] .

(0019483) octachron (developer) 2018-11-24 21:10	This issue should been fixed in OCaml 4.08 by https://github.com/ocaml/ocaml/pull/2140 [^] , which adds some context about the method type when an universal variable escapes. For instance, the error message in the reported example becomes Error: This expression has type < f : 'a -> int > but an expression was expected of type t_a The method f has type 'a -> int, but the expected method type was 'a0. 'a0 -> int The universal variable 'a0 would escape its scope