tracking: CORE-04 traits residual — associated-type substitution, where-clause supertraits, coherence checking

[hyperpolymath]

TECH-DEBT.adoc:261-262 carries CORE-04 as S2 'partial' with NO issue number; CAPABILITY-MATRIX.adoc:134-137. Residual: (1) associated-type substitution in method bodies, (2) where-clause supertraits, (3) coherence checking — without coherence, overlapping impls can resolve arbitrarily (accepts-wrong-program class → T0); (1)/(2) are feature-absence (shippable disclosed → T1/T2 cut decision). Filed to give the ledger row a tracking home. Part of the v1-readiness ledger.

[hyperpolymath]

Ground-truth update (post-#622). Residual item (3), coherence checking, is now partially delivered, so this issue's scope has narrowed:

• ✅ Concrete-overlap coherence — DONE. Overlapping impls whose self types unify are now rejected before the check pass (lib/typecheck.ml check_all_coherence; lib/trait.ml check_coherence/check_all_coherence). The accepts-wrong-program (T0) risk for concrete overlaps is closed.
• ⏳ Generic-subsumption overlap — still open. impl[T] Greet for Box[T] overlapping impl Greet for Box[Int] is not yet detected; blocked on generic-impl registration (the coherence check would catch it once impl[T] … for Box[T] registers without a spurious "Trait not found").
• ⏳ (1) associated-type substitution in method bodies, (2) where-clause supertraits — unchanged.

Test-anchored status is now maintained in docs/SOUNDNESS.adoc (the #559 rows). Not closing this issue — it remains the tracker for the three residual items above.

---

Generated by Claude Code