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

MPR7565 bis: more context for universal variable in error messages #2140

Merged
merged 4 commits into from Nov 24, 2018

Conversation

@Octachron
Copy link
Contributor

commented Nov 7, 2018

Mantis 7565:

This PR is a follow-up of #1212, it proposes to give more context for universal type variables that escape their scope when unifying methods, by precising the actual type and expected type at the method level, as suggested by @garrigue in #1212 .

For instance, the following code

type uv = [ `A of <f: 'a. 'a -> int > ]
type 'a v = [ `A of <f: 'a -> int > ]
let f (`A o:uv) = o # f 0
let () = f ( `A (object method f _ = 0 end): _ v)

currently raises an error message

Error: This expression has type 'a v but an expression was expected of type uv
The universal variable 'a0 would escape its scope

where the universal variable is mysteriously introduced on the last line (and is slightly renamed compared to the original type abbreviation ).

This PR adds a new line to this error message in order to introduce the universal variable:

The method f has type 'a -> int, but the expected method type was
'a0. 'a0 -> int

In the current implementation, this line is added whenever a universal variable introduced by a method escape its field. This can lead to quite redundant error messages like

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

However, this behavior seemed mostly harmless and it could be avoided with further tuning.

@gasche

This comment has been minimized.

Copy link
Member

commented Nov 7, 2018

(cc @Armael)

I agree that the slight redundancy in the new message is harmless.

@Octachron Octachron force-pushed the Octachron:universal_and_methods_error_message branch from e95aac6 to 293fc1f Nov 7, 2018

@Armael
Copy link
Member

left a comment

I will do a review later, but for the moment I have a question: can you explain a bit what prepare_trace does and why it is needed? It seems to me that this part of the code is now doing some subtle list manipulations on the trace, and I can't tell what is happening exactly.

Also, could you clarify whether the new implementation of filter_trace is a refactoring of the existing one (and therefore equivalent), or if there are differences?

typing/printtyp.ml Outdated Show resolved Hide resolved
@Octachron

This comment has been minimized.

Copy link
Contributor Author

commented Nov 19, 2018

In short, I have split the previous filter_trace function into prepare_trace and filter_trace in order to make it easier to look for meaningful previous elements in the trace in mismatch.

The function prepare_trace is here to discard as early as possible trace elements that are never printed. For instance, printing those elements in the second test example would yield something like:

Error: This expression has type < f : 'b -> int >
but an expression was expected of type t_a = < f : 'a. 'a -> int >
In method f, type 'b -> int is not compatible with type 'a. 'a -> int
Type 'b -> int is not compatible with type 'a. 'a -> int
Type 'b -> int is not compatible with type 'a -> int
Type 'b is not compatible with type 'a
The universal variable 'a would escape its scope

In this situation, connecting the escaping universal variable with its parent method required to wade through those discarded trace elements:

Type 'b -> int is not compatible with type 'a. 'a -> int
Type 'b -> int is not compatible with type 'a -> int
Type 'b is not compatible with type 'a

@Armael
Copy link
Member

left a comment

I have no strong opinion on the general design, but it seems to produce better or equally good error messages, with a tolerable overhead.

Regarding the implementation, modulo the comments below, it looks equivalent to the existing one to me. I'm however not very fond of the increased amount of code manipulating traces that looks like its doing something very tricky, and that I have to read 10 times before figuring out it's actually doing something fairly simple.
To me, mismatch was already hard to process and it's now a bit worse; the prev argument threaded to explanation and explain_escape feels ad-hoc, and the similar business in clean_trace as well.
Maybe I'm just not used to code iterating from right to left, but I'm wondering if the code couldn't be made easier to understand by reversing the trace, or using a more appropriate data structure (like a zipper?)

(its possible that there is no nice solution without doing more global changes; in that case I'm fine with merging the PR as-is. I'm not very familiar with the overall logic of the file, and the code around doesn't look particularly nice anyway, so...)

else elt :: rem'
| _elt :: rem -> filter_trace keep_last rem
| _ -> []
|| same_path t1 t1' && same_path t2 t2' && not is_last

This comment has been minimized.

Copy link
@Armael

Armael Nov 23, 2018

Member

If you can, could you maybe give (in a comment) an informal explanation of what is being computed here?

This comment has been minimized.

Copy link
@Octachron

Octachron Nov 24, 2018

Author Contributor

I have added a comment on the relevant new constructor.

elt :: clean_trace rem

(** Keep elements that are not [Diff _ ] and take the decision
for the last element, require a prepared trace *)

This comment has been minimized.

Copy link
@Armael

Armael Nov 23, 2018

Member

So, AFAIU, the semantics of filter_trace change a bit since it now requires a prepared trace, while previously it "prepared" the trace itself.

github doesn't seem to allow me to comment on the relevant lines directly, but I checked that the call sites of filter_trace satisfy this new precondition.

  • First one is in unification_error; the precondition is trivially satisfied by the call to prepare_trace a few lines above in the same function
  • Second one is in trace, and a bit less obvious. I have no idea what this function is doing, but it only seems to be called in report_subtyping_error, on traces that have been prepared. Maybe it would be good to write down that trace assumes that its input trace has been "prepared".
typing/printtyp.ml Show resolved Hide resolved
for the last element, require a prepared trace *)
let rec filter_trace keep_last = function
| [] -> []
| [Trace.Diff d as elt] when is_discarded false elt ->

This comment has been minimized.

Copy link
@Armael

Armael Nov 23, 2018

Member

I find is_discarded false elt confusing. The name of the first argument of is_discarded is is_last, and you set it to false, but elt is the last element! At this point I'm a bit too confused to understand whether this line and the next one are actually correct, but I would think something like follows is more natural:

| [Trace.Diff d as elt] ->
  if is_discarded keep_last elt then [] else [d]

This comment has been minimized.

Copy link
@Octachron

Octachron Nov 23, 2018

Author Contributor

Maybe a more natural solution would be to make is_discarded returns a variant Discard | Keep_if_last | Keep then the previous line would be checking when is_discarded elt = Keep_if_last .

This comment has been minimized.

Copy link
@Octachron

Octachron Nov 24, 2018

Author Contributor

I went ahead with this solution.

Octachron added some commits Nov 24, 2018

@Octachron

This comment has been minimized.

Copy link
Contributor Author

commented Nov 24, 2018

I have added a new commit to make the logic of mismatch more straightforward by reversing the trace in the first new commit. The second commit adds some comments and tries to make the code around the former is_discarded function more explicit.

@Armael

Armael approved these changes Nov 24, 2018

Copy link
Member

left a comment

Thanks, I like the new changes, especially the new printing_status type. I'm satisfied with the current status of the PR, and will merge if no one complains.

@Armael Armael merged commit 385223e into ocaml:trunk Nov 24, 2018

2 checks passed

continuous-integration/appveyor/pr AppVeyor build succeeded
Details
continuous-integration/travis-ci/pr The Travis CI build passed
Details

gretay-js added a commit to gretay-js/ocaml that referenced this pull request Dec 3, 2018

MPR7565 bis: more context for universal variable in error messages (o…
…caml#2140)

This PR is a follow-up of ocaml#1212, it proposes to give more context for universal type variables that escape their scope when unifying methods, by precising the actual type and expected type at the method level, as suggested by @garrigue in ocaml#1212 .
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment
Projects
None yet
3 participants
You can’t perform that action at this time.