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

error messages: always report missing polyvariant tag #12347

Merged
merged 2 commits into from Jul 3, 2023

Conversation

Octachron
Copy link
Member

This PR makes sure that missing polyvariant tags are always correctly reported in error messages even if the tag was discovered as absent during unification.

More concretely, on trunk, the following function

let f (x: [ `R of ([ `A | `R of 'b ] as 'b)]) =
  (x : [< `A | `R of 'a ] as 'a )

fails to typecheck with

 Error: This expression has type [ `R of [ `A | `R of 'a ] as 'a ]
       but an expression was expected of type [< `R of 'a0 ] as 'a0
       Types for tag `A are incompatible

when the real mismatch between the two types is that there is no tags `A in the second type.
With this PR, the error message correctly mentions the missing tag:

Error: This expression has type [ `R of [ `A | `R of 'a ] as 'a ]
       but an expression was expected of type [< `R of 'a0 ] as 'a0
       The second variant type does not allow tag(s) `A

The fix consists in recording in the error trace that we encountered a presence mismatch in the "low-level" function unify_row_field. This was not done before because in nearly all cases mismatches in term of tag presence are discovered when comparing the list tags of polymorphic variants in the higher level unify_row function.

Copy link
Member

@gasche gasche left a comment

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

This looks nice, but I think it would be natural to add more tests.

| (Rpresent None | Reither(true,_,_)),
(Rpresent (Some _) | Reither(false,_,_)) ->
(* constructor arity mismatch: 0 <> 1 *)
raise_unexplained_for Unify
Copy link
Member

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

I am not sure whether this is "unexplained" because this is left for future work, or for some other reason. Is this example covered in the testsuite?

Copy link
Member Author

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

The unify_row_field function is called under an exception handler that adds an Incompatible_types_for _ explanation to the error trace, thus we already handle the mismatched argument types case by default.

Copy link
Member

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

I don't understand if this case is exercised in the testsuite.

Copy link
Member Author

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

It wasn't (but mostly by accident).

| Reither(true, _ :: _, _ ), Rpresent _
| Rpresent _ , Reither(true, _ :: _, _ ) ->
(* inconsistent conjunction on a non-absent field *)
raise_unexplained_for Unify
Copy link
Member

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

Same here, testsuite coverage would be nice if not already present.

Copy link
Member Author

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

This case is arguably more interesting, since we have a type mismatch due to an impossible type. We could improve the error message but that would be a very niche case.

Copy link
Member

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

I'm fine with keeping a bad error message in this case, but I think it would be nice to document this decision and have a corresponding entry in the testsuite.

@Octachron
Copy link
Member Author

I have completed the testsuite coverage for Ctype.unify_row_field.

@gasche gasche added the merge-me label Jul 3, 2023
@Octachron Octachron force-pushed the error_messages_missing_polyvar branch from b0dd36c to 4135321 Compare July 3, 2023 13:23
@gasche gasche merged commit 53be7d1 into ocaml:trunk Jul 3, 2023
10 checks passed
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment
Labels
Projects
None yet
Development

Successfully merging this pull request may close these issues.

None yet

2 participants