Merge dev into new-type-hole-inference (elastatics)

[cyrus-]

Brings PR #1872 (new-type-hole-inference) up to date with dev. The big delta on dev is the elastatics refactor (#2213) — combined statics + elaborator, replaced Self.re with Mark.t / Warning.t / Message.t, added Mod / Sig / MPat sorts. This branch reconciles those with the THI work (annotated provenances, unification constraints, type-hole projector) so the build is green and the inference pipeline is wired end-to-end.

The 9 commits are sequenced for review:

1. 18af1c8 — merge commit (conflict resolution per the strategy in commit message: dev wholesale for Statics.re / Info.re / StaticsBase.re / CustomStatics.re / test files; THI grammar kept for TPat, annotated provenance, Typ.equivalence; deletions accepted for Self.re, Elaborator.re, helpful-assistant/, Test_Info.re, Test_Evaluator_Probe.re)
2. dff435c — WIP build fixes (intermediate; could be squashed with the next on merge)
3. 3ee4f51 — post-merge build fixes: project compiles
4. fd09895 — TypeHole.cycle_hole factory + Test_Grammar exhaustiveness
5. eaad5e2 — annotate_static_errors tolerates inner-Prov IDs
6. 9471fff — wire constraint emission and inference_map end-to-end (Info.exp / Info.pat gain constraints field; Statics.mk_with_inference runs Inference.go; CachedStatics populated)
7. 3bab547 — Test_Inference smoke tests
8. a33b6c4 — emit MatchedTyp and branch constraints into the inference pipeline (Arrow / Prod / List / Poly refinements; pairwise If / Match / ListLit branch constraints)
9. 8e0ff2d — thread label_cons through all four TupLabel sites; clean up warnings

Non-obvious decisions

• TPat grammar kept from this branch (Unknown(prov) | Var) rather than dev's flat Invalid | EmptyHole | MultiHole | Var. The whole "tpats use type provenances" thing depends on it. Consequence: every dev-side TPat pattern (EmptyHole, MultiHole, etc.) was rewritten to Unknown({term: Hole(_), _}).
• Annotated type_provenance_t wrapper kept (every Unknown wraps an annotated prov, not bare). Consequence: every dev-side Unknown(SynSwitch) / Unknown(Internal) / Unknown(Hole(_)) was rewritten — Unknown({term: ..., _}) in pattern position, Unknown(... |> Prov.fresh) in expression position. Inner Prov annotations carry their own IDs that statics doesn't populate; Test_Statics_Prelude.annotate_static_errors now treats missing-info lookups for those IDs as "no error" instead of failing.
• Typ.meet returns tuple (t, list(equivalence)) from this branch — every dev call site (fixed_typ, expectation_mismatch_mark, ascription transition, etc.) was updated to unpack the constraint list.
• MatchedTyp rewritten to return constraints from every shape (arrow, poly_pair, prod, list_strict, label). Refinable Unknown(SynSwitch) inputs delegate to Typ.matched_*_of_prov and emit Con(ty, Shape(...)) constraints.
• Dropped the branch's f_prov parameter from map_term signatures. Nothing outside TermBase.re / Grammar.re ever called it, and keeping it would have forced rewrites of every dev-added Mod / Sig / MPat case. The Prov module still has its own internal traversal.
• Exercise.re taken wholesale from dev (47 lines, thin dispatcher). The branch's zipper_of_code / transition / stitching code referenced types (state, transitionary_spec, hint, pos, Editor) that no longer exist after dev's exercise reorganization into CodeExercise.re / DerivationExercise.re / TheoremExercise.re.
• Dropped branch's analyze_hazel CLI command. It used Info.show_error and Statics.Map.errors which don't exist post-elastatics. Re-add when needed.
• Added TypeHole to Language.ProjectorKind (dev moved Kind to the language library; this branch had renamed dev's Info projector to Statics and added TypeHole inline in ProjectorCore). Kept dev's Statics name, added TypeHole alongside.
• ProjectorInfo.mk_info now takes both ~sample_focus (dev) and ~inference (this branch).
• Constraint aggregation strategy: rather than threading constraint lists by hand through every Statics handler return signature, each Info entry stores its own constraints list at add time. mk_with_inference walks the finalized info_map and aggregates them (deduped by user-term rep id). Lower risk than rewriting every handler signature.

Constraint surface

What now produces constraints into the inference pipeline:

• Subsumption + Typ.meet structural constraints — automatic in add
• Arrow refinement — Ap (no-custom path), DeferredAp (no-custom path), Fun
• Poly refinement — TypAp, TypFun
• Prod refinement — Tuple (exp + pat)
• List refinement — ListLit, Cons, ListConcat (exp + pat)
• TupLabel refinement — all four TupLabel sites (exp + pat, inside-tuple + standalone)
• Pairwise branch equivalence — If, Match, ListLit
• Builtin custom statics — to_lvs_statics, omit_all_labels_statics

Tests

test/Test_Inference.re adds 6 smoke tests directly exercising the constraint paths:

• 1 + 2 and let x : Int = 1 in x + 2 — no-unknowns no-crash
• (? : ? -> ?)(1) — arrow refinement
• if true then 1 else ? — If branch constraint
• [1, ?, ?] — ListLit branch constraint
• ((a=1, b=?) : (a=Int, b=?)) — TupLabel refinement

Build green, all 2694 tests pass.

🤖 Generated with Claude Code