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

[olivier-aws]

Summary

Fixes "Impossible to unify Any with Composite" when using PySpec.

Problem

When a factory-dispatched value (e.g., servicelib.connect("storage")) produces a Composite-typed value and it is passed to a function with an untyped parameter (which defaults to Any), the Core type checker fails because .tcons "Composite" [] cannot unify with .tcons "Any" [].

Fix

Apply coerceToAny to all translated arguments in translateCall, replacing Composite-typed arguments with Hole (unconstrained Any) before passing them to the callee. This extends the existing coercion mechanism (already used for return statements at line 1707) to cover call-site arguments.

Changes

• Strata/Languages/Python/PythonToLaurel.lean: Apply coerceToAny at both argument translation sites in translateCall
• StrataTestExtra/.../test_composite_arg_to_any_param.py: Reproduction test using servicelib
• StrataTestExtra/.../AnalyzeLaurelTest.lean: Register the new test

Testing

• lake build: ✅
• StrataTest (all unit tests): ✅
• Verified the test fails without the fix (Impossible to unify Any with Composite)

[olivier-aws]

@keyboardDrummer-bot , can you try to fix CI?

[olivier-aws]

@keyboardDrummer-bot The same code is duplicated in this PR (lines 1274 and 1312). Can you refactor?

[keyboardDrummer-bot]

Done — extracted the duplicated coercion logic into a coerceArgsToAny helper (defined right after coerceToAny) and replaced both call sites. Build passes.

[tautschnig]

Proof-coverage suggestions (what to prove next). coerceArgsToAny is partial, so direct object-level proof is not feasible without also making translateExpr / inferExprType non-partial. Three light-weight invariants are worth stating anyway, either as property-based tests via plausible or as meta-level checks invoked from a test harness:

• Length preservation. (coerceArgsToAny ctx args raw fd).map (·.length) = raw.length whenever the underlying coerceToAny doesn't throw. Catches regressions where an off-by-one in the zip pairing silently drops or duplicates arguments.

• Pointwise identity on non-Any params. For every i where fd.args[i]?.map (highTypeToPyLauType ·.laurelType.val) ≠ some PyLauType.Any, (coerceArgsToAny ...)[i]? = raw[i]?. Catches regressions where the Any-predicate is inverted.

• Pointwise coerceToAny-equivalence on Any params. For every i where the param type is Any, (coerceArgsToAny ...)[i]? equals some (← coerceToAny ctx args[i]! raw[i]!). Catches the dual regression.

Pre-existing gap noticed while reading, not this PR's problem. highTypeToPyLauType in PythonToLaurel.lean:283 maps .TFloat64 and .TReal to PyLauType.Any. That means a user-defined def f(x: float) has its x seen by this helper as Any-typed, and a Composite arg would be coerced to .Hole rather than type-error. Probably fine (float is not something you'd pass a Storage to anyway) but worth flagging.

Refactoring (non-blocking). The whole coercion path ultimately turns on isCompositeType and the PyLauType.Any string constant. Carrying a PyLauType enum (rather than a String type name) through the helpers would let the predicate param is Any be a pattern match rather than a string != and would remove a silent category of regressions — but that's well outside this PR's scope.

[tautschnig]

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".

[tautschnig]

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

[ssomayyajula]

FWIW, the fact that we have so many PRs around about Composite <-> Any (#727 and #677 for ex) deserves a more systematic review (#882 ?, but we'll get to that) - for callsite coercion, I'd be happy with the fixes @tautschnig is suggesting here.

[olivier-aws]

@keyboardDrummer-bot , please take into account @tautschnig 's inline comments

[keyboardDrummer-bot]

Addressed @tautschnig's inline review comments in commit 4790c1a:

coerceArgsToAny refactoring (all three issues):

• (a) Dead padding removed — the ++ List.replicate was never consumed since callers guarantee arity; removed entirely.
• (b) O(n²) fixed — replaced the mutable result := result ++ [x] loop with zipIdx.mapM, which builds the result list in one pass.
• (c) API asymmetry fixed — the helper now accepts Option PythonFunctionDecl. When none, all arguments are coerced to Any. This eliminates the match funcDecl with wrapper at the second call site and keeps the first call site's .get! only for the arity check (where it's still needed).

