Skip to content
New issue

Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.

By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.

Already on GitHub? Sign in to your account

Puzzling error message with free type variables #7565

Closed
vicuna opened this issue Jun 23, 2017 · 5 comments
Closed

Puzzling error message with free type variables #7565

vicuna opened this issue Jun 23, 2017 · 5 comments

Comments

@vicuna
Copy link

vicuna commented Jun 23, 2017

Original bug ID: 7565
Reporter: @sbriais
Assigned to: @Octachron
Status: resolved (set by @Octachron on 2018-11-24T20:10:04Z)
Resolution: fixed
Priority: low
Severity: feature
Fixed in version: 4.08.0+dev/beta1/beta2
Category: typing
Child of: #7338
Monitored by: @gasche

Bug description

Consider the following code:

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

let f (o:t_a) = o # f 0

let () =
let o =
object
method f _ = 0
end
in
f o

We got the following error message:

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

The error message is puzzling because there is no 'a0 in the inferred type.

@vicuna
Copy link
Author

vicuna commented Jun 23, 2017

Comment author: @Octachron

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

@vicuna
Copy link
Author

vicuna commented Jun 23, 2017

Comment author: @lpw25

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.

@vicuna
Copy link
Author

vicuna commented Jun 24, 2017

Comment author: @Octachron

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.

@vicuna
Copy link
Author

vicuna commented Jun 24, 2017

Comment author: @Octachron

I have an implementation PR for the type expansion solution here: #1212 .

@vicuna
Copy link
Author

vicuna commented Nov 24, 2018

Comment author: @Octachron

This issue should been fixed in OCaml 4.08 by #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

Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment
Projects
None yet
Development

No branches or pull requests

2 participants