feat(frontend): detect uninhabited (uninhabited) required-recursion schemas - #13
Merged
Conversation
Add an inhabitation analysis over the reference graph: a least fixed point that proves which nodes have a finite JSON instance. Required self-recursion (an object that requires a property whose schema resolves back to itself with no nullable/optional escape) never bottoms out, so it is uninhabited — yet the SCC pass classifies it guarded/representable. Report such recursive nodes via Schema.Uninhabited; Compile surfaces a SeverityWarning so a generator does not emit a dead type. The analysis is a sound over-approximation: unmodeled constructs (combinators, arrays, const/enum) are assumed inhabited, so no satisfiable schema is ever flagged. `required` only bites when the node is object-only — a non-object kind gives a witness that ignores it. Closes #8 Co-Authored-By: Claude Opus 4.8 (1M context) <noreply@anthropic.com>
Codecov Report✅ All modified and coverable lines are covered by tests. Additional details and impacted files@@ Coverage Diff @@
## main #13 +/- ##
==========================================
+ Coverage 75.43% 75.90% +0.46%
==========================================
Files 42 43 +1
Lines 3143 3204 +61
==========================================
+ Hits 2371 2432 +61
Misses 629 629
Partials 143 143 ☔ View full report in Codecov by Harness. 🚀 New features to boost your workflow:
|
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
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.
Summary
Closes #8. Required self-recursion — e.g.
{type:object, required:[self], properties:{self:{$ref:"#"}}}— has no finite JSON instance (every value must contain a strictly smaller one of itself), but SCC analysis classifies it Guarded/representable: it only checks termination (a base case could exist in the Go type), not inhabitation (whether any instance reaches it). This adds the missing inhabitation analysis.Approach
A least-fixed-point pass over the reference graph (
internal/frontend/inhabit.go, modeled onrefkinds.go's cycle-safe walk):inhabited(n)starts false and is proven true only when a finite witness can be built from already-inhabited parts. A purely-required cycle never produces a witness, so it stays uninhabited at the fixed point.Sound over-approximation — the analysis never false-positives a satisfiable schema:
requiredonly constrains object instances, so it bites only when the node is object-only (type:object); a permitted non-object kind yields a scalar/null witness that ignoresrequired.$refis treated as a conjunctive constraint: a provably-uninhabited target makes the referrer uninhabited too.Only recursive required-object emptiness is reported (the surprising case the SCC pass misses); local emptiness (
falseschema, disjoint kinds) is already modeled by normalization and intentionally not re-reported.Surfacing
Schema.Uninhabited []UninhabitedNode(alongsideUnresolved), turned into aSeverityWarningbyCompile(uninhabitedDiagnostics) — the schema is representable but no value inhabits it, so a generator should warn rather than emit a dead recursive type.Tests (
internal/frontend/inhabit_test.go+ oneCompiletest)Positive: self-recursion and mutual A↔B recursion flagged. Negative (no false positives): optional-property escape, nullable node (
type:["object","null"]), untyped (scalar witness), nullable-branch-via-combinator, and finitely-nested required chains — all correctly not flagged.Verification
go build ./...,go test ./...(incl. conformance),golangci-lint run ./...→ 0 issuesUnrelated hygiene note: a graphviz test writes
graph.dotto the repo root without cleaning it up (and it isn't gitignored). Not touched here; happy to fix separately.🤖 Generated with Claude Code