fix(semantics): specialize collection body result types

[devin-ai-integration]

What and why

The checker typed xs->collect { in x : C; x.mass } (and xs.{ in x : C; x.mass }) by the library's declared result, Anything[0..*], so the value never carried the body's type and every collect was indistinguishable from an untyped one — a MassValue rollup through a collect could not be checked, and an enumerated value or trigger argument written over a collect passed or failed only by the collection.

The typer now specializes each collection operation's static result by the argument the library's declaration hands through, identified by the resolved ControlFunctions declaration (not the spelling):

operation	element type of the result	multiplicity
collect (->collect {…}, xs.{…}, ->collect f)	the body's / named function's result	[0..*]
select, reject	the elements of the collection	[0..*]
selectOne	the elements of the collection	[0..1]
reduce	the reducer's result, and the element a one-element collection hands back unreduced unless the collection provably holds ≥2	[0..*]
forAll, exists	Boolean (declared; unchanged)	[1]

Nested collects type by the innermost body; a body answering a sequence (x.mass, x.name) contributes every element type; receiver, plain and named-argument notations map to the same parameter through the declaration's signature. A body whose result cannot be typed (an untyped parameter) keeps the library's Anything rather than a guess. A collection over () or a feature admitting no value (part none : C[0]) applies nothing, so neither reducer nor element types it; it conforms as null does (an empty value typed Anything, untyped).

Element-wise judgement. Model.CollectionElements exposes the produced elements (node, scope, types) of a collection value — xs.{…}, xs.?{…}, and the collect/select/reject/selectOne/reduce calls — so a feature's bound value, an invocation argument, a cast and a bound quantity's dimension are judged per element rather than through the library's Anything: attribute i : Integer = xs.{ in x : C; 1.5 } is refused because the literal stays exact (no bidirectional conformance), attribute t : DurationValue = xs.{ in x : C; 5 [m] } is refused as L vs T, and the shorthand xs.?{…} binds exactly as xs->select {…}. The collection value is inferred once with the reporting checker; the produced elements' types are then read through a silent checker (carrying chaining/performed), so an invalid body reports once. The ≥2 analysis (valuesHeldBy) is a full range: () is 0, a literal 1, a sequence the sum, a feature its declared or redefinition-inherited multiplicity, a chain the product.

// semantics/collection.go
func (m *Model) collectionResultTypes(scope, e *ast.InvocationExpr, fn *symbols.Symbol) []*symbols.Symbol
    // collect, reduce  -> appliedResultTypes(argumentTo(e, fn, 1))   // body / function reference
    // select, reject, selectOne -> resultTypes(argumentTo(e, fn, 0)) // the collection
func (m *Model) collectResultTypes(scope, e *ast.CollectExpr) []*symbols.Symbol // xs.{…}

ExprResultType, exprConformance/invocationConformance (valuetype.go) and resultTypes (operator_conformance.go) consult these before the generic result-parameter typing, so non-collection invocations are typed as before.

Recursion. The SelectCall/callArguments typingArgs guard from the self-referential-argument fix is untouched and TestRecursiveRollupThroughACall is byte-for-byte unchanged. Typing bodies exposed one more cycle in the passes layer: exprChecker.invocationResultParameter selected the invocation through a fresh checker, dropping the chaining set of features being typed, so total = subcomponents->collect {in c; c.total}->reduce '+' recursed without bound. It now selects through a silent checker carrying chaining/performed; TestRecursiveRollupThroughACollectBody pins it.

Diagnostics that move (intentionally). Two passes tests encoded "every collect is Anything":

• TestCollectAndSelectTriggerArguments: when counts.{in n; n > 3} was rejected (found … Anything) and is now accepted — the body returns Boolean. Explicitly typed bodies are now reported by their type (when counts.{in n : Integer; n} → found Integer); untyped bodies still report Anything.
• TestW7GASelectedEnumeratedValueKeepsItsOperandType: xs.{in r : Real; r} in a non-Real enumeration is now flagged (q, r, s); the same collect in RightNum :> Real (ok17) and an untyped one (ok1) are accepted.

