Skip to content

typecore: clarify the backtracking logic of type_label_exp#11900

Closed
gasche wants to merge 1 commit intoocaml:trunkfrom
gasche:type_label_exp_wrappers
Closed

typecore: clarify the backtracking logic of type_label_exp#11900
gasche wants to merge 1 commit intoocaml:trunkfrom
gasche:type_label_exp_wrappers

Conversation

@gasche
Copy link
Copy Markdown
Member

@gasche gasche commented Jan 16, 2023

This PR is a follow-up to #11536, proposing a code simplification that was first sketched during the review of that PR: #11536 (comment)

The difficulty in the code that is being fixed is an unpleasant interaction between backtracking logic and the new with_local_level wrappers:

  • The idiomatic way to use the wrappers is to perform generalization logic in the ~post action of the wrapper, so that the results returned to the outer level have been correctly generalized.
  • The backtracking logic in this function must backtrack on an error condition that is only detected during the generalization step, but backracking from within the ~post action is not easy as it is not supposed to return any results, just unit.
  • In consequence the code was written in an unidiomatic way, with generalization logic left after the ~post action

The solution proposed in this PR is to use a local exception to signal the need to backtrack from within the ~post action to the outer code.

I also tried to simplify the code and clarify what is going on, with more comments and some code factorization.

Review

I believe that it is better to be familiar (not necessarily expert) with the type-checking code, or interested in learning it on the fly, to review this PR. There is code moving in and out of the with_local_level callback or ~post action, so it is not easy to convince oneself that the behavior is preserved without knowing these abstractions.

cc @garrigue @t6s, or possibly @goldfirere

@goldfirere
Copy link
Copy Markdown
Contributor

I'm not convinced that the new code is better than the old. It is nice, indeed, to make sure that the result of with_local_scope has been properly generalized. But I think we will fail to reach this standard comfortably in all cases. (Indeed, I have wanted this fact for years within GHC but tried and failed to come up with the right set of abstractions that would cover all the corner cases.) So my thought here would be to comment the old code carefully (the new comment about two tries is very helpful!) but not to do this refactor with the awkward local exception.

@gasche gasche self-assigned this Jan 26, 2023
@gasche
Copy link
Copy Markdown
Member Author

gasche commented Feb 13, 2023

Grmph. I'm a bit disappointed by @goldfirere's assessment because I personally do find the new code more readable than the previous one, but on the other hand no one stood up with a different opinion. In general it's healthier to trust the reviewers more than ourselves on these not-clearly-necessary PRs, so I am going to consider that the case for the proposed change is closed with a "reject".

There is still some work left over to move the comments to the old code version. This is TODO for me, so I'm leaving open for now.

@goldfirere
Copy link
Copy Markdown
Contributor

To be clear: I'm very happy for others to disagree here. It was a close call for me, and I see the value in both approaches.

@lpw25
Copy link
Copy Markdown
Contributor

lpw25 commented Feb 23, 2023

At the risk of being Grmph'd at, I think I agree with Richard on this one. At the very least the new code is not obviously easier to read, so probably isn't worth the churn. I'll close now, obviously people can reopen if they disagree or see some way to make the refactoring more obviously clearer.

@lpw25 lpw25 closed this Feb 23, 2023
@gasche
Copy link
Copy Markdown
Member Author

gasche commented Feb 24, 2023

No, on the contrary, it's helpful to get more feedback. Thanks!

@goldfirere
Copy link
Copy Markdown
Contributor

Before we permanently wander off, can I request that the comment about the two tries makes it in? That piece, for me, is still a big improvement over the status quo!

gasche added a commit to gasche/ocaml that referenced this pull request Mar 1, 2023
@gasche
Copy link
Copy Markdown
Member Author

gasche commented Mar 1, 2023

Right, right, I submitted a comment-only PR at #12054.

gasche added a commit to gasche/ocaml that referenced this pull request Mar 1, 2023
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment

Projects

None yet

Development

Successfully merging this pull request may close these issues.

3 participants