refactor: decompose synth/check into helpers in typeinfer.py

[alcides]

What

Behavior-preserving decomposition of the two large match statements in aeon/typechecking/typeinfer.py.

synth dispatch table

The heavy arms — Application, Let, Rec, If — each carried 30–60 lines of binder/existential bookkeeping inline. They are extracted into module-level helpers _synth_application, _synth_let, _synth_rec, and _synth_if. The top-level synth match now reads as a dispatch table; each helper takes the context plus the destructured term fields and returns exactly what the arm returned.

Shared Rec logic

The Rec handling was duplicated almost verbatim between synth and check. It is now factored into one helper:

_rec_constraints(ctx, t, self_type, comp_types, body_handler) -> (Constraint, Type | None)

The two call sites differ only in:

• the type bound for the recursive occurrence / siblings (declared type in synth, a freshened copy in check), passed as self_type / comp_types;
• how the body is processed (synth returns the body type; check discards it and returns None), passed as body_handler.

The Form B existential wrap of the body type stays at the synth call site, since only synth propagates a type outward.

Behavior preservation

This is pure code motion. The emitted constraints, the order of context extension, fresh-name generation (fresh_counter), and existential/binder handling are all identical to before — both Rec call sites produce the same constraints they did when the logic was inline. No public API changed: synth, check, check_type, and check_type_errors keep their signatures.

Validation

• uv run pytest -q: 1686 passed, 14 skipped, 73 warnings — no failures, no errors.
• Pre-commit (mypy + ruff legacy + ruff format) passes.

🤖 Generated with Claude Code

[alcides]

@claude can you fix this PR?