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.

Sign up for GitHub

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

Jump to bottom

feat!: API gives more details on mismatched types #1172

Merged
merged 2 commits into from
Nov 20, 2023
Merged

feat!: API gives more details on mismatched types #1172

merged 2 commits into from
Nov 20, 2023

Conversation

brprice
Copy link
Contributor

@brprice brprice commented Nov 8, 2023 •
edited
Loading

For non-empty holes (aka "mismatches"), the OpenAPI now gives both the expected and actual types. We also record the checked-at kind of non-empty type holes in the metadata rather than the synthesised one, for consistency with the term level.

BREAKING CHANGE: this changes the OpenAPI schema.

@brprice brprice mentioned this pull request Nov 9, 2023
Merged
@brprice
Copy link
Contributor Author

brprice commented Nov 9, 2023 •
edited
Loading

This PR works pretty well for terms, but for types it is somewhat lacking: in List {? Maybe ?} we will report that the mismatch has actual type * -> * (good), but say we expect ? (a kind hole). This makes sense given the kindchecker's behaviour, but we could probably do a better job with the metadata there -- I'll investigate.

We also have a more tricky(?) issue with {? Nat ?} Bool, where the mismatch has actual type * (good -- this is the kind of Nat), and expected type ? (misleading -- we expected an arrow kind).

Similarly with the term {? Zero ?} True we report we expected ?, but we may prefer to say ? -> ? (or even Bool -> ?, but that is heading to #81 territory)

@brprice
Copy link
Contributor Author

brprice commented Nov 9, 2023

This PR works pretty well for terms, but for types it is somewhat lacking: in List {? Maybe ?} we will report that the mismatch has actual type * -> * (good), but say we expect ? (a kind hole). This makes sense given the kindchecker's behaviour, but we could probably do a better job with the metadata there -- I'll investigate.

We also have a more tricky(?) issue with {? Nat ?} Bool, where the mismatch has actual type * (good -- this is the kind of Nat), and expected type ? (misleading -- we expected an arrow kind).

Similarly with the term {? Zero ?} True we report we expected ?, but we may prefer to say ? -> ? (or even Bool -> ?, but that is heading to #81 territory)

I've pushed a draft commit that does this for kinds, but not types. The remaining cases to consider are "a term hole in SYN position where the typing rule has a matchArrow/Forall constraint" where we could say ? $ True expects an arrow type, and ? @Bool expects a forall type. Reporting ? -> ? and ∀α:?.? I think is fairly straightforward, but being smarter and constraining those holes is best left to #81. (Note that this includes saying ? x y expects type ? -> ? -> ? rather than just ? -> ?)

@brprice
Copy link
Contributor Author

brprice commented Nov 15, 2023

On further thought, I have decided to not include any inference/constraint propagation in this PR. Mismatches in synthesisable position which nonetheless have constraints will simply say "expected a hole type", e.g. in ? $ True, the hole in function position won't say that it requires an arrow type. Further work is left to #81. However we will ensure to treat non-empty type holes in "checkable" position similarly to term holes even though our type level is synthesis-only rather than properly bidirectional.

The reasoning here is

  • let's keep this pr simple so we can merge soon
  • further work is lower priority than getting a basic version
  • doing better is difficult to do consistently. Consider
    • {? 1 ?} True, we could say expected: ? -> ?, but why not Bool -> ?
    • ? True should probably have the same "expected" as the non-empty hole version, but this PR is only focusing on displaying the mismatch for non-empty holes
    • {? 1 ?} True ? Nil should probably say Bool -> ? -> List ? (or maybe ? -> ? -> ?), but actually reporting this is non-trivial without properly representing and propagating constraints (since this expression is curried, i.e. is actually two nested applications, and thus knowing we need two arrows in the type needs some slightly non-local information)

@brprice brprice changed the title (WIP) API gives more details on mismatched types feat!: API gives more details on mismatched types Nov 15, 2023
@brprice brprice marked this pull request as ready for review November 15, 2023 14:32
@brprice brprice requested a review from a team November 15, 2023 14:33
georgefst
georgefst approved these changes Nov 16, 2023
View reviewed changes
Copy link
Contributor

@georgefst georgefst left a comment

Choose a reason for hiding this comment

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

Looks good.

This is obviously useful even without (some form of) #81, so I agree with merging in its current state, much as some outputs are unsatisfying.

primer-api/src/Primer/API.hs Outdated Show resolved Hide resolved
@brprice
feat!: expose "expected" and "got" mismatch metadata in api
aabf9e4 
This simply gives more information in the api `selection/`
(i.e. `getTypeOrKind` operation). We give both the type assigned to the
hole itself as well as the type assigned to the contents. This doesn't
actually expose more information, since one could always call the old api
on both the hole and its contained node, but it is much more convenient
for a consumer to have all the relevant information to understand a
mismatch in one place.

BREAKING CHANGE: this changes the return type of an endpoint in the openapi.

Signed-off-by: Ben Price <ben@hackworthltd.com>
@brprice
feat: better reporting of kinds of non-empty type holes
b01a481 
This is implemented by a small change to the metadata assigned by the
kindchecker on non-empty holes.

`List {? Maybe ?}` now reports "expected `*`, got `* -> *`".
However, `{? Nat ?} Bool` still reports "expected `?`, got `*`".
This is consistent with the term level where
`not {? Zero ?}` reports "expected `Bool`, got `Nat`".
`{? Zero ?} True` reports "expected `?`, got `Nat`".

Improving this (we may want to report "expected `* -> ?`" and
"expected `Bool -> ?`" above) is left as future work, as this is starting
to veer into type inference territory, which we have avoided so far. We
may further wish to use non-local information to improve our reporting,
e.g. `List ({? Nat ?} Bool)` could report "expected `* -> *`" by noting
`Bool : *` and `List : * -> *`, and `not ({? Nil ?} Zero True)` could
report "expected `Nat -> Bool -> Bool`". Note that if we improve this
in future we should probably also report these expected types/kinds for
empty holes as well.

Signed-off-by: Ben Price <ben@hackworthltd.com>
@brprice brprice added this pull request to the merge queue Nov 20, 2023
Merged via the queue into main with commit 9623693 Nov 20, 2023
70 checks passed
@brprice brprice deleted the brprice/nehole-api-type branch November 20, 2023 13:55
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment
Reviewers

@georgefst georgefst georgefst approved these changes

Assignees
No one assigned
Labels
None yet
Projects
None yet
Milestone
No milestone
Development

Successfully merging this pull request may close these issues.
2 participants
@brprice @georgefst