Add resolution diagnostic for multi-output procedure in expression position#1116
Add resolution diagnostic for multi-output procedure in expression position#1116tautschnig wants to merge 3 commits intomainfrom
Conversation
…sition When a StaticCall to a multi-output procedure appears in expression position (not as the RHS of an Assign), emit an error diagnostic: the extra outputs would be silently discarded, which is a semantic bug (e.g., error channels lost). The diagnostic is suppressed when the call is the direct RHS of an assignment (where the target count check already validates arity). Includes a test in ResolutionKindTests demonstrating the diagnostic. Co-authored-by: Kiro <kiro-agent@users.noreply.github.com>
| let name' ← defineNameCheckDup param.name (.var param.name ty') | ||
| pure (⟨.Declare ⟨name', ty'⟩, vs⟩ : VariableMd) | ||
| let savedFlag := (← get).inAssignRhs | ||
| modify fun s => { s with inAssignRhs := true } |
There was a problem hiding this comment.
I think this won't work for issues that occur inside the RHS of an assignment. You need to set inAssignRhs to false when you find things that aren't assignments.
However, I think the easier to understand fix is to do type checking, which wouldn't rely on state. Could we ask a bot to add that to Resolution.lean? I don't think it's very difficult.
Something like:
Please add type checking to Resolution.lean. Let resolveStmtExpr return a ResolveM (StmtExprMd x HighTypeMd)and let the case for each StmtExpr constructor check that the types of its children are what is expected, if a particular type is expected.
Assigned this prompt to kbd-bot: #1120
There was a problem hiding this comment.
Pull request overview
Copilot reviewed 2 out of 2 changed files in this pull request and generated 3 comments.
💡 Add Copilot custom instructions for smarter, more guided reviews. Learn how to get started.
Address review feedback: - Replace coarse inAssignRhs flag with inValueContext that is set when recursing into arguments of StaticCall/PrimitiveOp. This correctly diagnoses nested multi-output calls (e.g., f(multi(1))) while not firing for statement-position calls or direct assignment RHS. - Factor out duplicate staticProcedure/instanceProcedure branches into a single outputCount lookup. Co-authored-by: Kiro <kiro-agent@users.noreply.github.com>
These are all value contexts where a multi-output procedure call would silently discard outputs. Co-authored-by: Kiro <kiro-agent@users.noreply.github.com>
|
How about instead of this PR we look at merging #1121 ? I know this PR is a strict improvement, but I think it might be confusing to temporarily have this code. We'll have to make sure to remove it later as well. Since it's so easy to add a more long term solution, shouldn't we do that? |
keyboardDrummer
left a comment
keyboardDrummer
left a comment
There was a problem hiding this comment.
Prefer to wait for #1121, but approving in case you prefer not to wait
When a StaticCall to a multi-output procedure appears in expression position (not as the RHS of an Assign), emit an error diagnostic: the extra outputs would be silently discarded, which is a semantic bug (e.g., error channels lost).
The diagnostic is suppressed when the call is the direct RHS of an assignment (where the target count check already validates arity).
Includes a test in ResolutionKindTests demonstrating the diagnostic.
By submitting this pull request, I confirm that you can use, modify, copy, and redistribute this contribution, under the terms of your choice.