diff --git a/changes/unreleased/collection-body-result-type.fixed.md b/changes/unreleased/collection-body-result-type.fixed.md
new file mode 100644
index 000000000..83ffba9e2
--- /dev/null
+++ b/changes/unreleased/collection-body-result-type.fixed.md
@@ -0,0 +1 @@
+- **A collection operation's static type follows what its declaration hands through, not the element type of the collection.** `xs->collect { in x : C; x.mass }` and `xs.{ in x : C; x.mass }` are typed by the body's result (`MassValue`), a nested collect by its innermost body, a body answering a sequence by every element type and `xs->collect f` by the named function's result; `select`, `reject` and `selectOne` keep the elements of `xs`, `reduce` follows its reducer's result — and the element a one-element collection hands back unreduced, unless the collection is known to hold two or more, by its own multiplicity, one it inherits by redefinition, or a chain through such features; a collection holding one at most is never reduced, so its element alone is the result — and `forAll`/`exists` stay `Boolean`, each with the multiplicity the Kernel Function Library declares. A body whose result cannot be typed keeps the library's `Anything`. Value conformance, a feature's bound value, invocation arguments, trigger arguments and enumerated values are judged by the specialized type, so `accept when counts.{in n : Integer; n}` is refused where it was silent, and `when counts.{in n; n > 3}` is accepted where it was refused. A scalar literal a body writes out is as exact as one bound directly: `attribute i : Integer = xs.{ in x : C; 1.5 }` is refused, and a quantity it writes out is measured against the target's dimension: `attribute t : DurationValue = xs.{ in x : C; 5 [m] }` is refused. `xs.?{…}` binds and is typed as `xs->select {…}` is — `(v1, v2).?{ in v : Vehicle; true }` is a `Vehicle` collection, not the `Anything` the sequence is; elements of sibling types share their nearest common supertype, so `(truck, car).?{ in v : Vehicle; true }` is a `Vehicle` collection too — and an element that is itself a collection value binds by the elements it holds, so `attribute i : Integer = xs.{ in x : C; xs.{ in y : C; 1.5 } }` is refused. A collection over `()` or a feature admitting no value keeps its declared type — `()->collect { in a : Integer; "s" }` is a `String` collection — but holds no element, so none is judged and its `reduce` takes nothing from an element it would hand back unreduced; so does one mapping every element to a `[0]` feature or function result — the multiplicity read through an alias, or from the feature or result a redefinition inherits it from — or any operation over such a collection, and an argument holding nothing is judged against no parameter type. An argument or constructor value that is a collection binds each element it holds on its own, so `Sail(vs.{ in v : Vehicle; (v, boat) })` and `new Fleet(vs.{ in v : Vehicle; 1.5 })` are refused by the element that does not bind where they were silent. A collection value binds as many values as it is known to hold, counted against the feature's multiplicity — `part b : Boat[1] = pair.items.{ in v : Vehicle; boat }` binds two — a `reduce` counting the one element it hands back unreduced or what its reducer yields over two or more, so `pair.items->reduce { in a : Vehicle; in b : Vehicle; (a, b) }` binds two and one over `()` none. A body reading the feature it values terminates as a self-referential argument does.
diff --git a/docs/project/spec-compliance.md b/docs/project/spec-compliance.md
index 6eb920c68..c154bf822 100644
--- a/docs/project/spec-compliance.md
+++ b/docs/project/spec-compliance.md
@@ -1376,10 +1376,12 @@ they cannot drift apart.
 | A failing expression of literals alone is answered at the prompt with the failure itself, so `sysml -e "(1,2,3)#(0)"` reports the index rather than "no declarations loaded" | `repl/meta.go` `tryEvalLiteral`, `isLiteralAnswerError` | `repl/runtime_commands_test.go` `TestEvalReportsTheAnswerOfALiteralExpressionThatFails` | ✅ Faithful |
 | A name the session declares is answered by that declaration, so the prompt's literal pass declines an expression using one rather than letting a library operation of the same unqualified name stand in for it | `repl/meta.go` `tryEvalLiteral`, `declaresANameIn` | `repl/runtime_commands_test.go` `TestEvalPrefersASessionDeclarationOverALibraryOperation` | ✅ Faithful |
 
-⚠️ A body parameter takes its type from the element type of whatever the operand
-turns out to hold, which the expression checker does not track: an expression
-over the parameter (`xs.?{in e; e + 1}`) therefore has no static type, and its
-selector is checked at evaluation rather than where it is written. Statically the
+⚠️ An untyped body parameter takes its type from the element type of whatever the
+operand turns out to hold, which the expression checker does not track: an
+expression over the parameter (`xs.?{in e; e + 1}`) therefore has no static type,
+and its selector is checked at evaluation rather than where it is written; a body
+over a typed parameter (`xs.{in e : Real; e + 1}`) types the collect by its result
+(the collection-operation row under *Static Expression Type Checking*). Statically the
 checker reports what it can know — a selector whose result type *is* known and is
 not Boolean, an index that is no whole number, a literal index of 0 or past a sequence
 written out (`passes/typecheck_expr.go` `inferIndex`, `inferSelect`) — and the
@@ -1460,6 +1462,7 @@ known, so unmodelled types never produce a false positive.
 | Each argument of an invocation corresponds to one `in` parameter of the invoked type (KerML 1.1 §8.3.4.8 `validateInvocationExpressionParameterRedefinition`, pilot `Must correspond to one input parameter of the invoked type`): a named argument naming an `out` or `return` parameter, a feature that is no parameter, or a general's parameter the invoked function's own redefines by position; and a positional argument past the last `in` parameter, in a function, a `calc def`, a step or a feature typed by a behavior, with inherited and redefined parameters counted through `effectiveInParameters` | `passes/typecheck_expr.go` `checkArguments`, `checkNamedArguments` (`msgInvocationParameterRedefinition`) | `passes/duplicate_binding_test.go` `TestInvocationParameterRedefinitionKerML`; census probe `validateInvocationExpressionParameterRedefinition.kerml`; corpus `semantic/k32-too-many-arguments.kerml` | ✅ Faithful; the pilot's wording heads ours, followed by the cause (`…: F has no parameter named "y"`, `…: F takes 1 argument(s), found 2`) at the offending argument. A required parameter left unbound (`F()`) draws OpenSysML's own `unbound-parameter` advisory (warning), a check the pilot does not make |
 | A constructor expression binds each feature of the instantiated type at most once (KerML 1.1 §8.3.4.8 `validateConstructorExpressionNoDuplicateFeatureRedefinition`, pilot `Feature already bound`): `new C(x = 1, x = 2)`, an alias or a qualified name of the same feature, and an inherited feature bound under its own and its redefining name all count; reported at the second binding, `x of C is already bound by an earlier argument`, and the same rule reaches a constructor nested in a send payload (under a conditional, a sequence, a feature chain, a call argument or a body expression) or in a feature chain's operand | `passes/typecheck_expr.go` `inferConstructor` (the constructor row below), `inferFeatureChain` | `passes/duplicate_binding_test.go` (`TestConstructorDuplicateFeatureBindingKerML`, `TestConstructorDuplicateFeatureBindingSysML`); corpus `semantic/k34-constructor-feature-bound-twice.kerml`; census probe `validateConstructorExpressionNoDuplicateFeatureRedefinition.kerml` | ✅ Faithful (a call's named argument is not indexed as a member reference of the called type, so editor rename and find-references do not reach `f(F::x = …)` — an editor follow-up; constructor labels are) |
 | Invocation overload selection: a name visible as several function/calc declarations (owned, inherited, imported or re-exported — a library function only where the model imports its package) selects the one whose effective input parameters take the arguments — each argument, by position or name, to a distinct parameter it conforms to; a candidate the arguments bind every default-less parameter of is preferred to one they leave a parameter of, which stays applicable and draws the `unbound-parameter` advisory, so `pick("a")` against `pick(in x : Integer)` and `pick(in s : String; in y : Real)` binds to the second rather than reporting a mismatch against the first, `pick(2)` against `pick(in x : Real; in y : Real)` and `pick(in x : Integer)` runs the complete one, and `pick()` against two candidates it fits alike is `invocation-ambiguous` — and by type conformance (the `ScalarValues` lattice, strings, booleans, collections, quantities and declared types through `Model.Conforms` — a non-literal argument's type only bounds its values, so a broader declared type fits a narrower parameter, while declared types neither of which conforms to the other, `MassValue` to a `VolumeValue` parameter, never bind, as the pinned validator judges a binding; a `Collections` parameter takes any sequence, as the runtime reads it, and a `KerML::Root::Element` parameter the element any argument names, as `DocumentQueries` bind it, ranked between a declared type and `Anything`); among several fits the most specific wins, a tie or incomparable pair is reported as `invocation-ambiguous` naming the tied candidates (`InvocationSelection.Tied`, the applicable ones none is more specific than, so a broader overload the arguments also fit is not among them), and no fit keeps the argument diagnostic against the first candidate, naming the others considered. The selection is memoized in a side table keyed by the invocation node and scope, the runtime dispatches the declaration selected there, and a named argument written twice is reported (`binds parameter twice` for a calc call, `ErrDuplicateArgument` for a nested action call) and dispatched by none. A feature typed by a behavior is a candidate performing that behavior, so `ref pick : Twice;` is selected beside a same-named calc when only its signature fits. An expression evaluates to a calc's result, so a call in expression context whose name denotes a calc selects among the calcs alone, whatever the import order and however closely a same-named action's inputs fit — the arguments are then checked and dispatched against the calc, and the action is never evaluated — while `action call = tag(3);` and `perform tag(3);` select among actions only. A bodiless calc specializing a library function (`calc def Renamed :> sqrt { in y :>> x; }`, or a feature typed by one) is computed by that function through its own effective signature: the runtime binds the written arguments to the specialization's parameters as any calc's are bound — renamed, defaulted, optional; each default evaluated where it is declared with the earlier parameters in scope (`in y :>> y = x + 1.0;`), each value checked against the effective type and multiplicity the specialization states (`in n : Integer :>> x;`, `[1]`) before the library computes it — and lays them out in the library's order (`runtime/invoke_calc.go` `libraryCalcPerformed`, `effectiveParameter`, `invokeLibraryPerformance`), for an expression, a `send` and the `InvokeCalc`/`InvokeCalcNamed` API alike; a calc with a body of its own is never redirected. A nested action call with an explicit empty argument list (`action call = tag();`) binds nothing — a required input is unbound, a defaulted one takes its default — where only the bare `perform tag;` and `action call : Tag;` forms read the caller's same-named values | `resolve/invocation.go` `Resolver.InvocationCandidates` (all matches of the winning visibility category), `semantics/invocation.go` `Model.SelectInvocation`, `passes/typecheck_expr.go` `inferInvocation`, `passes/invocation.go` `argument`, `runtime/eval.go` `invocationTarget` and `runtime/invoke_action.go` `resolveActionSymbol` for a nested `action call = A(...)` or `perform A(...)`, whose receiver `x->A()` is the first argument (`ErrAmbiguousInvocation`, `ErrReceiverWithNamedArgs`), `model/workspace.go` `calledDeclaration` and `Workspace.AmbiguousInvocationInDoc` for editor navigation (a call selecting one overload navigates to it; a tied call lists every tied overload under go-to-definition and hover, and is left out of find-references and rename, which refuses to start from it), `semantics/invocation.go` `Model.SelectCall` (the checker's argument typing installed by `passes.NewArgumentTyper`) for `queryplan/compiler.go` `compileInvocation` and `columns.go` `compileColumn` (a tie is `ErrorAmbiguousInvocation`) and `runtime/signal.go` `invokesCalc` (a send names a signal unless the call selects a calc) | `passes/invocation_test.go` (`TestInvocationOverloadRedeclaredLibraryInputs`, `TestInvocationOverloadOmittedInputSelectsTheFittingCandidate`, `TestInvocationOverloadCompleteCandidateBeatsOmission`, `TestInvocationOverloadOmittedInputsAreAmbiguous`), `runtime/invocation_selection_test.go` (`calc_call_binds_a_library_function_through_redeclared_inputs`, `calc_call_selects_a_calc_over_a_more_specific_action`, `calc_call_omitting_an_input_runs_the_fitting_candidate`, `calc_call_omitting_every_input_is_ambiguous`), `queryplan/overload_test.go`, `runtime/signal_test.go:TestActionSendCallsACalcSharingASignalsName`, `lsp/invocation_navigation_test.go`, `lsp/ambiguous_invocation_navigation_test.go`, conformance `calc_library_overload_by_argument_type`, `calc_library_overload_partial_import`, `calc_library_overload_ambiguous`, `calc_library_function_shadowed_by_model`, `action_node_invocation_overload_inherited_input` (the winning action's matching input is inherited, and the runtime frame binds it), `lsp/library_invocation_test.go:TestPublishDiagnosticsSelectsLibraryOverloadByArgumentType`, pilot-exec-diff `w6d:complex-abs`, `:complex-is-zero` | ⚠️ Approximate: a model's own `calc` of the name still shadows every library declaration, and an argument whose type is statically unknown (an unresolved parameter type, an untyped feature) keeps today's first-visible selection with no new diagnostic — the corpus gates hold at zero movement. The pinned pilot evaluates none of the probes (`ToInteger`, `abs`, `isZero` over their overload sets come back as the unevaluated `InvocationExpression`), so the most-specific rule is self-assessed against KerML 1.1 §8.3.4.8 (a decimal literal is a `LiteralRational`, so `ToInteger(7.9)` selects `RationalFunctions::ToInteger` over `RealFunctions`'). A parameter's `[m..n]` multiplicity decides only whether a call may omit it: one admitting none, or one a default reaches along its redefinitions (`Model.OptionalParameter`, `Model.ParameterDefault`), is optional to the checker and to `runtime/action_frame.go` `checkInputsBound` alike, and the omitted input is read as empty or as the inherited default (`passes/invocation_test.go:TestInvocationPerformedActionOptionalInputs`, `runtime/invocation_selection_test.go:action_call_omits_optional_inputs`). Not done: a value's element count is not checked against the multiplicity |
