Emit Hole for Composite return values assigned to Any#727
Merged
tautschnig merged 7 commits intomainfrom Apr 4, 2026
Merged
Conversation
When a Python function returns a typed service client, the return value has type Composite but LaurelResult has type Any. Without coercion, Core type checking fails with "Impossible to unify Any with Composite". Add coerceToAny helper that wraps Composite values with from_ClassInstance (serializing fields to DictStrAny) when assigning to LaurelResult in return statements. Reuses the same pattern already used for f-string interpolation of Composite values. Co-authored-by: Kiro <kiro-agent@users.noreply.github.com>
Contributor
There was a problem hiding this comment.
Pull request overview
This PR addresses a Core type-checking failure in the Python→Laurel pipeline when a Python function returns a composite-typed value while the generated LaurelResult output is typed as Any. It introduces a coercion step that wraps composite return values into the Any runtime representation (from_ClassInstance + DictStrAny of fields), and adds a regression test.
Changes:
- Add
coerceToAnyhelper to wrap composite expressions intoAnyviafrom_ClassInstance+ serialized fields. - Apply
coerceToAnyto Pythonreturnstatements before assigning toLaurelResult. - Add a CBMC pipeline test covering a function annotated
-> Anythat returns a class instance.
Reviewed changes
Copilot reviewed 3 out of 3 changed files in this pull request and generated 3 comments.
| File | Description |
|---|---|
| Strata/Languages/Python/PythonToLaurel.lean | Adds coerceToAny and uses it in return-statement translation to prevent Any vs Composite unification failures. |
| StrataTest/Languages/Python/tests/test_composite_return.py | New regression test returning a composite value from a function typed as Any. |
| StrataTest/Languages/Python/tests/cbmc_expected.txt | Registers the new test as expected PASS in the CBMC pipeline test list. |
💡 Add Copilot custom instructions for smarter, more guided reviews. Learn how to get started.
- Add TODO comments on coerceToAny noting shared limitations with f-string interpolation: duplicated evaluation of translated expr in FieldSelect nodes, and no recursive handling of nested composites. - Fix column alignment in cbmc_expected.txt. - Add regression test in VerifyPythonTest exercising Composite return value coercion through the full Python → Laurel → Core → SMT pipeline. Co-authored-by: Kiro <kiro-agent@users.noreply.github.com>
keyboardDrummer
requested changes
Apr 2, 2026
Per consensus from keyboardDrummer and joehendrix: emit a Hole (unconstrained value) instead of building from_ClassInstance coercion when a Composite-typed expression is assigned to an Any-typed variable (e.g., LaurelResult in return statements). This avoids the type unification crash while being honest about the limitation — the verifier treats the return value as unconstrained, which limits bug-finding but doesn't produce unsound results. The from_ClassInstance coercion approach had additional issues (duplicated evaluation, no nested composite support) that this sidesteps entirely. Auto-generated coercions can be revisited once the Composite/Any typing design is resolved. Co-authored-by: Kiro <kiro-agent@users.noreply.github.com>
…posite # Conflicts: # Strata/Languages/Python/PythonToLaurel.lean
tautschnig
changed the title
joehendrix
reviewed
Apr 3, 2026
joehendrix
reviewed
Apr 3, 2026
joehendrix
reviewed
Apr 3, 2026
- Add missing 'from typing import Any' to test_composite_return.py - Check diags.size == 0 in VerifyPythonTest instead of discarding - Fix column alignment in cbmc_expected.txt Co-authored-by: Kiro <kiro-agent@users.noreply.github.com>
joehendrix
approved these changes
Apr 3, 2026
MikaelMayer
approved these changes
Apr 4, 2026
keyboardDrummer
approved these changes
Apr 4, 2026
tautschnig
added a commit
that referenced
this pull request
Apr 6, 2026
The Hole-based Composite→Any coercion (from PR #727) causes CBMC verification to fail. Skip for now. Co-authored-by: Kiro <kiro-agent@users.noreply.github.com>
This file contains hidden or bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
Sign up for free
to join this conversation on GitHub.
Already have an account?
Sign in to comment
Add this suggestion to a batch that can be applied as a single commit.This suggestion is invalid because no changes were made to the code.Suggestions cannot be applied while the pull request is closed.Suggestions cannot be applied while viewing a subset of changes.Only one suggestion per line can be applied in a batch.Add this suggestion to a batch that can be applied as a single commit.Applying suggestions on deleted lines is not supported.You must change the existing code in this line in order to create a valid suggestion.Outdated suggestions cannot be applied.This suggestion has been applied or marked resolved.Suggestions cannot be applied from pending reviews.Suggestions cannot be applied on multi-line comments.Suggestions cannot be applied while the pull request is queued to merge.Suggestion cannot be applied right now. Please check back later.
Problem
When a Python function returns a Composite-typed value (e.g., a service client) but the Laurel return variable
LaurelResulthas typeAny, Core type checking fails with "Impossible to unify Any with Composite".Approach
Per design discussion with @keyboardDrummer and @joehendrix: emit a Hole (unconstrained value) when a Composite-typed expression is returned from a function with Any return type. This avoids the type unification
crash while being honest about the limitation — the verifier treats the return value as unconstrained, which limits bug-finding but doesn't produce unsound results.
Auto-generated Composite -> Any coercions can be revisited once the broader Composite/Any typing design is resolved.
Changes:
coerceToAnyhelper that replaces Composite-typed expressions with a Hole when assigned to an Any-typed contextLaurelResultVerifyPythonTest.leanand CBMC pipelineBy submitting this pull request, I confirm that you can use, modify, copy, and redistribute this contribution, under the terms of your choice.