Skip to content

Commit 5c377b9

Browse files
reid-spencerclaude
andcommitted
[1.13] Type-check put, return and require -- and give literals a type
Reid ruled these three in, corpus cost accepted. `put` and `return` already compared types, but only when BOTH sides resolved to a NAMED type: `valueType` yields None for a predefined one, so exactly the case a generator trips over was skipped in silence. The named comparison is KEPT -- it is the stricter rule and the right one where it applies, since RIDDL treats a declared alias as a distinct name rather than a transparent synonym -- and the TypeExpression check runs only where the named one could not, so the two cannot double-report. `require … with` was never type-checked at all: only presence, plus a prompt ascription. It is checked in `checkStatementScopes` rather than `validateStatement` because `valueTypeExpr` needs the in-scope lets and foreach elements, which only that walk carries. **The real find was that LITERALS had no type**, which I hit by instrumenting the require check and watching `valueTypeExpr` answer None for `"a string"`. That was not a gap in these three positions -- it was a gap in the shared helper, so every position built on it, constructor arguments included, silently skipped its most common argument shape. Literals are typed now; a NumericLiteral deliberately still is not, because `checkNumericLiteralConformance` already judges those with a better message. It found nine genuine type errors in our OWN fixtures -- a string into an Integer field in six suites, a string where a record or an entity reference was wanted in two more. Every one is fixed as a fixture defect, not worked around. One test asserted SILENCE for a string literal on the stated grounds that "a literal has no resolvable type expression here". That premise is now false, so the case now asserts the opposite and a NEW case covers the still-valid rule using a value that is genuinely undeterminable. Also corrects two mislabelled rule ids that this made visible. `checkAssignable`'s GENERIC arm -- any assignability failure -- carried `stmt-id-entity-mismatch`, telling an author their plain type error was a problem with entity identity. It is `value-type-mismatch` now, and the wrong-entity arm takes the name that describes it. `stmt-id-type-mismatch` is left with no producer and is RETIRED rather than deleted: it shipped in rc.25, so its code stays reserved and can never come back meaning something else. Corpus cost is two models, both true positives: reactive-bbq returns a String where an aggregate is declared, ToDoodles puts one where a record is. Tasks filed. Co-Authored-By: Claude Opus 5 <noreply@anthropic.com>
1 parent b05c541 commit 5c377b9

15 files changed

Lines changed: 252 additions & 32 deletions

File tree

BACKLOG.md

Lines changed: 12 additions & 3 deletions
Original file line numberDiff line numberDiff line change
@@ -1026,7 +1026,10 @@ Each was noticed while doing something else, checked against the code at the
10261026
`file:line` cited, and deliberately not fixed in the same commit. **The
10271027
verification is carried here so it is not repeated.**
10281028

1029-
- **[1.13]** **Type-check `put`, `return` and `require … with`.** Constructor
1029+
- ~~**[1.13]** **Type-check `put`, `return` and `require … with`.**~~**DONE 2026-08-26.**
1030+
Reid: type-check them, corpus cost accepted. Original entry follows.
1031+
1032+
**[1.13 — as filed]** Constructor
10301033
arguments gained type checking on 2026-08-25 and these three did not.
10311034
**Verified**: `checkAssignable` (`ValidationPass.scala:7473`) has exactly two
10321035
call sites — `:1853` (constructor arguments) and `:9011` — while `put` and
@@ -1036,7 +1039,10 @@ verification is carried here so it is not repeated.**
10361039
shape as the constructor gap, which riddl-generator found by emitting Java that
10371040
would not compile. Expect corpus cost, and measure it before ruling.
10381041

1039-
- **[1.14]** **`find -type <unknown>` silently matches nothing.** A typo in a type
1042+
- ~~**[1.14]** **`find -type <unknown>` silently matches nothing.**~~**DONE 2026-08-26**: a
1043+
typo is now a parameter error with close matches, exit 7. Original entry follows.
1044+
1045+
**[1.14 — as filed]** A typo in a type
10401046
name produces `0 matched` and exit 0, which is indistinguishable from a correct
10411047
query with no hits — the exact "confident answer computed over nothing" failure
10421048
`find` was built to end.
@@ -1048,7 +1054,10 @@ verification is carried here so it is not repeated.**
10481054
already flagged as a risk — so do that first, and put it beside the AST rather
10491055
than in the command.
10501056