Call sites simplified:

• First call site (isVarKwargs branch): coerceArgsToAny ctx args rawPosArgs (some funcDecl)
• Second call site: coerceArgsToAny ctx args rawTransArgs funcDecl (one-liner, funcDecl is already Option)

New tests:

• test_composite_arg_to_any_param_kwargs.py — passes a Composite as a positional arg alongside **kwargs expansion, exercising the first coerceArgsToAny call site (isVarKwargs branch).
• test_composite_arg_typed_param.py — uses a class with a Storage-typed field and calls put_item on it, verifying that Composite-typed values retain their type for dispatch when not aligned with an Any parameter.

Not addressed: the optional expected-Laurel snapshot test (@tautschnig mentioned it as optional). Happy to add it if desired.

Build ✅ | lake test -- Languages.Python.AnalyzeLaurelTest ✅

[olivier-aws]

FWIW, the fact that we have so many PRs around about Composite <-> Any (#727 and #677 for ex) deserves a more systematic review (#882 ?, but we'll get to that) - for callsite coercion, I'd be happy with the fixes @tautschnig is suggesting here.

I agree that there are many such PRs, and would be worth a refactoring at some point. If that's fine with you, I'd like to still merge this PR as it fixes a bug we hit frequently. @ssomayyajula

[tautschnig]

Design trade-off introduced in d8d233de: the none arm leaves unknown-parameter-type arguments uncoerced. Walked the reasoning with the commit message:

• test_class_field_use has process_buffer(my_buf) called before process_buffer's signature is registered, so funcDecl = none. With the previous "coerce on unknown" behaviour, my_buf (a typed-Composite CircularBuffer) would become a Hole, and buf.buffer inside the function body would fail to dispatch. The new "leave on unknown" behaviour fixes that.
• The symmetric case is unknown_func(composite_val) where unknown_func happens to have an Any parameter. Under the old behaviour this worked (coerced to Hole). Under the new behaviour, the original Internal error when accessing a field from a Any typed composite #875 Impossible to unify Any with Composite is back for this specific shape.

The test_class_field_use evidence says the new behaviour is right for real code. But the #875 hazard-in-this-shape is now undocumented and unguarded.

Suggestion: add a fixture under dispatch_test/ that exercises the unknown-function-with-Any-parameter path — even as .failPrefix expecting the unification error if that's what the current behaviour produces. Pins the trade-off so a future "let's coerce unknown" refactor silently flipping the direction is caught. Two minutes of work; turns an implicit decision into an explicit regression test.

Alternative if the trade-off is judged clean: a one-line doc-comment on the none arm (-- See #875: we may get a unification error here if the unknown function's param is Any, but coercing on unknown broke test_class_field_use where a typed-Composite forward reference was being turned into Hole). No code change, just surfaces the decision for future readers.

[tautschnig]

Reversing my earlier approval on the grounds that a more foundational discussion is needed:

Follow-on to my earlier (already-approved) review. After submitting that, I kept pulling on the coerceArgsToAny design to understand why the none-arm trade-off in d8d233de felt unsatisfying, and surfaced a deeper concern that's worth a second look before merge. This is separate from the refactor threads (all resolved) and from the test_class_field_use regression trade-off (resolved via d8d233de).

The concern: coerceArgsToAny defeats the Any-wrapping-plus-preconditions design.

Strata's Python front-end has a consistent type-discipline model: every Python value is wrapped in the Any algebraic datatype; type annotations become preconditions on procedure bodies (assert Any..isfrom_int(x) for PySpec-declared callees). Type-annotation violations surface at call time through these preconditions, not through Laurel's type checker.

coerceArgsToAny now rewrites Composite arguments to .Hole before the callee's precondition fires. This has two bad effects:

1. For PySpec-declared callees: the precondition assert Any..isfrom_int(x) now evaluates on Hole rather than on the Composite. Hole is an unconstrained Any, so isfrom_int(Hole) is unprovable but not falsifiable — the diagnostic changes from a clear "isfrom_int precondition does not hold" (when the Composite was the actual argument) to a softer "cannot prove precondition on opaque value". The bug is still detected but the error is less informative.
2. For Python-native callees (no PySpec): there is no precondition at all. The Any-wrapping model relies on Laurel's own type checker to catch Impossible to unify Any with Composite in this case. The coercion defeats that check by rewriting the Composite out of existence. Result: a real user bug — passing a class instance to a primitive-typed parameter — now translates cleanly with no diagnostic at all. Silent miscompile.

Concrete Python that demonstrates (2):

class Container:
    def __init__(self):
        self.n: int = 0

def add_one(x: int) -> int:
    return x + 1

def main():
    c = Container()
    y = add_one(c)   # type error in Python; should be caught

• Pre-PR: add_one(c) failed Laurel type check with Impossible to unify Any with Composite. Imperfect error message, but present.
• Post-PR: coerceArgsToAny sees paramTypeNames[0] == PyLauType.Any (because pyArgLaurelType upstream-collapses x: int to TCore "Any"), calls coerceToAny on c, isCompositeType ctx "Container" is true, c becomes .Hole. The call translates cleanly. No diagnostic. y silently equals add_one(Hole), which returns an unconstrained int.

This is the same class of regression we dodged for test_class_field_use via d8d233de, just on a different axis: d8d233de covers the case where a Composite is passed to a known-Composite-typed forward-reference parameter; this covers the case where a Composite is passed to a primitive-typed (= upstream-collapsed-to-Any) parameter.

Root cause (why I think this is worth a structural fix rather than another band-aid):

coerceArgsToAny has to decide whether to coerce based on paramTypeNames[i] == PyLauType.Any, but at that point two very different situations look identical:

• Python-native def f(x): (no annotation): genuinely Any; coercion is desirable to enable the Any-wrapping convention at the call site.
• Python-native def f(x: int): (annotated primitive): intended-int but upstream-collapsed to Any by pyArgLaurelType; coercion is a silent miscompile.

The distinction was lost at pyArgLaurelType/specTypeToLaurelType earlier in the pipeline. coerceArgsToAny can't recover it.

Three possible directions, in increasing invasiveness:

1. Narrow the coercion predicate. Preserve enough upstream to distinguish "truly Any" from "collapsed-to-Any" — e.g. pyArgLaurelType could return TCore "Any" for real Any annotations (and no annotation) and a distinct marker like TCore "AnyFromInt" or TCore "CollapsedAny" for annotated primitives. coerceArgsToAny fires only on TCore "Any". Small, localized, keeps the Any-wrapping model intact.

2. Replace call-site coercion with a call-site assumption. At every f(composite) where f's param is Any-typed, instead of rewriting the argument to Hole, emit assume Any..isfrom_ClassInstance(translated_composite); f(translated_composite). This sidesteps the Laurel unification error (giving the solver a hint that the Composite-wrapped value is Any-compatible) without erasing type information. Preconditions at the callee still see the original Composite shape.

3. Preserve primitive types through the pipeline (pyArgLaurelType, specTypeToLaurelType, translateFieldType stop collapsing int/float/etc. to Any). Largest change; closes the hazard at the root but ripples across operator translation, expected snapshots, and overload dispatch. I flagged this in my earlier review as "out of scope"; I still think that's right for this PR. Worth its own design discussion.

Option 1 seems like the right fit for this PR: it's narrow, it preserves the design, and it closes the silent-miscompile for Python-native annotated code. Option 2 is also attractive but touches more call-site code. Option 3 belongs in a follow-up.

If none of the above is acceptable for this PR, at minimum worth landing a .failPrefix fixture that pins the current behaviour — a Python program shaped like the add_one(c) snippet above, with an expectation file documenting what diagnostic (if any) the pipeline currently produces. That makes the silent-miscompile explicit as a known limitation and prevents a future refactor from flipping the direction without triggering a visible test change.

This PR genuinely does fix the #875 hazard it targets. But since my earlier review approved on the strength of the resolved refactor threads, I want this design concern on the record before merge rather than discovering it in a future issue.

No inline comments; this is a body-level design observation. I ran a local branch audit to confirm the unreachability claims (all primitive branches of highTypeToPyLauType are dead code today, which is why the Any-wrapping design was working as intended pre-PR).