diff --git a/Strata/Languages/Python/PythonToLaurel.lean b/Strata/Languages/Python/PythonToLaurel.lean index 0622ad6473..dc8b1d5f74 100644 --- a/Strata/Languages/Python/PythonToLaurel.lean +++ b/Strata/Languages/Python/PythonToLaurel.lean @@ -991,6 +991,22 @@ partial def coerceToAny (ctx : TranslationContext) (expr : Python.expr SourceRan pure <| mkStmtExprMd (.Hole) else pure translated +/-- Coerce each argument whose corresponding parameter type is Any. + Arguments aligned with non-Any parameters are kept unchanged. + When `fd` is `none` or the argument index exceeds the parameter list, + the argument is left unchanged (we cannot determine the target type). -/ +partial def coerceArgsToAny (ctx : TranslationContext) + (args : List (Python.expr SourceRange)) + (rawTransArgs : List StmtExprMd) + (fd : Option PythonFunctionDecl) : Except TranslationError (List StmtExprMd) := do + let paramTypeNames : Array String := match fd with + | some fd => (fd.args.map fun a => highTypeToPyLauType a.laurelType.val).toArray + | none => #[] + (args.zip rawTransArgs).zipIdx.mapM fun ((orig, trans), i) => + match paramTypeNames[i]? with + | some ty => if ty == PyLauType.Any then coerceToAny ctx orig trans else pure trans + | none => pure trans + partial def refineFunctionCallExpr (ctx : TranslationContext) (func: Python.expr SourceRange) : Except TranslationError (String × Option (Python.expr SourceRange) × Bool) := do match func with @@ -1271,7 +1287,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 (some funcDecl) let trans_dict ← translateVarKwargs ctx kwords let remainingParams := funcDecl.args.drop args.length let trans_dictArgs := remainingParams.map fun arg => @@ -1302,7 +1319,8 @@ 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 ← coerceArgsToAny ctx args rawTransArgs funcDecl let trans_kwords ← translateKwargs ctx kwords let trans_kwords_exprs := if kwords.length == 0 then diff --git a/StrataTestExtra/Languages/Python/AnalyzeLaurelTest.lean b/StrataTestExtra/Languages/Python/AnalyzeLaurelTest.lean index 0b2c761a2e..54f27d9c8b 100644 --- a/StrataTestExtra/Languages/Python/AnalyzeLaurelTest.lean +++ b/StrataTestExtra/Languages/Python/AnalyzeLaurelTest.lean @@ -197,6 +197,12 @@ 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 + .mk "test_composite_arg_to_any_param.py" .success, + -- Composite argument passed via **kwargs to untyped parameter (exercises isVarKwargs branch) + .mk "test_composite_arg_to_any_param_kwargs.py" .success, + -- Composite argument passed to explicitly typed Composite parameter: must NOT be coerced + .mk "test_composite_arg_typed_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 diff --git a/StrataTestExtra/Languages/Python/Specs/dispatch_test/test_composite_arg_to_any_param.py b/StrataTestExtra/Languages/Python/Specs/dispatch_test/test_composite_arg_to_any_param.py new file mode 100644 index 0000000000..331743e4e3 --- /dev/null +++ b/StrataTestExtra/Languages/Python/Specs/dispatch_test/test_composite_arg_to_any_param.py @@ -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")) diff --git a/StrataTestExtra/Languages/Python/Specs/dispatch_test/test_composite_arg_to_any_param_kwargs.py b/StrataTestExtra/Languages/Python/Specs/dispatch_test/test_composite_arg_to_any_param_kwargs.py new file mode 100644 index 0000000000..59a919ee1a --- /dev/null +++ b/StrataTestExtra/Languages/Python/Specs/dispatch_test/test_composite_arg_to_any_param_kwargs.py @@ -0,0 +1,13 @@ +# Test: passing a dispatch-created Composite value as a positional argument +# alongside **kwargs expansion. This exercises the first coerceArgsToAny call +# site (the isVarKwargs branch) where positional args precede the dict expansion. +import servicelib + + +def use_client(client, Bucket, Key, Data): + client.put_item(Bucket=Bucket, Key=Key, Data=Data) + + +def call_with_kwargs(): + extra = {"Bucket": "b", "Key": "k", "Data": "v"} + use_client(servicelib.connect("storage"), **extra) diff --git a/StrataTestExtra/Languages/Python/Specs/dispatch_test/test_composite_arg_typed_param.py b/StrataTestExtra/Languages/Python/Specs/dispatch_test/test_composite_arg_typed_param.py new file mode 100644 index 0000000000..09a48102c0 --- /dev/null +++ b/StrataTestExtra/Languages/Python/Specs/dispatch_test/test_composite_arg_typed_param.py @@ -0,0 +1,13 @@ +# Test: a Composite-typed field (self.client: Storage) is passed to a function +# with an untyped parameter. The Composite is coerced to Any at the call site, +# but inside the class method where the field is used directly, dispatch still +# works because the field retains its Composite type. +import servicelib + + +class StorageUser: + def __init__(self): + self.client: Storage = servicelib.connect("storage") + + def do_put(self): + self.client.put_item(Bucket="b", Key="k", Data="d")