Inference-first annotation rules: BSK-0001/0002 never fire on inferable types#319
Merged
Conversation
- The LSP watches every root's config server-side (250ms content poll of pyproject.toml/uv.lock/.python-version) and re-checks, republishes diagnostics, and pushes basilisk/configurationChanged on any change, whether from a file edit or the configuration-editor UI - The in-memory root config is authoritative over disk: per-file discovery walks only strictly below the owning root (load_basilisk_config_below), so an applied UI change is never clobbered by stale on-disk content - basilisk format [paths] [--check] via the embedded Ruff formatter, plus a generated release-notes component block from shipwright.json and the release binary itself - Guards: disk-edit and UI-apply reactivity e2e tests, stale-disk authority unit test, empty-PATH format CLI e2e, release-notes drift test, and nvim client-module specs (Lua coverage 45% >= 44%) - Coverage ratchets: basilisk-lsp 83->84, basilisk-config 96->97
…le types (Refs #317) - BSK-0001 skips parameters whose literal default determines the type ([TYPEINF-FUNC-DEFAULTS]); BSK-0002 skips functions whose return type the engine already infers ([TYPEINF-FUNC-RETURN]); exemptions exactly as strong as the current inference engine (shared rhs_fully_determines_type) - Specs updated: CHECKER-ARCHITECTURE-SPEC, CHECKER-TYPE-INFERENCE-SPEC - CLI adopt/fix and LSP autofix/mass-fix follow the same predicate - Tests updated across checker, CLI e2e fixtures, and LSP e2e to enforce the new behavior in both directions - Mutation baseline refreshed by the full 142-mutant run (0 missed, 100% kill) - Benchmark CSV re-established under the post-#313 config-neutral harness (see PR body: no code regression; the old baseline predates the harness change)
…g testing 1aa6e0e replaced the entire wheel packaging definition (maturin build-system, basilisk-python project metadata, bundled license notices) with a scratch [tool.basilisk.rule-tags] config that also downgraded pep rules to warnings. The wheel is how the python/typing conformance suite installs checkers via uv sync, and the release pipeline builds it — restore main's file verbatim. Verified: config_override_tests, rule_tags_tests, basilisk-cli bin tests all pass.
# Conflicts: # crates/basilisk-lsp/src/server/activity_panel/module_tree.rs # mutation_testing/mutants_report.html # mutation_testing/mutation_scores.json # vscode-extension/src/module-explorer.ts
…tion-level Salsa queries
Stage 0 (NARROWPLAN-CHECKLIST): two-mode bidirectional core (synth/check,
check primary) over the ruff AST; two-stage constraint architecture with a
separate solver delegating every ground leaf to is_assignable_to; bounded
polar type variables with deferred generalization (list[Var{lower=Literal[1]}]);
gradual-guarantee differential harness (curated corpus + conformance-fixture
sweep); prototype validation against five pinned real typeshed stubs.
Stage 1: definition/expression-level tracked queries with slice-keyed early
cutoff (proven via WillExecute log), compact module-interface boundary with
backdating, salsa fixpoint cycles seeded by the Unknown sentinel with a hard
cap. Measured on a seeded 1.12M-LOC corpus: keystroke re-check p50 0.16ms /
p99 0.22ms, RSS ~312MB.
Fixes found by the new gradual harness and reflexivity validation, all
conformance-verified (100%, 0 FP, CSV byte-identical): classes_override no
longer treats an absent annotation as a signature mismatch; is_assignable_to
gains the documented-but-missing bool <: int <: float arm; union-left
decomposition now precedes Optional-target unwrapping so A | None <: Optional[B]
holds. types.rs split under the 500-line cap (types_star_tuples.rs).
Refs #317
…erations First consumer of the resolver's collected NarrowingGuards (TYPEINF-TARGET-NARROWING): intersection-and-negation set operations over InferredType delegating every atomic decision to is_assignable_to; a flow-scoped NarrowEnv with branch push/pop, phi-join at merges, whole-scope assert narrowing, declared-type anchoring (narrowing never changes the type assignment validation uses), and fresh-environment nested-function boundaries; guard interpretation for isinstance (including tuple form), is None/is not None, truthiness, TypeGuard (PEP 647, positive-only), TypeIs (PEP 742, both branches), and assert, with loop-collected guards suppressed per TYPEINF-NARROWING-SCOPE. Refs #317
… early-exit persistence Statement-level flow analysis driving NarrowEnv through function bodies: guards matched to if/assert statements by resolver-collected span; positive frame in the if body, complement in the else, phi-join at merges; a diverging branch (return/raise/continue/break) persists the other branch's narrowing (the 'if x is None: return' pattern); assert narrows whole-scope through a dedicated scope layer that never touches the declared-type anchor; assignment narrowing via the bidirectional engine; loop bodies and try/except walk in discarded frames; nested functions are a narrowing boundary. End-to-end tests run parse -> resolve -> analyse_function over the checklist's positive/complement, early-exit, loop, closure, merge, and assignment cases. Refs #317
… items match subjects narrow per case (resolver Match guard matched by body span, value patterns conservatively skipped so Never is never fabricated from non-type pattern text). Plan checklist updated: scoped environment, guard consumption (now including match), and declared-type-anchored assignment narrowing are done. Refs #317
…plied-else, issubclass/hasattr extraction Resolver: five new NarrowingGuardKind variants extracted from if/assert tests — issubclass, hasattr(x, 'name'), x == <literal> (case-preserving literal text, never the lowercasing annotation parser), x in (<literals>), and '\''key'\'' in td. Checker: equality/membership narrowing with exact-literal complements; TypedDict key narrowing filters union members through a NarrowContext of per-class key sets (required keys prune the complement, optional keys survive both branches, unknown schemas stay conservative); exhaustive fully-diverging match statements narrow the subject afterwards by subtracting covered pattern types. issubclass and hasattr interpret as identity until type[] modelling and synthetic-protocol intersections exist (documented in the plan checklist). Refs #317
…, fix too_many_lines - narrowed_uses: tracked query running the flow walker per definition slice; editing one function re-executes only its narrowing (WillExecute-proven). Checks off the Salsa-backed use-def checklist item. - Attribute-narrowing-across-calls tradeoff decided and documented (TYPEINF-NARROWING-ATTR-CALLS): survives calls by default (usable), narrow-attributes-across-calls = false opts into strict; parsed and merged in BasiliskConfig. - Split outcome_for_kind to satisfy clippy too_many_lines after rustfmt reflow (the CI Lint failure on the previous push). Refs #317
…rowing FlowResult now carries unreachable_ranges: a branch whose guard narrows the scrutinised variable to Never is reported unreachable — reachability derived from the type lattice rather than pattern-matched idioms. Groundwork for the checklist item; rules migrate off static-condition idiom matching at the Integration stage. Refs #317
…seline measured Resolver extracts type(x) is C / is not C ([TYPEINF-NARROWING-TYPEOF]); the checker narrows the positive branch by intersection and excludes C in the negative branch only when C is @Final (NarrowContext.final_classes) — the exact soundness split the utahplt/ifT-benchmark exercises. ifT-benchmark harness (examples/ift_measure.rs) over a fresh clone's Pyright suite: baseline 11/37 functions (29%) produce a flow-narrowing signal; the silent families each map to a named pending guard form (connectives, nesting, cross-function TypeGuard, attribute and tuple narrowing), recorded in the plan as the ratchet floor. 8/9 flow checklist items now checked. Refs #317
An unannotated function's return type is now synthesized from its body through the bidirectional engine: union of return-expression types, plus None for bare returns or fall-through (last-statement divergence check); no return statement at all infers None precisely. Explicitly documented as display/assist-grade per the gradual guarantee — inferred-from-unannotated types must never be enforced as declarations when rules consume them at the Integration stage (differential harness stays green). Refs #317
…ctor, method, subscript synthesis One builtins table (bidir/builtins.rs) for builtin call returns and str/list/dict/set method returns — the single home the checklist demands; rule-local string tables migrate onto it at Integration. Engine synthesis now covers: builtin calls (len -> int, sorted -> list, ...), builtin method calls inferred from the receiver's synthesized type (dict.get -> Optional[V]), user-class constructor calls (Named callee -> Named instance), and subscripts (list element, dict value, tuple position via literal index with deferred-generalization precision, str indexing, slice preservation). Argument-dependent builtins stay Unknown - no guessing. Refs #317
…traints and call sites Pure module-level core (param_infer.rs) shared by the Salsa layer and the future BSK-0001 exemption: unannotated parameters bind to input-polarity variables; body constraints (p passed to a callee with a declared param type) accumulate demands through the bidirectional engine, same-module call sites contribute lower bounds, and resolution follows input polarity (demand wins, else union of flows, else Unknown - never a guess). Engine gains three small entry points (fresh_param_var, bind_global, add_var_lower_bound). Refs #317
…backdated callable interface x = f() now resolves through the sibling's declared-or-synthesized return. Sibling callables reach variable inference via a new callable_interface tracked query (functions/classes only, PartialEq) so a body-only edit to a declared-signature sibling backdates and the variable's memo survives - the early-cutoff test caught the naive version depending on raw definition identities and recomputing on every sibling edit. Variable-to-variable aliases stay on the direct cycle-recovered definition_type edge. Refs #317
imported_callable_globals maps the cross-module layer's imported_symbols into engine scope: imported functions become gradual Callable[..., R] from their return annotation (so calls to imported names infer returns), classes map to their instance form, annotated variables to their annotation, and anything without type information stays Unknown. Checks off the same-module + imported returns checklist item. Refs #317
…ss schemas class_attribute_interface collects each class definition's annotated class-level attributes (PartialEq value, backdates when schemas are unchanged); the engine's new attribute-load synthesis answers instance.attr from those schemas (Point().x -> float composing constructor + schema + load). Completes the structured-AST expression inference checklist item: constructors, attributes, subscripts, binary/unary, conditionals, and walrus are all inferred. Refs #317
MelbourneDeveloper
enabled auto-merge (squash)
July 18, 2026 04:06
Self-declared TEMPORARY verification harness ('delete after use. Not part of
the suite') accidentally committed to the branch. It breaks the Lint job with
clippy::doc_markdown + clippy::filter_next under -D pedantic/-D all.
Self-declared TEMPORARY verification repro ('to be deleted') accidentally
committed alongside tmp_rebind_claim_verify.rs. Not part of the suite.
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
1 participant
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.
TLDR
Annotation house rules (BSK-0001/0002) no longer fire where the current inference engine already knows the type; ships with the config-editor deep-link hover UX, module-explorer/config-editor VSIX test hardening, honest mutation + benchmark baseline refreshes, and a restored PyPI packaging file. Refs #317
What Was Added?
rhs_fully_determines_typeincrates/basilisk-checker/src/inference.rs(+119);ParameterInfo.default_rhs_kindin the resolver feeds BSK-0001 so a type-determining literal default (timeout=30) suppresses the diagnostic; BSK-0002 stays silent when everyreturnis bare or literal-inferable (generators still require annotations). Exemptions are exactly as strong as today's engine — nothing else was loosened.command:URI (basilisk.openConfigurationEditor, declared inbasilisk-common) focused on the rule; PEP rules get no link ([CONFIGEDITOR-VSIX-EXPERIENCE]). Newhover/tests_diagnostics.rscases cover both.module-explorer-render.ts), configuration-editor focus/menu/webview-DOM test suites (+755 lines of tests),package.jsoncommand contributions.missing_parameter_annotation_tests.rs(+71),missing_return_annotation_tests.rs(+90) enforcing both directions (inferable ⇒ silent, non-inferable ⇒ fires).What Was Changed or Deleted?
missing_parameter_annotation.rs/missing_return_annotation.rs: filters consult the new predicates; diagnostic help text now teaches the inference rule.adopt/fixand LSP autofix/mass-fix follow the same predicate so they never insert annotations the checker doesn't demand; CLI fixtures updated accordingly.activity_panel/module_tree.rs: module-tree rendering fixes (+47).pyproject.tomlrestored from main: an on-branch commit (1aa6e0e) had replaced the entire PyPI wheel packaging (maturin build-system,basilisk-pythonmetadata, bundled license notices) with a scratch[tool.basilisk.rule-tags]config that downgraded PEP severities. The wheel is how thepython/typingconformance suite installs checkers (uv sync) and how releases publish to PyPI — restored verbatim.mutation_testing/mutation_scores.json: baseline overwritten by the full fresh run (pool 125 → 141 viable, 0 missed, kill_rate 100%).benchmarks/status/*.csv+results/*.json: re-recorded by a full quietmake benchrun — see baseline note below.docs/plans/NVIM-UPGRADE-PLAN.mddeleted (completed plan); README/quick-start rule counts refreshed fromrules.json.How Do The Automated Tests Prove It Works?
missing_parameter_annotation_tests.rs/missing_return_annotation_tests.rs: literal defaults (timeout=30), literal-only returns (return 42), and no-return functions produce no diagnostic;Nonedefaults, call-result defaults/returns, and generators still fire — proving the exemption is exactly as strong as current inference.e2e_rules_a.rs+ fixtures):basilisk check/fix/adoptoutput matches the new behavior end-to-end.lsp_e2e_code_actions.rs,ws_test_code_actions.rs): autofix only offered where the rule still fires;hover/tests_diagnostics.rs: severity link present for BSK codes, absent for PEP codes.python/typingharness: 141/141 files, 0 false positives, VSIX (555 passing, 93% coverage), Shipwright, Neovim (45% ≥ 44%).Spec / Doc Changes
CHECKER-TYPE-INFERENCE-SPEC.md(+621): inference-first principle stated normatively with worked examples;CHECKER-ARCHITECTURE-SPEC.mdcross-references it from the diagnostic-ownership sections.CHECKER-TYPE-NARROWING-INFERENCE-PLAN.mdupdated;EXTENSION-ACTIVITY-PANEL-SPEC.md,LSP-ARCHITECTURE-SPEC.md,LSP-CONFIGURATION-EDITOR-SPEC.md,VSIX-SPEC.mdaligned with the hover deep-link and module-explorer changes.Benchmark baseline re-established (post-#313 harness)
make benchfailed its zero-tolerance gate on 6 of 26 fixtures (worst:callables_subtyping+13.9%). Forensics show this is not a code regression:callables_subtyping), 10.5 vs 10.7 (unresolved_imports), within σ.94d196f3, rebuilt fresh) measures 26.6ms oncallables_subtypingtoday vs HEAD's 11.1ms — current code is 2.4× faster under identical conditions.[tool.basilisk]house rules) to a config-neutral temp-dir copy, without re-recording the CSV. The committed 10.6ms is unreproducible today by any binary, including its own commit's.make benchand commit the CSV in the same PR.Breaking Changes