Fix DictNoneTest Test 6: len() rejection is an error, not a diagnostic (#1035)

Test 6 (len() on a class without __len__) was always broken since its
introduction in PR #761 (bb11e70). The test expected processPythonFile
to return diagnostics, but the len() rejection throws a TranslationError
in PythonToLaurel.lean, which withPythonToLaurel converts to an IO.Error
before the diagnostic stage is reached.

The test was never caught because:
1. It was authored in an environment without Python, so withPython
skipped and #guard_msgs saw empty output (matching the empty docstring).
2. DictNoneTest was not in CI's explicit Python test list in ci.yml, so
it was never run in CI either.

Fix: catch the IO.Error and verify it contains the expected message, and
add DictNoneTest to CI's Python test list.

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: Remy Willems <rwillems@amazon.com>
Co-authored-by: Copilot <175728472+Copilot@users.noreply.github.com>

Author: 4 people

.github/workflows/ci.yml

@@ -304,7 +304,7 @@ jobs:
               sudo cp z3-4.13.4-x64-glibc-2.35/bin/z3 /usr/local/bin/
             fi
     - name: Run PySpec and dispatch tests
-      run: PYTHON=python PYTHON_TEST=1 lake build StrataTest.Languages.Python.SpecsTest StrataTest.Languages.Python.AnalyzeLaurelTest StrataTest.Languages.Python.Specs.IdentifyOverloadsTest StrataTest.Languages.Python.VerifyPythonTest StrataTest.Languages.Python.PropertySummaryTest
+      run: PYTHON=python PYTHON_TEST=1 lake build StrataTest.Languages.Python.SpecsTest StrataTest.Languages.Python.AnalyzeLaurelTest StrataTest.Languages.Python.Specs.IdentifyOverloadsTest StrataTest.Languages.Python.VerifyPythonTest StrataTest.Languages.Python.PropertySummaryTest StrataTest.Languages.Python.DictNoneTest
     - name: Run test script
       run: FAIL_FAST=1 ./scripts/run_cpython_tests.sh ${{ matrix.python_version }}
       working-directory: Tools/Python

StrataTest/Languages/Python/DictNoneTest.lean

@@ -93,7 +93,8 @@ def main() -> None:
     throw <| .userError s!"Expected assertion failure for negative indexing on empty list, got: {diags.map (·.message)}"
 
 -- Test 6: len() on a class instance without __len__.
--- This should be rejected as a user error.
+-- This should be rejected as a user error during translation (before
+-- diagnostics are produced), so processPythonFile throws an IO.Error.
 #guard_msgs in
 #eval withPython (warnOnSkip := false) fun pythonCmd => do
   let program :=
@@ -106,8 +107,10 @@ def main() -> None:
     obj: MyObj = MyObj(\"test\")
     n: int = len(obj)
 "
-  let diags ← processPythonFile pythonCmd (stringInputContext "test.py" program)
-  if diags.size == 0 then
-    throw <| .userError s!"Expected ≥1 diagnostic for len() on Composite, got 0"
+  match ← (processPythonFile pythonCmd (stringInputContext "test.py" program)).toBaseIO with
+  | .ok _ => throw <| IO.userError "Expected error for len() on class without __len__"
+  | .error err =>
+    unless containsSubstr (toString err) "len() is not supported" do
+      throw <| IO.userError s!"Unexpected error: {err}"
 
 end Strata.Python.DictNoneTest