fix(python): Resolve Composite/Any type unification and nested class field coercion (#882)#918
Draft
olivier-aws wants to merge 5 commits intomainfrom
Draft
fix(python): Resolve Composite/Any type unification and nested class field coercion (#882)#918olivier-aws wants to merge 5 commits intomainfrom
olivier-aws wants to merge 5 commits intomainfrom
Conversation
Fix two root causes of "Impossible to unify" type checking errors when
user-defined class instances are used in contexts expecting Any:
1. Rename heap Box datatype to $Box to avoid name collision with
user-defined Python classes named "Box". Python identifiers cannot
contain $ so this eliminates the collision. Affects
HeapParameterizationConstants.lean and HeapParameterization.lean.
2. Add Composite→Any coercion (via Hole) in PythonToLaurel.lean for:
- Comparison operands (is/is not None on Composite values)
- List literal elements (Composite objects in [a, b])
- Dict literal values (Composite objects in {"k": obj})
- Field assignments on non-self objects (a.field = composite_val)
- Variable assignments where target is Any-typed
Also fix with-statement variable handling: stop hoisting with-variables
(which incorrectly typed them as Any) and let the With case handle
declaration with the correct type.
Fixes 8 of 11 tests from GitHub issue #882. Remaining 3 have different
root causes (resolution failures, Composite __enter__ return type).
Core type checker fails to unify Composite with Any/Box
- Rename targetIsComposite to targetNeedsCoercion with inverted logic to clarify intent (Bug 1 / Recommendation 2) - Add Composite→Any coercion for self.field = composite_val when no type annotation is present (Recommendation 5) - Remove unused _ctx parameter from getWithItemsVars (Design Concern 2) - Add TODO for replacing Hole-based coercion with from_ClassInstance pattern to preserve field values (Design Concern 1 / Recommendation 3) - Clarify with-statement coercion comments: mkInstanceMethodCall already returns Any for new variables, so additional coercion is unnecessary (Bug 2 addressed with documentation) - Fix stale comments: Box → $Box in HeapParameterization.lean (Stale Content 1, 2)
When a user-defined class has a field whose type is another user-defined class (e.g., Outer.inner: Inner), the translation failed with "Coercion from user-defined class to Any is not yet supported". Root cause: four interrelated gaps in PythonToLaurel.lean: 1. wrapFieldInAny threw for UserDefined fields instead of passing through 2. self.field access threw for UserDefined fields 3. translateMethod typed all non-self params as Any, causing Composite/Any mismatch when __init__ assigns to Composite-typed fields 4. self.field = value coerced Composite RHS to Hole via coerceToAny Fix: return UserDefined field expressions as-is (they are Composite heap references used for further field access or coerced later); type composite method parameters as UserDefined to match heap model expectations; skip coercion for Composite-to-Composite field assignments. Object-to-Any coercion not supported for nested class fields
…upported for nested class fields - Fix non-self attribute assignment path to skip coercion for composite fields, mirroring the self path logic (Bug 1) - Restore wrapFieldInAny for primitive self-field accesses so self.val gets wrapped in from_int/from_bool/etc., matching non-self path (Bug 2) - Add TODO for annotated composite assignment using New instead of RHS when RHS is an existing variable (Design Concern 1) - Add TODO for forward-reference class ordering issue in translateMethod (Design Concern 2) - Update stale comment about RHS type in self.field assignment - Fix misleading statement in memory doc about coerceToAny - Add test for non-self receiver composite field reassignment
olivier-aws
force-pushed
the
fix/issue-882-composite-any-unification
branch
from
c92aeac to
e538f6f
Compare
olivier-aws
changed the title
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
2 participants
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.
Summary
Fixes two related root causes from #882 that prevented pending Python tests involving user-defined classes from progressing through the analysis pipeline.
Changes
1. Composite/Any/Box type unification
Any(list insertion, dict storage, Any-typed variables).2. Nested class field coercion
PythonToLaurel.leanhad an explicit guard blocking coercion from user-defined class types to Any for nested object fields.Test status
test_object_in_listandtest_recursive_data(field resolution after container retrieval — separate root cause)Files changed
Strata/Languages/Python/PythonToLaurel.lean— main translation logicStrata/Languages/Laurel/HeapParameterization.lean— heap parameter handlingStrata/Languages/Laurel/HeapParameterizationConstants.lean— constantsStrataTest/Languages/Python/— new test files and expected outputsPartially addresses #882