Repository navigation
fix: type whole rows, null elements and json numbers soundly - #5
Conversation
|
No configured credential can serve this run. Your Claude Pro/Max subscription was rejected. Sign in again by running The providers' responses
|
|
The latest updates on your projects. Learn more about Vercel for GitHub.
|
1e19a29 to
ea2a9e7
Compare
There was a problem hiding this comment.
ℹ️ No correctness issues found. One small doc-comment slip is noted inline.
Reviewed changes
Pullfrog hadn't reviewed this PR before, so this pass covers the whole of ea2a9e7. The only difference from 1e19a29 is that the branch was rebased onto main.
- Treated
t.*in a call as the whole row.jsonb_agg(t.*),json_agg(t.*) filter (…),jsonb_build_object('t', t.*)andto_jsonb(t.*)now go through the newBuilder::whole, the same path the baretuses.leafnow refuses any star, so a star never ends up in a probe's select list. - Narrowed whole-row nullability under outer joins. A row is now non-null when the probe proves any of its columns non-null. This is sound because probe columns get the same outer-join nulling from
describe(by name, or by position viaitem_columns) that result columns get. - Kept NULL elements of a statement-built array inside JSON.
ResolveCtx::columnnow applieswith_itemsfrom the probe's analysis. - Typed non-finite numbers and unread rows inside documents. Inside JSON, Postgres
float4/float8/numericnow admit"NaN","Infinity"and"-Infinity", and MySQL keepsnumber. Arecordis now an object. - Made duplicate result column names error
reylo14. The newanalysis::clashescheck runs on all three engines. On Postgres,column_spansplaces the error on the alias or column name; on MySQL and SQLite it lands on the statement's first word. On the TS side,lastOfEachNameandobject()keep the last column of each name, which matches what drivers andJSON.parsedo. - Made the oracle check value kinds inside documents.
json_contradictionnow walks array elements and checks scalars (viajson_admits) and enum labels.
claude-opus-5-5 ｜ 𝕏
95de6c2 to
0e78008
Compare
There was a problem hiding this comment.
ℹ️ No correctness issues from the rebase. One comment went stale under #12 and is noted inline.
Reviewed changes
Since the last review at 95de6c2, the branch was rebased onto 7de25a3 (#12, returned array elements nullable). git range-diff shows the code patches are unchanged. Only the context of the site/lib/sql-modules.json hunk moved.
- Rebased onto #12. All three
engine.wasmblobs differ from both the new base and the previous head, so they were rebuilt on top of #12's engine. - Checked how the PR combines with #12. An array whose
nullable_itemsis absent now renders(T | null)[]inside JSON too. Sowith_itemsinResolveCtx::columnnow mostly narrows: an array proven non-null (array_non_null.sql→(text!)[]) rendersT[]. The oracle's new in-JSON element check (nullable_items == Some(false)) matches that rule. The PR'sschema.rs,render.tsandschema.tshunks (non-finite numbers,record,lastOfEachName) don't overlap #12's array changes in those files.
ℹ️ The PR description's "typed before" for array[name, null] no longer holds against main
Since #12, main already types json_build_object('v', array[name, null]) as { v: (string | null)[] }. The bullet "An array the statement builds keeps its NULL elements inside JSON" now describes behavior main already has. What this PR still adds there is the narrowing to T[] where the probe proves the elements non-null. Worth updating before squash-merge if the description becomes the commit message.
claude-opus-5-5 ｜ 𝕏
1bd32a8 to
98ec189
Compare
There was a problem hiding this comment.
✅ No new issues found. The rebase onto #15 is clean, and the open
seed.rscomment is fixed.
Reviewed changes
Since the last review at 0e78008, the branch was rebased several times, most recently onto 3cfd016 (#15, #23, #24). It also gained one commit.
- Took the suggested wording for the oracle's array comment.
json_contradictioninoracle/src/seed.rsnow says any array may hold NULL elements unlessnullable_itemsis false, which matchessrc/render.tsafter #12. The check itself is unchanged. - Rebased onto #15. The PR no longer makes
is_starpub(crate), because #15 already does.column_spansnow sits after #15'saliased_columns. Onlypackages/postgres/engine.wasmwas rebuilt; the MySQL and SQLite blobs are the same as at1bd32a8. - Checked how the whole-row rule combines with #15. A whole-row probe is
SELECT u.* ….aliased_columnsgives up on a*, andhiddenstill covers a repeated table, so a self-joined row's probe columns stay nullable. The PR's "any probe column non-null" rule therefore cannot narrow the nulled side (whole_row_self_joinkeepslater: [users{…}?]). #15's newprecision_rulesstatements have no duplicate output names and no float,numericorrecordinside JSON, so neitherreylo14nor the new in-document types touch them.
claude-opus-5-5 ｜ 𝕏
c407a92 to
e343616
Compare
|
On the review of 0e78008 noting that the |
e343616 to
60ac8cf
Compare
- jsonb_agg(t.*), json_agg(t.*) filter (...), jsonb_build_object('r', t.*)
and to_jsonb(t.*) are the whole row, not the row's first column
- an array built inside json keeps what the statement shows of its
elements, so array[t.name] over a not null name has no null element
- a float or numeric inside json may be "NaN", "Infinity" or "-Infinity",
and a row whose columns were not read is an object there
- two result columns of one name are an error (reylo14) at the second,
and the row type keeps the last, as drivers do
- the oracle checks each value's kind inside a json document
Found by running SafeQL's test statements through the oracle.
60ac8cf to
00b6ff8
Compare
Three types inside JSON a statement builds were unsound, one was looser than the statement shows, and one shape of result was silently wrong. Each was found by running SafeQL's generator test statements through the soundness oracle, which also gained the check that would have caught them.
select jsonb_agg(team.*) from teamnumber[] | null[{"id": 1, "name": "core"}]{ id: number; name: string }[] | nullselect json_build_object('v', array[name]) from team(nameisnot null){ v: (string | null)[] }{"v": ["core"]}{ v: string[] }select jsonb_build_object('n', 'NaN'::numeric){ n: number }{"n": "NaN"}{ n: number | "NaN" | "Infinity" | "-Infinity" }select jsonb_agg(s) from (select id from team) s(string | null)[] | null[{"id": 1}](Record<string, unknown> | null)[] | nullselect m.first_name as x, mt.id as x from …{ x: string }{"x": null}(drivers keep the last column)reylo14at the second columnt.*inside a call is the whole row.jsonb_agg(t.*),json_agg(t.*) filter (…),jsonb_build_object('t', t.*)andto_jsonb(t.*)read the row, as the baretalready did. A row with a column the probe proved non-null is no longer nullable under an outer join, since an unmatched row is every column NULL.array[name]over anot nullcolumn isstring[], andarray[name, null]stays(string | null)[]. (When this PR was opened,array[name, null]inside JSON was typedstring[]; fix(postgres): type returned array elements as nullable #12 has since made every array's elements nullable unless the statement shows otherwise, so what this PR adds there is the narrowing.)float4,float8ornumericinside a document as text, and a row whose columns were not read as an object. The TypeScript types,.outputSchemaand the engine's JSON Schema say so; MySQL, which stores no infinity, keepsnumber.reylo14) on all three databases, at the second column on Postgres and on the statement's first word elsewhere, and the row type keeps one key, the last, as drivers andJSON.parsedo.oracle/cases/json_whole_rows; four existing cases re-blessed for the new error and one more precise row.Verified locally: the engine's native tests, all 98 oracle cases on Postgres 18.6, SQLite and MySQL 8.4 with
--strict-coverage, the three rebuiltengine.wasmartifacts,nub run typecheck, the loader's tests with every lab installed, the package build and the docs site.