Add an at-rest type checker - #5707
Merged
Merged
Conversation
OceanOak
force-pushed
the
at-rest-type-checker
branch
5 times, most recently
from
August 23, 2026 19:31
dc0134d to
e59ef5b
Compare
OceanOak
changed the title
OceanOak
force-pushed
the
at-rest-type-checker
branch
2 times, most recently
from
August 25, 2026 11:21
311bb32 to
7d1faf7
Compare
OceanOak
marked this pull request as ready for review
August 25, 2026 19:12
StachuDotNet
force-pushed
the
at-rest-type-checker
branch
from
August 28, 2026 03:25
03983fd to
373e27f
Compare
Three related moves, all in service of being able to read one without the other. - `PackageOpPlayback` had grown a general prepared-command abstraction over raw Microsoft.Data.Sqlite (the Ctx cache, exec/execRows/bytesOption, the parameter binders) on top of a file whose job is applying PackageOps to projection tables. That block knows nothing about packages, so it's now `LibDB.PreparedBatch`. - The three `applyAdd*` handlers each carried the same insert / detect-conflict / verify-fingerprint / update sequence, differing only in table, columns and which hash function to call. They share `upsertContentAddressed` now and keep only their own serialization. - `duplicateDeclarations`, `hashClashes` and `kindClashes` are the checks a batch must pass before anything is written, and PackageOps.fs calls all three in a row, but they lived in two files named for other jobs. They're `LibDB.OpValidation`. `duplicateDeclarations` and `hashClashes` are also rewritten while moving: the first loses a recursive walker for a `pairwise`, the second loses a fold into a Map-of-lists for a group-and-count. Same results, and `hashClashes` now says in a paragraph what it was saying in two jammed-together sentences.
3009 lines in one file, with no seam a reader could stop at. The `// ---` banners already marked the seams; this makes them module boundaries. - `AtRest.Types` is the vocabulary: the type language, verdicts, diagnostic codes, the type environment. Nothing here depends on the inference engine. - `AtRest.Unification` is the checker state, conversion out of ProgramTypes, and unification over the result. - `AtRest.Patterns` checks a pattern's shape and proves a match exhaustive. - `AtRest.Inference` is the `inferExpr` chain, which stays one file because it is one `let rec ... and` group. - `AtRestTypeChecker` keeps the entry points and the batch layer, and is still what callers name. Consumers change in one place each: `Checker` now aliases `AtRest.Types`, so every `Checker.TypeMismatch` and `Checker.Checked` reads as before, and the four entry points are `CheckerApi`. Keeping the vocabulary qualified matters more than it looks: `StaticType.TUnit` and `TypeReference.TUnit` would otherwise collide on an unqualified open. Cost worth knowing: `Proof`, `TypeScheme` and `TypeEnvironment` had `private` fields, and crossing a module boundary means `internal`. Still assembly-scoped, so nothing new is public, but it is a loosening and it's noted in the module headers. Also here, since it's the same reading problem: `ProgramTypesToDarkTypes`'s stack probe said what it did but not why it mattered or what it bought, and the twin in the checker didn't know about it. Both now explain that a .NET stack overflow can't be caught, name what catches the exception instead, and point at each other.
`Cli.Deps` spelled `PackageLocation * ItemKind` out in full in every signature, and the pair is wider than a line, so the formatter shredded four signatures into stacks of type arguments. It's a `Deps.Item` alias now, and the signatures fit on one line. While there: `collectTransitiveDependents` built `newDeps` and `newTargets` with two identical lambdas that differed only in whether the last field's name had an underscore. `Queries.getDependentsByLocationsChunk` stated three shadowing rules in one sentence and left the reader to map them onto a three-key ORDER BY inside a ROW_NUMBER window. The rule is one sentence now, and each tiebreaker is commented next to the clause it is. The reason the outer ORDER BY is by name and not by hash had been dropped in a rewrite; it's back. `docs/at-rest-type-checker.md` was carrying a rollout log: audit counts from two dates, a 700-to-129 narrative, and four named checker defects that are all fixed. That's PR-description material and it went stale on merge. What's left is the policy a reader needs, plus a new section saying where the checker should live and why it isn't there yet.
…entences `Diagnostic.context` and `Blocker.context` were English prose built in F#, with `countNoun`, `wasOrWere` and three `display*` helpers to build it. AGENTS.md says builtins carry data and Dark formats it, and this is a good demonstration of why: the checker has no name resolver, so the best sentence it could write was "Type #a1b2c3d4 is not available to the checker". The Dark side already had the hash lookup, so the same diagnostic now names the type. `context` is a `Context` DU carrying what the issue is about, and `AtRestTypeChecker.contextToStringWith` in Darklang turns it into a sentence. The `unify` and `checkExpr` "context" parameter, which was a site label like "Function application", is now a `Site`, so "In argument 3: expected Int, got Int64" instead of "Function argument 2: ...". Two pieces of prose stay in F# and are marked: the uncovered-pattern witness (it wants a MissingPattern mirror) and an adapter failure's exception message (which has no structure to keep). The mirror this creates is the extensibility problem underneath your notes. Adding a diagnostic used to be four edits, two of them unchecked, failing at runtime in the editor on the day someone first hit the code. `tests/AtRestTypeChecker/dark mirror` now compares the F# and Dark case names directly for every mirrored type, which immediately found `TRigidVar`/`TRigidVariable` and `TInferenceVar`/`TInferenceVariable` already spelled differently on the two sides. Renamed the F# ones to match rather than teach the test about exceptions. Also here: a `checkerVersion` constant, since the docs promise verdicts keyed by item hash and checker version and there was nothing to key on; and a CLEANUP on the module recording that this should be Darklang eventually, so people can choose which at-rest checks apply to their packages and write their own. `run-cli typecheck` over the corpus: 5754 checked, 0 failed, 6 incomplete, same six as before.
`InfixOperandUnsupported` was holding the DU case name as a string, so a message read "Operator ArithmeticPower". The mirror and the converter already existed, so it carries the `InfixFnName` and Darklang renders it through `PrettyPrinter.ProgramTypes.infixFnName`, which is what the reader wrote. That was the last Context case not actually structured.
Updating a widely-used item printed every dependent it repointed, one per line, and then every dependent that broke, with its diagnostics. Changing `Stdlib.Option.map`'s signature produced about 900 lines from a single `fn`. The type errors, which are the part you needed, were at the bottom of it. Both are grouped and capped now, and each footer names the command that prints everything: `deps usedby <name> --all` for the repoints, `typecheck --failed` for the errors. That same signature change is 55 lines. The two are capped unconditionally rather than through `Listing.shouldCap`, which is the part worth knowing. `shouldCap` asks whether stdout is a terminal, and `run-in-docker` allocates a TTY based on stdin. Authoring reads the declaration from stdin, so there is no TTY, so `shouldCap` is false and nothing caps on the one path that floods. Wrote that down in AGENTS.md; it is not obvious and it silently makes the helper a no-op. `Listing` grew `footerSeeAlso`, `withFooterSeeAlso` and `cappedGroupsSeeAlso`, because the existing footer hardcodes "pass --all to see them" and `fn` has no such flag. The old three delegate to them, so every other listing is unchanged.
The diagnostic restructure kept the facts but dropped the sentences for every code whose context is just a name. `[UnknownVariable] Local variable 'nope' is not in scope` had become `[UnknownVariable] 'nope'`, and the same for unknown record fields, unknown enum cases, undeclared type variables, missing fields, and all three arity messages. The renderer only looked at the context; it takes the code now, which is what says whether a name is a variable, a field or a case. I had checked the diagnostics I happened to exercise and not the ones I hadn't. They read as well as before or better, since Darklang can resolve a hash: `Darklang.ReviewUx.Pair expects 2 type arguments, but 1 was provided`, where F# could only ever have said `Type #a1b2c3d4`. Also narrowed 27 helpers back to `private`. Splitting the checker meant widening what crosses a module boundary, but I did it with a blanket regex and caught `isNumeric`, `finiteConstructors`, `specializePattern` and 24 others that never leave their own file. 27 genuine cross-file `internal`s remain, which is what the split commit should have said.
I added it because the doc promises verdicts keyed by item hash and checker version. Nothing reads it, and a version nobody has a reason to bump is worse than no version: the day something does trust a stored verdict, a forgotten bump makes it trust a stale one silently. The discipline only becomes real alongside the thing being invalidated, so it belongs with whoever builds persistence. The doc still says persistence will key on a checker version. That reads fine as a statement about the future.
Rebasing onto main brought in the builtin-description whitespace test, which this description fails: written as one multi-line F# literal, it keeps the source indentation and renders with a gap mid-sentence. Same fix as the rest of the codebase, separate literals joined with `+`.
CI caught this on the rebased branch: the test expects a 300,000-deep alias chain to come back Incomplete, and on my branch it comes back Checked. The cause is not depth. Taking the interpolated strings out of `normalizeAliases` and `validateTypeClosureFrom` left the recursive call in tail position, so in Release the JIT tail-calls it and the walk runs in near-constant stack. It reaches the end of the chain and returns a real verdict instead of tripping the stack probe. Debug emits no tail calls, so there the probe still fires and the answer is still Incomplete. Raising the depth does not help: I tried a million, and 100,000 on a 512KB stack still completed, which is what finally gave the mechanism away. So the verdict here is a build-configuration detail, and asserting either one passes in one configuration and fails in the other. The test now asserts the property it was written for: pathological input never takes the process down, and never comes back as a definite type error. An Incomplete answer still has to be the depth guard rather than some other blocker. The two tests above it cover the probe itself in both configurations, and `detects alias cycles through containers` still covers the walk visiting every link, so nothing lost coverage. Verified both ways: Debug and Release, full suite, 10,423 passing.
StachuDotNet
force-pushed
the
at-rest-type-checker
branch
from
August 28, 2026 04:11
373e27f to
967ae5a
Compare
Member
|
Hey -- I had a long review message drafted, and ended up having an agent address the feedback rather than dump a wall of thoughts here. About to merge, but please LMK if I've done anything negative :) Notable changes:
Longer term I imaginea lot of this living in package-land rather than F#. The set of at-rest checks is fixed right now, and I think people should be able to pick which ones apply to their packages and write their own, which pretty much means they need to be ordinary Darklang. |
This file contains hidden or bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
Sign up for free
to join this conversation on GitHub.
Already have an account?
Sign in to comment
2 participants
Add this suggestion to a batch that can be applied as a single commit.This suggestion is invalid because no changes were made to the code.Suggestions cannot be applied while the pull request is closed.Suggestions cannot be applied while viewing a subset of changes.Only one suggestion per line can be applied in a batch.Add this suggestion to a batch that can be applied as a single commit.Applying suggestions on deleted lines is not supported.You must change the existing code in this line in order to create a valid suggestion.Outdated suggestions cannot be applied.This suggestion has been applied or marked resolved.Suggestions cannot be applied from pending reviews.Suggestions cannot be applied on multi-line comments.Suggestions cannot be applied while the pull request is queued to merge.Suggestion cannot be applied right now. Please check back later.
This PR adds a type checker that validates serialized packages (ProgramTypes) without executing them, then wires it through the whole workflow: save, commit, CLI, and editor.
The checker
Integration