Census path is not laxer than compile: the probe keyed the wrong class; fix the qualified-Nat spellings that made the census stricter

[gunbai-bot]

Lane adhoc-561ab822-50b. The brief's premise does not hold. The census fixture path (compile_dag_diagnostic_census) refuses every mismatch that gunbc compile --entry refuses. The "0 TypeMismatch" reported in #12375 was a class-key miss: the probe counted the wrong diagnostic class for its shape. The census was not reaching less than compile. One real census/compile divergence did turn up, and it is fixed here at its source.

Reproduction (8-probe matrix, srv1 via neat-boar-16)

Two shapes (return position, call argument) × two type origins (imported v2.compiler.inferred_tree InferredFacts/InferredTree, and local A/B) × red/green, each through both paths.

shape	compile	census
return red	TypeMismatch	TypeMismatch
argument red (Product)	DeclaredTypeNotInhabited ("value does not inhabit its declared type at the direct call argument")	DeclaredTypeNotInhabited
all greens	0 blocking	0 blocking (after this PR; see below)

#12375's census pair was argument-shaped but counted only TypeMismatch. Its String-at-Int control does emit TypeMismatch. So one inhabitance defect lands in two classes, depending on its position and on whether the value is primitive or a Product.

The imported pair substitutes InferredFacts/InferredTree because ObligatedInferredTree is not on main yet. The class rule does not depend on the particular types, so #12375's fixture is enrollable on the census path: key it on DeclaredTypeNotInhabited for the argument form, or TypeMismatch for the return form.

The real divergence, fixed

Before this PR, the imported greens carried 7 blocking UnresolvedType v2.std.nat.Nat rows on the census path only.

• v2.std.cardinality (2 rows) and v2.std.integer (5 rows) both import v2.std.nat { Nat } but spelled their type positions v2.std.nat.Nat.
• Production reports each such use as an advisory UnlistedImportUse. The census-only N1a arm (v1.compiler.infer_resolve resolve_node_bounded under type_ref_hit_ne_bind_measure_active) makes the same finding blocking, by design.
• So the census was the stricter path here. The fix is to spell the bound names; there is no compiler change.

Evidence: srv1 census runs at 5eed55a (pre-fix: n=7), afcf820 (cardinality only: n=5) and e832377 (both modules: no rows). The two partial runs double as the mutation baseline.

Probe audit (gunbc.guarantee_probe_corpus)

There are four ExpectBlockingRefusal { TypeMismatch } rows:

• conformance_scalar_red
• direct_call_arg_type_ordinary_module_red
• direct_call_arg_type_v2_module_red
• floor_generic_instantiation_monomorphic_control

All four use primitive String-at-Int sources, which do emit TypeMismatch. No expected verdict changes, and none was passing vacuously. The Product-argument shape was not enrolled anywhere, and this PR adds it.

Changes

• src/v2/std/cardinality.dag and src/v2/std/integer.dag: spell Nat (plus Zero/Succ in cardinality) by the imported name.
• New test.claim.product_inhabitance_class_by_shape witness:
  • Each Product red is asserted in the class it emits, and the other class is asserted absent.
  • The imported green is asserted fully clean. Reverting either module fix turns that row red, since the rows return, as the partial runs showed.
• New RFM row probe_keys_a_diagnostic_class_its_fixture_shape_does_not_emit, recording the actual finding. Its ceiling is one class authority for one inhabitance defect (DESIGN §3), and its trigger is consolidating the two refusals in v1.compiler.infer. That consolidation is a proposal and is not done here.

Not verified locally: the witness file itself first executes in CI, because there is no single-module claim runner.

🤖 Generated with Claude Code

[gunbai-bot]

Addressing review 71752: confirmed. After the main merge, synthesis.dag no longer names AdvisoryLens, so that import was unused, and the three names resolved only through v2.lens.application's own import of v2.std.report. Fixed in 82c3975: synthesis.dag now imports Report, SynthesisGapDecisionTree and SynthesisGapInformationTheoretic directly from v2.std.report, and the AdvisoryLens import is gone. The ImportsFixed retirement of those three roster rows is now literally true.

— sent from still-hawk-901

[gunbai-bot]

Correction to my reply on review 71752: synthesis.dag DOES use AdvisoryLens, at the decision_tree_synthesis_advisory_lens and information_theoretic_synthesis_advisory_lens data rows. CI at 82c3975 refused them as unresolved. So the review's 'never used' was wrong on that point, though right that the three report names needed a direct import. cfdc7f2 keeps both imports: v2.std.report for the three report names and v2.lens.application for AdvisoryLens.

— sent from still-hawk-901