unify: lenient {m0, mw} compatibility (eigentrust pitfall #2)

[kumavis]

Fixes pitfall #2 from docs/tracking/2026-04-23_eigentrust_pitfalls.md.

Summary

spec scale-vec Rat [List Rat] -> [List Rat]
defn scale-vec [s xs]
  [map (fn [x : Rat] [rat* s x]) xs]

failed with a QTT multiplicity error. The pitfall report described it as "closure capture of s at multiplicity 1 vs many uses." Investigation showed that diagnosis is wrong — the closure is fine. The actual root cause is at the kind level.

Root cause (the surprise)

Tracing checkQ-fb revealed:

• List is registered with kind Pi(m0, Type, Type)
• map's {C : Type → Type} elaborates to Pi(mw, Type, Type) (the inner → defaults to mw via surf-arrow)
• Implicit type-arg unification then tries to unify m0 and mw and fails

The "closure captures linearly" message was misleading — the failure was in implicit-type-arg unification at the kind level, not in the value-level closure mult system.

Approach (a) — surgical {m0, mw} lenience in unify-mult

In unify.rkt's classify-mult-problem: extend the compatibility table so {m0, mw} (and {mw, m0}) unify successfully without solving either to the other.

Why principled: m0 ("zero runtime uses") trivially satisfies mw ("any number, including zero"). Treating these as compatible is sound. {m1, *} pairs stay incompatible — linearity is a real value-level constraint.

Latent bug exposed: three solve-mult-meta! call sites in typing-core.rkt re-solve already-solved metas, which the new lenience path makes observable. Guarded with mult-meta-solved? checks.

Deferred to a future PR

Approach (c) — full type-driven closure-capture mult inference from the callee's spec — is the principled long-term fix for cases the {m0, mw} lenience doesn't cover (e.g., spec-position threading into closure elaboration). Out of scope here.

Files changed

• racket/prologos/unify.rkt (~12 LoC) — classify-mult-problem extended with {m0, mw} compatibility case
• racket/prologos/typing-core.rkt — three solve-mult-meta! calls guarded with mult-meta-solved? (latent bug exposed by the unify change)
• racket/prologos/tests/test-unify.rkt — replaced one stale assertion with two new tests covering both directions of the new lenience
• racket/prologos/tests/test-closure-mult.rkt (new, 10 cases)

Test plan

• Eigentrust scale-vec example now produces '[1/4 1/8 1/16] : [List Rat]
• All 105 mult/qtt-related tests pass
• All 51 unify tests pass
• All 141 capability/qtt-pipeline tests pass
• Full suite: 7818 tests / 545s — 9 failures, all pre-existing environmental (prologos/propagator and rackcheck collections unavailable in the agent's Racket install). None are caused by this change.
• CI fix included (benchmarks/micro/info.rkt skip; redundant once PR Migrate bench-bsp-le-track2.rkt to current ATMS API (CI unblock) #10's actual migration lands)

Commits

1. 5fb3930 — primary fix in unify.rkt + typing-core.rkt guards + tests
2. 691addb — CI fix (skip stale bench)

https://claude.ai/code/session_01MbncYJnrvjzhbVWw4xGi5x

---

Generated by Claude Code

[kumavis]

this should wait hiero's elaboration refactor

[hierophantos]

Substantive review with disposition pending. Let me explain.

Strong PR. Surgical fix (~12 LoC core), self-corrected diagnosis (the original pitfall report's closure-capture framing was wrong; you traced it to the actual kind-level mult mismatch when type constructor Pi(m0, Type, Type) flows into the combinator's Pi(mw, Type, Type) slot), well-tested with both lenience directions and m1 incompatibility regression. The technical fix is sound under QTT's multiplicity semiring partial order (m0 ≤ mw).

We're holding to consider a structural alternative — see #23 — and decide disposition after we audit our prior subtyping infrastructure.

The reasoning, briefly:

The lenience extends unify's semantics from structural-equality to "{m0, mw} compatible." This is a real subtype relation (m0 <: mw in QTT's semiring partial order), and the principled treatment is an explicit subtype? predicate composing with — not extending — unify. Per workflow.md adversarial framing rule, lenience-as-scaffolding risks sticking around even after the structural fix lands. We'd rather pay the architectural cost upfront if it's tractable.

Verified the bug reproduces on current main (post-S2.e). Your fix is correct for the case it covers; the question is whether to land it tactically while the structural fix is in flight, or hold for the structural fix and accept eigentrust's scale-vec blocked in the meantime.

Specifically, our concerns from the review thread (now superseded by the issue):

1. Lenience-under-unify vs explicit subtyping — addressed by #23's subtype?-as-separate-predicate proposal
2. Defensive mult-meta-solved? guards as symptom treatment — likely obviated when re-entry semantics are clarified under the structural fix
3. Coordination with PPN 4C mult-domain universe migration (S2.c-iv, S2.e-iv) — the structural fix can be designed to compose with the universe model from the start

Three observations for if you'd like to engage with #23:

• The auditing work on unify-mult call sites and the solve-mult-meta! re-entry paths in your investigation is directly reusable in scoping the structural fix
• The 10 test cases you wrote (especially the m1 regression and the eigentrust reproducer) become acceptance criteria for #23's implementation
• If you want to author the structural fix, very welcome — help wanted may go on #23 after our prior-art audit. Your familiarity with classify-mult-problem is an advantage

Disposition decision pending the prior-art audit (how much existing subtyping infrastructure we can compose with, refining the LoC estimate). Will update here once we have a clearer picture. Thanks for the depth of the investigation — the kind-level diagnosis is the load-bearing piece for the structural design.

[hierophantos]

Updating to formal decline (request-changes) following the prior-art audit summarized in #23 comment. Short version: the structural fix is more tractable than initially estimated.

Audit found ~80% of the subtyping infrastructure already exists (subtype-predicate.rkt, subtype-lattice-merge, variance-aware structural-subtype-ground?, mult-leq partial order, mult ctor-desc with component-lattice). The PPN Track 4 design (2026-04-04) explicitly specifies "multiplicities merge via mult-lattice (max)" — the partial-order join is the named target.

The fix is literally "do for mults what's already done for types": add mult-subtype-merge (parallels subtype-lattice-merge), register it with the SRE domain at the 'subtype relation, change Pi's mult variance from = to +, handle mult-meta interaction. ~220-360 LoC, 2-3 days. The lenience-under-unify scaffolding doesn't pay for itself when the structural fix is this small.

What this means for your work:

1. Closing this PR is what we're requesting — the diff itself is correct work, but landing it would create scaffolding our charter explicitly retires (workflow.md adversarial framing rule)
2. Your investigation contributions land in #23 — the kind-level diagnosis (type constructor Pi(m0, Type, Type) vs combinator Pi(mw, Type, Type)) is load-bearing for the structural fix's design
3. Your tests become acceptance criteria — the eigentrust reproducer + m1 incompatibility regression are exactly what #23's implementation must satisfy
4. help wanted may go on #23 — we'll audit our scheduling in coordination with PPN 4C tropical addendum work; if you'd like to author the structural fix, very welcome. Your classify-mult-problem familiarity is an advantage

Practical implication: eigentrust's scale-vec use case stays blocked until #23 lands. We accept that — 2-3 days work for the proper architecture is better than landing scaffolding that risks sticking around.

Apologies for the disposition reversal between my earlier comment and this one. The prior-art audit changed our cost estimate substantially (initial fear was multi-week; reality is multi-day given existing infrastructure), which moves the structural fix from "ideal-but-expensive" to "ideal-and-tractable." Your initial PR did its job: forced us to look at the architectural seam.

Closing recommendation. Will reopen if our scheduling shifts and we want to land #17 as bridge — but that's not the current plan.