fix(semantics): specialize collection body result types

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.

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:

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

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