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

fix: Output checked type in getSelectionTypeOrKind if none is synthed #1062

Merged
merged 1 commit into from
Jun 8, 2023

Conversation

georgefst
Copy link
Contributor

This fixes an issue when using this functionality in our frontend to display the type of the currently-selected node: the fallback trivialTree was displayed for nodes in checkable positions (lambdas, constructors).

@brprice would be better placed than I am to explain why we originally ignored this part of the typecache in #1050, or whether this is quite the right approach. But in his absence, and with the Zurihac push, I'd suggest we merge this anyway. I doubt there are any serious downsides.

@georgefst georgefst requested a review from a team June 8, 2023 09:16
Signed-off-by: George Thomas <georgefsthomas@gmail.com>
@dhess dhess force-pushed the georgefst/get-type-chked branch from 29c65b6 to fdd5b31 Compare June 8, 2023 10:04
@dhess
Copy link
Member

dhess commented Jun 8, 2023

This does improve things, but holes (empty & non-empty) still return the "trivial tree" with this change. Clearly the typechecker knows the proper type of holes because we can return the appropriate action options etc in other API calls, but there's just something not quite right in the getSelectionTypeOrKind implementation.

Anyway, let's merge it and we'll revisit when we have a chance.

@dhess dhess added this pull request to the merge queue Jun 8, 2023
Merged via the queue into main with commit fdcdd6c Jun 8, 2023
102 checks passed
@dhess dhess deleted the georgefst/get-type-chked branch June 8, 2023 11:18
@brprice
Copy link
Contributor

brprice commented Jun 10, 2023

@brprice would be better placed than I am to explain why we originally ignored this part of the typecache in #1050, or whether this is quite the right approach.

I think it was a combination of

  • thinking that maybe the correct thing to do was to report both, but the api only had room for one (and UI for two is somewhat unclear), and the synthed is perhaps a better notion of "what type does this node have" than the checked if both are available (though this is not a well-thought-through statement)
  • an oversight

@brprice
Copy link
Contributor

brprice commented Jun 10, 2023

This does improve things, but holes (empty & non-empty) still return the "trivial tree" with this change. Clearly the typechecker knows the proper type of holes because we can return the appropriate action options etc in other API calls, but there's just something not quite right in the getSelectionTypeOrKind implementation.

Anyway, let's merge it and we'll revisit when we have a chance.

See #1068

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

Successfully merging this pull request may close these issues.

None yet

3 participants