fix: extend available actions property test to cover typedefs, and fix revealed bugs #1040
Conversation
primer/src/Primer/App.hs
Outdated
| . over (_exprMeta % _type % _Just) \case | ||
| TCSynthed t -> TCSynthed $ updateType' t | ||
| TCChkedAt t -> TCChkedAt $ updateType' t | ||
| TCEmb (TCBoth t1 t2) -> TCEmb (TCBoth (updateType' t1) (updateType' t2)) |
There was a problem hiding this comment.
Is there a better way to write this? Maybe we should just define a getter.
georgefst
force-pushed
the
georgefst/typedef-actions
branch
2 times, most recently
from
f353179
to
c42e031
Compare
brprice
force-pushed
the
georgefst/typedef-actions-tests
branch
2 times, most recently
from
1ff01a4
to
c2b3cae
Compare
|
I have added some (somewhat messy) commits fixing the remaining issues that I know about. (In case it is helpful, my even more messy debugging is recorded on brprice/tmp/typedef-actions-tests-debugging, but note I'll probably prune this branch at some point). If you don't mind, I'll leave tidying my commits to you, @georgefst -- especially the task of giving nicer commit messages. |
|
Thanks @brprice! |
georgefst
force-pushed
the
georgefst/typedef-actions-tests
branch
5 times, most recently
from
2e74b20
to
5af11f7
Compare
|
OK, this PR is meant to fix more things than it might break, but it's not in good enough shape to merge into |
| (StudentProvided, (Left (TypeDefAlreadyExists _), _)) -> do | ||
| pure () | ||
| (StudentProvided, (Left (ConAlreadyExists _), _)) -> do | ||
| pure () | ||
| (StudentProvided, (Left (ParamAlreadyExists _), _)) -> do | ||
| pure () |
There was a problem hiding this comment.
Improving the generators to exercise these clashes would be a good idea.
My current (somewhat scattered) thoughts:
- I'm not sure we will hit
TypeDefAlreadyExists, since we don't "offer" to create new (type)defs, those global actions are somewhat separate ConAlreadyExists: when doing this action wegenName, which often picks from a small set to increase clashes; however, when we initially generate the program, we generate constructor names viafreshNameForCxt, which has an entirely different mechanism, thus avoiding clashes.ParamAlreadyExists: this is similar to the case for constructors.
primer/test/Tests/Action/Prog.hs
Outdated
| -- Forbid clash between type name and parameter name | ||
| unit_create_typedef_bad_6 :: Assertion |
There was a problem hiding this comment.
@dhess In the "less strict duplicate name checking" commit, we have loosened our rules that forbid type definitions akin to data T (C :: *) (T :: * -> *) = C Bool | T Int (where we have name clashes between type-and-parameter, parameter-and-ctor and type-and-ctor). I recall that we talked about this when initially implementing user-specified typedefs, and decided to forbid these clashes as they are too confusing.
(EDIT for clarity: the type above has the same meaning as (I have renamed parameters and constructors) data T (a :: *) (f :: * -> *) = C1 Bool | C2 Int)
I assume that these checks were removed to make the property test pass easier, but expect that we could instead engineer the test to treat these like name capture and ignore these specific errors. (@georgefst could you confirm?)
@dhess what are your thoughts -- should we forbid such clashes still? Note that in the commit message George wrote
we never consistently checked these things in
applyProgAction, and it would be awkward to do so. besides, why do we care
so there may be some extra work to do to check these properly if we want to keep the restrictions.
There was a problem hiding this comment.
Before I answer, in actually no, that doesn't make sense, does it?data T (C :: *) (T :: * -> *) = ..., the parameter T is a recursive reference to the typedef T itself, is that correct?
There was a problem hiding this comment.
I think no good can come of this, however clever it might seem to allow names within a particular typedef scope to clash. It might be slightly annoying to Haskellers to have to write data F a = MkF a rather than data F a = F a, but I don't think the cleverness is worth the potential for confusion for beginners, or even intermediate students. I can imagine teachers needing to spend an awful lot of time explaining the difference between T as type name vs T as type parameter vs T as value constructor, all depending on which side of the = they're on, or whether they appear in a term or an annotation, or whether they appear in head position or as a parameter, etc. That doesn't seem like time spent constructively, when we could just instead outlaw these clashes.
So I'm very much in favor of not allowing name conflicts within a given typedef scope.
Once we have better support in the UI for displaying the type of a value constructor when it appears in an action input, I think it might be OK to treat value constructor names as being prefixed by their type and therefore allowing the same value constructor name in different types [*], but I assume that scenario is not covered by this particular commit.
[*] In other words, at the moment if we have data A = Foo | Bar and data B = Foo | Baz, when the student selects the "Use value constructor" action, she is presented with [Foo, Bar, Foo, Baz] and there is no way to tell which Foo is which, so this would be bad. But if instead we presented her with [Foo : A, Bar : A, Foo : B, Baz : B] then I think we could make a case for allowing Foo in A and B. Students will already need to understand the same constructor name belonging to different types when importing other modules, anyway, so there's no compelling reason to treat their own module differently, IMO.
There was a problem hiding this comment.
Ok, I'll change approach here to forbid such clashes again.
There was a problem hiding this comment.
Ok, I'll change approach here to forbid such clashes again.
Done -- dropped that commit (not needed to pass testsuite, cf comment above) and added a new commit on the end to actually do the checks.
There was a problem hiding this comment.
I assume that these checks were removed to make the property test pass easier, but expect that we could instead engineer the test to treat these like name capture and ignore these specific errors. (@georgefst could you confirm?)
Yes, that is the case. At the time I chose this approach, I wasn't sure how to ignore the errors. I am less sure than @dhess about the pros of outlawing such pseudo-clashes, but I'll write my thoughts about that up in a separate thread.
brprice
force-pushed
the
georgefst/typedef-actions-tests
branch
from
5af11f7
to
ebb4fbe
Compare
brprice
changed the title
brprice
force-pushed
the
georgefst/typedef-actions-tests
branch
from
ebb4fbe
to
224de87
Compare
This will be necessary when we extend to typedefs, since we need to branch here, but can't use `label` in `GenT`. Signed-off-by: George Thomas <[email protected]> Signed-off-by: Ben Price <[email protected]>
This should have been done back when `forDef` etc. acquired their current names. Signed-off-by: George Thomas <[email protected]> Signed-off-by: Ben Price <[email protected]>
Signed-off-by: George Thomas <[email protected]> Signed-off-by: Ben Price <[email protected]>
Signed-off-by: George Thomas <[email protected]> Signed-off-by: Ben Price <[email protected]>
Signed-off-by: George Thomas <[email protected]> Signed-off-by: Ben Price <[email protected]>
We rename these local definitions to clarify that they work on type definitions, rather than types in the signature of term definitions or elsewhere. We also wish to free up the name `updateType` for a future helper that operates on types both in signatures and embedded inside expressions. Signed-off-by: Ben Price <[email protected]>
Signed-off-by: George Thomas <[email protected]> Signed-off-by: Ben Price <[email protected]>
Signed-off-by: George Thomas <[email protected]> Signed-off-by: Ben Price <[email protected]>
Signed-off-by: George Thomas <[email protected]> Signed-off-by: Ben Price <[email protected]>
Instead of synthesising the type of the scrutinee from scratch, we just read it from the TypeCache. This relies on the program always being in a consistent state, which is tested by tasty_available_actions_accepted, at least for interactions using SmartHoles and the "offered action" api. This also fixes a bug: previously when we synthesised the type, we needed to know the context that the scrutinee lives in. However, we only used the `progCxt`, which is the "top-level"/"global" context -- in particular this would fail if the scrutinee used a variable introduced by a lambda (or let, etc). Signed-off-by: Ben Price <[email protected]>
Signed-off-by: Ben Price <[email protected]>
Signed-off-by: Ben Price <[email protected]>
Since 6197cc1, type definitions have contained metadata (since they need IDs so that we can run actions on them). When forgetting metadata in a Prog, we also need to forget this metadata. The reason we have noticed this now is that we are aiming to upgrade the `tasty_available_actions_accepted` test to cover typedef actions which will require upgrading `checkEverything` to modify typedefs in a subsequent commit (it may need to do smartholes, rather than just saying "no"). As it will then update typecaches, the benchmark tests would start to fail as (before this current commit) we were not properly forgetting them. Signed-off-by: George Thomas <[email protected]> Signed-off-by: Ben Price <[email protected]>
This is needed now that we have actions that affect typedefs. Signed-off-by: Ben Price <[email protected]>
We now explicitly distinguish "two parameters in a typedef are named the same" and "a parameter is named the same as a constructor, or two constructors are named the same". (This is a somewhat silly split, as the second one arguably would be better as two separate checks. The reason it is broken up this way is that the first makes sense for primitive typedefs, and the second does not.) Previously, for ADTs, a repeated parameter name would have been caught by the check that all parameters+ctors are distinctly named. However, we now call `checkTypeDef` on primitives as well, which would not be covered by the ADT check (but primitives are hardcoded and don't repeat parameter names, so this is a somewhat pointless check). Signed-off-by: Ben Price <[email protected]>
Signed-off-by: Ben Price <[email protected]>
Signed-off-by: George Thomas <[email protected]> Signed-off-by: Ben Price <[email protected]>
Previously we would reset the selection to the root of the field's type, instead of simply updating the metadata of the selection which may point to some subtype. Signed-off-by: Ben Price <[email protected]>
Signed-off-by: George Thomas <[email protected]> Signed-off-by: Ben Price <[email protected]>
This wasn't actually due to test failures, just something I noticed in passing. The generators which create the initial program are very unlikely to pick the same names as the test will try to create -- we leave tweaking the generators to try to exercise this sort of thing more as future work. (Also note that adding a typedef is not an "offered" action, so that error wouldn't be hit here, however there is no harm in explicitly ignoring it.) Signed-off-by: George Thomas <[email protected]> Signed-off-by: Ben Price <[email protected]>
Previously we did not consistently check our input names were fresh, leading to some actions being accepted, only to later throw a typechecker error. We now always check the new name is fresh, but for ease of maintainability we collapse all such errors into one category (previously we had both `ParamAlreadyExists` and `TyConParamClash`). Instead of collapsing them, we could split out 5 different sorts of clashes (see comment on `TypeDefModifyNameClash` in this commit), but this does not seem necessary -- as far as I know, nobody actually wants to distinguish which of these 5 sorts of clashes happened. BREAKING CHANGE: this changes `ProgError`, which is serialised in the richly-typed API (but not the OpenAPI -- they are converted into http error codes instead). Signed-off-by: Ben Price <[email protected]>
brprice
force-pushed
the
georgefst/typedef-actions-tests
branch
from
224de87
to
88728cf
Compare
This was originally intended to be a part of #949, but the sheer number of issues revealed by the property test meant it was worth splitting out. Especially as the bugs are actually from much earlier work in adding the core
ProgActions for editing typedefs, rather than the higher-level API-related work in #949. Also, this branch might now be taken over by @brprice (though I'd be happy to clean things up a little before handing over, or at least walk through on a video call), since the remaining fixes (see final commit) are more in his wheelhouse.We may wish to document the fixes better by adding a regression test for each, and/or adding hedgehog replay seeds to the commit messages. I was unable to do this originally since the version of Hedgehog we were using had replay issues (#1027).
It might be worth bearing in mind that some remaining bugs could be caused by the presence of holes in typedefs. We have never really considered the extent to which we support this possibility, since we didn't initially think we'd need it. But since we decided that we want a UI for incrementally building typedefs, as opposed to a one-shot form, it became necessary to support. #949 imposes no restrictions on the presence of holes in typedefs, but neither does it to anything explicitly to support them.
#399 may also be relevant.