+| A collection operation's static result is typed by the argument the library's declaration hands through, not by the `Anything[0..*]` it declares (KerML 1.1 §8.3.4.8 `checkSelectExpressionResultSpecialization`: a select's result subsets the collection's; §9.2 Kernel Function Library `ControlFunctions.kerml`, `collect`'s result "the collection of results" of `mapper`, `select`/`reject`/`selectOne` elements of `collection`, `reduce` the `reducer`'s result, `forAll`/`exists` `Boolean[1]`): `xs->collect {in x : C; x.mass}` and `xs.{in x : C; x.mass}` are typed `MassValue`, `xs->collect {in x : C; x.name}` `String`, a nested collect by the innermost body, a body answering a sequence `(x.mass, x.name)` by every element type, `xs->collect Mass` by the named function's result, `xs->select {…}`/`->reject {…}`/`->selectOne {…}` as `xs` is, `->reduce '+'` by the reducer's result — and, as the runtime hands a one-element collection back unreduced, by the element too unless the collection is known to hold two or more (a `[2..*]` feature, a sequence of two literals), and by the element alone where it holds one at most (`[1]`, `[0..1]`), the reducer never applied — and `->forAll`/`->exists` `Boolean`; the operation is the resolved library declaration, in the receiver, plain and named-argument notations alike, and a body whose result cannot be typed — its parameter declares no type — leaves the library's `Anything`, never a guess. The multiplicity stays the declaration's (`collect`/`select`/`reject`/`reduce` `[0..*]`, `selectOne` `[0..1]`, `forAll`/`exists` `[1]`). A collection value bound to a typed feature or passed as an argument is judged by these element types, each element a sequence-valued body answers on its own, so `part b : Boat = vs->select {in v : Vehicle; true}` and `Sail(vs.{in v : Vehicle; v})` are refused where the declared `Anything` would bind. A body reading the feature it values (`total = cs->collect {in x : C; total}->reduce '+'`) terminates under the same guard as an argument that does | `semantics/collection.go` `Model.CollectionResultTypes`, `CollectionElementTypes`, `sourcesOf`, `invocationSources`, `holdsAtLeastTwo`, `collectSources`, `appliedSources`, `bodySources`, `argumentTo`, `sourcesElementTypes`, reached from `semantics/valuetype.go` `Model.ExprResultType`, `exprConformance`, `invocationConformance` and `semantics/operator_conformance.go` `resultTypes`; `semantics/invocation.go` `SelectCall`/`callArguments` (`typingArgs`); `passes/typecheck_value.go` `exprChecker.checkValueConformance`, `unboundElementTypes`, `invocationResultTypeSymbol`, `invocationResultParameter` (selects under the chains being typed) | `semantics/collection_test.go` `TestCollectionResultTypes`, `TestCollectionResultMultiplicity`, `TestCollectionNestedAndSequenceBodies`, `TestCollectionArgumentNotations`, `TestCollectionUntypedBodyFallsBackToLibraryResult`, `TestCollectionSelfReferentialBodyTerminates`, `TestCollectionResultConformance`, `TestCollectionReduceMayReturnTheElement`; `passes/typecheck_value_test.go:TestValueCollectionResultIsJudged`, `:TestValueReduceResultIsJudged`, `:TestArgumentCollectionResultIsJudged`; `passes/typecheck_dimension_test.go:TestRecursiveRollupThroughACall`, `:TestRecursiveRollupThroughACollectBody`; `passes/typecheck_trigger_test.go:TestCollectAndSelectTriggerArguments`; `passes/w7g_one_type_test.go:TestW7GASelectedEnumeratedValueKeepsItsOperandType`; grammar `PrimaryExpression` (`'->' … BodyExpression`, `'.' BodyExpression`, `'.?' BodyExpression`) | ✅ Faithful for `select`/`reject`/`selectOne`/`forAll`/`exists` (the pinned pilot subsets a select's result from its collection and types the rest by the declared result); ⚠️ Approximate for `collect`/`reduce` (self-assessed: the specification declares their result `Anything[0..*]` and the pilot types it so, giving `xs.{in x : C; x.mass}` no static type; typing it by the body is stricter than the reference, so a diagnostic it raises — a `when` trigger over a collect of Integers, an enumerated value collecting Reals — the pilot stays silent on) |
 | An unqualified call to a Kernel Function Library function the model does not import is `unresolved` for the checker and the runtime alike: the library packages are members of the root namespace but not implicitly imported, so a bare `sqrt(4.0)` with no `import RealFunctions::*;` draws the `unresolved` diagnostic offering the imports that would resolve it and fails to evaluate with the same text, `RealFunctions::sqrt(4.0)` resolves anywhere, and under the import the call checks clean, is selected among the imported overloads and evaluates; the OpenSysML extension functions (`exp`, `ln`, `log`, `atan2`) are gated by the same rule | `resolve/invocation.go` `ResolveInvocationName` (the name resolves as any other), `runtime/eval.go` `invocationTarget` (dispatch by the declaration resolved, `passes.SelectInvocation` choosing among several) | `passes/invocation_test.go:TestInvocationUnimportedLibraryFunction`, `:TestInvocationQualifiedLibraryFunctionArgumentsChecked`, `:TestInvocationOverloadOnlyImportedPackagesContribute`, `runtime/library_functions_test.go:TestLibraryFunctionUnqualifiedNames`, `:TestLibraryFunctionQualifiedCallNeedsNoImport`, conformance `calc_library_function_unimported`, `calc_library_function_imported`, `lsp/library_invocation_test.go:TestPublishDiagnosticsAgreesWithRuntimeOnLibraryCall`, `:TestPublishDiagnosticsKeepsExtensionFunctionImportGated`, `lsp/invocation_navigation_test.go:TestDefinitionReachesImportedLibraryFunction` | ✅ Faithful. Observed against the pinned pilot: it reports `Couldn't resolve reference to Element 'sqrt'` for the unimported call and resolves the qualified one |
 | No false positives on the shipped library and examples | corpus guard | `model/typecheck_expr_corpus_test.go` | ✅ Faithful |
 | `[` is not an index in KerML (pilot `validateOperatorExpressionBracketOperator`, `Use #(...) for indexing`; the specification gives `[` no KerML function — `BaseFunctions::'['` is abstract): every bracket in a `.kerml` document warns at the operator expression, a `.sysml` document is judged by the quantity rule instead | `passes/typecheck_expr.go` `exprChecker.checkBracket`; code `bracket-operator` | `typecheck_operator_test.go:TestBracketOperatorInKerML`, `TestBracketOperatorIsKerMLOnly`; census probe `validateOperatorExpressionBracketOperator.kerml` | ✅ Faithful (warning, as the pilot) |
diff --git a/internal/core/passes/invocation.go b/internal/core/passes/invocation.go
index bedd3b68a..0e4222f48 100644
--- a/internal/core/passes/invocation.go
+++ b/internal/core/passes/invocation.go
@@ -108,19 +108,22 @@ func (t argumentTypes) arguments() []semantics.Argument {
 // of the feature it names, or of the result of the call it makes. A collection
 // literal binds its elements, so it is typed by the type they have in common.
 func (ec *exprChecker) argument(scope *symbols.Scope, value ast.Node, name *ast.QualifiedName) semantics.Argument {
+	elements := []ast.Node{value}
 	if seq, ok := value.(*ast.SequenceExpr); ok {
-		return semantics.Argument{
-			Prim:  ec.commonElementType(scope, seq),
-			Type:  ec.commonElementTypeSymbol(scope, seq),
-			Exact: len(seq.Elements) > 0 && allSpellOneValue(seq.Elements),
-			Name:  name,
-		}
+		elements = seq.Elements
 	}
+	arg := ec.argumentOf(scope, elements)
+	arg.Exact = len(elements) > 0 && allSpellOneValue(elements)
+	arg.Name = name
+	return arg
+}
+
+// argumentOf types the values an argument writes together: by the scalar type and the declared
+// type they share, unknown where they share none.
+func (ec *exprChecker) argumentOf(scope *symbols.Scope, elements []ast.Node) semantics.Argument {
 	return semantics.Argument{
-		Prim:  ec.infer(scope, value),
-		Type:  ec.declaredValueType(scope, value),
-		Exact: spellsOneValue(value),
-		Name:  name,
+		Prim: ec.commonElementType(scope, elements),
+		Type: ec.commonElementTypeSymbol(scope, elements),
 	}
 }
 
@@ -144,11 +147,11 @@ func (ec *exprChecker) declaredValueType(scope *symbols.Scope, value ast.Node) *
 	return ec.invocationResultTypeSymbol(scope, value)
 }
 
-// commonElementTypeSymbol is the declared type every element of seq conforms to,
-// nil when one has none or they share none.
-func (ec *exprChecker) commonElementTypeSymbol(scope *symbols.Scope, seq *ast.SequenceExpr) *symbols.Symbol {
+// commonElementTypeSymbol is the declared type every element conforms to, nil when one
+// has none or they share none.
+func (ec *exprChecker) commonElementTypeSymbol(scope *symbols.Scope, elements []ast.Node) *symbols.Symbol {
 	var common *symbols.Symbol
-	for _, el := range seq.Elements {
+	for _, el := range elements {
 		elem := ec.declaredValueType(scope, el)
 		switch {
 		case elem == nil:
diff --git a/internal/core/passes/typecheck_dimension.go b/internal/core/passes/typecheck_dimension.go
index f26f459bb..dcf43ead4 100644
--- a/internal/core/passes/typecheck_dimension.go
+++ b/internal/core/passes/typecheck_dimension.go
@@ -55,24 +55,39 @@ func (ec *exprChecker) checkValueDimension(valueScope, declScope *symbols.Scope,
 	}
 	want, known := ec.model.DimensionOfType(declared)
 	for _, element := range valueElements(value) {
-		if ec.judgedByType(valueScope, element) {
-			// A named value is judged against the target by specialization,
-			// which reports the same mismatch as a clash of types.
-			continue
-		}
-		if statesNoMeasurement(element) {
-			continue
-		}
-		if ec.judgedAsMeasurementRef(valueScope, declared, element) || ec.judgedAsFramedQuantity(valueScope, declared, element) || !known {
-			continue
-		}
-		got, ok := ec.model.DimensionOfExpr(valueScope, element)
-		if !ok || want.Term.Commensurable(got.Term) {
+		// A collection value binds each element it may hold, which is measured on its own.
+		if elements, collection := ec.model.CollectionElements(valueScope, element); collection {
+			for _, produced := range elements {
+				if produced.Node != nil {
+					ec.checkElementDimension(produced.Scope, declared, want, known, produced.Node)
+				}
+			}
 			continue
 		}
-		ec.errorf(element.Span(), msgIncommensurableBinding,
-			describeDimension(got), describeDimension(want))
+		ec.checkElementDimension(valueScope, declared, want, known, element)
+	}
+}
+
+// checkElementDimension reports one bound element measured in a dimension the target's
+// declared type, of dimension want where known, does not measure in.
+func (ec *exprChecker) checkElementDimension(scope *symbols.Scope, declared *symbols.Symbol, want semantics.Dimension, known bool, element ast.Node) {
+	if ec.judgedByType(scope, element) {
+		// A named value is judged against the target by specialization,
+		// which reports the same mismatch as a clash of types.
+		return
+	}
+	if statesNoMeasurement(element) {
+		return
+	}
+	if ec.judgedAsMeasurementRef(scope, declared, element) || ec.judgedAsFramedQuantity(scope, declared, element) || !known {
+		return
+	}
+	got, ok := ec.model.DimensionOfExpr(scope, element)
+	if !ok || want.Term.Commensurable(got.Term) {
+		return
 	}
+	ec.errorf(element.Span(), msgIncommensurableBinding,
+		describeDimension(got), describeDimension(want))
 }
 
 // judgedAsMeasurementRef judges a unit composed by `*`, `/` or `**` as the DerivedUnit
diff --git a/internal/core/passes/typecheck_dimension_test.go b/internal/core/passes/typecheck_dimension_test.go
index a317f8685..35d388720 100644
--- a/internal/core/passes/typecheck_dimension_test.go
+++ b/internal/core/passes/typecheck_dimension_test.go
@@ -47,6 +47,44 @@ func TestBoundNestedCollectionQuantityOfAnotherDimension(t *testing.T) {
 	wantNoDimensionDiags(t, `attribute ls : LengthValue[*] = (1 [m], (2 [m], 3 [mm]));`)
 }
 
+// TestBoundCollectionQuantityOfAnotherDimension: a collection value binds each element its
+// body produces, or keeps, so a unit written in the body is measured against the target too.
+func TestBoundCollectionQuantityOfAnotherDimension(t *testing.T) {
+	const parts = `private import ControlFunctions::*; part def Part; part parts : Part[*];`
+	wantOneDimensionError(t, parts+`attribute t : DurationValue = parts.{ in p : Part; 5 [m] };`,
+		"cannot bind m (dimension L) to a feature typed by DurationValue (dimension T)")
+	wantOneDimensionError(t, parts+`attribute t : DurationValue = parts->collect { in p : Part; 5 [m] };`,
+		"cannot bind m (dimension L) to a feature typed by DurationValue (dimension T)")
+	wantOneDimensionError(t, parts+`attribute t : DurationValue = parts.{ in p : Part; (5 [s], 5 [m]) };`,
+		"cannot bind m (dimension L) to a feature typed by DurationValue (dimension T)")
+	wantOneDimensionError(t, parts+`attribute t : DurationValue = (5 [m], 6 [s]).?{ in l : LengthValue; true };`,
+		"cannot bind m (dimension L) to a feature typed by DurationValue (dimension T)")
+	wantOneDimensionError(t, parts+`attribute t : DurationValue = (5 [s], 6 [m])->select { in l : LengthValue; true };`,
+		"cannot bind m (dimension L) to a feature typed by DurationValue (dimension T)")
+	wantOneDimensionError(t, parts+`attribute t : DurationValue = (5 [m])->reduce { in a : LengthValue; in b : LengthValue; 1 [s] };`,
+		"cannot bind m (dimension L) to a feature typed by DurationValue (dimension T)")
+	wantNoDimensionDiags(t, parts+`
+		attribute t : DurationValue = parts.{ in p : Part; 5 [min] };
+		attribute t2 : DurationValue = parts->collect { in p : Part; (5 [s], 5 [min]) };
+		attribute t3 : DurationValue = (5 [s], 6 [min]).?{ in d : DurationValue; true };
+		attribute t4 : DurationValue = (5 [s], 6 [min])->reduce { in a : DurationValue; in b : DurationValue; 1 [min] };
+		attribute l : LengthValue = parts.{ in p : Part; 5 [m] };`)
+}
+
+// A body mapping every element to a quantity held by no value, or an operation over such a
+// collection, binds no quantity, so no dimension is measured against the target.
+func TestBoundCollectionQuantityOfNothing(t *testing.T) {
+	const parts = `private import ControlFunctions::*; part def Part { attribute none : LengthValue[0]; } part parts : Part[*];`
+	wantNoDimensionDiags(t, parts+`
+		attribute t : DurationValue = parts.{ in p : Part; p.none };
+		attribute t2 : DurationValue = parts->collect { in p : Part; (p.none, p.none) };
+		attribute t3 : DurationValue = (parts.{ in p : Part; p.none }).{ in l : LengthValue; 5 [m] };
+		attribute t4 : DurationValue = (parts.{ in p : Part; p.none }).?{ in l : LengthValue; true };
+		attribute t5 : DurationValue = (parts.{ in p : Part; p.none })->reduce { in a : LengthValue; in b : LengthValue; 1 [m] };`)
+	wantOneDimensionError(t, parts+`attribute t : DurationValue = parts.{ in p : Part; (p.none, 5 [m]) };`,
+		"cannot bind m (dimension L) to a feature typed by DurationValue (dimension T)")
+}
+
 // TestBoundQuantityOfTheSameDimensionAtAnotherScale: a dimension has no scale,
 // so any unit measuring in it conforms.
 func TestBoundQuantityOfTheSameDimensionAtAnotherScale(t *testing.T) {
@@ -128,6 +166,19 @@ func TestRecursiveRollupThroughACall(t *testing.T) {
 	}`)
 }
 
+// TestRecursiveRollupThroughACollectBody: the rollup written with a collect whose
+// body names the feature being typed — its result type is the body's — terminates too.
+func TestRecursiveRollupThroughACollectBody(t *testing.T) {
+	wantNoDimensionDiags(t, `private import NumericalFunctions::*;
+	private import ControlFunctions::*;
+	part def MassedComponent {
+		part subcomponents : MassedComponent [*] default null;
+		attribute mass :> ISQ::mass;
+		attribute totalMass :> ISQ::mass = mass + sum(subcomponents->collect { in c : MassedComponent; c.totalMass });
+		attribute heaviest :> ISQ::mass = subcomponents->collect { in c : MassedComponent; c.heaviest }->reduce '+';
+	}`)
+}
+
 // TestBoundMeasurementUnit: a unit binds to the unit definition typing it, to any
 // measurement-reference supertype, and to no quantity value type; the checker
 // judges each as the runtime's write conformance does. A quantity bound to a
diff --git a/internal/core/passes/typecheck_expr.go b/internal/core/passes/typecheck_expr.go
index 74746b58d..fdedb4309 100644
--- a/internal/core/passes/typecheck_expr.go
+++ b/internal/core/passes/typecheck_expr.go
@@ -2,6 +2,7 @@ package passes
 
 import (
 	"fmt"
+	"slices"
 	"strconv"
 
 	"github.com/Open-MBEE/OpenSysML/internal/core/ast"
@@ -118,22 +119,40 @@ func (ec *exprChecker) checkBoundValue(valueScope, declScope *symbols.Scope, d f
 	// A collection literal binds elementwise, so each element is checked
 	// against the feature's type rather than the sequence as a whole.
 	for _, element := range valueElements(value) {
+		// A collection value binds the elements its body or collection produces. Inferring
+		// the value checks and reports on them; their types are then read silently.
+		if elements, collection := ec.model.CollectionElements(valueScope, element); collection {
+			ec.infer(valueScope, element)
+			silent := ec.silent()
+			for _, produced := range elements {
+				if produced.Node != nil {
+					ec.checkScalarBinding(produced.Node, silent.infer(produced.Scope, produced.Node), want)
+				}
+			}
+			continue
+		}
 		var got semantics.PrimType
 		if inv, ok := element.(*ast.InvocationExpr); ok && node != nil {
 			got = ec.inferNodeInvocation(valueScope, inv, node)
 		} else {
 			got = ec.infer(valueScope, element)
 		}
-		if want == semantics.PrimUnknown || got == semantics.PrimUnknown {
-			continue
-		}
-		if !bindable(element, got, want) {
-			ec.errorf(element.Span(), "cannot bind %s value to a feature typed by %s", got, want)
-		}
+		ec.checkScalarBinding(element, got, want)
 	}
 	ec.checkValueConformance(valueScope, declScope, d, value)
 	ec.checkValueDimension(valueScope, declScope, d, value)
-	ec.checkValueCount(declScope, d, value)
+	ec.checkValueCount(valueScope, declScope, d, value)
+}
+
+// checkScalarBinding reports a got-typed value that may not bind to a want-typed feature,
+// where both are known.
+func (ec *exprChecker) checkScalarBinding(value ast.Node, got, want semantics.PrimType) {
+	if want == semantics.PrimUnknown || got == semantics.PrimUnknown {
+		return
+	}
+	if !bindable(value, got, want) {
+		ec.errorf(value.Span(), "cannot bind %s value to a feature typed by %s", got, want)
+	}
 }
 
 // bindable reports whether a got-typed value may bind to a want-typed feature: a literal's
@@ -234,7 +253,8 @@ func (ec *exprChecker) checkCondition(scope *symbols.Scope, n ast.Node, code, fo
 // redefined duration, a quantity.
 func (ec *exprChecker) checkNonScalarCondition(scope *symbols.Scope, n ast.Node, code, format string, mustType bool) {
 	typeSym := ec.valueTypeSymbol(scope, n)
-	if typeSym == nil {
+	// A collection value is judged element by element by the model below.
+	if _, collection := ec.model.CollectionResultTypes(scope, n); typeSym == nil && !collection {
 		typeSym = ec.invocationResultTypeSymbol(scope, n)
 	}
 	if typeSym == nil {
@@ -329,7 +349,7 @@ func (ec *exprChecker) inferIndex(scope *symbols.Scope, e *ast.IndexExpr) semant
 	// what walks them, so they are not inferred a second time below.
 	var elem semantics.PrimType
 	if seq, isSeq := e.Operand.(*ast.SequenceExpr); isSeq {
-		elem = ec.commonElementType(scope, seq)
+		elem = ec.commonElementType(scope, seq.Elements)
 	} else {
 		elem = ec.infer(scope, e.Operand)
 	}
@@ -391,10 +411,10 @@ func isLiteral(n ast.Node) bool {
 // expression conforms to, or PrimUnknown where they have none in common or any
 // one of them has no known type: PrimConforms holds of PrimUnknown either way
 // round, so it decides conformance but cannot merge types.
-func (ec *exprChecker) commonElementType(scope *symbols.Scope, seq *ast.SequenceExpr) semantics.PrimType {
+func (ec *exprChecker) commonElementType(scope *symbols.Scope, elements []ast.Node) semantics.PrimType {
 	common := semantics.PrimUnknown
 	unknown := false
-	for i, el := range seq.Elements {
+	for i, el := range elements {
 		elem := ec.infer(scope, el)
 		if elem == semantics.PrimUnknown {
 			// Every element is still typed, so an error inside one is reported.
@@ -799,10 +819,10 @@ func (ec *exprChecker) inferInvocation(scope *symbols.Scope, e *ast.InvocationEx
 // call).
 func (ec *exprChecker) inferNodeInvocation(scope *symbols.Scope, e *ast.InvocationExpr, node *symbols.Symbol) semantics.PrimType {
 	args := InvocationArgs(e)
-	// Typed once and reused by checkArguments, so nested errors report once.
+	// Typed once, for selecting the overload, so nested errors report once.
 	argTypes := ec.argumentTypes(scope, e)
 	if chain := ChainCallee(e); chain != nil {
-		return ec.inferChainInvocation(scope, e, chain, args, argTypes, node)
+		return ec.inferChainInvocation(scope, e, chain, args, node)
 	}
 	if e.Type == nil {
 		for _, arg := range e.NamedArgs {
@@ -864,7 +884,7 @@ func (ec *exprChecker) inferNodeInvocation(scope *symbols.Scope, e *ast.Invocati
 	if !ok {
 		return semantics.PrimUnknown
 	}
-	ec.checkArguments(scope, invocation{e, sym, args, argTypes, params}, considered)
+	ec.checkArguments(scope, invocation{e, sym, args, params}, considered)
 	if considered != nil {
 		return semantics.PrimUnknown
 	}
@@ -873,7 +893,7 @@ func (ec *exprChecker) inferNodeInvocation(scope *symbols.Scope, e *ast.Invocati
 
 // inferChainInvocation is inferNodeInvocation for `x.f(a)`: the chain names the
 // calc feature applied, whose effective inputs the arguments bind.
-func (ec *exprChecker) inferChainInvocation(scope *symbols.Scope, e *ast.InvocationExpr, chain *ast.FeatureChainExpr, args []ast.Node, argTypes argumentTypes, node *symbols.Symbol) semantics.PrimType {
+func (ec *exprChecker) inferChainInvocation(scope *symbols.Scope, e *ast.InvocationExpr, chain *ast.FeatureChainExpr, args []ast.Node, node *symbols.Symbol) semantics.PrimType {
 	ec.infer(scope, chain)
 	sym, ok := ec.resolver.ResolveTarget(scope, chain)
 	if !ok || sym == nil {
@@ -898,7 +918,7 @@ func (ec *exprChecker) inferChainInvocation(scope *symbols.Scope, e *ast.Invocat
 	if !ok {
 		return semantics.PrimUnknown
 	}
-	ec.checkArguments(scope, invocation{e, sym, args, argTypes, params}, nil)
+	ec.checkArguments(scope, invocation{e, sym, args, params}, nil)
 	return ec.model.PrimTypeOf(ec.model.ResultParameterOf(sym))
 }
 
@@ -921,19 +941,18 @@ func listing(report reporter, considered []*symbols.Symbol) reporter {
 const msgInvocationParameterRedefinition = "Must correspond to one input parameter of the invoked type"
 
 // invocation is a call under argument checking: the expression, the behavior it names,
-// its positional arguments and their types, and the `in` parameters.
+// its positional arguments, and the `in` parameters.
 type invocation struct {
-	e        *ast.InvocationExpr
-	sym      *symbols.Symbol
-	args     []ast.Node
-	argTypes argumentTypes
-	params   []parameter
+	e      *ast.InvocationExpr
+	sym    *symbols.Symbol
+	args   []ast.Node
+	params []parameter
 }
 
 // checkArguments reports the arguments of the call that do not bind to its `in` parameters,
 // listing considered (the other declarations the call could name) on each report.
 func (ec *exprChecker) checkArguments(scope *symbols.Scope, call invocation, considered []*symbols.Symbol) {
-	e, sym, args, argTypes, params := call.e, call.sym, call.args, call.argTypes, call.params
+	e, sym, args, params := call.e, call.sym, call.args, call.params
 	report := listing(ec.errorf, considered)
 	advise := listing(func(span source.Span, format string, args ...any) {
 		ec.warnCode(CodeUnboundParameter, span, format, args...)
@@ -947,8 +966,8 @@ func (ec *exprChecker) checkArguments(scope *symbols.Scope, call invocation, con
 		return
 	}
 	for i, arg := range args {
-		if mismatch := ec.argumentMismatch(arg, argTypes.positional[i], params[i]); mismatch != "" {
-			report(arg.Span(), "argument %d of %s %s", i+1, sym.Name, mismatch)
+		for _, m := range ec.argumentMismatches(scope, arg, params[i]) {
+			report(m.span, "argument %d of %s %s", i+1, sym.Name, m.why)
 		}
 	}
 	// Arguments bind in order, so the parameters past the last one are unbound.
@@ -966,13 +985,11 @@ const msgUnboundParameter = "%s leaves parameter %s unbound, so the call cannot
 // positional argument binds the feature at its position, a label the feature it
 // names, and a feature is bound at most once.
 func (ec *exprChecker) inferConstructor(scope *symbols.Scope, e *ast.ConstructorExpr) semantics.PrimType {
-	argTypes := make([]semantics.PrimType, len(e.Args))
-	for i, a := range e.Args {
-		argTypes[i] = ec.infer(scope, a)
+	for _, a := range e.Args {
+		ec.infer(scope, a)
 	}
-	namedTypes := make([]semantics.PrimType, len(e.NamedArgs))
-	for i, na := range e.NamedArgs {
-		namedTypes[i] = ec.infer(scope, na.Value)
+	for _, na := range e.NamedArgs {
+		ec.infer(scope, na.Value)
 	}
 	if e.Type == nil {
 		return semantics.PrimUnknown
@@ -1000,9 +1017,9 @@ func (ec *exprChecker) inferConstructor(scope *symbols.Scope, e *ast.Constructor
 			break
 		}
 		bound[features[i]] = true
-		ec.checkFeatureBinding(scope, arg, argTypes[i], features[i], typ)
+		ec.checkFeatureBinding(scope, arg, features[i], typ)
 	}
-	for i, na := range e.NamedArgs {
+	for _, na := range e.NamedArgs {
 		if na.Name == nil {
 			continue
 		}
@@ -1026,56 +1043,73 @@ func (ec *exprChecker) inferConstructor(scope *symbols.Scope, e *ast.Constructor
 			continue
 		}
 		bound[slot] = true
-		ec.checkFeatureBinding(scope, na.Value, namedTypes[i], feature, typ)
+		ec.checkFeatureBinding(scope, na.Value, feature, typ)
 	}
 	return semantics.PrimUnknown
 }
 
-// checkFeatureBinding reports a constructor argument its feature cannot take: by
-// scalar type, by conformance to its declared or inherited type, or by count.
-func (ec *exprChecker) checkFeatureBinding(scope *symbols.Scope, arg ast.Node, got semantics.PrimType, feature, typ *symbols.Symbol) {
+// checkFeatureBinding reports a constructor argument its feature cannot take: the values written
+// together by scalar type or each by conformance, each held element on its own, and the count.
+func (ec *exprChecker) checkFeatureBinding(scope *symbols.Scope, arg ast.Node, feature, typ *symbols.Symbol) {
 	u, ok := feature.Decl.(*ast.Usage)
 	if !ok {
 		return
 	}
-	// An argument with no scalar type (an object, a constructor) is checked by
+	want := ec.model.PrimTypeOf(feature)
+	wants := w8cMostSpecific(ec.model, ec.model.DeclaredFeatureTypes(feature))
+	written, held := ec.argumentElements(scope, arg)
+	// A value with no scalar type (an object, a constructor) is checked by
 	// conformance against the feature's types whether or not those are scalar.
-	if want := ec.model.PrimTypeOf(feature); want != semantics.PrimUnknown && got != semantics.PrimUnknown {
+	if got := ec.silent().commonElementType(scope, written); want != semantics.PrimUnknown && got != semantics.PrimUnknown {
 		if !bindable(arg, got, want) {
 			ec.errorf(arg.Span(), "%s of %s expects %s, found %s", feature.Name, typ.Name, want, got)
 		}
 	} else {
-		ec.checkObjectBinding(scope, arg, feature, typ)
+		for _, value := range written {
+			ec.checkObjectBinding(value, value.Span(), ec.argumentTypeSymbols(scope, value), wants, feature, typ)
+		}
 	}
-	if count, known := exactCount(arg); known {
+	for _, el := range held {
+		if got := ec.heldPrim(el); want != semantics.PrimUnknown && got != semantics.PrimUnknown {
+			if !bindable(el.Node, got, want) {
+				ec.errorf(heldSpan(el, arg), "%s of %s expects %s, found %s", feature.Name, typ.Name, want, got)
+			}
+			continue
+		}
+		ec.checkObjectBinding(el.Node, heldSpan(el, arg), el.Types, wants, feature, typ)
+	}
+	if held, known := ec.heldCount(scope, arg); known {
 		if r, ok := ec.effectiveRange(feature.OwnerScope, usageDecl(u), 0); ok {
-			if msg := r.CountViolation(count); msg != "" {
+			if msg := r.HeldViolation(held); msg != "" {
 				ec.errorf(arg.Span(), "%s of %s: %s", feature.Name, typ.Name, msg)
 			}
 		}
 	}
 }
 
-// checkObjectBinding checks each value of a constructor argument against the
-// non-scalar types its feature declares or inherits; a `new T(…)` is exactly a T.
-func (ec *exprChecker) checkObjectBinding(scope *symbols.Scope, arg ast.Node, feature, typ *symbols.Symbol) {
-	wants := w8cMostSpecific(ec.model, ec.model.DeclaredFeatureTypes(feature))
-	if len(wants) == 0 {
+// checkObjectBinding checks one value a constructor argument binds, typed gots, against wants,
+// the types its feature declares or inherits; a `new T(…)` is exactly a T, another may be a subtype.
+func (ec *exprChecker) checkObjectBinding(value ast.Node, at source.Span, gots, wants []*symbols.Symbol, feature, typ *symbols.Symbol) {
+	if len(gots) == 0 {
 		return
 	}
-	for _, value := range valueElements(arg) {
-		got := ec.argumentTypeSymbol(scope, value)
-		if got == nil {
+	_, exact := value.(*ast.ConstructorExpr)
+	for _, want := range wants {
+		if slices.ContainsFunc(gots, func(got *symbols.Symbol) bool {
+			return ec.model.Conforms(got, want) || (!exact && ec.model.Conforms(want, got))
+		}) {
 			continue
 		}
-		_, exact := value.(*ast.ConstructorExpr)
-		for _, want := range wants {
-			if ec.model.Conforms(got, want) || (!exact && ec.model.Conforms(want, got)) {
-				continue
-			}
-			ec.errorf(value.Span(), "%s of %s is typed by %s; cannot bind a value of type %s", feature.Name, typ.Name, want.Name, got.Name)
-		}
+		ec.errorf(at, "%s of %s is typed by %s; cannot bind a value of type %s", feature.Name, typ.Name, want.Name, typeNames(gots))
+	}
+}
+
+// argumentTypeSymbols is argumentTypeSymbol as a list, empty for none.
+func (ec *exprChecker) argumentTypeSymbols(scope *symbols.Scope, value ast.Node) []*symbols.Symbol {
+	if got := ec.argumentTypeSymbol(scope, value); got != nil {
+		return []*symbols.Symbol{got}
 	}
+	return nil
 }
 
 // argumentTypeSymbol resolves a value's type in scope (feature reference or
@@ -1122,7 +1156,7 @@ func (ec *exprChecker) memberOf(typ, feature *symbols.Symbol) bool {
 // not bind to it, a parameter bound twice (by whichever name or position), and advises
 // of default-less parameters no argument names.
 func (ec *exprChecker) checkNamedArguments(scope *symbols.Scope, call invocation, report, advise reporter) {
-	e, sym, args, argTypes, params := call.e, call.sym, call.args, call.argTypes, call.params
+	e, sym, args, params := call.e, call.sym, call.args, call.params
 	// A receiver binds by position, which named arguments leave unstated; runtime/eval.go
 	// reports the same call.
 	if e.Operand != nil && ChainCallee(e) == nil {
@@ -1136,12 +1170,12 @@ func (ec *exprChecker) checkNamedArguments(scope *symbols.Scope, call invocation
 	bound := make([]bool, len(params))
 	for i, arg := range args {
 		bound[i] = true
-		if mismatch := ec.argumentMismatch(arg, argTypes.positional[i], params[i]); mismatch != "" {
-			report(arg.Span(), "argument %d of %s %s", i+1, sym.Name, mismatch)
+		for _, m := range ec.argumentMismatches(scope, arg, params[i]) {
+			report(m.span, "argument %d of %s %s", i+1, sym.Name, m.why)
 		}
 	}
 	unknown := false
-	for i, arg := range e.NamedArgs {
+	for _, arg := range e.NamedArgs {
 		if arg.Name == nil || len(arg.Name.Parts) == 0 {
 			continue
 		}
@@ -1157,8 +1191,8 @@ func (ec *exprChecker) checkNamedArguments(scope *symbols.Scope, call invocation
 			continue
 		}
 		bound[at] = true
-		if mismatch := ec.argumentMismatch(arg.Value, argTypes.named[i], p); mismatch != "" {
-			report(arg.Value.Span(), "argument %s of %s %s", p.name(), sym.Name, mismatch)
+		for _, m := range ec.argumentMismatches(scope, arg.Value, p) {
+			report(m.span, "argument %s of %s %s", p.name(), sym.Name, m.why)
 		}
 	}
 	// A misspelt name is the likelier cause of a parameter left unbound.
@@ -1202,22 +1236,54 @@ func (ec *exprChecker) parameterPrimType(p parameter) semantics.PrimType {
 	return ec.declaredPrimType(p.scope(), p.usage.Relationships)
 }
 
-// argumentMismatch says why value, typed got, does not bind to p ("" when it does or a type is
-// unknown): a scalar parameter is judged by the lattice, any other by declared type, a Collection
-// taking any sequence and Element the element any argument names.
-func (ec *exprChecker) argumentMismatch(value ast.Node, got semantics.Argument, p parameter) string {
+// misbinding is a value an argument binds that does not bind to its parameter, and why.
+type misbinding struct {
+	span source.Span
+	why  string
+}
+
+// argumentMismatches says why value does not bind to p (none when it does or a type is unknown):
+// the values written are judged together, as a collection literal is; each held element on its own.
+func (ec *exprChecker) argumentMismatches(scope *symbols.Scope, value ast.Node, p parameter) []misbinding {
+	var out []misbinding
+	written, held := ec.argumentElements(scope, value)
+	if len(written) > 0 {
+		got := ec.silent().argumentOf(scope, written)
+		if why := ec.argumentMismatch(value, got.Prim, symbolList(got.Type), p); why != "" {
+			out = append(out, misbinding{value.Span(), why})
+		}
+	}
+	for _, el := range held {
+		if why := ec.argumentMismatch(el.Node, ec.heldPrim(el), el.Types, p); why != "" {
+			out = append(out, misbinding{heldSpan(el, value), why})
+		}
+	}
+	return out
+}
+
+// symbolList is sym as a list, empty for nil.
+func symbolList(sym *symbols.Symbol) []*symbols.Symbol {
+	if sym == nil {
+		return nil
+	}
+	return []*symbols.Symbol{sym}
+}
+
+// argumentMismatch says why value, of scalar type prim and declared types, does not bind to p (""
+// when it does or a type is unknown); a Collection parameter takes any sequence, Element any element.
+func (ec *exprChecker) argumentMismatch(value ast.Node, prim semantics.PrimType, types []*symbols.Symbol, p parameter) string {
 	if want := ec.parameterPrimType(p); want != semantics.PrimUnknown {
-		if got.Prim == semantics.PrimUnknown || bindable(value, got.Prim, want) {
+		if prim == semantics.PrimUnknown || bindable(value, prim, want) {
 			return ""
 		}
-		return fmt.Sprintf("expects %s, found %s", want, got.Prim)
+		return fmt.Sprintf("expects %s, found %s", want, prim)
 	}
 	want := ec.declaredTypeSymbol(p.scope(), p.usage.Relationships)
-	if want == nil || got.Type == nil || semantics.IsCollection(want) || semantics.IsElementType(want) ||
-		ec.model.Conforms(got.Type, want) || ec.model.Conforms(want, got.Type) {
+	if want == nil || len(types) == 0 || semantics.IsCollection(want) || semantics.IsElementType(want) ||
+		ec.boundTypesConform(nil, types, []*symbols.Symbol{want}) {
 		return ""
 	}
-	return fmt.Sprintf("expects %s, found %s", want.Name, got.Type.Name)
+	return fmt.Sprintf("expects %s, found %s", want.Name, typeNames(types))
 }
 
 // isBehaviorKind reports the behavior kinds whose parameter lists are checked.
diff --git a/internal/core/passes/typecheck_operator_test.go b/internal/core/passes/typecheck_operator_test.go
index 7caff3857..f002faddd 100644
--- a/internal/core/passes/typecheck_operator_test.go
+++ b/internal/core/passes/typecheck_operator_test.go
@@ -104,7 +104,7 @@ const castFixture = `package P {
 	classifier Box { feature base : A; feature str : String; }
 	feature box : Box;
 	classifier Box2 :> Box { feature :>> base; %s }
-	function F { return r : A; }
+	function F { return r : A; } function Nothing { in x : A; return r : String[0]; } feature nothing : String[0];
 	classifier Q; classifier R :> Q; classifier CQ ~ Q; feature cq : CQ;
 	feature xs : A[*];
 	feature d : D; feature b : B; datatype U unions B, C; datatype I intersects A, C; datatype NI intersects I, B; datatype Diff differences A, C; feature u : U; feature dd : Diff;
@@ -151,6 +151,25 @@ func TestCastConformanceUnrelatedTypes(t *testing.T) {
 		"16:17 cast argument is typed by A, unrelated to the target C")
 }
 
+// A collection body's result types the cast argument element by element: a body
+// mapping to a String selects no C; one mapping each element to a Boolean and an
+// Integer selects no String, while it does select the Integers; an element the
+// body leaves untyped may be anything, so nothing is known.
+func TestCastConformanceCollectionBody(t *testing.T) {
+	castDiags(t, "", `feature bad = xs.{in x : A; s} as C;`, "16:16 cast argument is typed by String, unrelated to the target C")
+	castDiags(t, "", `feature bad = xs.{in x : A; (true, 1)} as String;`, "16:16 cast argument is typed by Boolean and Integer, unrelated to the target String")
+	castDiags(t, "", `feature bad = xs.{in x : A; (x, 1)} as String;`, "16:16 cast argument is typed by A and Integer, unrelated to the target String")
+	castDiags(t, "", `feature bad = xs->ControlFunctions::collect {in x : A; (true, 1)} as String;`, "16:16 cast argument is typed by Boolean and Integer, unrelated to the target String")
+	castDiags(t, "", `feature some = xs.{in x : A; (true, 1)} as Integer; feature other = xs.{in x : A; (x, 1)} as B;`)
+	castDiags(t, "", `feature open = xs.{in x; (x, 1)} as String; feature open2 = xs.{in x; (untyped, 1)} as String;`)
+	castDiags(t, "", `feature kept = xs->ControlFunctions::select {in x : A; true} as B;`)
+	castDiags(t, "", `feature kept = xs.?{in x : A; true} as B;`)
+	castDiags(t, "", `feature bad = xs.?{in x : A; true} as String;`, "16:16 cast argument is typed by A, unrelated to the target String")
+	castDiags(t, "", `feature none = ()->ControlFunctions::reduce {in x : A; in y : A; s} as C;`)
+	castDiags(t, "", `feature none = xs.{in x : A; nothing} as C; feature none2 = xs->ControlFunctions::collect Nothing as C;`)
+	castDiags(t, "", `feature none = (().{in x : A; x}).{in y : A; s} as C; feature none2 = (xs.{in x : A; nothing}).?{in y : String; true} as C;`)
+}
+
 // A cast up, down, or sideways through one of several types conforms; so does
 // one whose argument's type is not statically known, or is Anything, and one
 // between a composed type and a type it is composed of.
diff --git a/internal/core/passes/typecheck_trigger_test.go b/internal/core/passes/typecheck_trigger_test.go
index 5f9277d9b..cd1039230 100644
--- a/internal/core/passes/typecheck_trigger_test.go
+++ b/internal/core/passes/typecheck_trigger_test.go
@@ -71,6 +71,7 @@ const triggerFixture = `package P {
 		attribute pairWait = (5 [s], 6 [s]);
 		attribute flags : Boolean[2];
 		attribute counts : Integer[2];
+		attribute noCount : Integer[0];
 		attribute waits : DurationValue[2];
 		attribute times : TimeInstantValue[2];
 		attribute firstFlag = flags#(1);
@@ -499,25 +500,46 @@ func TestIndexedTriggerArgument(t *testing.T) {
 	}
 }
 
-// `xs.{…}` is the Anything-typed result of collect; `xs.?{…}` keeps elements of
-// xs and is typed as xs is. The pilot rejects each shape below and accepts the
-// select shapes kept silent.
+// `xs.{…}` is the result of collect, typed as its body's result is — Anything where
+// the body returns an untyped parameter; `xs.?{…}` keeps elements of xs and is
+// typed as xs is. The pilot leaves every collect Anything, so it rejects the
+// collect shapes kept silent too, and accepts the select shapes kept silent.
 func TestCollectAndSelectTriggerArguments(t *testing.T) {
 	const collected = "found a collection `.{…}` maps to, typed Anything"
+	const nothing = "found an empty value over a collection holding nothing, typed Anything"
 	for _, tc := range []struct{ trigger, code, found string }{
-		{"when counts.{in n; n > 3}", "trigger-when-boolean", collected},
+		{"when counts.{in n : Integer; n}", "trigger-when-boolean", "found Integer"},
 		{"when flags.{in f; f}", "trigger-when-boolean", collected},
 		{"when counts.?{in n; n > 3}", "trigger-when-boolean", "found Integer"},
 		{"when holder.ok.{in f; f}", "trigger-when-boolean", collected},
 		{"after waits.{in w; w}", "trigger-after-duration", collected},
+		{"after counts.{in n : Integer; n}", "trigger-after-duration", "found Integer"},
 		{"after counts.?{in n; n > 3}", "trigger-after-duration", "found Integer"},
 		{"after times.?{in i; true}", "trigger-after-duration", "found TimeInstantValue"},
 		{"at counts.?{in n; true}", "trigger-at-time-instant", "found Integer"},
 		{"at times.{in i; i}", "trigger-at-time-instant", collected},
+		{"when flags.{in f : Boolean; (f, 1)}", "trigger-when-boolean", "found Natural"},
+		{"when flags.{in f; (f, 1)}", "trigger-when-boolean", "found Natural"},
+		{"when flags.{in f : Boolean; (f, (1, label))}", "trigger-when-boolean", "found Natural and String"},
+		{"when flags.{in f; (f, label)}", "trigger-when-boolean", "found String"},
+		{"when counts.{in n : Integer; (n > 3, untyped)}", "trigger-when-boolean", collected},
+		{"when counts->ControlFunctions::reduce {in a : Integer; in b : Integer; 5}", "trigger-when-boolean", "found Natural"},
+		{"when ()->ControlFunctions::reduce {in a : Integer; in b : Integer; 5}", "trigger-when-boolean", nothing},
+		{"when ()->ControlFunctions::collect {in a : Integer; 5}", "trigger-when-boolean", nothing},
+		{"when ().{in a : Integer; 5}", "trigger-when-boolean", nothing},
+		{"when counts.{in n : Integer; noCount}", "trigger-when-boolean", nothing},
+		{"when (counts.{in n : Integer; noCount}).{in n : Integer; 5}", "trigger-when-boolean", nothing},
+		{"when (().{in a : Integer; a}).?{in n : Integer; true}", "trigger-when-boolean", nothing},
+		{"when counts.{in n : Integer; (noCount, 5)}", "trigger-when-boolean", "found Natural"},
 	} {
 		wantTriggerDiag(t, "transition first a accept "+tc.trigger+" then b;", tc.code, tc.found)
 	}
 	for _, trigger := range []string{
+		"when counts.{in n; n > 3}",
+		"when flags.{in f : Boolean; f}",
+		"when flags.{in f : Boolean; (f, true)}",
+		"when flags.{in f; (f > 3, true)}",
+		"after waits.{in w : DurationValue; w}",
 		"when flags.?{in f; f}",
 		"when flags.?{in f; f}#(1)",
 		"after waits.?{in w; w > 1 [s]}",
@@ -528,6 +550,10 @@ func TestCollectAndSelectTriggerArguments(t *testing.T) {
 	} {
 		wantTriggerSilent(t, "transition first a accept "+trigger+" then b;")
 	}
+	wantTriggerSilent(t, "entry action { if ()->ControlFunctions::reduce {in a : Integer; in b : Integer; 5} { assign x := 1; } }")
+	wantTriggerSilent(t, "entry action { if ().{in a : Integer; 5} { assign x := 1; } }")
+	wantTriggerSilent(t, "entry action { if counts.{in n : Integer; noCount} { assign x := 1; } }")
+	wantTriggerSilent(t, "entry action { if (counts.{in n : Integer; noCount}).{in n : Integer; 5} { assign x := 1; } }")
 }
 
 // `{ … }` written as a trigger argument is the expression itself, an Evaluation,
diff --git a/internal/core/passes/typecheck_value.go b/internal/core/passes/typecheck_value.go
index 5bd2852be..5504a1d24 100644
--- a/internal/core/passes/typecheck_value.go
+++ b/internal/core/passes/typecheck_value.go
@@ -1,10 +1,12 @@
 package passes
 
 import (
+	"slices"
 	"strings"
 
 	"github.com/Open-MBEE/OpenSysML/internal/core/ast"
 	"github.com/Open-MBEE/OpenSysML/internal/core/semantics"
+	"github.com/Open-MBEE/OpenSysML/internal/core/source"
 	"github.com/Open-MBEE/OpenSysML/internal/core/symbols"
 )
 
@@ -43,6 +45,14 @@ func (ec *exprChecker) checkValueConformance(valueScope, declScope *symbols.Scop
 			}
 			continue
 		}
+		if elements, collection := ec.model.CollectionElements(valueScope, value); collection {
+			// Every element a collection value may hold binds, not the Anything the
+			// library declares; a scalar one written out is the lattice rules' to report.
+			if gots := ec.unboundElementTypes(elements, wants, scalar); len(gots) > 0 {
+				ec.errorf(value.Span(), "cannot bind a value of type %s to a feature typed by %s", typeNames(gots), typeNames(wants))
+			}
+			continue
+		}
 		if result := ec.invocationResultParameter(valueScope, value); result != nil {
 			gots := ec.featureValueTypes(result)
 			if len(gots) > 0 && !(scalar && ec.anyScalar(gots)) && !ec.boundTypesConform(result, gots, wants) {
@@ -88,8 +98,8 @@ func literalPrimType(value ast.Node) semantics.PrimType {
 
 // checkValueCount checks a bound value's element count against the multiplicity
 // governing the feature.
-func (ec *exprChecker) checkValueCount(declScope *symbols.Scope, d featureDecl, value ast.Node) {
-	count, known := exactCount(value)
+func (ec *exprChecker) checkValueCount(valueScope, declScope *symbols.Scope, d featureDecl, value ast.Node) {
+	held, known := ec.heldCount(valueScope, value)
 	if !known {
 		return
 	}
@@ -97,7 +107,7 @@ func (ec *exprChecker) checkValueCount(declScope *symbols.Scope, d featureDecl,
 	if !ok {
 		return
 	}
-	if msg := r.CountViolation(count); msg != "" {
+	if msg := r.HeldViolation(held); msg != "" {
 		ec.errorf(value.Span(), "%s", msg)
 	}
 }
@@ -135,35 +145,32 @@ func (ec *exprChecker) effectiveRange(scope *symbols.Scope, d featureDecl, depth
 	return semantics.Range{}, false
 }
 
-// exactCount returns how many values a bound expression produces, and whether
-// that is statically known. A literal contributes one value and a collection
-// literal the values of its elements; anything else (a feature reference, an
-// invocation) may itself be multi-valued, so its count is unknown — as is that
-// of a collection holding one.
-func exactCount(value ast.Node) (int64, bool) {
+// heldCount is how many values a bound expression produces, where statically bounded: one per
+// literal, the sum over a collection literal, what a collection operation holds; else unknown.
+func (ec *exprChecker) heldCount(scope *symbols.Scope, value ast.Node) (semantics.Range, bool) {
 	if value == nil {
-		return 0, false
+		return semantics.Range{}, false
 	}
 	if _, ok := value.(*ast.NullExpr); ok {
-		return 0, true
+		return semantics.CountRange(0), true
 	}
 	// Binding flattens a collection into the values its elements produce, so a
 	// nested literal contributes its own elements rather than one value.
 	if seq, ok := value.(*ast.SequenceExpr); ok {
-		var total int64
+		total := semantics.CountRange(0)
 		for _, element := range seq.Elements {
-			n, ok := exactCount(element)
+			held, ok := ec.heldCount(scope, element)
 			if !ok {
-				return 0, false
+				return semantics.Range{}, false
 			}
-			total += n
+			total = total.Plus(held)
 		}
 		return total, true
 	}
 	if literalPrimType(value) != semantics.PrimUnknown {
-		return 1, true
+		return semantics.CountRange(1), true
 	}
-	return 0, false
+	return ec.model.CollectionValues(scope, value)
 }
 
 // valueElements returns the values a bound expression contributes: the elements
@@ -185,6 +192,46 @@ func valueElements(value ast.Node) []ast.Node {
 	return []ast.Node{value}
 }
 
+// argumentElements is the values an argument binds: those written — the argument, or the elements
+// of a collection literal — and, apart, each element a collection value among them holds.
+func (ec *exprChecker) argumentElements(scope *symbols.Scope, value ast.Node) (written []ast.Node, held []semantics.CollectionElement) {
+	for _, element := range valueElements(value) {
+		if elements, collection := ec.model.CollectionElements(scope, element); collection {
+			held = append(held, elements...)
+			continue
+		}
+		written = append(written, element)
+	}
+	return written, held
+}
+
+// heldSpan is where a held element is written, or the argument when a result parameter produces it.
+func heldSpan(el semantics.CollectionElement, argument ast.Node) source.Span {
+	if el.Node != nil {
+		return el.Node.Span()
+	}
+	return argument.Span()
+}
+
+// heldPrim is the scalar type of a held element, read silently — the collection value has been
+// typed and reported once already; a result parameter's by its type.
+func (ec *exprChecker) heldPrim(el semantics.CollectionElement) semantics.PrimType {
+	if el.Node != nil {
+		return ec.silent().infer(el.Scope, el.Node)
+	}
+	for _, t := range el.Types {
+		if prim := ec.model.PrimTypeOf(t); prim != semantics.PrimUnknown {
+			return prim
+		}
+	}
+	return semantics.PrimUnknown
+}
+
+// silent is a checker typing as ec does, under the same chains and performances, reporting nothing.
+func (ec *exprChecker) silent() *exprChecker {
+	return &exprChecker{resolver: ec.resolver, model: ec.model, lang: ec.lang, chaining: ec.chaining, performed: ec.performed}
+}
+
 // declaredTypeSymbol returns the symbol a usage is typed by, or nil.
 func (ec *exprChecker) declaredTypeSymbol(scope *symbols.Scope, rels []*ast.Relationship) *symbols.Symbol {
 	if types := ec.declaredTypeSymbols(scope, rels); len(types) > 0 {
@@ -234,6 +281,28 @@ func (ec *exprChecker) boundTypesConform(feature *symbols.Symbol, gots, wants []
 	return false
 }
 
+// unboundElementTypes is the types of those elements of a collection value none of whose
+// types binds to a feature typed by wants; an untyped element binds, and a scalar expression
+// bound to a scalar feature is left to the lattice rules.
+func (ec *exprChecker) unboundElementTypes(elements []semantics.CollectionElement, wants []*symbols.Symbol, scalar bool) []*symbols.Symbol {
+	var out []*symbols.Symbol
+	for _, element := range elements {
+		gots := element.Types
+		if len(gots) == 0 || ec.boundTypesConform(nil, gots, wants) {
+			continue
+		}
+		if scalar && element.Node != nil && ec.anyScalar(gots) {
+			continue
+		}
+		for _, got := range gots {
+			if !slices.Contains(out, got) {
+				out = append(out, got)
+			}
+		}
+	}
+	return out
+}
+
 // typeNames joins the names of types as a declaration lists them.
 func typeNames(types []*symbols.Symbol) string {
 	names := make([]string, 0, len(types))
@@ -310,8 +379,16 @@ func (ec *exprChecker) featureValueTypes(sym *symbols.Symbol) []*symbols.Symbol
 }
 
 // invocationResultTypeSymbol returns the type of the result parameter of the
-// behavior an invocation names, which is the type of the value it produces.
+// behavior an invocation names, which is the type of the value it produces; for
+// a collection value (`xs.{…}`, a collection function call) the one type the elements it holds
+// have — none when it holds nothing.
 func (ec *exprChecker) invocationResultTypeSymbol(scope *symbols.Scope, value ast.Node) *symbols.Symbol {
+	if types, collection := ec.model.CollectionHeldTypes(scope, value); collection {
+		if len(types) == 1 {
+			return types[0]
+		}
+		return nil
+	}
 	result := ec.invocationResultParameter(scope, value)
 	if result == nil {
 		return nil
@@ -334,7 +411,10 @@ func (ec *exprChecker) invocationResultParameter(scope *symbols.Scope, value ast
 	if chain := ChainCallee(inv); chain != nil {
 		sym, _ = ec.resolver.ResolveTarget(scope, chain)
 	} else if inv.Type != nil {
-		sym = SelectInvocation(ec.resolver, ec.model, scope, inv, ec.performs(inv)).Selected
+		// The arguments type silently, but under the chains being typed: one whose
+		// body reads the feature being valued would otherwise type it again.
+		silent := ec.silent()
+		sym = silent.selectInvocation(scope, inv, silent.argumentTypes(scope, inv), ec.performs(inv)).Selected
 	}
 	if sym == nil || !ec.isInvocationBehavior(sym, map[*symbols.Symbol]bool{}) {
 		return nil
diff --git a/internal/core/passes/typecheck_value_test.go b/internal/core/passes/typecheck_value_test.go
index d92a17608..53d6b1cf3 100644
--- a/internal/core/passes/typecheck_value_test.go
+++ b/internal/core/passes/typecheck_value_test.go
@@ -1,6 +1,9 @@
 package passes
 
-import "testing"
+import (
+	"slices"
+	"testing"
+)
 
 // enumPrelude declares types outside the scalar lattice: an enumeration, a
 // structural hierarchy, and an unrelated definition.
@@ -290,3 +293,401 @@ func TestValueIndexedCollectionElementIsUnknown(t *testing.T) {
 		part v : M::Vehicle = bs#(1);
 	}`, "cannot bind a value of type Boat to a feature typed by Vehicle")
 }
+
+// collectionValueDiags is the name-resolution and type diagnostics of a model of vehicles and
+// boats whose collection values, in members, are judged element by element against the library.
+func collectionValueDiags(t *testing.T, members string) []string {
+	t.Helper()
+	diags := libraryDiags(t, `package P {
+		private import ScalarValues::*;
+		private import ControlFunctions::*;
+		part def Vehicle; part def Truck :> Vehicle; part def Car :> Vehicle; part def Boat;
+		part vs : Vehicle[*];
+		part truck : Truck;
+		part car : Car;
+		part one : Vehicle[1];
+		part two : Vehicle[2..*];
+		part none : Vehicle[0];
+		part boat : Boat;
+		function Boats { in v : Vehicle; return r : Boat; }
+		function Sail { in b : Boat; return r : Boat; }
+		function Drive { in v : Vehicle; return r : Vehicle; }
+		function Half { in v : Vehicle; return r : Real; }
+		function Name { in v : Vehicle; return r : String; }
+		function Nobody { in v : Vehicle; return r : Vehicle[0]; }
+		function Nobody2 :> Nobody { in v : Vehicle; return r :>> r; }
+		function Nobody3 :> Nobody { in v : Vehicle; return r : Vehicle; }
+		alias noone for none;
+		attribute nothing : Integer[0];
+		part def Pair { part items : Vehicle[2]; part item : Vehicle[1]; }
+		part def Pairs :> Pair { part :>> items; part :>> item; }
+		part pair : Pairs[1];
+		part couple : Pairs[2];
+		part nobody : Pairs[0];
+		`+members+`
+	}`)
+	var got []string
+	for _, d := range diags {
+		got = append(got, d.Message)
+	}
+	return got
+}
+
+func wantCollectionValueDiags(t *testing.T, members string, want ...string) {
+	t.Helper()
+	if got := collectionValueDiags(t, members); !slices.Equal(got, want) {
+		t.Errorf("%s:\n got %q\nwant %q", members, got, want)
+	}
+}
+
+// A collection value binds by the elements it maps to or keeps, not by the Anything the
+// library declares its result: collect and `xs.{…}` by the body's result, select and
+// selectOne by the collection's elements, a sequence-valued body element by element.
+func TestValueCollectionResultIsJudged(t *testing.T) {
+	wantCollectionValueDiags(t, `part b : Boat = vs.{ in v : Vehicle; v };`,
+		"cannot bind a value of type Vehicle to a feature typed by Boat")
+	wantCollectionValueDiags(t, `part b : Boat = vs->collect { in v : Vehicle; v };`,
+		"cannot bind a value of type Vehicle to a feature typed by Boat")
+	wantCollectionValueDiags(t, `part b : Boat = vs->collect Drive;`,
+		"cannot bind a value of type Vehicle to a feature typed by Boat")
+	wantCollectionValueDiags(t, `part b : Boat = vs->select { in v : Vehicle; true };`,
+		"cannot bind a value of type Vehicle to a feature typed by Boat")
+	wantCollectionValueDiags(t, `part b : Boat = vs->selectOne { in v : Vehicle; true };`,
+		"cannot bind a value of type Vehicle to a feature typed by Boat")
+	wantCollectionValueDiags(t, `part b : Boat = vs.?{ in v : Vehicle; true };`,
+		"cannot bind a value of type Vehicle to a feature typed by Boat")
+	wantCollectionValueDiags(t, `attribute i : Integer = vs.{ in v : Vehicle; true };`,
+		"cannot bind Boolean value to a feature typed by Integer")
+	wantCollectionValueDiags(t, `attribute i : Integer = vs->collect { in v : Vehicle; (true, 1) };`,
+		"cannot bind Boolean value to a feature typed by Integer")
+	wantCollectionValueDiags(t, `attribute i : Integer = vs->collect Name;`,
+		"cannot bind a value of type String to a feature typed by Integer")
+	wantCollectionValueDiags(t, `part b : Boat = vs.{ in v : Vehicle; (v, boat) };`,
+		"cannot bind a value of type Vehicle to a feature typed by Boat")
+	wantCollectionValueDiags(t, `
+		part t : Truck = vs->collect { in v : Vehicle; v };
+		part v : Vehicle = vs->select { in v : Vehicle; true };
+		part v2 : Vehicle = vs.?{ in v : Vehicle; true };
+		part b : Boat = vs->collect { in v : Vehicle; boat };
+		part b2 : Boat = vs->collect Boats;
+		attribute i : Integer = vs->collect { in v : Vehicle; (1, 2) };
+		attribute b3 : Boolean = vs->forAll { in v : Vehicle; true };
+		part open : Boat = vs.{ in v; v };
+		part open2 : Boat = vs.{ in v; (v, boat) };`)
+}
+
+// A scalar element a collection value spells out is exact, as a literal bound directly is:
+// a decimal does not bind to an Integer feature because Integer values are Real. An
+// element a feature or function result types only bounds its values, so it binds either way.
+func TestValueCollectionElementLiteralIsExact(t *testing.T) {
+	wantCollectionValueDiags(t, `attribute i : Integer = vs.{ in v : Vehicle; 1.5 };`,
+		"cannot bind Rational value to a feature typed by Integer")
+	wantCollectionValueDiags(t, `attribute i : Integer = vs->collect { in v : Vehicle; 1.5 };`,
+		"cannot bind Rational value to a feature typed by Integer")
+	wantCollectionValueDiags(t, `attribute i : Integer = vs->collect { in v : Vehicle; (1, 2.5) };`,
+		"cannot bind Rational value to a feature typed by Integer")
+	wantCollectionValueDiags(t, `attribute n : Natural = vs.{ in v : Vehicle; -1 };`,
+		"cannot bind Integer value to a feature typed by Natural")
+	wantCollectionValueDiags(t, `attribute i : Integer = (1, 2)->reduce { in a : Integer; in b : Integer; 1.5 };`,
+		"cannot bind Rational value to a feature typed by Integer")
+	wantCollectionValueDiags(t, `attribute i : Integer = (1.5, 2.5)->select { in a : Real; true };`,
+		"cannot bind Rational value to a feature typed by Integer",
+		"cannot bind Rational value to a feature typed by Integer")
+	wantCollectionValueDiags(t, `attribute i : Integer = (1.5, 2.5).?{ in a : Real; true };`,
+		"cannot bind Rational value to a feature typed by Integer",
+		"cannot bind Rational value to a feature typed by Integer")
+	wantCollectionValueDiags(t, `
+		attribute r : Real;
+		attribute i : Integer = vs.{ in v : Vehicle; r };
+		attribute i2 : Integer = vs->collect { in v : Vehicle; r / 2 };
+		attribute i3 : Integer = vs->collect Half;
+		attribute i4 : Integer = vs.{ in v : Vehicle; 2 };
+		attribute r2 : Real = vs.{ in v : Vehicle; 2 };
+		attribute i5 : Integer = (1, 2)->select { in a : Integer; true };
+		attribute i6 : Integer = (1, 2).?{ in a : Integer; true };`)
+}
+
+// An element that is itself a collection value binds by the elements it holds: a scalar
+// literal nested in an inner collect, or kept by a selection, is judged as if written out.
+func TestValueNestedCollectionElementsAreJudged(t *testing.T) {
+	wantCollectionValueDiags(t, `attribute i : Integer = vs.{ in v : Vehicle; vs.{ in w : Vehicle; 1.5 } };`,
+		"cannot bind Rational value to a feature typed by Integer")
+	wantCollectionValueDiags(t, `attribute i : Integer = vs->collect { in v : Vehicle; vs->collect { in w : Vehicle; 1.5 } };`,
+		"cannot bind Rational value to a feature typed by Integer")
+	wantCollectionValueDiags(t, `attribute i : Integer = vs->select { in v : Vehicle; true }.{ in w : Vehicle; (1, 2.5) };`,
+		"cannot bind Rational value to a feature typed by Integer")
+	wantCollectionValueDiags(t, `attribute i : Integer = (vs.{ in v : Vehicle; 1.5 }).?{ in r : Real; true };`,
+		"cannot bind Rational value to a feature typed by Integer")
+	wantCollectionValueDiags(t, `attribute i : Integer = (vs.{ in v : Vehicle; 1.5 })->select { in r : Real; true };`,
+		"cannot bind Rational value to a feature typed by Integer")
+	wantCollectionValueDiags(t, `part b : Boat = vs.{ in v : Vehicle; vs->select { in w : Vehicle; true } };`,
+		"cannot bind a value of type Vehicle to a feature typed by Boat")
+	wantCollectionValueDiags(t, `
+		attribute i : Integer = vs.{ in v : Vehicle; vs.{ in w : Vehicle; 2 } };
+		attribute r : Real = vs.{ in v : Vehicle; vs.{ in w : Vehicle; 1.5 } };
+		attribute i2 : Integer = vs.{ in v : Vehicle; ().{ in w : Integer; 1.5 } };`)
+}
+
+// A feature valued by `xs.?{…}` over a sequence written out takes the type its elements share,
+// as one valued by `xs->select {…}` does, so a result, a subject or a cast it is bound to is
+// judged by that type rather than by the Anything the sequence is.
+func TestValueSelectShorthandOfSequenceTypesFeature(t *testing.T) {
+	for _, keep := range []string{`.?{ in v : Vehicle; true }`, `->select { in v : Vehicle; true }`} {
+		wantCollectionValueDiags(t, `function F { return r : Boat; (one, one)`+keep+` }`,
+			"Bound features should have conforming types")
+		wantCollectionValueDiags(t, `
+			part picked = (one, one)`+keep+`;
+			function F { return r : Boat; picked }`,
+			"Bound features should have conforming types")
+		wantCollectionValueDiags(t, `
+			part picked = (one, one)`+keep+`;
+			requirement def R { subject s : Boat; }
+			requirement r : R { subject s = picked; }`,
+			"Bound features should have conforming types")
+		wantCollectionValueDiags(t, `
+			part picked = (one, one)`+keep+`;
+			function F { return r : Vehicle; picked }
+			requirement def R { subject s : Vehicle; }
+			requirement r : R { subject s = picked; }`)
+	}
+	wantCollectionValueDiags(t, `
+		attribute picked = (1, 2).?{ in v : Integer; true };
+		part b = picked as Boat;`,
+		"cast argument is typed by Integer, unrelated to the target Boat: neither type specializes the other, so the cast selects no value")
+	wantCollectionValueDiags(t, `
+		part any = (one, boat).?{ in v; true };
+		function F { return r : Boat; any }`)
+}
+
+// Sibling elements kept or mapped to share their nearest supertype: a feature valued by a
+// selection of a Truck and a Car is a Vehicle, so it is judged as one where it is bound or cast.
+func TestValueSiblingElementsShareSupertype(t *testing.T) {
+	for _, keep := range []string{`.?{ in v : Vehicle; true }`, `->select { in v : Vehicle; true }`} {
+		wantCollectionValueDiags(t, `
+			part kin = (truck, car)`+keep+`;
+			function F { return r : Boat; kin }`,
+			"Bound features should have conforming types")
+		wantCollectionValueDiags(t, `
+			part kin = (truck, car)`+keep+`;
+			part b = kin as Boat;`,
+			"cast argument is typed by Vehicle, unrelated to the target Boat: neither type specializes the other, so the cast selects no value")
+		wantCollectionValueDiags(t, `
+			part kin = (truck, car)`+keep+`;
+			function F { return r : Vehicle; kin }
+			part t = kin as Truck;`)
+	}
+	wantCollectionValueDiags(t, `
+		part kin = vs.{ in v : Vehicle; (truck, car) };
+		function F { return r : Boat; kin }`,
+		"Bound features should have conforming types")
+}
+
+// A collection value's body is checked once, as inferring the value: reading the types of
+// the elements it produces to judge their binding reports nothing again.
+func TestValueCollectionBodyIsCheckedOnce(t *testing.T) {
+	wantCollectionValueDiags(t, `attribute i : Integer = vs.{ in v : Vehicle; 1 + true };`,
+		"operator '+' is not defined for Natural and Boolean")
+	wantCollectionValueDiags(t, `attribute i : Integer = vs->collect { in v : Vehicle; 1 + true };`,
+		"operator '+' is not defined for Natural and Boolean")
+	wantCollectionValueDiags(t, `attribute i : Integer = vs->collect { in v : Vehicle; (1 + true, 2.5) };`,
+		"operator '+' is not defined for Natural and Boolean",
+		"cannot bind Rational value to a feature typed by Integer")
+	wantCollectionValueDiags(t, `attribute i : Integer = one->reduce { in a : Vehicle; in b : Vehicle; 1 + true };`,
+		"cannot bind a value of type Vehicle to a feature typed by Integer",
+		"operator '+' is not defined for Natural and Boolean")
+}
+
+// reduce returns the reducer's result, or the collection's one element unreduced:
+// both bind unless the collection is known to hold two or more.
+func TestValueReduceResultIsJudged(t *testing.T) {
+	wantCollectionValueDiags(t, `part b : Boat = vs->reduce { in a : Vehicle; in b : Vehicle; boat };`,
+		"cannot bind a value of type Vehicle to a feature typed by Boat")
+	wantCollectionValueDiags(t, `part b : Boat = one->reduce { in a : Vehicle; in b : Vehicle; boat };`,
+		"cannot bind a value of type Vehicle to a feature typed by Boat")
+	wantCollectionValueDiags(t, `part v : Vehicle = vs->reduce { in a : Vehicle; in b : Vehicle; boat };`,
+		"cannot bind a value of type Boat to a feature typed by Vehicle")
+	wantCollectionValueDiags(t, `attribute s : String = (1, 2)->reduce { in a : Integer; in b : Integer; 3 };`,
+		"cannot bind Natural value to a feature typed by String")
+	wantCollectionValueDiags(t, `part b : Boat = pair.item->reduce { in a : Vehicle; in b : Vehicle; boat };`,
+		"cannot bind a value of type Vehicle to a feature typed by Boat")
+	wantCollectionValueDiags(t, `
+		part b : Boat = two->reduce { in a : Vehicle; in b : Vehicle; boat };
+		part b2 : Boat = pair.items->reduce { in a : Vehicle; in b : Vehicle; boat };
+		part b3 : Boat = couple.item->reduce { in a : Vehicle; in b : Vehicle; boat };
+		part v : Vehicle = vs->reduce { in a : Vehicle; in b : Vehicle; a };
+		attribute s : String = (1, 2)->reduce { in a : Integer; in b : Integer; "s" };
+		attribute s2 : String = (one, boat)->reduce { in a : Vehicle; in b : Vehicle; "s" };
+		attribute i : Integer = (two->collect Name)->reduce { in a : String; in b : String; 3 };`)
+}
+
+// A collection value binds as many values as it is known to hold: none over a collection
+// holding none, one per element a collect maps over a known count, from a reduce the one element
+// unreduced or as many as the reducer yields over two or more; one only bounded is reported where
+// even its fewest or its most cannot fit, else left to evaluation.
+func TestValueCollectionCountIsJudged(t *testing.T) {
+	wantCollectionValueDiags(t, `part b : Boat[1] = none.{ in v : Vehicle; boat };`,
+		"0 value(s) bound to a feature with multiplicity lower bound 1")
+	wantCollectionValueDiags(t, `part b : Boat[1..2] = ()->collect { in v : Vehicle; boat };`,
+		"0 value(s) bound to a feature with multiplicity lower bound 1")
+	wantCollectionValueDiags(t, `part b : Boat[2] = none->select { in v : Vehicle; true };`,
+		"0 value(s) bound to a feature with multiplicity lower bound 2")
+	wantCollectionValueDiags(t, `part b : Boat[1] = ()->reduce { in a : Boat; in b : Boat; a };`,
+		"0 value(s) bound to a feature with multiplicity lower bound 1")
+	wantCollectionValueDiags(t, `part b : Boat[1] = pair.items.{ in v : Vehicle; boat };`,
+		"2 value(s) bound to a feature with multiplicity upper bound 1")
+	wantCollectionValueDiags(t, `part b : Boat[0..1] = pair.items->collect { in v : Vehicle; (boat, boat) };`,
+		"4 value(s) bound to a feature with multiplicity upper bound 1")
+	wantCollectionValueDiags(t, `attribute s : String[3] = ("a", one.{ in v : Vehicle; "b" });`,
+		"2 value(s) bound to a feature with multiplicity lower bound 3")
+	wantCollectionValueDiags(t, `part b : Boat[3] = pair.items->collect Boats;`,
+		"2 value(s) bound to a feature with multiplicity lower bound 3")
+	wantCollectionValueDiags(t, `
+		part huge : Vehicle[9223372036854775807];
+		attribute s : String[9223372036854775807] = (huge.{ in v : Vehicle; "a" }, "b");`,
+		"more than 9223372036854775807 value(s) bound to a feature with multiplicity upper bound 9223372036854775807")
+	wantCollectionValueDiags(t, `part b : Boat[1] = two.{ in v : Vehicle; boat };`,
+		"at least 2 value(s) bound to a feature with multiplicity upper bound 1")
+	wantCollectionValueDiags(t, `part v : Vehicle[3] = one->select { in v : Vehicle; true };`,
+		"at most 1 value(s) bound to a feature with multiplicity lower bound 3")
+	wantCollectionValueDiags(t, `part v : Vehicle[2] = pair.items->selectOne { in v : Vehicle; true };`,
+		"at most 1 value(s) bound to a feature with multiplicity lower bound 2")
+	wantCollectionValueDiags(t, `part b : Boat[1] = pair.items->reduce { in a : Vehicle; in b : Vehicle; (boat, boat) };`,
+		"2 value(s) bound to a feature with multiplicity upper bound 1")
+	wantCollectionValueDiags(t, `part b : Boat[1] = pair.items->reduce { in a : Vehicle; in b : Vehicle; () };`,
+		"0 value(s) bound to a feature with multiplicity lower bound 1")
+	wantCollectionValueDiags(t, `part b : Boat[1] = two->reduce { in a : Vehicle; in b : Vehicle; (boat, boat) };`,
+		"2 value(s) bound to a feature with multiplicity upper bound 1")
+	wantCollectionValueDiags(t, `part v : Vehicle[3] = vs->reduce { in a : Vehicle; in b : Vehicle; (a, b) };`,
+		"at most 2 value(s) bound to a feature with multiplicity lower bound 3")
+	wantCollectionValueDiags(t, `
+		part b : Boat[2] = pair.items.{ in v : Vehicle; boat };
+		part b2 : Boat[1] = pair.items->reduce { in a : Vehicle; in b : Vehicle; boat };
+		part b5 : Boat[2] = pair.items->reduce { in a : Vehicle; in b : Vehicle; (boat, boat) };
+		part b6 : Boat[0..1] = pair.items->reduce { in a : Vehicle; in b : Vehicle; () };
+		part v3 : Vehicle[1..2] = vs->reduce { in a : Vehicle; in b : Vehicle; (a, b) };
+		part v4 : Vehicle[1] = one->reduce { in a : Vehicle; in b : Vehicle; (a, b) };
+		part v5 : Vehicle[0..1] = pair.items->reduce { in a : Vehicle; in b : Vehicle; a };
+		part v : Vehicle[0..1] = pair.items->selectOne { in v : Vehicle; true };
+		part b3 : Boat[1] = vs.{ in v : Vehicle; boat };
+		part v2 : Vehicle[0..2] = pair.items->select { in v : Vehicle; true };
+		part b4 : Boat[2] = pair.items->collect Boats;`)
+}
+
+// A collection operation over a collection known to hold nothing returns nothing, and never
+// applies the reducer or body: no element is bound, though the value is still typed by them.
+func TestValueReduceOfNothingIsJudgedByNeither(t *testing.T) {
+	wantCollectionValueDiags(t, `
+		attribute s : String = ()->reduce { in a : Integer; in b : Integer; 3 };
+		attribute s2 : String = none->reduce { in a : Vehicle; in b : Vehicle; 3 };
+		part b : Boat = none->reduce { in a : Vehicle; in b : Vehicle; a };
+		part b2 : Boat = nobody.item->reduce { in a : Vehicle; in b : Vehicle; a };
+		attribute s3 : String = ()->collect { in a : Integer; 3 };
+		attribute s4 : String = none.{ in a : Vehicle; 3 };
+		part b3 = Sail(none->reduce { in a : Vehicle; in b : Vehicle; a });`)
+}
+
+// A body mapping every element to nothing — a `[0]` feature or function result — holds nothing
+// either, as does any operation over such a collection: no element is judged.
+func TestValueMappingToNothingIsJudgedByNeither(t *testing.T) {
+	wantCollectionValueDiags(t, `
+		attribute s : String = vs.{ in v : Vehicle; nothing };
+		attribute s2 : String = vs->collect { in v : Vehicle; (nothing, nothing) };
+		part b : Boat = vs->collect Nobody;
+		part b2 : Boat = vs.{ in v : Vehicle; Nobody(v) };
+		attribute s3 : String = (vs.{ in v : Vehicle; nothing }).{ in n : Integer; 3 };
+		attribute s4 : String = (().{ in a : Integer; a }).{ in b : Integer; 3 };
+		part b3 : Boat = (none->select { in v : Vehicle; true })->reduce { in a : Vehicle; in b : Vehicle; a };
+		part b4 : Boat = (vs->collect Nobody).?{ in v : Vehicle; true };
+		part b5 : Boat = (vs->selectOne { in v : Vehicle; true }).{ in v : Vehicle; Nobody(v) }->collect { in v : Vehicle; v };
+		part b6 = Sail(vs.{ in v : Vehicle; Nobody(v) });
+		part b7 = Sail((vs->collect Nobody)->select { in v : Vehicle; true });
+		part b8 : Boat = vs->collect Nobody2;
+		part b11 : Boat = vs->collect Nobody3;
+		part b9 : Boat = noone.{ in v : Vehicle; v };
+		part b10 : Boat = noone->reduce { in a : Vehicle; in b : Vehicle; a };`)
+	wantCollectionValueDiags(t, `attribute s : String = vs.{ in v : Vehicle; (nothing, 3) };`,
+		"cannot bind Natural value to a feature typed by String")
+	wantCollectionValueDiags(t, `part b : Boat = (vs.{ in v : Vehicle; v }).{ in v : Vehicle; v };`,
+		"cannot bind a value of type Vehicle to a feature typed by Boat")
+}
+
+// A collection value passed as an argument is typed by its elements, so the parameter
+// it binds is judged and the overload selected by them.
+func TestArgumentCollectionResultIsJudged(t *testing.T) {
+	wantCollectionValueDiags(t, `part b = Sail(vs->collect { in v : Vehicle; v });`,
+		"argument 1 of Sail expects Boat, found Vehicle")
+	wantCollectionValueDiags(t, `part b = Sail(vs->select { in v : Vehicle; true });`,
+		"argument 1 of Sail expects Boat, found Vehicle")
+	wantCollectionValueDiags(t, `part b = Sail(vs->selectOne { in v : Vehicle; true });`,
+		"argument 1 of Sail expects Boat, found Vehicle")
+	wantCollectionValueDiags(t, `part b = Sail(vs.{ in v : Vehicle; v });`,
+		"argument 1 of Sail expects Boat, found Vehicle")
+	wantCollectionValueDiags(t, `part b = Sail(vs.?{ in v : Vehicle; true });`,
+		"argument 1 of Sail expects Boat, found Vehicle")
+	wantCollectionValueDiags(t, `part v = Drive(two->reduce { in a : Vehicle; in b : Vehicle; boat });`,
+		"argument 1 of Drive expects Vehicle, found Boat")
+	wantCollectionValueDiags(t, `part v = Drive(vs->reduce { in a : Vehicle; in b : Vehicle; boat });`,
+		"argument 1 of Drive expects Vehicle, found Boat")
+	wantCollectionValueDiags(t, `part b = Sail(one->reduce { in a : Vehicle; in b : Vehicle; boat });`,
+		"argument 1 of Sail expects Boat, found Vehicle")
+	wantCollectionValueDiags(t, `
+		part b = Sail(vs->collect { in v : Vehicle; boat });
+		part v = Drive(vs->select { in v : Vehicle; true });
+		part v4 = Drive(vs.?{ in v : Vehicle; true });
+		part v2 = Drive(two->reduce { in a : Vehicle; in b : Vehicle; one });
+		part v3 = Drive(vs->reduce { in a : Vehicle; in b : Vehicle; a });
+		part v5 = Drive(one->reduce { in a : Vehicle; in b : Vehicle; boat });
+		part v6 = Drive((none, one)->reduce { in a : Vehicle; in b : Vehicle; boat });`)
+}
+
+// Each element a collection value holds is judged on its own, so a collection whose elements
+// share no type does not pass unjudged, and a literal an element spells binds exactly.
+func TestArgumentCollectionElementsAreJudgedSeverally(t *testing.T) {
+	wantCollectionValueDiags(t, `part b = Sail(vs.{ in v : Vehicle; (v, boat) });`,
+		"argument 1 of Sail expects Boat, found Vehicle")
+	wantCollectionValueDiags(t, `part b = Sail((boat, vs.{ in v : Vehicle; v }));`,
+		"argument 1 of Sail expects Boat, found Vehicle")
+	wantCollectionValueDiags(t, `part v = Drive(vs->collect { in v : Vehicle; (boat, v) });`,
+		"argument 1 of Drive expects Vehicle, found Boat")
+	wantCollectionValueDiags(t, `
+		function Count { in n : Integer; return r : Integer; }
+		part n = Count(vs.{ in v : Vehicle; 1.5 });`,
+		"argument 1 of Count expects Integer, found Rational")
+	wantCollectionValueDiags(t, `
+		function Count { in n : Integer; return r : Integer; }
+		part n = Count(n = vs->collect { in v : Vehicle; (1, 1.5) });`,
+		"argument n of Count expects Integer, found Rational")
+	wantCollectionValueDiags(t, `
+		function Count { in n : Integer; return r : Integer; }
+		attribute h : Real;
+		part n = Count(vs.{ in v : Vehicle; 1 });
+		part n2 = Count(vs.{ in v : Vehicle; h });
+		part b = Sail((boat, vs.{ in v : Vehicle; boat }));`)
+}
+
+// A constructor argument binds each element a collection value holds to the feature: a mixed
+// collection is refused by the element that does not conform, a collected literal by its exact type.
+func TestConstructorCollectionElementsAreJudgedSeverally(t *testing.T) {
+	wantCollectionValueDiags(t, `
+		part def Fleet { part b : Boat; }
+		part f = new Fleet(vs.{ in v : Vehicle; (v, boat) });`,
+		"b of Fleet is typed by Boat; cannot bind a value of type Vehicle")
+	wantCollectionValueDiags(t, `
+		part def Fleet { part b : Boat; }
+		part f = new Fleet(b = (boat, vs.{ in v : Vehicle; v }));`,
+		"b of Fleet is typed by Boat; cannot bind a value of type Vehicle")
+	wantCollectionValueDiags(t, `
+		part def Fleet { attribute n : Integer; }
+		part f = new Fleet(vs.{ in v : Vehicle; 1.5 });`,
+		"n of Fleet expects Integer, found Rational")
+	wantCollectionValueDiags(t, `
+		part def Fleet { attribute n : Integer; }
+		part f = new Fleet(n = vs->collect { in v : Vehicle; (1, 1.5) });`,
+		"n of Fleet expects Integer, found Rational")
+	wantCollectionValueDiags(t, `
+		part def Fleet { part b : Boat; attribute n : Integer; }
+		attribute h : Real;
+		part f = new Fleet(vs.{ in v : Vehicle; boat }, vs.{ in v : Vehicle; 1 });
+		part f2 = new Fleet(n = vs.{ in v : Vehicle; h });
+		part f3 = new Fleet((boat, vs.{ in v : Vehicle; boat }));`)
+}
diff --git a/internal/core/passes/w7g_one_type_test.go b/internal/core/passes/w7g_one_type_test.go
index 4d30621d6..03fee9513 100644
--- a/internal/core/passes/w7g_one_type_test.go
+++ b/internal/core/passes/w7g_one_type_test.go
@@ -239,7 +239,9 @@ func TestW7GACastAndBodyEnumeratedValuesAreTyped(t *testing.T) {
 // TestW7GASelectedEnumeratedValueKeepsItsOperandType: `xs.?{…}` keeps the
 // elements of xs, so it types the value as xs is typed — through a chain, an
 // alias, a feature typed only by its own value or subsetting/redefining one, a
-// nested selection or an indexed element — while `.{…}` and `,` yield Anything (pilot 2026-07 agrees on every case).
+// nested selection or an indexed element — and `xs.{…}` is typed as its body's
+// result is, Anything where that is untyped, while `,` yields Anything (pilot
+// 2026-07 agrees on every case but the typed collect bodies, which it leaves Anything).
 func TestW7GASelectedEnumeratedValueKeepsItsOperandType(t *testing.T) {
 	const src = `package T {
 		private import ScalarValues::*;
@@ -270,13 +272,16 @@ func TestW7GASelectedEnumeratedValueKeepsItsOperandType(t *testing.T) {
 			l = zz.?{in r : Real; r > 1.0};
 			m = zz;
 			n = w2.qq.?{in r : Real; r > 1.0};
+			q = xs.{in r : Real; r};
+			r = others.{in o : Other; o};
 		}
 		enum def WrongNum :> Real {
 			o = ns.?{in n : Natural; n > 1};
 			p = others.?{in o : Other; true};
+			s = ns.{in n : Natural; n};
 		}
 		enum def Right {
-			ok1 = xs.{in r : Real; r};
+			ok1 = xs.{in r; r};
 			ok2 = Right::ok1.?{in l : Right; true};
 		}
 		enum def RightNum :> Real {
@@ -294,6 +299,7 @@ func TestW7GASelectedEnumeratedValueKeepsItsOperandType(t *testing.T) {
 			ok14 = zz.?{in r : Real; r > 1.0};
 			ok15 = zz;
 			ok16 = w2.qq.?{in r : Real; r > 1.0};
+			ok17 = xs.{in r : Real; r};
 		}
 	}`
 	var got []string
@@ -303,7 +309,7 @@ func TestW7GASelectedEnumeratedValueKeepsItsOperandType(t *testing.T) {
 		}
 		got = append(got, strings.Fields(src[d.Span.Offset:d.Span.End()])[0])
 	}
-	want := []string{"a", "b", "c", "d", "e", "f", "g", "h", "i", "j", "k", "l", "m", "n", "o", "p"}
+	want := []string{"a", "b", "c", "d", "e", "f", "g", "h", "i", "j", "k", "l", "m", "n", "q", "r", "o", "p", "s"}
 	if strings.Join(got, " ") != strings.Join(want, " ") {
 		t.Fatalf("selected enumerated values typed outside their enumeration: got %v, want %v", got, want)
 	}
diff --git a/internal/core/semantics/collection.go b/internal/core/semantics/collection.go
new file mode 100644
index 000000000..47d5811ff
--- /dev/null
+++ b/internal/core/semantics/collection.go
@@ -0,0 +1,861 @@
+package semantics
+
+import (
+	"math"
+	"strings"
+
+	"github.com/Open-MBEE/OpenSysML/internal/core/ast"
+	"github.com/Open-MBEE/OpenSysML/internal/core/symbols"
+)
+
+// Kernel Function Library collection functions whose result the arguments specialize.
+const (
+	fqnCollect   = "ControlFunctions::collect"
+	fqnSelect    = "ControlFunctions::select"
+	fqnReject    = "ControlFunctions::reject"
+	fqnSelectOne = "ControlFunctions::selectOne"
+	fqnReduce    = "ControlFunctions::reduce"
+)
+
+// collectionSource is what the elements of a collection function's result are: an
+// expression in its scope — the result of the body applied, or the collection kept —
+// or the result parameter of the function applied by name.
+type collectionSource struct {
+	scope  *symbols.Scope
+	node   ast.Node
+	result *symbols.Symbol
+}
+
+// CollectionResultTypes is the types every element of a collection value — `xs.{…}` or a call
+// of a ControlFunctions collection function — has, and whether its arguments decide the value
+// rather than the declared result alone; nil types where they are unknown or say nothing.
+func (m *Model) CollectionResultTypes(scope *symbols.Scope, node ast.Node) ([]*symbols.Symbol, bool) {
+	if m == nil || m.resolver == nil || node == nil {
+		return nil, false
+	}
+	srcs, ok := m.sourcesOf(scope, node)
+	if !ok {
+		return nil, false
+	}
+	return m.sourcesTypes(srcs), true
+}
+
+// CollectionValues is how many values a collection value — `xs.{…}`, `xs.?{…}` or a call of a
+// ControlFunctions collection function — holds, where the value is one and its size is known.
+func (m *Model) CollectionValues(scope *symbols.Scope, node ast.Node) (Range, bool) {
+	if m == nil || m.resolver == nil || node == nil {
+		return Range{}, false
+	}
+	if _, ok := m.collectionOf(scope, node); !ok {
+		return Range{}, false
+	}
+	return m.valuesHeldBy(scope, node)
+}
+
+// sourcesOf is the sources typing a collection value: `xs.{…}` by its body, `xs.?{…}` by xs, a
+// collection function call by its arguments; not ok for any other value.
+func (m *Model) sourcesOf(scope *symbols.Scope, node ast.Node) ([]collectionSource, bool) {
+	switch n := node.(type) {
+	case *ast.CollectExpr:
+		return m.collectSources(scope, n)
+	case *ast.SelectExpr:
+		return m.keptSources(scope, n.Operand)
+	case *ast.InvocationExpr:
+		return m.invocationSources(scope, n, m.invocationCallee(scope, n))
+	}
+	return nil, false
+}
+
+// heldSourcesOf is the sources of the elements a collection value holds: those typing it, less
+// any known to yield nothing — all of them over a collection holding nothing.
+func (m *Model) heldSourcesOf(scope *symbols.Scope, node ast.Node) ([]collectionSource, bool) {
+	if collection, ok := m.collectionOf(scope, node); ok && m.holdsNothing(scope, collection) {
+		return nil, true
+	}
+	srcs, ok := m.sourcesOf(scope, node)
+	if !ok {
+		return nil, false
+	}
+	held := make([]collectionSource, 0, len(srcs))
+	for _, src := range srcs {
+		if src.result != nil && m.resultHoldsNothing(src.result) || src.result == nil && m.holdsNothing(src.scope, src.node) {
+			continue
+		}
+		held = append(held, src)
+	}
+	return held, true
+}
+
+// resultHoldsNothing reports a result parameter whose multiplicity admits no value.
+func (m *Model) resultHoldsNothing(result *symbols.Symbol) bool {
+	r, ok := m.governingMultiplicity(result)
+	return ok && r.Upper.Known && !r.Upper.Infinite && r.Upper.Value == 0
+}
+
+// governingMultiplicity is the multiplicity a feature declares, or inherits from a feature it
+// redefines by clause or position, read through an alias; not ok where it declares and inherits none.
+func (m *Model) governingMultiplicity(sym *symbols.Symbol) (Range, bool) {
+	if alias, ok := m.resolver.ResolveAliasTarget(sym); ok && alias != nil {
+		sym = alias
+	}
+	if declared, ok := m.MultiplicityOf(sym); ok {
+		return declared, true
+	}
+	for _, redefined := range m.AllRedefinedFeatures(sym) {
+		if inherited, ok := m.MultiplicityOf(redefined); ok {
+			return inherited, true
+		}
+	}
+	return Range{}, false
+}
+
+func knownRange(r Range, ok bool) (Range, bool) {
+	return r, ok && r.Lower.Known && r.Upper.Known
+}
+
+// collectionOf is the collection a collection value operates over: the operand of `xs.{…}` or
+// `xs.?{…}`, the first argument of a collection function call; not ok for any other value.
+func (m *Model) collectionOf(scope *symbols.Scope, node ast.Node) (ast.Node, bool) {
+	switch n := node.(type) {
+	case *ast.CollectExpr:
+		return n.Operand, true
+	case *ast.SelectExpr:
+		return n.Operand, true
+	case *ast.InvocationExpr:
+		fn := m.invocationCallee(scope, n)
+		if fn == nil || !m.isCollectionFunction(fn) {
+			return nil, false
+		}
+		return m.argumentTo(scope, n, fn, 0), true
+	}
+	return nil, false
+}
+
+func (m *Model) isCollectionFunction(fn *symbols.Symbol) bool {
+	for _, fqn := range []string{fqnCollect, fqnSelect, fqnReject, fqnSelectOne, fqnReduce} {
+		if fn == m.libSymbol(fqn) {
+			return true
+		}
+	}
+	return false
+}
+
+// invocationSources type a collection function call: collect by what it applies, select/reject/
+// selectOne by the collection, reduce by the reducer and the one element it may return unreduced.
+func (m *Model) invocationSources(scope *symbols.Scope, e *ast.InvocationExpr, fn *symbols.Symbol) ([]collectionSource, bool) {
+	if fn == nil || e == nil {
+		return nil, false
+	}
+	switch fn {
+	case m.libSymbol(fqnCollect):
+		return m.appliedSources(scope, m.argumentTo(scope, e, fn, 1))
+	case m.libSymbol(fqnReduce):
+		return m.reducedSources(scope, m.argumentTo(scope, e, fn, 0), m.argumentTo(scope, e, fn, 1))
+	case m.libSymbol(fqnSelect), m.libSymbol(fqnReject), m.libSymbol(fqnSelectOne):
+		return m.keptSources(scope, m.argumentTo(scope, e, fn, 0))
+	}
+	return nil, false
+}
+
+// reducedSources type a reduction: the reducer is applied only over two elements or more, the one
+// element a collection may hold is returned unreduced; over nothing the reducer types the result.
+func (m *Model) reducedSources(scope *symbols.Scope, collection, reducer ast.Node) ([]collectionSource, bool) {
+	var srcs []collectionSource
+	size, known := m.valuesHeldBy(scope, collection)
+	if !known || size.Upper.Infinite || size.Upper.Value != 1 {
+		applied, ok := m.appliedSources(scope, reducer)
+		if !ok {
+			return nil, false
+		}
+		srcs = applied
+	}
+	if collection != nil && (!known || !size.Lower.Infinite && size.Lower.Value <= 1 && (size.Upper.Infinite || size.Upper.Value >= 1)) {
+		srcs = append(srcs, collectionSource{scope: scope, node: collection})
+	}
+	return srcs, true
+}
+
+// keptSources is the source of a selection: the collection whose elements it keeps.
+func (m *Model) keptSources(scope *symbols.Scope, collection ast.Node) ([]collectionSource, bool) {
+	if collection == nil {
+		return nil, false
+	}
+	return []collectionSource{{scope: scope, node: collection}}, true
+}
+
+// holdsNothing reports a collection statically known to hold no element: `()`, or a feature
+// whose multiplicity admits none.
+func (m *Model) holdsNothing(scope *symbols.Scope, collection ast.Node) bool {
+	r, ok := m.valuesHeldBy(scope, collection)
+	return ok && !r.Upper.Infinite && r.Upper.Value == 0
+}
+
+// valuesHeldBy is how many values a collection expression holds: `()` none, a literal one, a
+// sequence the sum over its elements, a feature or chain the multiplicity governing it, a chain
+// holding through each value of its operand the values of its last feature, a collection
+// operation what it maps to, keeps or reduces; not ok where unknown.
+func (m *Model) valuesHeldBy(scope *symbols.Scope, node ast.Node) (Range, bool) {
+	switch n := node.(type) {
+	case *ast.NullExpr:
+		return CountRange(0), true
+	case *ast.CollectExpr:
+		return m.valuesMappedBy(scope, n.Operand, n.Body)
+	case *ast.SelectExpr:
+		return m.valuesKeptFrom(scope, n.Operand, Bound{Infinite: true, Known: true})
+	case *ast.InvocationExpr:
+		return m.valuesHeldByCall(scope, n)
+	case *ast.LiteralInteger, *ast.LiteralReal, *ast.LiteralString, *ast.LiteralBool:
+		return CountRange(1), true
+	case *ast.SequenceExpr:
+		sum := CountRange(0)
+		for _, element := range n.Elements {
+			r, ok := m.valuesHeldBy(scope, element)
+			if !ok {
+				return Range{}, false
+			}
+			sum = addRanges(sum, r)
+		}
+		return sum, true
+	case *ast.FeatureReference, *ast.QualifiedName:
+		return m.valuesHeldByFeature(scope, n)
+	case *ast.FeatureChainExpr:
+		last, ok := m.valuesHeldByFeature(scope, n)
+		if !ok {
+			return Range{}, false
+		}
+		through, ok := m.valuesHeldBy(scope, n.Operand)
+		if !ok {
+			return Range{}, false
+		}
+		return mulRanges(through, last), true
+	}
+	return Range{}, false
+}
+
+// valuesHeldByCall is how many values a call holds: collect what it maps to, select/reject up to
+// all, selectOne up to one, reduce what it reduces to, any other function what its result
+// parameter declares.
+func (m *Model) valuesHeldByCall(scope *symbols.Scope, e *ast.InvocationExpr) (Range, bool) {
+	fn := m.invocationCallee(scope, e)
+	if fn == nil {
+		return Range{}, false
+	}
+	switch fn {
+	case m.libSymbol(fqnCollect):
+		return m.valuesMappedBy(scope, m.argumentTo(scope, e, fn, 0), m.argumentTo(scope, e, fn, 1))
+	case m.libSymbol(fqnSelect), m.libSymbol(fqnReject):
+		return m.valuesKeptFrom(scope, m.argumentTo(scope, e, fn, 0), Bound{Infinite: true, Known: true})
+	case m.libSymbol(fqnSelectOne):
+		return m.valuesKeptFrom(scope, m.argumentTo(scope, e, fn, 0), Bound{Value: 1, Known: true})
+	case m.libSymbol(fqnReduce):
+		return m.valuesReducedFrom(scope, m.argumentTo(scope, e, fn, 0), m.argumentTo(scope, e, fn, 1))
+	}
+	if result := m.ResultParameterOf(fn); result != nil {
+		return m.valuesGoverning(result)
+	}
+	return Range{}, false
+}
+
+// valuesMappedBy is how many values mapping each of a collection's values through applied
+// yields: as many as the body's result or the function's result parameter holds per value.
+func (m *Model) valuesMappedBy(scope *symbols.Scope, collection, applied ast.Node) (Range, bool) {
+	if collection == nil {
+		return Range{}, false
+	}
+	through, ok := m.valuesHeldBy(scope, collection)
+	if !ok {
+		return Range{}, false
+	}
+	return mulRanges(through, m.valuesApplied(scope, applied)), true
+}
+
+// valuesReducedFrom is how many values reducing a collection yields: none from none, the one
+// element it holds unreduced, the reducer's result over two or more; either where it may hold
+// one or more than one.
+func (m *Model) valuesReducedFrom(scope *symbols.Scope, collection, reducer ast.Node) (Range, bool) {
+	if collection == nil {
+		return Range{}, false
+	}
+	through, ok := m.valuesHeldBy(scope, collection)
+	if !ok {
+		return Range{}, false
+	}
+	one := Bound{Value: 1, Known: true}
+	unreduced := Range{Lower: minBound(through.Lower, one), Upper: minBound(through.Upper, one)}
+	if !through.Upper.Infinite && through.Upper.Value <= 1 {
+		return unreduced, true
+	}
+	reduced := m.valuesApplied(scope, reducer)
+	if through.Lower.Infinite || through.Lower.Value >= 2 {
+		return reduced, true
+	}
+	return Range{Lower: minBound(unreduced.Lower, reduced.Lower), Upper: maxBound(unreduced.Upper, reduced.Upper)}, true
+}
+
+// valuesApplied is how many values one application of a body or named function yields: as many
+// as the body's result or the function's result parameter holds; any number where unknown.
+func (m *Model) valuesApplied(scope *symbols.Scope, applied ast.Node) Range {
+	switch a := applied.(type) {
+	case *ast.BodyExpr:
+		if a.Result != nil {
+			if r, ok := m.valuesHeldBy(symbols.BodyExprScope(scope, a), a.Result); ok {
+				return r
+			}
+		}
+	case *ast.FeatureReference, *ast.QualifiedName, *ast.FeatureChainExpr:
+		if result := m.appliedResult(scope, a); result != nil {
+			if r, ok := m.valuesGoverning(result); ok {
+				return r
+			}
+		}
+	}
+	return Range{Lower: Bound{Known: true}, Upper: unbounded}
+}
+
+// valuesKeptFrom is how many values a selection keeps: none up to the collection's, capped at most.
+func (m *Model) valuesKeptFrom(scope *symbols.Scope, collection ast.Node, most Bound) (Range, bool) {
+	if collection == nil {
+		return Range{}, false
+	}
+	through, ok := m.valuesHeldBy(scope, collection)
+	if !ok {
+		return Range{}, false
+	}
+	return Range{Lower: Bound{Known: true}, Upper: minBound(through.Upper, most)}, true
+}
+
+// valuesHeldByFeature is how many values the feature a name or chain resolves to holds.
+func (m *Model) valuesHeldByFeature(scope *symbols.Scope, node ast.Node) (Range, bool) {
+	sym, ok := m.resolver.ResolveTarget(scope, node)
+	if !ok || sym == nil {
+		return Range{}, false
+	}
+	return m.valuesGoverning(sym)
+}
+
+// valuesGoverning is how many values a feature holds: the multiplicity governing it, through an
+// alias, declared or inherited by redefinition — one where it has none; not ok while a bound
+// it declares is not evaluable.
+func (m *Model) valuesGoverning(sym *symbols.Symbol) (Range, bool) {
+	if r, ok := m.governingMultiplicity(sym); ok {
+		return knownRange(r, true)
+	}
+	return AssumedRange(), true
+}
+
+// CountRange is the range admitting n values alone.
+func CountRange(n int64) Range {
+	b := Bound{Value: n, Known: true}
+	return Range{Lower: b, Upper: b}
+}
+
+// Plus is the values two collections hold together: the sum of their bounds.
+func (r Range) Plus(o Range) Range {
+	return addRanges(r, o)
+}
+
+// addRanges is the values two collections hold together; a bound summing past int64 exceeds
+// every multiplicity bound, so it is unbounded.
+func addRanges(a, b Range) Range {
+	return Range{Lower: addBounds(a.Lower, b.Lower), Upper: addBounds(a.Upper, b.Upper)}
+}
+
+// mulRanges is the values held through each value of a, each holding b; a bound multiplying
+// past int64 exceeds every multiplicity bound, so it is unbounded.
+func mulRanges(a, b Range) Range {
+	return Range{Lower: mulBounds(a.Lower, b.Lower), Upper: mulBounds(a.Upper, b.Upper)}
+}
+
+var unbounded = Bound{Infinite: true, Known: true}
+
+// addBounds is a + b, unbounded past where int64 reaches.
+func addBounds(a, b Bound) Bound {
+	if a.Infinite || b.Infinite || a.Value > math.MaxInt64-b.Value {
+		return unbounded
+	}
+	return Bound{Value: a.Value + b.Value, Known: true}
+}
+
+func minBound(a, b Bound) Bound {
+	switch {
+	case a.Infinite:
+		return b
+	case b.Infinite || a.Value <= b.Value:
+		return a
+	}
+	return b
+}
+
+func maxBound(a, b Bound) Bound {
+	switch {
+	case a.Infinite || b.Infinite:
+		return unbounded
+	case a.Value >= b.Value:
+		return a
+	}
+	return b
+}
+
+// mulBounds is a × b, none through none, unbounded past where int64 reaches.
+func mulBounds(a, b Bound) Bound {
+	if (!a.Infinite && a.Value == 0) || (!b.Infinite && b.Value == 0) {
+		return Bound{Known: true}
+	}
+	if a.Infinite || b.Infinite || a.Value > math.MaxInt64/b.Value {
+		return unbounded
+	}
+	return Bound{Value: a.Value * b.Value, Known: true}
+}
+
+// collectSources is the source of `xs.{ in x; … }`: its body's result.
+func (m *Model) collectSources(scope *symbols.Scope, e *ast.CollectExpr) ([]collectionSource, bool) {
+	body, ok := e.Body.(*ast.BodyExpr)
+	if !ok {
+		return nil, false
+	}
+	return m.bodySources(scope, body)
+}
+
+// appliedSources is the source of the expression applied to each element: a body
+// `{ in x; … }` by its result, a function or expression named by its result parameter.
+func (m *Model) appliedSources(scope *symbols.Scope, applied ast.Node) ([]collectionSource, bool) {
+	switch n := applied.(type) {
+	case *ast.BodyExpr:
+		return m.bodySources(scope, n)
+	case *ast.FeatureReference, *ast.QualifiedName, *ast.FeatureChainExpr:
+		if result := m.appliedResult(scope, n); result != nil {
+			return []collectionSource{{result: result}}, true
+		}
+	}
+	return nil, false
+}
+
+// bodySources is the result of a body `{ in x; … }`, resolved among its parameters.
+func (m *Model) bodySources(scope *symbols.Scope, body *ast.BodyExpr) ([]collectionSource, bool) {
+	if body == nil || body.Result == nil || m.resolver == nil {
+		return nil, false
+	}
+	return []collectionSource{{scope: symbols.BodyExprScope(scope, body), node: body.Result}}, true
+}
+
+// appliedResult is the result parameter of the function or expression the name applied denotes.
+func (m *Model) appliedResult(scope *symbols.Scope, applied ast.Node) *symbols.Symbol {
+	if m.resolver == nil {
+		return nil
+	}
+	sym, ok := m.resolver.ResolveTarget(scope, applied)
+	if !ok || sym == nil {
+		return nil
+	}
+	if alias, ok := m.resolver.ResolveAliasTarget(sym); ok {
+		sym = alias
+	}
+	return m.ResultParameterOf(sym)
+}
+
+// argumentTo is the expression e passes to the i-th input parameter of fn: the receiver of
+// `xs->fn(…)` binds the first, then positional arguments in order, then named ones by name.
+func (m *Model) argumentTo(scope *symbols.Scope, e *ast.InvocationExpr, fn *symbols.Symbol, i int) ast.Node {
+	positional := make([]ast.Node, 0, len(e.Args)+1)
+	if e.Operand != nil {
+		positional = append(positional, e.Operand)
+	}
+	positional = append(positional, e.Args...)
+	if i < len(positional) {
+		return positional[i]
+	}
+	if len(e.NamedArgs) == 0 {
+		return nil
+	}
+	sig := m.signatureOf(fn)
+	for _, arg := range e.NamedArgs {
+		if arg.Name != nil && m.parameterIndex(scope, sig, arg.Name) == i {
+			return arg.Value
+		}
+	}
+	return nil
+}
+
+// collectionResultTypes is the types every element of a collection function call's result
+// has; nil where they are unknown or say nothing.
+func (m *Model) collectionResultTypes(scope *symbols.Scope, e *ast.InvocationExpr, fn *symbols.Symbol) []*symbols.Symbol {
+	srcs, ok := m.invocationSources(scope, e, fn)
+	if !ok {
+		return nil
+	}
+	return m.sourcesTypes(srcs)
+}
+
+// collectResultTypes is the types every element of `xs.{ in x; … }` has; nil when unknown.
+func (m *Model) collectResultTypes(scope *symbols.Scope, e *ast.CollectExpr) []*symbols.Symbol {
+	srcs, ok := m.collectSources(scope, e)
+	if !ok {
+		return nil
+	}
+	return m.sourcesTypes(srcs)
+}
+
+// selectResultTypes is the types every element of `xs.?{ in x; … }` has: those of the elements
+// of xs, as `xs->select {…}` keeps them; nil when unknown.
+func (m *Model) selectResultTypes(scope *symbols.Scope, e *ast.SelectExpr) []*symbols.Symbol {
+	srcs, ok := m.keptSources(scope, e.Operand)
+	if !ok {
+		return nil
+	}
+	return m.sourcesTypes(srcs)
+}
+
+// CollectionElement is one element a collection value may hold: the expression producing it,
+// in its scope, or nil where a function's result parameter does; and its types, nil where unknown.
+type CollectionElement struct {
+	Scope *symbols.Scope
+	Node  ast.Node
+	Types []*symbols.Symbol
+}
+
+// CollectionElements is each element a collection value may hold (a nested collection value by
+// its own elements), and whether the value's arguments decide it rather than its declaration.
+func (m *Model) CollectionElements(scope *symbols.Scope, node ast.Node) ([]CollectionElement, bool) {
+	if m == nil || m.resolver == nil || node == nil {
+		return nil, false
+	}
+	srcs, ok := m.heldSourcesOf(scope, node)
+	if !ok {
+		return nil, false
+	}
+	return m.heldElements(srcs), true
+}
+
+// CollectionHeldTypes is the types every element a collection value holds has, and whether the
+// value's arguments decide it; nil types where it holds nothing or they are unknown.
+func (m *Model) CollectionHeldTypes(scope *symbols.Scope, node ast.Node) ([]*symbols.Symbol, bool) {
+	elements, ok := m.CollectionElements(scope, node)
+	if !ok {
+		return nil, false
+	}
+	lists := make([][]*symbols.Symbol, 0, len(elements))
+	for _, element := range elements {
+		lists = append(lists, element.Types)
+	}
+	return informativeTypes(m.sharedAmong(lists)), true
+}
+
+// heldElements is each element the sources hold, a collection-valued one by its elements in turn.
+func (m *Model) heldElements(srcs []collectionSource) []CollectionElement {
+	var out []CollectionElement
+	for _, element := range m.sourcesElements(srcs) {
+		if element.Node == nil {
+			out = append(out, element)
+			continue
+		}
+		if m.holdsNothing(element.Scope, element.Node) {
+			continue
+		}
+		inner, ok := m.heldSourcesOf(element.Scope, element.Node)
+		if !ok {
+			out = append(out, element)
+			continue
+		}
+		out = append(out, m.heldElements(inner)...)
+	}
+	return out
+}
+
+// sourcesTypes is the types every element of every source conforms to; nil when unknown or
+// when only Anything, which says nothing.
+func (m *Model) sourcesTypes(srcs []collectionSource) []*symbols.Symbol {
+	var lists [][]*symbols.Symbol
+	for _, element := range m.sourcesElements(srcs) {
+		lists = append(lists, element.Types)
+	}
+	return informativeTypes(m.sharedAmong(lists))
+}
+
+// sourcesElements is each element of every source: a result parameter by its own types, a
+// sequence `(a, b)` each element in turn; types nil where they say nothing.
+func (m *Model) sourcesElements(srcs []collectionSource) []CollectionElement {
+	var out []CollectionElement
+	for _, src := range srcs {
+		if src.result != nil {
+			out = append(out, CollectionElement{Types: informativeTypes(m.featureResultTypes(src.result))})
+			continue
+		}
+		out = append(out, m.elementsOf(src.scope, src.node)...)
+	}
+	return out
+}
+
+func (m *Model) elementsOf(scope *symbols.Scope, node ast.Node) []CollectionElement {
+	seq, ok := node.(*ast.SequenceExpr)
+	if !ok {
+		return []CollectionElement{{Scope: scope, Node: node, Types: informativeTypes(m.resultTypes(scope, node))}}
+	}
+	var out []CollectionElement
+	for _, element := range seq.Elements {
+		out = append(out, m.elementsOf(scope, element)...)
+	}
+	return out
+}
+
+// sharedAmong is the types a value of every list conforms to; nil when there is no list or
+// one is empty.
+func (m *Model) sharedAmong(lists [][]*symbols.Symbol) []*symbols.Symbol {
+	var common []*symbols.Symbol
+	for i, types := range lists {
+		if i > 0 {
+			types = m.sharedTypes(common, types)
+		}
+		if common = types; len(common) == 0 {
+			return nil
+		}
+	}
+	return common
+}
+
+// sharedTypes is the most specific types a value of each list conforms to: those of either
+// list, else the nearest supertypes the lists share (Truck and Car share Vehicle).
+func (m *Model) sharedTypes(a, b []*symbols.Symbol) []*symbols.Symbol {
+	var out []*symbols.Symbol
+	for _, list := range [][]*symbols.Symbol{a, b} {
+		for _, typ := range list {
+			if !containsElement(out, typ) && m.anyConforms(a, typ) && m.anyConforms(b, typ) {
+				out = append(out, typ)
+			}
+		}
+	}
+	if len(out) > 0 {
+		return out
+	}
+	return m.nearestShared(a, b)
+}
+
+// nearestShared is the types a value of each list conforms to, among all either list's types
+// may conform to, less any a more specific one among them specializes.
+func (m *Model) nearestShared(a, b []*symbols.Symbol) []*symbols.Symbol {
+	var shared []*symbols.Symbol
+	for _, sup := range m.conformableFrom(append(append([]*symbols.Symbol(nil), a...), b...)) {
+		if m.anyConforms(a, sup) && m.anyConforms(b, sup) {
+			shared = append(shared, sup)
+		}
+	}
+	var out []*symbols.Symbol
+	for _, typ := range shared {
+		if !m.anySpecializes(shared, typ) {
+			out = append(out, typ)
+		}
+	}
+	return out
+}
+
+// conformableFrom is every type the types may conform to: their supertypes, and — a union
+// conforming to whatever all its unioning types do — those of their unioning types in turn.
+func (m *Model) conformableFrom(types []*symbols.Symbol) []*symbols.Symbol {
+	var out []*symbols.Symbol
+	visited := make(map[*symbols.Symbol]bool)
+	var visit func(sym *symbols.Symbol)
+	visit = func(sym *symbols.Symbol) {
+		if visited[sym] {
+			return
+		}
+		visited[sym] = true
+		for _, sup := range m.AllSupertypes(sym) {
+			if !containsElement(out, sup) {
+				out = append(out, sup)
+			}
+		}
+		for _, u := range m.UnioningTypes(sym) {
+			if !containsElement(out, u) {
+				out = append(out, u)
+			}
+			visit(u)
+		}
+	}
+	for _, typ := range types {
+		visit(typ)
+	}
+	return out
+}
+
+// anySpecializes reports a type among types conforming to want that want does not conform to.
+func (m *Model) anySpecializes(types []*symbols.Symbol, want *symbols.Symbol) bool {
+	for _, typ := range types {
+		if typ != want && m.Conforms(typ, want) && !m.Conforms(want, typ) {
+			return true
+		}
+	}
+	return false
+}
+
+func (m *Model) anyConforms(types []*symbols.Symbol, want *symbols.Symbol) bool {
+	for _, typ := range types {
+		if m.Conforms(typ, want) {
+			return true
+		}
+	}
+	return false
+}
+
+// collectionConformance judges `xs.{…}` or a collection function call by the elements it
+// holds: every one must conform. Not ok where they are unknown and the declaration decides.
+func (m *Model) collectionConformance(scope *symbols.Scope, node ast.Node, want *symbols.Symbol, byUnit bool) (Conformance, bool) {
+	srcs, ok := m.heldSourcesOf(scope, node)
+	if !ok {
+		return conformanceUnknown(), false
+	}
+	return m.sourcesConformance(srcs, want, byUnit)
+}
+
+// sourcesConformance judges a collection value by its sources: every element must conform. A
+// value with no source holds nothing, an empty value typed Anything as `null` is.
+func (m *Model) sourcesConformance(srcs []collectionSource, want *symbols.Symbol, byUnit bool) (Conformance, bool) {
+	if len(srcs) == 0 {
+		c := m.typeConformance(m.libSymbol(fqnAnything), want)
+		if c.Known && !c.Holds {
+			c.Found = "an empty value over a collection holding nothing, typed Anything"
+			c.Untyped = true
+		}
+		return c, true
+	}
+	judged := m.judgeSources(srcs,
+		func(scope *symbols.Scope, node ast.Node) Conformance {
+			return m.elementConformance(scope, node, want, byUnit)
+		},
+		func(result *symbols.Symbol) Conformance { return m.featureConformance(result, want) })
+	return decided(everyHolds(judged))
+}
+
+// collectionCastConformance judges a collection value cast to T by the elements it holds: sound
+// when some element and T specialize one another, or none is held (as `null as T` is).
+func (m *Model) collectionCastConformance(scope *symbols.Scope, operand ast.Node, target *symbols.Symbol) (Conformance, bool) {
+	srcs, ok := m.heldSourcesOf(scope, operand)
+	if !ok {
+		return conformanceUnknown(), false
+	}
+	if len(srcs) == 0 {
+		return Conformance{Known: true, Holds: true}, true
+	}
+	judged := m.judgeSources(srcs,
+		func(scope *symbols.Scope, node ast.Node) Conformance { return m.castConformance(scope, node, target) },
+		func(result *symbols.Symbol) Conformance {
+			return m.castTypesConformance(m.featureResultTypes(result), target)
+		})
+	return decided(anyHolds(judged))
+}
+
+// judgeSources judges each element of every source: a result parameter as the feature, an
+// expression by itself, a sequence `(a, b)` element by element, one holding nothing not at all.
+func (m *Model) judgeSources(srcs []collectionSource, byNode func(*symbols.Scope, ast.Node) Conformance, byResult func(*symbols.Symbol) Conformance) []Conformance {
+	var out []Conformance
+	for _, src := range srcs {
+		if src.result != nil {
+			out = append(out, byResult(src.result))
+			continue
+		}
+		out = append(out, m.elementJudgements(src.scope, src.node, byNode)...)
+	}
+	return out
+}
+
+func (m *Model) elementJudgements(scope *symbols.Scope, node ast.Node, judge func(*symbols.Scope, ast.Node) Conformance) []Conformance {
+	if m.holdsNothing(scope, node) {
+		return nil
+	}
+	seq, ok := node.(*ast.SequenceExpr)
+	if !ok {
+		return []Conformance{judge(scope, node)}
+	}
+	var out []Conformance
+	for _, element := range seq.Elements {
+		out = append(out, m.elementJudgements(scope, element, judge)...)
+	}
+	return out
+}
+
+// elementConformance judges one element; a value typed Anything alone says nothing of it.
+func (m *Model) elementConformance(scope *symbols.Scope, node ast.Node, want *symbols.Symbol, byUnit bool) Conformance {
+	c := m.exprConformance(scope, node, want, byUnit)
+	if c.Known && !c.Holds && m.typedAnything(scope, node) {
+		return conformanceUnknown()
+	}
+	return c
+}
+
+// typedAnything reports a value whose only type is Anything.
+func (m *Model) typedAnything(scope *symbols.Scope, node ast.Node) bool {
+	types := m.resultTypes(scope, node)
+	return len(types) > 0 && len(informativeTypes(types)) == 0
+}
+
+// everyHolds holds when every judgement does, fails naming each known not to, and is
+// unknown while none fails and one is unknown or untyped.
+func everyHolds(judged []Conformance) Conformance {
+	if len(judged) == 0 {
+		return conformanceUnknown()
+	}
+	var found []string
+	unknown := false
+	for _, c := range judged {
+		switch {
+		case !c.Known || c.Untyped:
+			unknown = true
+		case !c.Holds:
+			found = appendUnique(found, c.Found)
+		}
+	}
+	switch {
+	case len(found) > 0:
+		return Conformance{Known: true, Found: strings.Join(found, " and ")}
+	case unknown:
+		return conformanceUnknown()
+	}
+	return Conformance{Known: true, Holds: true}
+}
+
+// anyHolds holds when any judgement does, fails naming each when every one is known not
+// to, and is unknown while none holds and one is unknown or untyped.
+func anyHolds(judged []Conformance) Conformance {
+	if len(judged) == 0 {
+		return conformanceUnknown()
+	}
+	var found []string
+	unknown := false
+	for _, c := range judged {
+		switch {
+		case c.Known && c.Holds:
+			return c
+		case !c.Known || c.Untyped:
+			unknown = true
+		default:
+			found = appendUnique(found, c.Found)
+		}
+	}
+	if unknown {
+		return conformanceUnknown()
+	}
+	return Conformance{Known: true, Found: strings.Join(found, " and ")}
+}
+
+// decided is c with whether it decides anything: an unknown or untyped value leaves the
+// declared result to decide.
+func decided(c Conformance) (Conformance, bool) {
+	return c, c.Known && !c.Untyped
+}
+
+// informativeTypes is types unless every one is Anything, which says nothing; then nil.
+func informativeTypes(types []*symbols.Symbol) []*symbols.Symbol {
+	for _, typ := range types {
+		if !IsAnything(typ) {
+			return types
+		}
+	}
+	return nil
+}
+
+func appendUnique(list []string, s string) []string {
+	for _, item := range list {
+		if item == s {
+			return list
+		}
+	}
+	return append(list, s)
+}
diff --git a/internal/core/semantics/collection_test.go b/internal/core/semantics/collection_test.go
new file mode 100644
index 000000000..d7650d308
--- /dev/null
+++ b/internal/core/semantics/collection_test.go
@@ -0,0 +1,668 @@
+package semantics
+
+import (
+	"math"
+	"slices"
+	"strings"
+	"testing"
+
+	"github.com/Open-MBEE/OpenSysML/internal/core/ast"
+	"github.com/Open-MBEE/OpenSysML/internal/core/symbols"
+)
+
+// collectionModel builds a model of parts C with a mass and a name, held by S as
+// cs [*], where the collection expressions under test are S's attribute values.
+func collectionModel(t *testing.T, attributes string) (*Model, *symbols.Scope) {
+	t.Helper()
+	m, root := stdlibModelWithDoc(t, "collection.sysml", `package P {
+		private import ScalarValues::*;
+		private import ISQ::*;
+		private import SI::*;
+		private import ControlFunctions::*;
+		private import ScalarFunctions::'+';
+		part def C { attribute mass :> ISQ::mass; attribute name : String; attribute nothing : String[0]; }
+		part def S {
+			part cs : C[*];
+			`+attributes+`
+		}
+	}`)
+	return m, sym(t, sym(t, root, "P").Scope, "S").Scope
+}
+
+// valueOf is the value expression of the attribute named in scope.
+func valueOf(t *testing.T, scope *symbols.Scope, name string) ast.Node {
+	t.Helper()
+	u, ok := sym(t, scope, name).Decl.(*ast.Usage)
+	if !ok || u.Value == nil {
+		t.Fatalf("%s: not a valued usage", name)
+	}
+	return u.Value
+}
+
+// typeNamesOf is the leaf names of ExprResultTypes of the attribute's value, and
+// checks ExprResultType agrees with its first.
+func typeNamesOf(t *testing.T, m *Model, scope *symbols.Scope, name string) []string {
+	t.Helper()
+	value := valueOf(t, scope, name)
+	types := m.ExprResultTypes(scope, value)
+	first := m.ExprResultType(scope, value)
+	if len(types) == 0 {
+		if first != nil {
+			t.Fatalf("%s: ExprResultType = %s, ExprResultTypes none", name, first.Name)
+		}
+		return nil
+	}
+	if first != types[0] {
+		t.Fatalf("%s: ExprResultType = %v, ExprResultTypes start with %v", name, first, types[0])
+	}
+	names := make([]string, 0, len(types))
+	for _, typ := range types {
+		names = append(names, leafName(typ.Name))
+	}
+	return names
+}
+
+func wantValueTypes(t *testing.T, m *Model, scope *symbols.Scope, name string, want ...string) {
+	t.Helper()
+	if got := typeNamesOf(t, m, scope, name); !slices.Equal(got, want) {
+		t.Errorf("%s: result types %v, want %v", name, got, want)
+	}
+}
+
+// wantResultRange checks the multiplicity of the result parameter of the function
+// the attribute's value calls, which the specialized type does not narrow.
+func wantResultRange(t *testing.T, m *Model, scope *symbols.Scope, name string, lower, upper int64, unbounded bool) {
+	t.Helper()
+	call, ok := valueOf(t, scope, name).(*ast.InvocationExpr)
+	if !ok {
+		t.Fatalf("%s: not an invocation", name)
+	}
+	r, ok := m.MultiplicityOf(m.invocationResult(scope, call))
+	if !ok {
+		t.Fatalf("%s: result parameter declares no multiplicity", name)
+	}
+	if !r.Lower.Known || r.Lower.Value != lower || !r.Upper.Known || r.Upper.Infinite != unbounded || (!unbounded && r.Upper.Value != upper) {
+		t.Errorf("%s: result multiplicity %+v, want [%d..%d] unbounded=%v", name, r, lower, upper, unbounded)
+	}
+}
+
+// collect results in what its body returns, in either notation, whatever the
+// element type; select, reject and selectOne keep the elements of the collection.
+func TestCollectionResultTypes(t *testing.T) {
+	m, s := collectionModel(t, `
+		attribute masses = cs->collect { in x : C; x.mass };
+		attribute masses2 = cs.{ in x : C; x.mass };
+		attribute names = cs->collect { in x : C; x.name };
+		attribute heavy = cs->select { in x : C; x.mass > 1 [kg] };
+		attribute heavy2 = cs.?{ in x : C; x.mass > 1 [kg] };
+		attribute light = cs->reject { in x : C; x.mass > 1 [kg] };
+		attribute one = cs->selectOne { in x : C; x.mass > 1 [kg] };
+		attribute all = cs->forAll { in x : C; x.mass > 1 [kg] };
+		attribute some = cs->exists { in x : C; x.mass > 1 [kg] };
+		attribute total = cs->collect { in x : C; x.mass }->reduce '+';
+		attribute total2 = cs->collect { in x : C; x.mass }->reduce { in a : MassValue; in b : MassValue; a };
+		attribute plain = cs.mass;`)
+	wantValueTypes(t, m, s, "masses", "MassValue")
+	wantValueTypes(t, m, s, "masses2", "MassValue")
+	wantValueTypes(t, m, s, "names", "String")
+	wantValueTypes(t, m, s, "heavy", "C")
+	wantValueTypes(t, m, s, "heavy2", "C")
+	wantValueTypes(t, m, s, "light", "C")
+	wantValueTypes(t, m, s, "one", "C")
+	wantValueTypes(t, m, s, "all", "Boolean")
+	wantValueTypes(t, m, s, "some", "Boolean")
+	wantValueTypes(t, m, s, "total", "ScalarValue")
+	wantValueTypes(t, m, s, "total2", "MassValue")
+	wantValueTypes(t, m, s, "plain", "MassValue")
+}
+
+// The result multiplicity is the one the library declares for each function: a
+// body returning one value per element still collects to `[0..*]`.
+func TestCollectionResultMultiplicity(t *testing.T) {
+	m, s := collectionModel(t, `
+		attribute masses = cs->collect { in x : C; x.mass };
+		attribute heavy = cs->select { in x : C; x.mass > 1 [kg] };
+		attribute light = cs->reject { in x : C; x.mass > 1 [kg] };
+		attribute one = cs->selectOne { in x : C; x.mass > 1 [kg] };
+		attribute all = cs->forAll { in x : C; x.mass > 1 [kg] };
+		attribute some = cs->exists { in x : C; x.mass > 1 [kg] };
+		attribute total = cs->collect { in x : C; x.mass }->reduce '+';`)
+	wantResultRange(t, m, s, "masses", 0, 0, true)
+	wantResultRange(t, m, s, "heavy", 0, 0, true)
+	wantResultRange(t, m, s, "light", 0, 0, true)
+	wantResultRange(t, m, s, "one", 0, 1, false)
+	wantResultRange(t, m, s, "all", 1, 1, false)
+	wantResultRange(t, m, s, "some", 1, 1, false)
+	wantResultRange(t, m, s, "total", 0, 0, true)
+}
+
+// A nested collect types the outer body by the inner result; a body returning a
+// sequence is typed by what every element conforms to — the nearest supertype the
+// elements share, Anything where an element is untyped.
+func TestCollectionNestedAndSequenceBodies(t *testing.T) {
+	m, s := collectionModel(t, `
+		attribute nested = cs->collect { in x : C; cs->collect { in y : C; y.name } };
+		attribute nested2 = cs.{ in x : C; cs.{ in y : C; y.mass } };
+		attribute pairs = cs->collect { in x : C; (x.mass, x.mass) };
+		attribute widened = cs->collect { in x : C; (1, 2.5) };
+		attribute mixed = cs->collect { in x : C; (x.mass, (x.name, x.mass)) };
+		attribute partly = cs->collect { in x; (x, 1) };
+		attribute chained = cs->collect { in x : C; x.name }->select { in n : String; n == "a" };`)
+	wantValueTypes(t, m, s, "nested", "String")
+	wantValueTypes(t, m, s, "nested2", "MassValue")
+	wantValueTypes(t, m, s, "pairs", "MassValue")
+	wantValueTypes(t, m, s, "widened", "Real")
+	wantValueTypes(t, m, s, "mixed", "ScalarValue")
+	wantValueTypes(t, m, s, "partly", "Anything")
+	wantValueTypes(t, m, s, "chained", "String")
+}
+
+// The arguments bind by the library's parameters in the prefix and named notations too.
+func TestCollectionArgumentNotations(t *testing.T) {
+	m, s := collectionModel(t, `
+		attribute masses = collect(cs, { in x : C; x.mass });
+		attribute named = collect(mapper = { in x : C; x.name }, collection = cs);
+		attribute heavy = select(collection = cs, selector = { in x : C; x.mass > 1 [kg] });
+		attribute fromFunction = cs->collect Mass;
+		calc def Mass { in c : C; return : MassValue = c.mass; }`)
+	wantValueTypes(t, m, s, "masses", "MassValue")
+	wantValueTypes(t, m, s, "named", "String")
+	wantValueTypes(t, m, s, "heavy", "C")
+	wantValueTypes(t, m, s, "fromFunction", "MassValue")
+}
+
+// A body whose result the model cannot type — its parameter declares no type, so
+// the member is unresolved — leaves the result the library's Anything, not a guess.
+func TestCollectionUntypedBodyFallsBackToLibraryResult(t *testing.T) {
+	m, s := collectionModel(t, `
+		attribute unknown = cs->collect { in x; x.mass };
+		attribute unknown2 = cs.{ in x; x.mass };
+		attribute body = cs->collect { in x : C; { in y; y } };`)
+	wantValueTypes(t, m, s, "unknown", "Anything")
+	wantValueTypes(t, m, s, "unknown2", "Anything")
+	wantValueTypes(t, m, s, "body", "Evaluation")
+}
+
+// A body that names the feature it values leads the typer back to itself; typing terminates.
+func TestCollectionSelfReferentialBodyTerminates(t *testing.T) {
+	m, s := collectionModel(t, `
+		attribute total :> ISQ::mass = cs->collect { in x : C; total }->reduce '+';
+		attribute loop = cs->collect { in x : C; loop };
+		attribute loop2 = cs.{ in x : C; loop2 };
+		attribute kept = cs->select { in x : C; kept == x };`)
+	wantValueTypes(t, m, s, "total", "ScalarValue")
+	wantValueTypes(t, m, s, "loop", "Anything")
+	wantValueTypes(t, m, s, "loop2", "Anything")
+	wantValueTypes(t, m, s, "kept", "C")
+}
+
+// Conformance judges the specialized result: a collect of masses is a MassValue and
+// no String; a select keeps C, no ScalarValue; an untyped body stays untyped. A body
+// returning a sequence conforms when every element does, fails naming an element
+// known not to, and stays the untyped Anything while an element is untyped and none fails.
+func TestCollectionResultConformance(t *testing.T) {
+	m, s := collectionModel(t, `
+		attribute masses = cs->collect { in x : C; x.mass };
+		attribute masses2 = cs.{ in x : C; x.mass };
+		attribute heavy = cs->select { in x : C; x.mass > 1 [kg] };
+		attribute unknown = cs.{ in x; x.mass };
+		attribute pairs = cs->collect { in x : C; (x.mass, x.mass) };
+		attribute mixed = cs.{ in x : C; (true, 1) };
+		attribute partly = cs.{ in x; (x, 1) };
+		attribute partly2 = cs->collect { in x; (x, 1) };`)
+	for name, want := range map[string]string{"pairs": "ISQ::MassValue", "mixed": "Base::Anything"} {
+		if c := m.ExprConformsToLibrary(s, valueOf(t, s, name), want); !c.Known || !c.Holds {
+			t.Errorf("%s as %s: %+v, want it to hold", name, want, c)
+		}
+	}
+	if c := m.ExprConformsToLibrary(s, valueOf(t, s, "pairs"), fqnString); !c.Known || c.Holds || c.Untyped || c.Found != "MassValue" {
+		t.Errorf("pairs as String: %+v, want known, not holding, found MassValue", c)
+	}
+	for _, want := range []string{FQNBoolean, fqnInteger} {
+		if c := m.ExprConformsToLibrary(s, valueOf(t, s, "mixed"), want); !c.Known || c.Holds || c.Untyped || c.Found == "" {
+			t.Errorf("mixed as %s: %+v, want known, not holding, naming the element", want, c)
+		}
+	}
+	if c := m.ExprConformsToLibrary(s, valueOf(t, s, "partly"), fqnInteger); !c.Known || c.Holds || !c.Untyped || !strings.Contains(c.Found, "Anything") {
+		t.Errorf("partly as Integer: %+v, want untyped Anything", c)
+	}
+	for _, name := range []string{"partly", "partly2"} {
+		if c := m.ExprConformsToLibrary(s, valueOf(t, s, name), FQNBoolean); !c.Known || c.Holds || c.Untyped || c.Found != "Natural" {
+			t.Errorf("%s as Boolean: %+v, want known, not holding, found Natural", name, c)
+		}
+	}
+	for _, name := range []string{"masses", "masses2"} {
+		c := m.ExprConformsToLibrary(s, valueOf(t, s, name), "ISQ::MassValue")
+		if !c.Known || !c.Holds {
+			t.Errorf("%s as MassValue: %+v, want it to hold", name, c)
+		}
+		c = m.ExprConformsToLibrary(s, valueOf(t, s, name), fqnString)
+		if !c.Known || c.Holds || c.Untyped || c.Found != "MassValue" {
+			t.Errorf("%s as String: %+v, want known, not holding, found MassValue", name, c)
+		}
+	}
+	c := m.ExprConformsToLibrary(s, valueOf(t, s, "heavy"), "ScalarValues::ScalarValue")
+	if !c.Known || c.Holds || c.Found != "C" {
+		t.Errorf("heavy as ScalarValue: %+v, want known, not holding, found C", c)
+	}
+	c = m.ExprConformsToLibrary(s, valueOf(t, s, "unknown"), fqnString)
+	if !c.Known || c.Holds || !c.Untyped || !strings.Contains(c.Found, "Anything") {
+		t.Errorf("unknown as String: %+v, want untyped Anything", c)
+	}
+}
+
+// reduce returns what its reducer does, or the collection's one element unreduced, so
+// the result is what both conform to — the library's Anything where they share nothing —
+// unless the collection holds two or more: a declared `[2..*]`, one inherited by
+// redefinition, a chain through such a feature, or a sequence of two literals; a collection
+// holding one at most, `[1]` or `[0..1]`, is never reduced, so its element alone is the result.
+func TestCollectionReduceMayReturnTheElement(t *testing.T) {
+	m, s := collectionModel(t, `
+		part two : C[2..*];
+		part one : C[1];
+		part atMost : C[0..1];
+		part def Pair { part items : C[2]; part item : C[1]; }
+		part def Pairs :> Pair { part :>> items; part :>> item; }
+		part pair : Pairs[1];
+		part pairs : Pairs[*];
+		part couple : Pairs[2];
+		attribute names = cs->reduce { in a : C; in b : C; a.name };
+		attribute names1 = one->reduce { in a : C; in b : C; a.name };
+		attribute names01 = atMost->reduce { in a : C; in b : C; a.name };
+		attribute names1lit = (one)->reduce { in a : C; in b : C; "s" };
+		attribute names2 = two->reduce { in a : C; in b : C; a.name };
+		attribute inherited = pair.items->reduce { in a : C; in b : C; a.name };
+		attribute chained = couple.item->reduce { in a : C; in b : C; a.name };
+		attribute chained1 = pair.item->reduce { in a : C; in b : C; a.name };
+		attribute chainedAny = pairs.items->reduce { in a : C; in b : C; a.name };
+		attribute lits = (1, 2)->reduce { in a : Integer; in b : Integer; "s" };
+		attribute same = cs->reduce { in a : C; in b : C; a };
+		attribute cast = cs->reduce { in a : C; in b : C; a.name } as String;
+		attribute cast2 = two->reduce { in a : C; in b : C; a.name } as C;
+		attribute cast1 = one->reduce { in a : C; in b : C; a.name } as String;`)
+	wantValueTypes(t, m, s, "names", "Anything")
+	wantValueTypes(t, m, s, "names1", "C")
+	wantValueTypes(t, m, s, "names01", "C")
+	wantValueTypes(t, m, s, "names1lit", "C")
+	wantValueTypes(t, m, s, "names2", "String")
+	wantValueTypes(t, m, s, "inherited", "String")
+	wantValueTypes(t, m, s, "chained", "String")
+	wantValueTypes(t, m, s, "chained1", "C")
+	wantValueTypes(t, m, s, "chainedAny", "Anything")
+	wantValueTypes(t, m, s, "lits", "String")
+	wantValueTypes(t, m, s, "same", "C")
+	elements, ok := m.CollectionElements(s, valueOf(t, s, "names"))
+	if !ok || len(elements) != 2 || len(elements[0].Types) != 1 || len(elements[1].Types) != 1 ||
+		leafName(elements[0].Types[0].Name) != "String" || leafName(elements[1].Types[0].Name) != "C" ||
+		elements[0].Node == nil || elements[1].Node == nil {
+		t.Errorf("names: elements %v, want the reducer's String then the collection's C", elements)
+	}
+	for _, name := range []string{"names", "names1", "names01"} {
+		if c := m.ExprConformsToLibrary(s, valueOf(t, s, name), fqnString); !c.Known || c.Holds || c.Untyped || c.Found != "C" {
+			t.Errorf("%s as String: %+v, want known, not holding, found C", name, c)
+		}
+	}
+	for _, name := range []string{"names1", "names01"} {
+		elements, ok := m.CollectionElements(s, valueOf(t, s, name))
+		if !ok || len(elements) != 1 || len(elements[0].Types) != 1 || leafName(elements[0].Types[0].Name) != "C" {
+			t.Errorf("%s: elements %v, want the collection's C alone", name, elements)
+		}
+	}
+	if c := m.ExprConformsToLibrary(s, valueOf(t, s, "names2"), fqnString); !c.Known || !c.Holds {
+		t.Errorf("names2 as String: %+v, want it to hold", c)
+	}
+	if c := m.CastConformance(s, valueOf(t, s, "cast").(*ast.OperatorExpr)); !c.Known || !c.Holds {
+		t.Errorf("cast to String: %+v, want it to hold, the element may be one", c)
+	}
+	if c := m.CastConformance(s, valueOf(t, s, "cast2").(*ast.OperatorExpr)); !c.Known || c.Holds || c.Found != "String" {
+		t.Errorf("cast of two to C: %+v, want known, not holding, found String", c)
+	}
+	if c := m.CastConformance(s, valueOf(t, s, "cast1").(*ast.OperatorExpr)); !c.Known || c.Holds || c.Found != "C" {
+		t.Errorf("cast of one to String: %+v, want known, not holding, found C", c)
+	}
+}
+
+// Over a collection known to hold nothing — or mapping each element to nothing — reduce is typed
+// by the reducer alone and collect by its body; but no element is held, judged or refused a cast.
+func TestCollectionReduceOfNothing(t *testing.T) {
+	m, s := collectionModel(t, `
+		part none : C[0];
+		part one : C[1];
+		part def Holder { part item : C[1]; }
+		part holders : Holder[0..0];
+		attribute empty = ()->reduce { in a : Integer; in b : Integer; "s" };
+		attribute empty2 = none->reduce { in a : C; in b : C; a.name };
+		attribute empty3 = holders.item->reduce { in a : C; in b : C; a.name };
+		attribute emptyCollect = ()->collect { in a : Integer; "s" };
+		attribute emptyCollect2 = none.{ in a : C; a.name };
+		attribute emptyCollect3 = holders.item->collect { in a : C; a.name };
+		attribute emptyBody = cs.{ in x : C; x.nothing };
+		attribute emptyBody2 = cs->collect { in x : C; (x.nothing, x.nothing) };
+		attribute emptyNested = (().{ in a : Integer; a }).{ in b : Integer; "s" };
+		attribute emptyNested2 = (none->select { in a : C; true })->reduce { in a : C; in b : C; "s" };
+		attribute emptyNested3 = (cs.{ in x : C; x.nothing }).?{ in s : String; true };
+		attribute emptyNested4 = (cs->selectOne { in x : C; true }).{ in x : C; x.nothing }->collect { in s : String; s };
+		attribute cast = none->reduce { in a : C; in b : C; a.name } as Integer;
+		attribute cast2 = cs.{ in x : C; x.nothing } as Integer;
+		attribute two = (none, one, one)->reduce { in a : C; in b : C; a.name };
+		attribute maybe = (none, one)->reduce { in a : C; in b : C; a.name };`)
+	for _, name := range []string{"empty", "empty2", "empty3", "emptyCollect", "emptyCollect2", "emptyCollect3",
+		"emptyBody", "emptyBody2", "emptyNested", "emptyNested2", "emptyNested3", "emptyNested4"} {
+		wantValueTypes(t, m, s, name, "String")
+		elements, ok := m.CollectionElements(s, valueOf(t, s, name))
+		if !ok || len(elements) != 0 {
+			t.Errorf("%s: elements %v, want none", name, elements)
+		}
+		if types, ok := m.CollectionHeldTypes(s, valueOf(t, s, name)); !ok || len(types) != 0 {
+			t.Errorf("%s: held types %v, want none", name, types)
+		}
+		for _, want := range []string{fqnString, fqnInteger} {
+			if c := m.ExprConformsToLibrary(s, valueOf(t, s, name), want); c.Known && !c.Untyped {
+				t.Errorf("%s as %s: %+v, want nothing decided", name, want, c)
+			}
+		}
+	}
+	for _, name := range []string{"cast", "cast2"} {
+		if c := m.CastConformance(s, valueOf(t, s, name).(*ast.OperatorExpr)); c.Known && !c.Holds {
+			t.Errorf("%s of nothing to Integer: %+v, want it not to fail", name, c)
+		}
+	}
+	wantValueTypes(t, m, s, "two", "String")
+	wantValueTypes(t, m, s, "maybe", "C")
+	if types, ok := m.CollectionHeldTypes(s, valueOf(t, s, "two")); !ok || len(types) != 1 || leafName(types[0].Name) != "String" {
+		t.Errorf("two: held types %v, want String", types)
+	}
+}
+
+// How many values a feature or a mapper's result holds is read through an alias and, where
+// it declares no multiplicity, from the feature it redefines by clause or by position.
+func TestCollectionSizeThroughAliasAndRedefinition(t *testing.T) {
+	m, s := collectionModel(t, `
+		part none : C[0];
+		part two : C[2];
+		alias nobody for none;
+		alias pair for two;
+		function Nobody { in c : C; return r : C[0]; }
+		function Nobody2 :> Nobody { in c : C; return r :>> r; }
+		function Nobody3 :> Nobody { in c : C; return r : C; }
+		function Named { in c : C; return r : String; }
+		attribute viaAlias = nobody.{ in c : C; c.name };
+		attribute viaAlias2 = pair->reduce { in a : C; in b : C; a.name };
+		attribute inherited = cs->collect Nobody2;
+		attribute inherited2 = (cs->collect Nobody2)->reduce { in a : C; in b : C; a.name };
+		attribute implicit = cs->collect Nobody3;
+		attribute implicit2 = (cs->collect Nobody3)->reduce { in a : C; in b : C; a.name };
+		attribute named = cs->collect Named;`)
+	for _, name := range []string{"viaAlias", "inherited2", "implicit2"} {
+		wantValueTypes(t, m, s, name, "String")
+		if elements, ok := m.CollectionElements(s, valueOf(t, s, name)); !ok || len(elements) != 0 {
+			t.Errorf("%s: elements %v, want none", name, elements)
+		}
+	}
+	wantValueTypes(t, m, s, "viaAlias2", "String")
+	if elements, ok := m.CollectionElements(s, valueOf(t, s, "viaAlias2")); !ok || len(elements) != 1 || leafName(elements[0].Types[0].Name) != "String" {
+		t.Errorf("viaAlias2: elements %v, want the reducer's String alone", elements)
+	}
+	for _, name := range []string{"inherited", "implicit"} {
+		wantValueTypes(t, m, s, name, "C")
+		if elements, ok := m.CollectionElements(s, valueOf(t, s, name)); !ok || len(elements) != 0 {
+			t.Errorf("%s: elements %v, want none", name, elements)
+		}
+	}
+	if elements, ok := m.CollectionElements(s, valueOf(t, s, "named")); !ok || len(elements) != 1 {
+		t.Errorf("named: elements %v, want the result parameter", elements)
+	}
+}
+
+// CollectionValues sizes a collection value alone — an operation over a known collection — and
+// says nothing of a literal or a feature, whose sizes are read elsewhere. A reduce yields the one
+// element it holds unreduced, or what its reducer yields over two or more, or either.
+func TestCollectionValues(t *testing.T) {
+	m, s := collectionModel(t, `
+		part none : C[0];
+		part one : C[1];
+		part maybe : C[0..1];
+		part two : C[2];
+		function Pair { in a : C; in b : C; return r : C[2]; }
+		attribute mapped = two.{ in c : C; (c.name, c.name) };
+		attribute reduced = two->reduce { in a : C; in b : C; a.name };
+		attribute reducedTwo = two->reduce { in a : C; in b : C; (a, b) };
+		attribute reducedNone = two->reduce { in a : C; in b : C; () };
+		attribute reducedNamed = two->reduce Pair;
+		attribute reducedOpen = two->reduce { in a : C; in b : C; a.name + b.name };
+		attribute reducedOne = one->reduce { in a : C; in b : C; (a, b) };
+		attribute reducedMaybe = maybe->reduce { in a : C; in b : C; (a, b) };
+		attribute reducedAny = cs->reduce { in a : C; in b : C; (a, b) };
+		attribute reducedEmpty = none->reduce { in a : C; in b : C; (a, b) };
+		attribute nothing = none->select { in c : C; true };
+		attribute atMost = two->selectOne { in c : C; true };
+		attribute open = cs.{ in c : C; c.name };
+		attribute literal = (1, 2);
+		attribute named = two;`)
+	for name, want := range map[string]string{
+		"mapped": "[4]", "reduced": "[1]", "nothing": "[0]", "atMost": "[0..1]", "open": "[0..*]",
+		"reducedTwo": "[2]", "reducedNone": "[0]", "reducedNamed": "[2]", "reducedOpen": "[0..*]",
+		"reducedOne": "[1]", "reducedMaybe": "[0..1]", "reducedAny": "[0..2]", "reducedEmpty": "[0]",
+	} {
+		r, ok := m.CollectionValues(s, valueOf(t, s, name))
+		if !ok || r.Text() != want {
+			t.Errorf("%s: %s %v, want %s", name, r.Text(), ok, want)
+		}
+	}
+	for _, name := range []string{"literal", "named"} {
+		if _, ok := m.CollectionValues(s, valueOf(t, s, name)); ok {
+			t.Errorf("%s: sized as a collection value", name)
+		}
+	}
+	if n, ok := CountRange(3).Exactly(); !ok || n != 3 {
+		t.Errorf("[3] exactly %d %v, want 3", n, ok)
+	}
+	atLeastOne := Range{Lower: Bound{Value: 1, Known: true}, Upper: unbounded}
+	if _, ok := atLeastOne.Exactly(); ok {
+		t.Error("[1..*] is exact")
+	}
+	if sum := CountRange(math.MaxInt64).Plus(CountRange(1)); !sum.Lower.Infinite || !sum.Upper.Infinite {
+		t.Errorf("[%d] + [1] is %s, want [*..*]", int64(math.MaxInt64), sum.Text())
+	}
+	one := CountRange(1)
+	for _, c := range []struct{ held, want string }{
+		{"[2]", "2 value(s) bound to a feature with multiplicity upper bound 1"},
+		{"[0]", "0 value(s) bound to a feature with multiplicity lower bound 1"},
+		{"[2..*]", "at least 2 value(s) bound to a feature with multiplicity upper bound 1"},
+		{"[*..*]", "more than 9223372036854775807 value(s) bound to a feature with multiplicity upper bound 1"},
+		{"[0..*]", ""},
+		{"[0..1]", ""},
+	} {
+		held := map[string]Range{
+			"[2]": CountRange(2), "[0]": CountRange(0), "[0..1]": {Lower: CountRange(0).Lower, Upper: one.Upper},
+			"[2..*]": {Lower: CountRange(2).Lower, Upper: unbounded}, "[*..*]": {Lower: unbounded, Upper: unbounded},
+			"[0..*]": {Lower: CountRange(0).Lower, Upper: unbounded},
+		}[c.held]
+		if got := one.HeldViolation(held); got != c.want {
+			t.Errorf("%s held by [1]: %q, want %q", c.held, got, c.want)
+		}
+	}
+	if got := CountRange(3).HeldViolation(Range{Lower: CountRange(0).Lower, Upper: CountRange(2).Upper}); got != "at most 2 value(s) bound to a feature with multiplicity lower bound 3" {
+		t.Errorf("[0..2] held by [3]: %q", got)
+	}
+}
+
+// `xs.?{…}` is select written out: its elements are the collection's, so a binding or an
+// argument is judged by them as `xs->select {…}` is, and a sequence written out is typed by
+// what its elements share rather than the Anything the sequence itself is.
+func TestCollectionSelectShorthandElements(t *testing.T) {
+	m, s := collectionModel(t, `
+		part c1 : C;
+		part c2 : C;
+		attribute heavy = cs.?{ in x : C; x.mass > 1 [kg] };
+		attribute heavy2 = cs->select { in x : C; x.mass > 1 [kg] };
+		attribute picked = (c1, c2).?{ in x : C; true };
+		attribute picked2 = (c1, c2)->select { in x : C; true };
+		attribute mixed = (c1, "s").?{ in x; true };
+		attribute lits = (1, 2.5).?{ in x : Real; true };`)
+	for _, name := range []string{"heavy", "heavy2"} {
+		wantValueTypes(t, m, s, name, "C")
+		elements, ok := m.CollectionElements(s, valueOf(t, s, name))
+		if !ok || len(elements) != 1 || len(elements[0].Types) != 1 || leafName(elements[0].Types[0].Name) != "C" || elements[0].Node == nil {
+			t.Errorf("%s: elements %v, want the collection's C", name, elements)
+		}
+	}
+	for _, name := range []string{"picked", "picked2"} {
+		wantValueTypes(t, m, s, name, "C")
+	}
+	wantValueTypes(t, m, s, "mixed", "Anything")
+	wantValueTypes(t, m, s, "lits", "Real")
+	elements, ok := m.CollectionElements(s, valueOf(t, s, "lits"))
+	if !ok || len(elements) != 2 {
+		t.Fatalf("lits: elements %v, want one per literal", elements)
+	}
+	if _, isInt := elements[0].Node.(*ast.LiteralInteger); !isInt {
+		t.Errorf("lits: first element %T, want the literal 1", elements[0].Node)
+	}
+	if _, isReal := elements[1].Node.(*ast.LiteralReal); !isReal {
+		t.Errorf("lits: second element %T, want the literal 2.5", elements[1].Node)
+	}
+}
+
+// Elements of sibling types share their nearest common supertype, not Anything: a selection or
+// a body keeping a Truck and a Car is a collection of Vehicles; one keeping a Truck and a
+// String shares nothing worth saying.
+func TestCollectionSiblingElementsShareSupertype(t *testing.T) {
+	m, s := collectionModel(t, `
+		part def T :> C; part def U :> C; part def V :> U;
+		part t : T; part u : U; part v : V;
+		attribute kin = (t, u).?{ in x : C; true };
+		attribute kin2 = (t, u)->select { in x : C; true };
+		attribute kin3 = cs.{ in x : C; (t, v) };
+		attribute kin4 = (t, u, v)->reject { in x : C; false };
+		attribute line = (u, v).?{ in x : C; true };
+		attribute apart = (t, "s").?{ in x; true };`)
+	for _, name := range []string{"kin", "kin2", "kin3", "kin4"} {
+		wantValueTypes(t, m, s, name, "C")
+	}
+	wantValueTypes(t, m, s, "line", "U")
+	wantValueTypes(t, m, s, "apart", "Anything")
+}
+
+// A union conforms to whatever all its unioning types do, so elements typed by a union and by a
+// sibling share the unioning types' supertype whichever comes first, as do two such unions; a
+// union whose members share nothing with the sibling stays Anything.
+func TestCollectionUnionElementsShareSupertype(t *testing.T) {
+	m, s := collectionModel(t, `
+		part def T :> C; part def U :> C; part def V :> C;
+		classifier TU unions T, U;
+		classifier UV unions U, V;
+		classifier TS unions T, String;
+		part tu : TU; part uv : UV; part ts : TS; part v : V;
+		attribute unionFirst = (tu, v).?{ in x; true };
+		attribute unionLast = (v, tu).?{ in x; true };
+		attribute unions = (tu, uv)->select { in x; true };
+		attribute unions2 = cs.{ in x : C; (uv, tu) };
+		attribute apart = (ts, v).?{ in x; true };`)
+	for _, name := range []string{"unionFirst", "unionLast", "unions", "unions2"} {
+		wantValueTypes(t, m, s, name, "C")
+	}
+	wantValueTypes(t, m, s, "apart", "Anything")
+}
+
+// An element that is itself a collection value contributes the elements it holds: a nested
+// collect's literals, a selection's elements, none from one over nothing.
+func TestCollectionNestedElements(t *testing.T) {
+	m, s := collectionModel(t, `
+		attribute nested = cs.{ in x : C; cs.{ in y : C; 1.5 } };
+		attribute nested2 = cs->collect { in x : C; (x.name, cs->select { in y : C; true }) };
+		attribute selected = (cs.{ in x : C; 2 }).?{ in n : Integer; true };
+		attribute nestedEmpty = cs.{ in x : C; ().{ in y : Integer; 1.5 } };`)
+	wantValueTypes(t, m, s, "nested", "Real")
+	elements, ok := m.CollectionElements(s, valueOf(t, s, "nested"))
+	if !ok || len(elements) != 1 {
+		t.Fatalf("nested: elements %v, want the inner literal", elements)
+	}
+	if _, isReal := elements[0].Node.(*ast.LiteralReal); !isReal {
+		t.Errorf("nested: element %T, want the literal 1.5", elements[0].Node)
+	}
+	elements, ok = m.CollectionElements(s, valueOf(t, s, "nested2"))
+	if !ok || len(elements) != 2 {
+		t.Fatalf("nested2: elements %v, want the name and the selection's C", elements)
+	}
+	if _, isRef := elements[0].Node.(*ast.FeatureChainExpr); !isRef || len(elements[0].Types) != 1 || leafName(elements[0].Types[0].Name) != "String" {
+		t.Errorf("nested2: first element %T %v, want x.name : String", elements[0].Node, elements[0].Types)
+	}
+	if len(elements[1].Types) != 1 || leafName(elements[1].Types[0].Name) != "C" {
+		t.Errorf("nested2: second element %v, want the selection's C", elements[1].Types)
+	}
+	elements, ok = m.CollectionElements(s, valueOf(t, s, "selected"))
+	if !ok || len(elements) != 1 {
+		t.Fatalf("selected: elements %v, want the collected literal", elements)
+	}
+	if _, isInt := elements[0].Node.(*ast.LiteralInteger); !isInt {
+		t.Errorf("selected: element %T, want the literal 2", elements[0].Node)
+	}
+	wantValueTypes(t, m, s, "nestedEmpty", "Real")
+	if elements, ok := m.CollectionElements(s, valueOf(t, s, "nestedEmpty")); !ok || len(elements) != 0 {
+		t.Errorf("nestedEmpty: elements %v, want none", elements)
+	}
+}
+
+// A mapper named by function holds one value per element where its result declares no
+// multiplicity, as a feature does — not any number — while a result whose declared bound is not
+// evaluable holds an unknown number; a count past int64 exceeds every bound.
+func TestCollectionSizeThroughNamedMapperAndPastInt64(t *testing.T) {
+	m, s := collectionModel(t, `
+		part two : C[2];
+		attribute n : Positive;
+		function Named { in c : C; return r : String; }
+		function Unsure { in c : C; return r : String[n]; }
+		part def H { part many : C[9223372036854775807]; }
+		part hs : H[2];
+		part huge : C[9223372036854775807];
+		attribute named = (two->collect Named)->reduce { in a : String; in b : String; 1 };
+		attribute unsure = (two->collect Unsure)->reduce { in a : String; in b : String; 1 };
+		attribute sum = (huge, huge)->reduce { in a : C; in b : C; a.name };
+		attribute product = hs.many->reduce { in a : C; in b : C; a.name };`)
+	wantValueTypes(t, m, s, "named", "Integer")
+	if elements, ok := m.CollectionElements(s, valueOf(t, s, "named")); !ok || len(elements) != 1 || leafName(elements[0].Types[0].Name) != "Integer" {
+		t.Errorf("named: elements %v, want the reducer's Integer alone", elements)
+	}
+	wantValueTypes(t, m, s, "unsure", "ScalarValue")
+	if elements, ok := m.CollectionElements(s, valueOf(t, s, "unsure")); !ok || len(elements) != 2 {
+		t.Errorf("unsure: elements %v, want the reducer's Integer and the mapper's String", elements)
+	}
+	for _, name := range []string{"sum", "product"} {
+		wantValueTypes(t, m, s, name, "String")
+		if elements, ok := m.CollectionElements(s, valueOf(t, s, name)); !ok || len(elements) != 1 || leafName(elements[0].Types[0].Name) != "String" {
+			t.Errorf("%s: elements %v, want the reducer's String alone", name, elements)
+		}
+		collection := valueOf(t, s, name).(*ast.InvocationExpr).Operand
+		r, ok := m.valuesHeldBy(s, collection)
+		if !ok || !r.Lower.Known || !r.Lower.Infinite || !r.Upper.Known || !r.Upper.Infinite {
+			t.Errorf("%s: values held %s, want [*..*]", name, r.Text())
+		}
+	}
+}
+
+// A cast holds once any element it may hold specializes the target, whichever comes first: an
+// untyped element before an Integer leaves the Integer to decide; one beside a String leaves the
+// cast undecided, and none at all names every element refused.
+func TestCollectionCastDecidedByAnyElement(t *testing.T) {
+	holds := Conformance{Known: true, Holds: true}
+	if c := anyHolds([]Conformance{conformanceUnknown(), holds}); !c.Known || !c.Holds {
+		t.Errorf("unknown then holding: %+v, want it to hold", c)
+	}
+	if c := anyHolds([]Conformance{{Known: true, Found: "String"}, conformanceUnknown()}); c.Known {
+		t.Errorf("refused then unknown: %+v, want unknown", c)
+	}
+	if c := anyHolds([]Conformance{{Known: true, Found: "String"}, {Known: true, Found: "C"}}); !c.Known || c.Holds || c.Found != "String and C" {
+		t.Errorf("refused twice: %+v, want known, not holding, found String and C", c)
+	}
+	m, s := collectionModel(t, `
+		attribute loose;
+		attribute cast = cs.{ in x : C; (loose, 1) } as Integer;
+		attribute cast2 = cs.{ in x : C; (x.name, "s") } as Integer;`)
+	if c := m.CastConformance(s, valueOf(t, s, "cast").(*ast.OperatorExpr)); !c.Known || !c.Holds {
+		t.Errorf("cast to Integer: %+v, want it to hold by the literal 1", c)
+	}
+	if c := m.CastConformance(s, valueOf(t, s, "cast2").(*ast.OperatorExpr)); !c.Known || c.Holds || c.Found != "String" {
+		t.Errorf("cast2 to Integer: %+v, want known, not holding, found String", c)
+	}
+}
diff --git a/internal/core/semantics/multiplicity.go b/internal/core/semantics/multiplicity.go
index 2a3422d31..a6911e9af 100644
--- a/internal/core/semantics/multiplicity.go
+++ b/internal/core/semantics/multiplicity.go
@@ -2,6 +2,7 @@ package semantics
 
 import (
 	"fmt"
+	"math"
 	"strconv"
 
 	"github.com/Open-MBEE/OpenSysML/internal/core/ast"
@@ -195,6 +196,33 @@ func (r Range) CountViolation(count int64) string {
 	return ""
 }
 
+// HeldViolation is CountViolation for a value whose count is only bounded: reported where even
+// its fewest values exceed the upper bound, or its most fall short of the lower.
+func (r Range) HeldViolation(held Range) string {
+	if n, ok := held.Exactly(); ok {
+		return r.CountViolation(n)
+	}
+	if r.Upper.Known && !r.Upper.Infinite && held.Lower.Known && (held.Lower.Infinite || held.Lower.Value > r.Upper.Value) {
+		fewest := "at least " + held.Lower.Text()
+		if held.Lower.Infinite {
+			fewest = fmt.Sprintf("more than %d", int64(math.MaxInt64))
+		}
+		return fmt.Sprintf("%s value(s) bound to a feature with multiplicity upper bound %d", fewest, r.Upper.Value)
+	}
+	if r.Lower.Known && !r.Lower.Infinite && held.Upper.Known && !held.Upper.Infinite && held.Upper.Value < r.Lower.Value {
+		return fmt.Sprintf("at most %d value(s) bound to a feature with multiplicity lower bound %d", held.Upper.Value, r.Lower.Value)
+	}
+	return ""
+}
+
+// Exactly is the one count the range admits, ok where both bounds are that finite count.
+func (r Range) Exactly() (int64, bool) {
+	if !r.Lower.Known || !r.Upper.Known || r.Lower.Infinite || r.Upper.Infinite || r.Lower.Value != r.Upper.Value {
+		return 0, false
+	}
+	return r.Lower.Value, true
+}
+
 // HasBounds reports whether the range is exactly lower..upper — the spec's
 // multiplicityHasBounds (SysML v2 8.3.3.1). ok is false when a bound is not
 // evaluable, so callers can skip the check.
diff --git a/internal/core/semantics/operator_conformance.go b/internal/core/semantics/operator_conformance.go
index 7b8fe6aa7..3bb8303e0 100644
--- a/internal/core/semantics/operator_conformance.go
+++ b/internal/core/semantics/operator_conformance.go
@@ -19,7 +19,19 @@ func (m *Model) CastConformance(scope *symbols.Scope, e *ast.OperatorExpr) Confo
 	if target == nil {
 		return conformanceUnknown()
 	}
-	types := m.resultTypes(scope, e.Operands[0])
+	if c, ok := m.collectionCastConformance(scope, e.Operands[0], target); ok {
+		return c
+	}
+	return m.castConformance(scope, e.Operands[0], target)
+}
+
+// castConformance judges casting the value of node to target by the node's types.
+func (m *Model) castConformance(scope *symbols.Scope, node ast.Node, target *symbols.Symbol) Conformance {
+	return m.castTypesConformance(m.resultTypes(scope, node), target)
+}
+
+// castTypesConformance is sound when one of types and target specialize one another.
+func (m *Model) castTypesConformance(types []*symbols.Symbol, target *symbols.Symbol) Conformance {
 	if len(types) == 0 {
 		return conformanceUnknown()
 	}
@@ -56,15 +68,26 @@ func (m *Model) resultTypes(scope *symbols.Scope, node ast.Node) []*symbols.Symb
 		}
 		return m.featureResultTypes(sym)
 	case *ast.InvocationExpr:
-		if result := m.invocationResult(scope, n); result != nil {
+		called := m.invocationCallee(scope, n)
+		if types := m.collectionResultTypes(scope, n, called); len(types) > 0 {
+			return types
+		}
+		if result := m.ResultParameterOf(called); result != nil {
 			return m.featureResultTypes(result)
 		}
 		return nil
+	case *ast.CollectExpr:
+		if types := m.collectResultTypes(scope, n); len(types) > 0 {
+			return types
+		}
 	case *ast.IndexExpr:
 		if !n.Bracket {
 			return m.indexResultTypes(scope, n)
 		}
 	case *ast.SelectExpr:
+		if types := m.selectResultTypes(scope, n); len(types) > 0 {
+			return types
+		}
 		return m.resultTypes(scope, n.Operand)
 	}
 	if typ := m.ExprResultType(scope, node); typ != nil {
diff --git a/internal/core/semantics/valuetype.go b/internal/core/semantics/valuetype.go
index f278d66d3..5a8535e10 100644
--- a/internal/core/semantics/valuetype.go
+++ b/internal/core/semantics/valuetype.go
@@ -124,7 +124,7 @@ func (m *Model) exprConformance(scope *symbols.Scope, node ast.Node, want *symbo
 	case *ast.OperatorExpr:
 		return m.operatorConformance(scope, n, want, byUnit)
 	case *ast.InvocationExpr:
-		return m.invocationConformance(scope, n, want)
+		return m.invocationConformance(scope, n, want, byUnit)
 	case *ast.NullExpr:
 		// `null` evaluates to nothing, typed Anything (KerML nullEvaluations).
 		c := m.typeConformance(m.libSymbol(fqnAnything), want)
@@ -142,7 +142,10 @@ func (m *Model) exprConformance(scope *symbols.Scope, node ast.Node, want *symbo
 		}
 		return c
 	case *ast.CollectExpr:
-		// `xs.{…}` is the result of ControlFunctions::collect, typed Anything.
+		// `xs.{…}` is the result of ControlFunctions::collect: the body's results, else Anything.
+		if c, ok := m.collectionConformance(scope, n, want, byUnit); ok {
+			return c
+		}
 		c := m.typeConformance(m.libSymbol(fqnAnything), want)
 		if c.Known && !c.Holds {
 			c.Found = "a collection `.{…}` maps to, typed Anything"
@@ -151,6 +154,9 @@ func (m *Model) exprConformance(scope *symbols.Scope, node ast.Node, want *symbo
 		return c
 	case *ast.SelectExpr:
 		// `xs.?{…}` keeps elements of xs (KerML checkSelectExpressionResultSpecialization).
+		if c, ok := m.collectionConformance(scope, n, want, byUnit); ok {
+			return c
+		}
 		return m.exprConformance(scope, n.Operand, want, byUnit)
 	case *ast.BodyExpr:
 		c := m.typeConformance(m.bodyExprType(scope, n), want)
@@ -217,15 +223,28 @@ func (m *Model) ExprResultType(scope *symbols.Scope, node ast.Node) *symbols.Sym
 		return m.indexResultType(scope, n)
 	case *ast.SelectExpr:
 		// `xs.?{…}` keeps elements of xs (KerML checkSelectExpressionResultSpecialization).
+		if types := m.selectResultTypes(scope, n); len(types) > 0 {
+			return types[0]
+		}
 		return m.ExprResultType(scope, n.Operand)
-	case *ast.NullExpr, *ast.SequenceExpr, *ast.CollectExpr:
+	case *ast.CollectExpr:
+		// `xs.{…}` is the result of ControlFunctions::collect: the body's results, else Anything.
+		if types := m.collectResultTypes(scope, n); len(types) > 0 {
+			return types[0]
+		}
+		return m.libSymbol(fqnAnything)
+	case *ast.NullExpr, *ast.SequenceExpr:
 		return m.libSymbol(fqnAnything)
 	case *ast.BodyExpr:
 		return m.bodyExprType(scope, n)
 	case *ast.ConstructorExpr:
 		return m.namedType(scope, n.Type)
 	case *ast.InvocationExpr:
-		if result := m.invocationResult(scope, n); result != nil {
+		called := m.invocationCallee(scope, n)
+		if types := m.collectionResultTypes(scope, n, called); len(types) > 0 {
+			return types[0]
+		}
+		if result := m.ResultParameterOf(called); result != nil {
 			return m.featureResultType(result)
 		}
 	}
@@ -955,23 +974,33 @@ func (m *Model) incommensurableSum(scope *symbols.Scope, node ast.Node) (*ast.Op
 
 // invocationConformance judges an invocation's value by the declared type of the
 // result parameter of the overload it calls.
-func (m *Model) invocationConformance(scope *symbols.Scope, e *ast.InvocationExpr, want *symbols.Symbol) Conformance {
-	result := m.invocationResult(scope, e)
+func (m *Model) invocationConformance(scope *symbols.Scope, e *ast.InvocationExpr, want *symbols.Symbol, byUnit bool) Conformance {
+	called := m.invocationCallee(scope, e)
+	if c, ok := m.collectionConformance(scope, e, want, byUnit); ok {
+		return c
+	}
+	result := m.ResultParameterOf(called)
 	if result == nil {
 		return conformanceUnknown()
 	}
 	return m.featureConformance(result, want)
 }
 
-// invocationResult is the result parameter of the declaration e calls, as the
-// checker selects it; nil when the call is unresolved, ambiguous or fits none.
-func (m *Model) invocationResult(scope *symbols.Scope, e *ast.InvocationExpr) *symbols.Symbol {
+// invocationCallee is the declaration e calls, as the checker selects it; nil
+// when the call is unresolved, ambiguous or fits none.
+func (m *Model) invocationCallee(scope *symbols.Scope, e *ast.InvocationExpr) *symbols.Symbol {
 	if e.Type == nil || m.resolver == nil {
 		return nil
 	}
 	sym, ok := m.calledFunction(scope, e)
-	if !ok || sym == nil {
+	if !ok {
 		return nil
 	}
-	return m.ResultParameterOf(sym)
+	return sym
+}
+
+// invocationResult is the result parameter of the declaration e calls; nil when
+// the call is unresolved, ambiguous or fits none.
+func (m *Model) invocationResult(scope *symbols.Scope, e *ast.InvocationExpr) *symbols.Symbol {
+	return m.ResultParameterOf(m.invocationCallee(scope, e))
 }