1051-
- **[1.15]** **Decide whether `StatsPass.numPromptStatements` is renamed.** The
1057+
- ~~**[1.15]** **Decide whether `StatsPass.numPromptStatements` is renamed.**~~**RULED
1058+
2026-08-26**: add `numDoStatements`, deprecate the old name. Done. Original entry follows.
1059+
1060+
**[1.15 — as filed]** The
10521061
`PromptStatement``DoStatement` rename (`e226f240e`) deliberately stopped at
10531062
this field.
10541063
**Verified**: it survives at five sites in

language/input/dokn.riddl

Lines changed: 1 addition & 1 deletion
Original file line numberDiff line numberDiff line change
@@ -214,7 +214,7 @@ domain dokn is {
214214
reply result Location.LocationDetails
215215
}
216216
on query Location.getLocationNotes {
217-
reply result Location.LocationNotes(notes = "the notes")
217+
reply result Location.LocationNotes(notes = prompt("the notes for this location"))
218218
}
219219
}
220220
} with {

language/input/everything_full.riddl

Lines changed: 2 additions & 2 deletions
Original file line numberDiff line numberDiff line change
@@ -61,7 +61,7 @@ context full is {
6161
adaptor fromAPlant to context APlant is {
6262
handler adaptCommands is {
6363
on command ACommand {
64-
send command DoAThing(thingField = "the thing") to outlet APlant.Source.OutCommands
64+
send command DoAThing(thingField = 42) to outlet APlant.Source.OutCommands
6565
}
6666
on other { error "unexpected message" }
6767
}
@@ -90,7 +90,7 @@ context full is {
9090
// APlant.Source.OutCommands is declared `type DoAThing`, so only a DoAThing may be
9191
// placed on it. This used to send `event Inebriated`, which nothing rejected until the
9292
// send/portlet conformance check landed (2026-08-19).
93-
send command DoAThing(thingField = "another thing") to outlet APlant.Source.OutCommands
93+
send command DoAThing(thingField = 43) to outlet APlant.Source.OutCommands
9494
end
9595
}
9696
}

language/src/main/scala/com/ossuminc/riddl/language/RuleId.scala

Lines changed: 7 additions & 2 deletions
Original file line numberDiff line numberDiff line change
@@ -381,7 +381,6 @@ enum RuleId(
381381
case ClauseWrongArity extends RuleId("handler-clause-wrong-arity")
382382
case NotInstantiable extends RuleId("stmt-not-instantiable")
383383
case TerminateNeedsId extends RuleId("stmt-terminate-needs-id")
384-
case IdTypeMismatch extends RuleId("stmt-id-type-mismatch")
385384
case IdEntityMismatch extends RuleId("stmt-id-entity-mismatch")
386385
case TellValueNeedsId extends RuleId("stmt-tell-value-needs-id")
387386
case TellCrossesDomain extends RuleId("stmt-tell-crosses-domain")
@@ -527,7 +526,13 @@ object RuleId:
527526
*
528527
* Empty today because no rule has yet been withdrawn.
529528
*/
530-
val retired: Set[String] = Set.empty
529+
val retired: Set[String] = Set(
530+
// Published in 2.0.0-rc.25 on `checkAssignable`'s wrong-entity arm, which now answers to
531+
// `stmt-id-entity-mismatch` -- the name that says what it means. Retired rather than reused:
532+
// a consumer suppressing it, or keying a migration on it, must not have it silently come back
533+
// attached to a different rule.
534+
"stmt-id-type-mismatch"
535+
)
531536

532537
/** The closed set of subject prefixes -- the kind of thing a rule is ABOUT.
533538
*

passes/src/main/scala/com/ossuminc/riddl/passes/validate/ValidationPass.scala

Lines changed: 84 additions & 2 deletions
Original file line numberDiff line numberDiff line change
@@ -2396,6 +2396,37 @@ case class ValidationPass(
23962396
* predicate with nothing to read, and a superfluous one reads as if it were being checked when
23972397
* the invariant never looks at it.
23982398
*/
2399+
/** [1.13]: does the `with` value have the type the invariant `requires`?
2400+
*
2401+
* Separate from [[checkRequireArgument]], which answers a different question -- is a value
2402+
* PRESENT when one is required -- and runs where the `let` scope is not available.
2403+
*
2404+
* A `PromptValue` is skipped: `checkRequireArgument` already checks its ascription against the
2405+
* same `requires` type, and reporting both would double up on one mistake. So is an
2406+
* undeterminable value type: `valueTypeExpr` returning None means this check has nothing to say,
2407+
* which is the same conservative rule the constructor-argument check follows.
2408+
*/
2409+
private def checkRequireArgumentType(
2410+
rs: RequireStatement,
2411+
parents: Parents,
2412+
lets: Seq[LetStatement],
2413+
elements: Map[String, TypeExpression]
2414+
): Unit =
2415+
for
2416+
ir <- rs.condition match
2417+
case ir: InvariantRef => Some(ir)
2418+
case _ => None
2419+
inv <- resolution.refMap.definitionOf[Invariant](ir.pathId)
2420+
tr <- inv.requires match
2421+
case Some(tr: TypeRef) => Some(tr)
2422+
case _ => None
2423+
expected <- resolution.refMap.definitionOf[Type](tr.pathId).map(_.typEx)
2424+
arg <- rs.argument
2425+
if !arg.isInstanceOf[PromptValue]
2426+
actual <- valueTypeExpr(arg, parents, lets, elements)
2427+
do checkAssignable(expected, actual, None, parents, arg.loc, s"${inv.identify} requires")
2428+
end checkRequireArgumentType
2429+
23992430
private def checkRequireArgument(inv: Invariant, argument: Option[Value], loc: At): Unit =
24002431
inv.requires match
24012432
case Some(tr: TypeRef) if argument.isEmpty =>
@@ -7746,7 +7777,7 @@ case class ValidationPass(
77467777
s"'$adPath' is not an id of '$edPath'",
77477778
suggestion = s"Supply an id obtained from '$edPath' -- an id value identifies one " +
77487779
"instance of one processor and cannot stand in for another's.",
7749-
ruleId = Some(RuleId.IdTypeMismatch)
7780+
ruleId = Some(RuleId.IdEntityMismatch)
77507781
)
77517782
case _ =>
77527783
if !e.isAssignmentCompatible(a) then
@@ -7755,7 +7786,14 @@ case class ValidationPass(
77557786
s"$what is declared '${e.format}' but the value is '${a.format}'",
77567787
suggestion = s"Supply a value of type '${e.format}', or declare the field as " +
77577788
s"'${a.format}'.",
7758-
ruleId = Some(RuleId.IdEntityMismatch)
7789+
// `value-type-mismatch`, NOT an id rule. This arm is ANY assignability failure -- a
7790+
// String where a record is wanted, say -- and it carried `stmt-id-entity-mismatch`
7791+
// until 2026-08-26, which told an author their plain type error was a problem with
7792+
// entity identity. The mislabel was invisible while the check ran only on constructor
7793+
// arguments whose failures happened to be Id-vs-UUID; extending it to `put`/`return`/
7794+
// `require` made it visible immediately. **A wrong id is worse than no id**: it is
7795+
// exactly what a consumer filters and suppresses on.
7796+
ruleId = Some(RuleId.ValueTypeMismatch)
77597797
)
77607798
end checkAssignable
77617799

@@ -8410,6 +8448,18 @@ case class ValidationPass(
84108448
// `let e = empty T*` infers `T*` -- the ascription IS the type, which is the whole point of
84118449
// the ascribed form. A bare `empty` has no type of its own; the position supplies it.
84128450
case ev: EmptyValue => ev.typeEx
8451+
// [1.13]: a LITERAL denotes its own type, and until 2026-08-26 none of them did -- so every
8452+
// position built on this helper (constructor arguments, `put`, `return`, `require … with`)
8453+
// silently skipped an argument written as a literal. `require inv with "text"` where the
8454+
// invariant requires an Integer said nothing at all. Found by instrumenting the require
8455+
// check and watching `valueTypeExpr` answer None, not by reading it.
8456+
//
8457+
// A NumericLiteral deliberately gets NO arm: `checkNumericLiteralConformance` already judges
8458+
// a numeric literal against the expected type, and with a better message ("Natural is a
8459+
// positive whole number") than a bare assignability failure. Two checks on one mistake is
8460+
// the double-reporting this codebase keeps recording.
8461+
case _: LiteralString => Some(String_(v.loc))
8462+
case _: BooleanLiteral => Some(Bool(v.loc))
84138463
case vr: ValueRef => valueRefTypeExpr(vr, parents, lets, elements)
84148464
// A55/`self`: the SYNTHESIZED Aggregation is the only place `self`'s type is materialized.
84158465
// `let me = self` then `me.id` reaches this ARM through `valueRefTypeExpr`'s
@@ -9465,6 +9515,19 @@ case class ValidationPass(
94659515
ruleId = Some(RuleId.PutTypeMismatch)
94669516
)
94679517
case _ => ()
9518+
// [1.13]: the comparison above runs only when BOTH sides resolve to a NAMED type -- which is
9519+
// the stricter rule and the right one there, since RIDDL treats a declared alias as a distinct
9520+
// name rather than a transparent synonym. But `valueType` yields None for a PREDEFINED type,
9521+
// so `putting` a `String` where an `Id(E)` was wanted said nothing at all. Fall back to the
9522+
// TypeExpression level, which is what the constructor-argument check uses, and only when the
9523+
// named comparison could not run -- so the two can never double-report one mistake.
9524+
if expected.isEmpty || actual.isEmpty then
9525+
for
9526+
e <- output.putOut match
9527+
case tr: TypeRef => resolution.refMap.definitionOf[Type](tr.pathId).map(_.typEx)
9528+
case _ => None
9529+
a <- valueTypeExpr(ps.value, parents, lets, elements)
9530+
do checkAssignable(e, a, None, parents, ps.loc, "'put' value")
94689531
}
94699532
end validatePut
94709533

@@ -9497,6 +9560,19 @@ case class ValidationPass(
94979560
ruleId = Some(RuleId.ReturnTypeMismatch)
94989561
)
94999562
case _ => ()
9563+
// [1.13]: the comparison above runs only when BOTH sides resolve to a NAMED type -- which is
9564+
// the stricter rule and the right one there, since RIDDL treats a declared alias as a distinct
9565+
// name rather than a transparent synonym. But `valueType` yields None for a PREDEFINED type,
9566+
// so `returning` a `String` where an `Id(E)` was wanted said nothing at all. Fall back to the
9567+
// TypeExpression level, which is what the constructor-argument check uses, and only when the
9568+
// named comparison could not run -- so the two can never double-report one mistake.
9569+
if expected.isEmpty || actual.isEmpty then
9570+
for
9571+
e <- fn.output match
9572+
case Some(tr: TypeRef) => resolution.refMap.definitionOf[Type](tr.pathId).map(_.typEx)
9573+
case _ => None
9574+
a <- valueTypeExpr(rs.value, parents, lets, elements)
9575+
do checkAssignable(e, a, None, parents, rs.loc, "'return' value")
95009576
}
95019577
end validateReturn
95029578

@@ -9800,6 +9876,12 @@ case class ValidationPass(
98009876
rs.condition match
98019877
case be: BooleanExpression => validateValue(be, parents, lets, elements)
98029878
case _ => ()
9879+
// [1.13]: the `with` value is type-checked against what the invariant `requires`. Until
9880+
// now only its PRESENCE was checked (`checkRequireArgument`) plus a `prompt` ascription,
9881+
// so `require inv with someId` supplied an `Id(E)` where a `UUID` was wanted and nothing
9882+
// said so. Checked HERE rather than in `validateStatement` because `valueTypeExpr` needs
9883+
// the in-scope `let`s and `foreach` elements, which only this walk carries.
9884+
checkRequireArgumentType(rs, parents, lets, elements)
98039885
case ms: MatchStatement =>
98049886
validateMatch(
98059887
ms,

passes/src/test/scala-jvm-native/com/ossuminc/riddl/passes/validate/AskTest.scala

Lines changed: 1 addition & 1 deletion
Original file line numberDiff line numberDiff line change
@@ -61,7 +61,7 @@ class AskTest extends AbstractValidatingTest {
6161
| entity Ledger is {
6262
| state S of record D.C.R is {
6363
| handler H is {
64-
| on query D.C.Ask is { reply result D.C.Answer(v = "the answer") }
64+
| on query D.C.Ask is { reply result D.C.Answer(v = 1) }
6565
| } with { briefly "h" }
6666
| } with { briefly "st" }
6767
| } with { briefly "en" }

passes/src/test/scala-jvm-native/com/ossuminc/riddl/passes/validate/BoundMessageOperandValidationTest.scala

Lines changed: 1 addition & 1 deletion
Original file line numberDiff line numberDiff line change
@@ -78,7 +78,7 @@ class BoundMessageOperandValidationTest extends AbstractValidatingTest {
7878

7979
"leave a keyword-led operand unaffected" in { (td: TestData) =>
8080
val src = model(
81-
"""on command d.c.Foo is { tell command d.c.Foo(a = "the a") to entity d.c.target }"""
81+
"""on command d.c.Foo is { tell command d.c.Foo(a = 1) to entity d.c.target }"""
8282
)
8383
parseAndValidate(src, td.name, shouldFailOnErrors = false) { case (_, _, msgs: Messages) =>
8484
errorsOf(msgs) mustBe empty

passes/src/test/scala-jvm-native/com/ossuminc/riddl/passes/validate/CompletenessTest.scala

Lines changed: 2 additions & 2 deletions
Original file line numberDiff line numberDiff line change
@@ -1315,10 +1315,10 @@ class CompletenessTest extends AbstractValidatingTest {
13151315
| invariant BalanceNonNegative is "balance >= 0"
13161316
| state Main of record E.Fields
13171317
| handler H is {
1318-
| on init { set field E.Fields.balance to "0" }
1318+
| on init { set field E.Fields.balance to 0 }
13191319
| on command D.C.Cmd {
13201320
| require invariant BalanceNonNegative
1321-
| send event D.C.Evt(amount = "the amount") to outlet D.C.Events.out
1321+
| send event D.C.Evt(amount = 100) to outlet D.C.Events.out
13221322
| }
13231323
| }
13241324
| }

passes/src/test/scala-jvm-native/com/ossuminc/riddl/passes/validate/EntityValidatorTest.scala

Lines changed: 1 addition & 1 deletion
Original file line numberDiff line numberDiff line change
@@ -159,7 +159,7 @@ class EntityValidatorTest extends AbstractValidatingTest {
159159
| state field of record Hamburger.fields
160160
| handler baz is {
161161
| on command DoIt {
162-
| send event Message(a = "the a") to outlet ridOfIt
162+
| send event Message(a = 1) to outlet ridOfIt
163163
| }
164164
| }
165165
| } with {

passes/src/test/scala-jvm-native/com/ossuminc/riddl/passes/validate/MessageOperandSourceValidationTest.scala

Lines changed: 4 additions & 4 deletions
Original file line numberDiff line numberDiff line change
@@ -99,7 +99,7 @@ class MessageOperandSourceValidationTest extends AbstractValidatingTest {
9999
"accept a `let`-local bound to a constructed message as the operand" in { (td: TestData) =>
100100
val src = model(
101101
extraContext = "",
102-
srcBody = """let m = command d.c.Foo(a = "1")
102+
srcBody = """let m = command d.c.Foo(a = 1)
103103
|tell m to entity d.c.target""".stripMargin
104104
)
105105
parseAndValidate(src, td.name, shouldFailOnErrors = false) { case (_, _, msgs: Messages) =>
@@ -111,7 +111,7 @@ class MessageOperandSourceValidationTest extends AbstractValidatingTest {
111111
val src = model(
112112
extraContext = """function MakeFoo is {
113113
| returns command d.c.Foo
114-
| return command d.c.Foo(a = "1")
114+
| return command d.c.Foo(a = 1)
115115
|}""".stripMargin,
116116
srcBody = """let m = call function d.c.MakeFoo()
117117
|tell m to entity d.c.target""".stripMargin
@@ -127,7 +127,7 @@ class MessageOperandSourceValidationTest extends AbstractValidatingTest {
127127
|query Ask replies result d.c.Answer is { q: Integer }
128128
|entity Ledger is {
129129
| handler H is {
130-
| on query d.c.Ask is { reply result d.c.Answer(v = "the answer") }
130+
| on query d.c.Ask is { reply result d.c.Answer(v = 1) }
131131
| }
132132
|}""".stripMargin,
133133
srcBody = """let m = ask query d.c.Ask of entity d.c.Ledger
@@ -141,7 +141,7 @@ class MessageOperandSourceValidationTest extends AbstractValidatingTest {
141141
"accept a widened `send` operand too, not only `tell`" in { (td: TestData) =>
142142
val src = model(
143143
extraContext = "",
144-
srcBody = """let m = command d.c.Foo(a = "1")
144+
srcBody = """let m = command d.c.Foo(a = 1)
145145
|send m to outlet d.c.src.emitted""".stripMargin,
146146
srcExtra = "outlet emitted is command d.c.Foo"
147147
)

0 commit comments

Comments
 (0)