Emit Hole for Composite return values assigned to Any (#727)

### Problem

When a Python function returns a Composite-typed value (e.g., a service
client) but the Laurel return variable `LaurelResult` has type `Any`,
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:**
- Add `coerceToAny` helper that replaces Composite-typed expressions
with a Hole when assigned to an Any-typed context
- Apply coercion in return statement translation before assigning to
`LaurelResult`
- Add regression tests in `VerifyPythonTest.lean` and CBMC pipeline

By submitting this pull request, I confirm that you can use, modify,
copy, and redistribute this contribution, under the terms of your
choice.

---------

Co-authored-by: Kiro <kiro-agent@users.noreply.github.com>
Co-authored-by: Shilpi Goel <shigoel@gmail.com>

Author: 3 people

Strata/Languages/Python/PythonToLaurel.lean

@@ -738,6 +738,17 @@ If the function_name is a class, add __init__ into it
 The following function return a tuple (translated function name, first argument, is the first argument of unknown type)
 -/
 
+/-- Coerce an expression to Any if its inferred type is a Composite class.
+    Composite values are replaced with a Hole (unconstrained Any value)
+    since Composite→Any coercion is not yet modeled. This limits
+    bug-finding ability but avoids type unification errors. -/
+partial def coerceToAny (ctx : TranslationContext) (expr : Python.expr SourceRange)
+    (translated : StmtExprMd) : Except TranslationError StmtExprMd := do
+  let ty ← inferExprType ctx expr
+  if isCompositeType ctx ty then
+    pure <| mkStmtExprMd (.Hole)
+  else pure translated
+
 partial def refineFunctionCallExpr (ctx : TranslationContext) (func: Python.expr SourceRange) :
       Except TranslationError (String × Option (Python.expr SourceRange) × Bool) := do
   match func with
@@ -1207,6 +1218,8 @@ partial def translateStmt (ctx : TranslationContext) (s : Python.stmt SourceRang
     let stmts ← match value.val with
       | some expr => do
         let e ← translateExpr ctx expr
+        -- Coerce Composite return values to Any for LaurelResult : Any
+        let e ← coerceToAny ctx expr e
         let assign := mkStmtExprMd (StmtExpr.Assign [mkStmtExprMd (StmtExpr.Identifier PyLauFuncReturnVar)] e)
         .ok [assign, mkStmtExprMd (StmtExpr.Exit "$body")]
       | none => .ok [mkStmtExprMd (StmtExpr.Exit "$body")]

StrataTest/Languages/Python/VerifyPythonTest.lean

@@ -130,4 +130,25 @@ open Strata.Parser (stringInputContext)
   if diags.size ≠ 0 then
     throw <| .userError s!"Expected 0 diagnostics, got {diags.size}"
 
+-- Returning a Composite-typed value from a function with Any return type
+-- should not crash; the Composite is replaced with a Hole (unconstrained value).
+#guard_msgs in
+#eval withPython (warnOnSkip := false) fun pythonCmd => do
+  let program :=
+"from typing import Any
+
+class MyService:
+    name: str
+
+    def __init__(self, name: str) -> None:
+        self.name = name
+
+def create_service() -> Any:
+    svc: MyService = MyService(\"test\")
+    return svc
+"
+  let diags ← processPythonFile pythonCmd (stringInputContext "test.py" program)
+  if diags.size ≠ 0 then
+    throw <| .userError s!"Expected 0 diagnostics, got {diags.size}"
+
 end Strata.Python.VerifyPythonTest

StrataTest/Languages/Python/tests/cbmc_expected.txt

@@ -31,3 +31,4 @@ test_class_with_methods.py.ion  SKIP
 test_module_level.py.ion        SKIP
 test_if_elif.py.ion             SKIP
 test_variable_reassign.py.ion   SKIP
+test_composite_return.py.ion    PASS

StrataTest/Languages/Python/tests/test_composite_return.py

@@ -0,0 +1,11 @@
+from typing import Any
+
+class MyService:
+    name: str
+
+    def __init__(self, name: str) -> None:
+        self.name = name
+
+def create_service() -> Any:
+    svc: MyService = MyService("test")
+    return svc