Replace runtime-type quotation with splice-into-source typechecking

[datvo06]

Closes #696. Addresses #577, #576.

Currently, for synthesis, we are reconstructing a Template's lexical context as synthetic type stubs. This is brittle and likely unsound.

This PR splices the generated code into the Template module, and type checks the whole file. This come with a few changes

1. mypy_type_check now parameterized with generated (code) and anchor (the Template). The anchor is used to recover its module source,

Note, in practice there is a few more tweaks:

• Mypy runs on the whole module, but only diagnostics inside the spliced span are raised, so an unrelated pre-existing error elsewhere in the module can't fail synthesis.
• Non-nestable constructs (from x import *, __future__) are caught by an explicit AST pre-scan, since mypy silently accepts a nested star-import; a fatal mypy error (exit ≥ 2) is surfaced rather than silently passed; unrecoverable source (no file, no linecache) is skipped with a logged reason.

2. Name collisions (Synthesized Callable Name shouldn't matter #542) are now handled structurally: the generated def is a function-body local that shadows a colliding context name rather than redefining it at module level, so the AST-rename pass is gone. The whole quotation layer is deleted — type_to_ast, signature_to_ast, collect_variable_declarations, collect_runtime_type_stubs, collect_imports, and _RenameTransformer/_generate_unique_name (net +510 / −1991).

3. Behavior change. Runtime-only / local types, and names with no lexical presence at the splice point, now raise instead of being (partially, fakily) stubbed. The check is sound on annotated generated code; unannotated bodies are checked at their signature only (--check-untyped-defs is deliberately off — it rejects runnable heterogeneous-container code).

Tests.

1. Deleted the quotation-internals unit tests; kept the security/REPL tests
2. Added behavior tests asserting raise-or-not (not mypy text): Synthesized Callable Name shouldn't matter #542 collision shadowing, the gate (unrelated module error doesn't block a correct synthesis), closures (enclosing locals in scope), method/static/class templates, Enum + dataclass context (Decoding runtime-only Pydantic models in Callables fails #576), injected-name, non-nestable, linecache-backed recovery (the REPL tool code should be typechecked when possible #690 path), annotation-collision, and end-to-end decode through Encodable[Callable]. mypy effectful/handlers/llm/ clean, ruff clean, full LLM suite green.

[datvo06]

My intuition is mypy failed with stress test. Checking..

[eb8680]

Thanks, this seems like a big improvement. There are several heuristics and silent failures that I worry will undermine its correctness, though.

[eb8680]

Nearly there, just a few small things

[eb8680]

I'm not sure template.__default__ will work as anchor for bound-method Templates. You should make sure this case is covered in a test, which you'll probably then need to fix.

[datvo06]

I added an integration test, and it works ok after multiple retries (due to LLM flakiness), also added the replay record.

[datvo06]

The relay buffer gives me this:

┌───────┬────────────────────────────────────────────────────┬────────┐
│ Round │                   Generated code                   │ Valid? │
├───────┼────────────────────────────────────────────────────┼────────┤
│ 0     │ def add(a, b) -> int:\n    return a + b<br>\n\nadd │ ✗      │
├───────┼────────────────────────────────────────────────────┼────────┤
│ 1     │ def add(...): ...<br>\n\n# comment\n\nadd          │ ✗      │
├───────┼────────────────────────────────────────────────────┼────────┤
│ 2     │ def add(...): ...<br>\n\nadd                       │ ✗      │
├───────┼────────────────────────────────────────────────────┼────────┤
│ 3     │ def add(a: int, b: int) -> int:\n    return a + b  │ ✓      │
└───────┴────────────────────────────────────────────────────┴────────┘

The function body is correct every time — that's the part that "looks correct." But rounds 0–2 append a trailing bare add (the function name on its own line, as a "here's the result" hint). That makes the module's last statement a bare Expr, and decode requires it to be a FunctionDef:

Value error, decode() requires the last statement to be a function definition, got Expr

I think this is more of the mypy thing but not sure we should try adding fix in this PR cause
I'm not sure how sound/complete the solution could be, and it still works after multiple retries.