The pinned pilot (2026-07) leaves every collect Anything, so it is silent where these new diagnostics fire; the compliance row records that as ⚠️ Approximate (stricter than the reference) for collect/reduce, ✅ for the rest.

No runtime, parser or IR change; collection.go is the only new non-test file.

Specification basis

KerML 1.1 §8.3.4.8 (checkSelectExpressionResultSpecialization: a select's result subsets the collection's) and §9.2 Kernel Function Library ControlFunctions.kerml (collect → "the collection of results" of mapper; select/reject/selectOne → elements of collection; reduce → the reducer's result; forAll/exists → Boolean[1]). Pinned grammar PrimaryExpression ('->' InstantiatedTypeMember BodyExpression, '.' BodyExpression, '.?' BodyExpression). Adds one row under Static Expression Type Checking in docs/project/spec-compliance.md and amends the collection-body ⚠️ paragraph under the runtime collection section.

How it was verified

gofmt -l .        → (empty)
go build ./...    → ok
go vet ./...      → ok
go test ./...     → ok (67 packages)
staticcheck ./internal/core/semantics/... ./internal/core/passes/... → clean
python3 scripts/changelog.py check → ok
go run ./cmd/doc-counts -check → already current

./scripts/download-training-examples.sh && ./scripts/download-pilot-corpora.sh   (both already present, pinned)
OPENSYSML_REQUIRE_TRAINING_CORPUS=1 OPENSYSML_REQUIRE_PILOT_CORPORA=1 \
  go test -count=1 ./internal/core/model -run 'TestTrainingExamples|TestPilotCorpora'  → ok
OPENSYSML_REQUIRE_TRAINING_CORPUS=1 OPENSYSML_REQUIRE_PILOT_CORPORA=1 \
  go test -count=1 ./internal/core/export -run TestCorpusRoundTrip                    → ok

No corpus diagnostic moved: training_examples_expected.txt, the pilot ratchets and the RDF round-trip baselines are unchanged, so no per-file adjudication was needed in docs/project/training-examples.md / pilot-corpora.md.

New tests: internal/core/semantics/collection_test.go (each operation, nested and sequence-valued bodies, body type ≠ element type, positional/named/function-reference notations, untyped-body fallback, multiplicity, conformance, reduce returning the element, reduce/collect of nothing, shorthand select elements, self-referential body termination); in internal/core/passes: TestRecursiveRollupThroughACollectBody, TestBoundCollectionQuantityOfAnotherDimension, the collection cases of typecheck_value_test.go (bound values, arguments, exact literals, body checked once, known-empty reduce), the collection cast cases of typecheck_operator_test.go and the () trigger cases of typecheck_trigger_test.go. Two passes tests updated as described above (no assertion weakened — each moved case is replaced by the case that now holds, and the old shape is asserted under the type that makes it hold).

Known limitation: a body whose parameter declares no type (xs.{in x; x.mass}) is still Anything, because the checker does not derive a body parameter's type from the operand's element type; that is the pre-existing ⚠️ paragraph, now stated as such.

Checklist

• make test and make lint pass locally
• Tests added or updated for the change
• Documentation extended where it already covers the surface (see CONTRIBUTING.md)
• Changelog entry added as changes/unreleased/<slug>.<section>.md, not as an edit to CHANGELOG.md
• baselines regenerated and make docs-counts run if a gate count moved (compliance rows need nothing: the census is counted at docs build)
• No internal work-item labels (waves, slices, F4, K5) in the body, docs, or changelog

[devin-ai-integration]

🤖 Devin AI Engineer

I'll be helping with this pull request! Here's what you should know:

✅ I will automatically:

• Address comments on this PR. Add '(aside)' to your comment to have me ignore it.
• Look at CI failures and help fix them

Note: I can only respond to comments from users who have write access to this repository.

⚙️ Control Options:

• Disable automatic comment, CI, and merge conflict monitoring