Multiplicity subtyping: implement `m0 <: mw` (and broader subtyping infrastructure)

[hierophantos]

Summary

Implement multiplicity subtyping (m0 <: mw minimally; full QTT semiring partial order more generally) as a proper structural addition to the type system. The fix lands as a separate subtype? predicate composing with — not extending — unify's structural-equality semantics.

Motivated by PR #17 (eigentrust pitfall #2 — kind-level mult mismatch when a type constructor with kind Pi(m0, Type, Type) flows into a polymorphic combinator's Pi(mw, Type, Type) slot). Verified the bug reproduces on current main (post-S2.e):

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

Kumavis proposed a surface fix in #17 (extend classify-mult-problem with {m0, mw} lenience). We're declining that approach in favor of the structural fix tracked here, to avoid scaffolding that risks sticking around even after the structural correction lands.

The bug, structurally

map's spec elaborates {C : Type → Type} to Pi(mw, Type, Type) (the inner → defaults to mw via surf-arrow). List is registered with kind Pi(m0, Type, Type) (erased type arg). Implicit type-arg unification tries to unify these kinds, fails on the mult mismatch (m0 ≠ mw structurally), surfaces as "Multiplicity violation" at the value level — confusingly.

Under QTT's multiplicity semiring, m0 ≤ mw (zero uses trivially satisfies "any number of uses"). The relationship is a real subtype, not just a coincidence.

Soundness analysis

QTT multiplicities form a semiring with partial order:

Relation	Status
m0 ≤ mw	✅ Sound — value used 0 times satisfies "any number ≥ 0"
m1 ≤ mw	⚠️ Sound but lossy — preserves usage count but loses linearity contract; only sound at call sites not definition sites
m0 vs m1	❌ Incomparable — zero is not "exactly one" usage

For the eigentrust case: type-level kind subtyping (Pi(m0, Type, Type) <: Pi(mw, Type, Type)) is the immediate need. Value-level mult subtyping is a generalization to consider after the kind-level case lands.

Proposed shape — separate subtype? predicate

Keep unify pure (structural equality); add subtype? as the semantic-relation extension:

;; subtype? : ctx × Expr × Expr → Result
;;   #t       — t1 is a subtype of t2 (proceed)
;;   #f       — t1 is not a subtype of t2 (caller decides — fail or fallback)
;;   pending  — depends on a meta; needs solving, return constraint

Where called:

• check's Pi case (when the function's mult doesn't match the expected mult)
• infer's App case (when the argument's mult doesn't match the parameter's mult)
• Implicit type-arg synthesis (kind-level mult subtyping for HKT slots)

Composition with unify: unify remains structural; subtype? is checked at sites where the type system semantically permits a refinement. If unify would fail on a mult mismatch, the caller falls back to subtype?. If subtype? succeeds, the unification proceeds with the appropriate side's value (covariant: take the supertype; contravariant: take the subtype).

Mult-meta interaction: subtype? returns pending when one side is a meta. Caller then decides whether to solve the meta to make the relation hold (e.g., solving an unconstrained meta to mw to admit a value with mult m0 <: ?meta).

Scope

In scope (this issue):

