Skip to content

fix(python): Coerce Composite args to Any at call sites #1106

New issue

Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.

Sign up for GitHub

By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.

Already on GitHub? Sign in to your account

Open
olivier-aws wants to merge 9 commits into
base: main
Choose a base branch
from
Open

fix(python): Coerce Composite args to Any at call sites #1106

Show file tree
Hide file tree
Changes from 5 commits
Commits
Show all changes
9 commits
Select commit Hold shift + click to select a range
b58fff3
fix(python): Coerce Composite args to Any at function call sites
olivier-aws May 5, 2026
4d8c6e5
fix(python): Only coerce Composite args when parameter is explicitly Any
olivier-aws May 5, 2026
b3ba52e
Merge remote-tracking branch 'origin/main' into type_error_fix
keyboardDrummer-bot May 5, 2026
47fef11
fix: revert test_class_field_any expected file to Inconclusive
keyboardDrummer-bot May 5, 2026
74ed41b
refactor: extract coerceArgsToAny to eliminate duplication
keyboardDrummer-bot May 5, 2026
4790c1a
refactor(python): address review feedback on coerceArgsToAny
keyboardDrummer-bot May 5, 2026
f5f1dea
Merge branch 'main' into type_error_fix
keyboardDrummer-bot May 5, 2026
d8d233d
fix: don't coerce args when parameter type is unknown
keyboardDrummer-bot May 5, 2026
52f745b
Merge branch 'main' into type_error_fix
olivier-aws May 6, 2026
File filter

Filter by extension

Filter by extension
Conversations
Failed to load comments.
Loading
Jump to
Jump to file
Failed to load files.
Loading
Diff view
Diff view
23 changes: 21 additions & 2 deletions Strata/Languages/Python/PythonToLaurel.lean
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -991,6 +991,21 @@ partial def coerceToAny (ctx : TranslationContext) (expr : Python.expr SourceRan
pure <| mkStmtExprMd (.Hole)
else pure translated

/-- Coerce each argument whose corresponding parameter type is Any.

@MikaelMayer MikaelMayer May 26, 2026

Copy link
Copy Markdown
Contributor

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

I will reiterate what I said in the other PRs. In the current modeling, we assume that values of type Any are never composite since toString is a function that does not depend on the heap. Whereas by construction it was not possible to hit this soundness issue before, this PR would concretize the soundness issue by making it possible to cast a composite into an Any.

The solution is obviously to make toString a bodiless procedure and not a bodiless function and declare that this procedure modifies the heap.

Arguments aligned with non-Any parameters are kept unchanged. -/
partial def coerceArgsToAny (ctx : TranslationContext)
(args : List (Python.expr SourceRange))
(rawTransArgs : List StmtExprMd)
(fd : PythonFunctionDecl) : Except TranslationError (List StmtExprMd) := do
let paramTypeNames := fd.args.map (fun a => highTypeToPyLauType a.laurelType.val)
let mut result : List StmtExprMd := []
for (pair, paramTy) in (args.zip rawTransArgs).zip
(paramTypeNames ++ List.replicate args.length PyLauType.Any) do
let (orig, trans) := pair
if paramTy != PyLauType.Any then result := result ++ [trans]
else result := result ++ [← coerceToAny ctx orig trans]
pure result
Comment thread
olivier-aws marked this conversation as resolved.
Outdated

partial def refineFunctionCallExpr (ctx : TranslationContext) (func: Python.expr SourceRange) :
Except TranslationError (String × Option (Python.expr SourceRange) × Bool) := do
match func with
Expand Down Expand Up @@ -1271,7 +1286,8 @@ partial def translateCall (ctx : TranslationContext)
if args.length > funcDecl.args.length then
throwUserError callRange
s!"'{name}' called with too many positional arguments: expected at most {funcDecl.args.length}, got {args.length}"
let trans_posArgs ← args.mapM (translateExpr ctx)
let rawPosArgs ← args.mapM (translateExpr ctx)
let trans_posArgs ← coerceArgsToAny ctx args rawPosArgs funcDecl

@tautschnig tautschnig May 5, 2026

Copy link
Copy Markdown
Contributor

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

If you take the Option PythonFunctionDecl refactor from the other inline comment, this becomes:

Suggested change
let trans_posArgs ← coerceArgsToAny ctx args rawPosArgs funcDecl
let rawPosArgs ← args.mapM (translateExpr ctx)
let trans_posArgs ← coerceArgsToAny ctx args rawPosArgs (some funcDecl)

and the funcDecl := funcDecl.get! above this can stay as-is (it's still needed for the arity check, funcDecl.args, etc.). Or wrap: let trans_posArgs ← coerceArgsToAny ctx args rawPosArgs (funcDecl := funcDecl) with funcDecl already being the unwrapped value — the helper then just treats .none as "nothing to coerce".

let trans_dict ← translateVarKwargs ctx kwords
let remainingParams := funcDecl.args.drop args.length
let trans_dictArgs := remainingParams.map fun arg =>
Expand Down Expand Up @@ -1302,7 +1318,10 @@ partial def translateCall (ctx : TranslationContext)
else
let (args, kwords, funcdecl_hasKwargs) ←
combinePositionalAndKeywordArgs args kwords funcDecl methodName callRange
let trans_args ← args.mapM (translateExpr ctx)
let rawTransArgs ← args.mapM (translateExpr ctx)
let trans_args ← match funcDecl with
| none => pure rawTransArgs
| some fd => coerceArgsToAny ctx args rawTransArgs fd

@tautschnig tautschnig May 5, 2026

Copy link
Copy Markdown
Contributor

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

Paired with the Option-taking refactor in the other inline comment, this three-line match collapses to a one-liner that mirrors the first call site:

Suggested change
let trans_args ← match funcDecl with
| none => pure rawTransArgs
| some fd => coerceArgsToAny ctx args rawTransArgs fd
let rawTransArgs ← args.mapM (translateExpr ctx)
let trans_args ← coerceArgsToAny ctx args rawTransArgs funcDecl

let trans_kwords ← translateKwargs ctx kwords
let trans_kwords_exprs :=
if kwords.length == 0 then
Expand Down
2 changes: 2 additions & 0 deletions StrataTestExtra/Languages/Python/AnalyzeLaurelTest.lean
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -197,6 +197,8 @@ private meta def testCases : List (String × Expected) := [
.mk "test_annotation_dispatch.py" .success,
.mk "test_constructor_dispatch.py" .success,
.mk "test_reassign_dispatch.py" .success,
-- Composite argument passed to untyped (Any) parameter: coercion must prevent type error
Comment thread
olivier-aws marked this conversation as resolved.
.mk "test_composite_arg_to_any_param.py" .success,
-- Known failing tests:
-- With @ separator, Storage_put_item is no longer a known symbol, so it
-- falls through to the default Any type. These should produce an
Expand Down
12 changes: 12 additions & 0 deletions StrataTestExtra/Languages/Python/Specs/dispatch_test/test_composite_arg_to_any_param.py
View file
Open in desktop
Original file line number Diff line number Diff line change
@@ -0,0 +1,12 @@
# Test: passing a dispatch-created Composite value to a function with untyped parameter.
# Before the fix, this caused "Impossible to unify Any with Composite" because
# the factory dispatch produces a Composite-typed value but the function parameter
# defaults to Any.
import servicelib


def use_storage(client):
client.put_item(Bucket="test", Key="k", Data="v")


use_storage(servicelib.connect("storage"))
Loading