clarity refactors around typechecking in
#620
Conversation
| Some(EntityType::Unspecified) => { | ||
| // It's perfectly valid for `principal` or `resource` to be `EntityType::Unspecified` |
There was a problem hiding this comment.
The rest of the changes in this PR look good to me, but I think this case is a behavior change. To match the Dafny spec I think you just want to use Type::primitive_boolean() here.
There was a problem hiding this comment.
I don't think this is a behavior change, because the case where we return Type::singleton_boolean(false) is actually unreachable -- we would have already returned at line 1762 and never even reached this function.
For the question about the Dafny spec, I believe the Dafny spec returns singleton-false for this case as well (unspecified in RHS where RHS is a single specified entity literal or set of specified entity literals) at lines 417-418 at your link, and never reaches the line 439 which you pointed to.
Perhaps both the Rust and Dafny need additional comments to clarify which cases actually reach particular lines. It took me a long time to puzzle these out as well. I feel that neither codebase is particularly well organized in how it typechecks in.
There was a problem hiding this comment.
This part of the code is quite annoying due to the handling of unspecified entities 😞 Looking at it again, I think you're right that the earlier handling means that the else statement here will never be reached. I think the then part is also unreachable: it is impossible to have a set of entity literals that contains an unspecified entity. So maybe there was a reason to return TypecheckFail after all 🤔
There was a problem hiding this comment.
It still seems incorrect to ignore the failure of TypecheckFail though.
There was a problem hiding this comment.
I think changing the behavior many layers above to not ignore TypecheckFail would be a great idea but is well beyond the scope of this PR. Perhaps we could do that first though? If we're right that this is unreachable, then it shouldn't matter whether we return Fail or Success, at least until some refactor makes this code reachable again
There was a problem hiding this comment.
I agree with Kesha's assessment of the un-reachability of both branches. The then statement could only be reached if an entity literal had an unspecified entity type, but that can't happen. The else branch is more subtle, but Craig seems to be correct that the unspecified-in-specifed case rules out that branch.
Description of changes
This PR represents the parts of #603 which we still want to keep after #615 fixed the underlying issue. See discussion on #603. This PR should be no-functional-changes.
I threw in a small refactor in the caller
typecheck_in()that wasn't in #603, but which I feel improves clarity slightlyChecklist for requesting a review
The change in this PR is (choose one, and delete the other options):
cedar-policy-core,cedar-validator, etc.)I confirm that this PR (choose one, and delete the other options):
I confirm that
cedar-spec(choose one, and delete the other options):Disclaimer
By submitting this pull request, I confirm that you can use, modify, copy, and redistribute this contribution, under the terms of your choice.