• Multiplicity subtyping subtype-mult? : Mult × Mult → Result
• Pi-type subtyping with mult-subtyping (contravariant domain, covariant result)
• Integration at the typing rule sites named above
• Mult-meta interaction
• Tests including the eigentrust reproducer
• Acceptance: PR unify: lenient {m0, mw} compatibility (eigentrust pitfall #2) #17's failing reproducer works without lenience-in-unify

Out of scope (future generalizations):

• Numeric subtyping (already complete — 2026-02-27_REFINED_NUMERIC_SUBTYPING.md)
• Capability subtyping
• Refinement type subtyping
• User-facing subtyping syntax / annotations (keep implicit at type-check level)
• m1 ≤ mw — call-site-only soundness needs careful framing; defer

Implementation estimate (rough)

Will refine with prior-art audit (a follow-up task on this issue):

• subtype? predicate scaffolding: ~50 LoC
• Multiplicity subtyping: ~30 LoC (small partial-order check)
• Pi-type subtyping: ~50 LoC
• Integration at typing rule sites: 5-10 sites, ~50-100 LoC
• Mult-meta interaction: ~50-100 LoC (the tricky part)
• Tests: ~100-200 LoC
• Documentation: ~50 LoC

Total: 200-450 LoC, multi-day implementation. Real work but tractable.

Open question: do we have prior subtyping infrastructure (numeric subtyping is complete; capability subtyping mentioned in design docs) we can compose with? Audit pending.

Why structural rather than tactical

Per workflow.md Adversarial Framing rule: "preserved for backward-compat" / "for safety" / etc. red-flag patterns. Lenience-under-unify is a tactical fix that risks sticking around as scaffolding even after a proper subtyping framework lands. Our charter explicitly retires such patterns.

The pragmatic case for tactical fix is real (~12 LoC vs ~300 LoC; eigentrust unblocked sooner). We're choosing the structural path because:

1. The pattern recurs — every future "kind-level subtyping" or "value-level subtyping" question hits the same architectural seam
2. Prior subtyping infrastructure (numeric refinements, etc.) suggests we have machinery to compose with
3. PPN 4C's broader migration toward principled lattice-and-subtype reasoning makes this a natural component to land

References

• Motivating PR: #17 — declined in favor of this issue
• Eigentrust pitfalls memo: docs/tracking/2026-04-23_eigentrust_pitfalls.md (in PR Add EigenTrust reputation algorithm: implementation, tests, benchmark #2)
• Numeric subtyping prior art: docs/tracking/2026-02-27_REFINED_NUMERIC_SUBTYPING.md (status COMPLETE per MEMORY.md)
• QTT semiring: qtt.rkt, unify.rkt::classify-mult-problem
• Charter alignment: workflow.md adversarial framing rule, structural-thinking.md (subtyping as lattice morphism)

Out of scope for this issue (explicit deferrals)

• PPN 4C addendum integration — this issue stands independently of the addendum (PPN 4C: top-level form processing on-network — retire process-command sequential orchestrator #22) but the proper fix here is downstream of PPN 4C's typing-on-network completion. Coordinate timing.
• Detailed implementation design — this issue tracks the conceptual fix; design doc (docs/tracking/YYYY-MM-DD_MULT_SUBTYPING_DESIGN.md) when the work is scheduled.

Priority

Medium. Eigentrust use case is blocked without this; the architecture clarification it forces is independently valuable; not urgent enough to disrupt PPN 4C work in flight.

[hierophantos]

Prior-art audit findings — refined effort estimate

Audited current main for existing subtyping infrastructure before scheduling this work. Findings substantially reduce the implementation cost and clarify the architectural shape.

What we already have (~80% of infrastructure)

Piece	Status	Location
subtype? predicate (flat + structural + variance-aware)	✅ Complete	subtype-predicate.rkt (370 LoC)
subtype-lattice-merge (subtype-ordering join for types)	✅ Complete	subtype-predicate.rkt:339
structural-subtype-ground? (recursive variance check)	✅ Complete	subtype-predicate.rkt:165
mult-leq partial order (m0 ≤ m1 ≤ mw, tested)	✅ Complete	prelude.rkt:69
mult-lattice-merge (flat lattice, equality semantics)	✅ Complete	mult-lattice.rkt:49
Variance system (+ - = ø) for ctor-desc	✅ Complete	sre-core.rkt:545+
Pi ctor-desc with mult component-lattice	✅ Complete	ctor-registry.rkt:431

Design intent already documented

docs/tracking/2026-04-04_PPN_TRACK4_DESIGN.md explicitly specifies: "multiplicities merge via mult-lattice (max)" — the partial-order join is the named target. Implementation just hasn't fully wired it.

Architectural pattern — types already have what mults need

The fix is literally "do for mults what's already done for types":

	Types	Mults
Equality-semantics merge	type-lattice-merge ✅	mult-lattice-merge ✅
Subtype-ordering merge	subtype-lattice-merge ✅	MISSING
Registered SRE domain 'equality relation	✅	✅
Registered SRE domain 'subtype relation	✅	MISSING
Pi variance dispatch	mult =, dom -, codom +	(need mult +)

The subtype-predicate machinery is unchanged — variance dispatch already calls into the per-domain merge registry; we just register one more entry.

What's actually missing (the small list)

Missing piece	Estimated LoC
mult-subtype-merge function (uses mult-leq to compute max)	~30
Register mult-subtype-merge with SRE domain at 'subtype relation	~10
Pi mult variance change: = → + in ctor-registry.rkt:435	~1
Mult-meta interaction (pending/solve dispatch on unsolved metas)	~30-50
Call-site dispatch — audit unify-mult sites and decide subtype vs equality	~50-100
Tests including pitfall #2 reproducer + regression coverage	~80-150
Optional: subtype-mult? predicate as named export	~20

Refined total: ~220-360 LoC, 2-3 days of focused work.

Implication

Substantially smaller than the issue's original ~200-450 LoC / multi-day estimate. The infrastructure is mature; we're plugging a known gap that the PPN Track 4 design already anticipated.

The architectural elegance of the parallel-to-types pattern reinforces the case for the structural fix over the lenience-under-unify scaffolding (#17). The pragmatic argument for tactical (lenience faster than structural) doesn't carry — structural fix is 2-3 days, mechanical, using established patterns.

Updated next steps

1. PR unify: lenient {m0, mw} compatibility (eigentrust pitfall #2) #17 disposition updated to formal decline (request-changes posture; cross-link this issue) — this comment serves as the rationale.
2. Schedule the implementation track when ready (gates on PPN 4C tropical addendum closing or coordinated alongside).
3. Design doc (docs/tracking/YYYY-MM-DD_MULT_SUBTYPING_DESIGN.md) when implementation is scheduled.

Mempalace probe note

Attempted semantic search via mempalace MCP for additional architectural prior art; tool was experiencing connection failures. Direct grep + doc search surfaced all relevant infrastructure by name. Cross-verified findings against current main — all referenced files and line numbers match.