Skip to content

fix: SetConFieldType could create ill-typed programs#932

Merged
brprice merged 9 commits intomainfrom
brprice/ProgAction-ill-typed
Apr 18, 2023
Merged

fix: SetConFieldType could create ill-typed programs#932
brprice merged 9 commits intomainfrom
brprice/ProgAction-ill-typed

Conversation

@brprice
Copy link
Copy Markdown
Contributor

@brprice brprice commented Apr 6, 2023

When running this action, we don't run a full typechecking pass (for efficiency). Prior to this commit we could create ill-typed programs, by not taking into account directionality, since arguments to constructors may only be checkable, but the action may wrap those terms in a hole without adding an annotation.

Note that this would have been fixed in a different way by #931.

@brprice brprice force-pushed the brprice/ProgAction-ill-typed branch from 47ee50c to b45410a Compare April 6, 2023 16:51
@brprice brprice requested a review from a team April 6, 2023 16:52
@brprice
Copy link
Copy Markdown
Contributor Author

brprice commented Apr 6, 2023

We hadn't noticed this before because this action is rarely exercised. In particular, it is not part of the OpenAPI, and is never an "offered" action. Thus it does not participate in our property tests which check all offered actions are actually accepted (whilst that runs with smartholes, and this bug only happens because we don't do a smartholes pass, it still would have been caught since the test checks that the result is well-formed (with SH) and that that final TC pass did not change the program, in ensureSHNormal)

@georgefst I believe you were looking into exposing the typedef actions via the OpenAPI. Will that make them "offered" actions, and thus be part of the existing pbt? (If not, what's your plan / what is needed to get them tested in our existing test?)

Comment thread primer/test/Tests/Action/Prog.hs Outdated
brprice added 7 commits April 9, 2023 19:06
The tests all currently pass since we don't require the programs
actually be well typed. We change the tests so that they operate on
well typed programs now.
Currently we don't require these test cases to be well typed, so they
pass. We adjust them to bind the correct number of fields in case
expressions even though this is not technically required currently.
This makes the test align to our bidirectional typing discipline. This
is not enforced by our testsuite currently, but is good for futureproofing.
Let's not have testcases which are not even well-scoped.
(This is not enforced by the testsuite)
@brprice brprice force-pushed the brprice/ProgAction-ill-typed branch 3 times, most recently from 5ceed37 to d240f8d Compare April 9, 2023 18:46
@georgefst
Copy link
Copy Markdown
Contributor

@georgefst I believe you were looking into exposing the typedef actions via the OpenAPI. Will that make them "offered" actions, and thus be part of the existing pbt?

Yes. That should mean that almost all of ProgAction will be covered. The exceptions being those actions which we expose via other APIs (i.e. those which aren't used via the "action panel" in our frontend), such as CreateDef and AddTypeDef.

When running this action, we don't run a full typechecking pass (for
efficiency). Prior to this commit we could create ill-typed programs,
by not taking into account directionality, since arguments to
constructors may only be checkable, but the action may wrap those
terms in a hole without adding an annotation.
@brprice brprice force-pushed the brprice/ProgAction-ill-typed branch from d240f8d to c76d3ac Compare April 12, 2023 19:11
@brprice brprice added this pull request to the merge queue Apr 18, 2023
Merged via the queue into main with commit 62b344d Apr 18, 2023
@brprice brprice deleted the brprice/ProgAction-ill-typed branch April 18, 2023 11:29
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.

2 participants