Repository navigation
feat(postgres): infer more expressions non-null - #15
Conversation
|
The latest updates on your projects. Learn more about Vercel for GitHub.
|
There was a problem hiding this comment.
Important
Three of the new rules claim non-null where Postgres returns NULL. I confirmed each against the engine's plan/resolve and on PostgreSQL 16. Details are inline.
Reviewed changes
I reviewed the whole PR: the seven precision rules in the Postgres engine, the new precision_rules oracle case, the five re-blessed cases and the docs.
- Operators: the pattern matches, bit/shift/containment/overlap/JSON key operators and the prefix
|/ ||/ @ ~now prove non-null. All of them are still shadow-checked by name throughtrust()andtrusted_operator. - Array casts:
x::T[]now carries its operand's nullability. - Self joins:
aliased_columnsresolves a top-levelalias.columnto its reading when a table is repeated under an outer join. - Scalar subqueries:
one_rowhandles a no-FROMselect, andkeeps_one_rowlets an aggregate through aLIMIT n >= 1. - Nested views:
probeprefetches the relations a view's statement reads. - Set-returning functions:
generate_seriesandgenerate_subscriptsjoinPOSTGRES_TOTAL, andunnest(ARRAY[…])reads its written elements.
claude-opus-5-5 ｜ 𝕏
8697c13 to
bdba308
Compare
bdba308 to
9078431
Compare
There was a problem hiding this comment.
ℹ️ The rebase adds no new issues, but the four threads from the earlier review are still open.
infer.rsandjsonshape.rsare byte-for-byte the same as before.
Reviewed changes
Since the last review, the branch was rebased onto 7994836, which brings in main's per-column own_provenance. I checked how the conflicts were resolved.
- Merged the self-join reading with
own_provenance:degradedis nowhidden || !ownfor each column, andaliased_columnsstill runs only when there is no set operation. Without a set operation,ownis alltrue, so the result matches the previously reviewed commit. With one,aliasedis empty and main's rule decides. - Renamed the declared-nullability closure from
owntodeclared, so it no longer clashes with main'sown. The direct path and thereadingpath call it the same way. - Merged the docs: main's new bullet on
withqueries and derived tables is kept next to this PR's outer-join, operator, set-returning and scalar-subquery bullets.
claude-opus-5-5 ｜ 𝕏
- like, ilike, similar to, the regular expressions, and the bit, shift, containment, overlap and json key operators are non-null over non-null operands (not #, whose geometric overloads may be null) - a cast to an array type keeps an array non-null: array[]::int[] - a table read on both sides of an outer join is told apart by the alias a top-level column names - a scalar subquery with no from, or an aggregate kept by limit n, is one row - a view over a view keeps its columns' not null - generate_series and unnest(array[...]) give non-null values
A scalar subquery's target must call no function or operator that may return a set, since one can leave the row out. unnest(ARRAY[...]) needs every element to be a scalar, not an array. An array cast checks the array type's own cast and drops elements a JSON null cast makes NULL. unnest is now asked of the catalog.
9078431 to
beeeba4
Compare
There was a problem hiding this comment.
✅ No new issues found. The four soundness threads from the earlier review are fixed and resolved, and
cargo test -p reylo-engine-postgres --libpasses (144 tests) atbeeeba4.
Reviewed changes
This run reviewed beeeba4, which narrows the three rules that claimed non-null where Postgres returns NULL and adds unnest to the trust check.
- Split the one-value check into
one_value:one_row(noFROM) andkeeps_one_row(the aggregate path, in bothinfer.rsandjsonshape.rs) now both reject a target that calls a set-returning function, a function the rules don't know, or an operator outside the built-in lists. Aggregate arguments,ORDER BYandFILTERare not walked, which is sound because Postgres refuses a set-returning call there. - Guarded the
unnest(ARRAY[…])elements withPOSTGRES_SCALARS: an element of an array type, or of a type the build can't name, no longer proves the result non-null. - Tightened array casts: the rule now needs
trust.cast("_T")as well astrust.cast("T"). On PostgreSQL 18,elements_not_jsonbwraps each built element of a number or boolean array cast inNotJsonb, and it unwraps the same variants thatitems_nullabledoes. - Added
POSTGRES_SET_RETURNINGtopostgres_function_names: a user's or an extension'sunnestnow turns the rule off. - Added oracle statements and re-blessed
precision_rules:array_cast_elements,scalar_set_returning,unnest_array_elementandunnest_column_elementare new, and the docs bullets are updated to match.
claude-opus-5-5 ｜ 𝕏
Seven rules where the Postgres analysis was sound but wider than it needed to be. Each was measured against SafeQL's generator test suite, where it closes 29 of the 51 statements whose types differed, and each has statements in a new oracle case,
oracle/cases/precision_rules, that the oracle runs over seeded edge values.select first_name like 'A%' from memberboolean | nullbooleanselect id & 3, array[id] @> array[1], to_jsonb(m) ? 'id' from member m| nullselect coalesce(array_agg(id), array[]::int[]) from membernumber[] | nullnumber[]select m.id, b.first_name from member m left join member b on b.id = m.manager_idid: number | nullid: number(first_namestays nullable)select (select 1), (select count(*) from member limit 1)select id from v_outer(a view over a view)number | nullnumberselect g from generate_series(1, 3) as g,select unnest(array[[1, 2], [3, 4]])infer.rs):LIKE,ILIKEandSIMILAR TO(which the parse marks as kinds of their own), the regular expressions, and the bit, shift, containment, overlap and JSON key operators, plus the prefix|/,||/,@and~, are non-null over non-null operands. Every built-in overload of each was read frompg_operatoron PostgreSQL 18: each is strict and returns a value or raises for non-null input.#is left out, sinceline_interpt,lseg_interptandbox_intersectreturn NULL where nothing intersects, and so are->,->>and#>>. An operator a user or an extension defines under one of these names turns the rule off, as before.alias.columnnow names its reading (aliased_columns); everything else stays as it was.FROMand noWHEREwhose target calls only functions the rules know (so no set-returning function) is one row, and so is an aggregate kept byLIMIT nwithn >= 1.generate_seriesandgenerate_subscriptsgive non-null values, andunnest(array[…])does where every element written is non-null.Five existing oracle cases were re-blessed, each now more precise and each checked: a deeply nested no-
FROMsubquery,generate_seriesin a derived table and beside an ordered-set aggregate, the preserved side of a self join, and a stored row read through a view.Verified locally: the engine's native tests, every oracle case on Postgres 18.6, SQLite and MySQL 8.4 with
--strict-coverage, the rebuiltpackages/postgres/engine.wasm,nub run typecheck, the loader's tests with every lab installed, the package build and the docs site.