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

Order of well-definedness checks unexpected #435

Open
gauravpartha opened this issue Oct 4, 2022 · 1 comment
Open

Order of well-definedness checks unexpected #435

gauravpartha opened this issue Oct 4, 2022 · 1 comment

Comments

@gauravpartha
Copy link
Contributor

gauravpartha commented Oct 4, 2022

There are various cases where Carbon does well-definedness checks in an unexpected order. Some of these issues have been fixed in #429, but there are still some issues left. This is not a soundness issue, but an "error reporting" issue.

In particular, there are various cases where Carbon checks the well-definedness of a parent node before checking the well-definedness of a subnode. Currently, the reason for this (sometimes unexpected) order seems to be because certain parts of the implementation rely on this order (e.g., due to manipulation of mutable state).

Unexpected examples include:

  • Field accesses: Carbon checks whether there is permission to e.f before checking whether e is well-defined.
  • P(e): Carbon checks whether there is permission to P(e) before checking whether e is well-defined.
@gauravpartha
Copy link
Contributor Author

The order for field access was fixed in #451.

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

No branches or pull requests

1 participant