lever: cross-module recursive_type_set local-restrict + import-authority union (+ floor witness)

[gunbai-bot]

What

The cross-module recursive-set fix (the lever), plus a permanent floor witness. Stacked on #5623 (the 04_resolve (Y') prerequisite) — base will retarget to main when #5623 merges.

04_infer (both build_type_env_resolved + build_type_env_unresolved): compute the type-cycle set over local bindings only, then union the imported modules' recursive-type authority:

cross_type_all_names = concat(concat(local_cycle, import_recursive_names), kernel)

Why

Imported type bindings arrive as self-ref stubs (node_type_deps returns [own_name]), so detect_type_cycles_kahn over the merged bindings re-marked every imported type recursive — spuriously boxing ~non-recursive concrete types in the emitted Rust (the E0308 value-wrapping long pole) and, where it failed open, masking real resolution defects.

Single-authority fix: recursion is decided once, in the defining module. Local cycle detection stays local; imported types carry their defining-module recursive status via import_recursive_set (previously computed-then-discarded — now used). Sound + complete because cross-module value cycles are forbidden (§4 acyclic import DAG toward std) → every genuine cycle is intra-module → caught locally + carried by the import authority.

The prerequisite (#5623)

Correctly un-marking imported-recursive-arg coproduct aliases (e.g. Witness<StructurallyEqual>) as non-recursive exposed a latent collapse defect: those aliases lost their Holds/Violates arms during resolution → VariantNotFound. #5623 fixes that at the resolution layer (preserve the peelable form). This PR depends on it.

Floor witness (permanent, this PR)

src/v2/test/claim/algebra/witness_alias_recursion_independent_test.dag — NodePairEquality = Witness<NodePair> (a nullary Witness alias over a struct whose only recursion is the imported recursive Node, structurally identical to the production StageEmissionEquality = Witness<StructurallyEqual>). The test fn asserts both coproduct arms resolve (construction-stage; VariantNotFound = RED, fail-closed). Auto-enrolled by the *_test.dag + test fn naming.

It rides this PR (not #5623) because on main + (Y')-alone the alias is still recursive (non-discriminating); only with the lever does it exercise the (Y') resolved-alias path.

Proof (by execution)

• lever + (Y') full-corpus emit = 836 files, 0 diagnostics (835 + this floor witness). The 4 production Witness VariantNotFound gone; zero net-new.
• Floor-witness green: gunbc run --claim-run --entry … --function witness_alias_resolves_holds_violates_independent_of_recursion → true.
• Floor-witness red-on-revert: lever held + (Y') reverted → variant 'Holds'/'Violates' not found in type 'NodePairEquality'; restored → true. Discriminates precisely.
• req-3 (De-fork grounding keystone: fix v2 generic type-alias instantiation so FreeMonoid aliases resolve - brief in docs plans dsl-v2-defork-audit section 3b #5552) non-regression: 32 v1-compiler-tests green incl. generic_alias_field_access_resolves_through_expansion, list_and_freemonoid_* alias-compat, *coproduct*; generic_alias_coproduct_resolves() → true.
• Production StageEmissionEquality resolution is permanently floor-gated by self_host/fixed_point_test.dag test fns (predates this work) + the corpus compile-clean gate.

Seed mirror (v1_compiler_infer.rs) hand-edited (no regen); gunbc builds clean.

Note: a follow-up (the lever's full E0308 carrier delta + 3-way termination-delta witness) lands after this; the de-nickname of is_witness_type_name (the witness-synthesis path) is filed as a separate grounded lever.

🤖 Generated with Claude Code

[gunbai-bot]

Closing as SUPERSEDED — the v3 lever shape (filter-to-local + import-authority union) was refuted by execution and abandoned per parent's signed reorientation.

Why it's dead:

• The v3 filter+union regressed target_model (cross-module field-access cascade to bare T) while import_recursive_names is an incomplete authority — an architectural fail, not a tunable.
• Root-caused by execution: main's detect_type_cycles_kahn over-marks because node_type_deps reports a LEAF NOMINAL's own identity (Symbol deps=[Symbol], opaque/alias/branded leaves) as a structural self-dependency. The kahn algorithm and import handling are correct; only the dependency-extraction input was wrong.

Replacement (parent-signed reshape): a minimal de-conflation at the dependency-extraction call site (all_deps_map) — a binding whose resolved form is a bare leaf and whose only dep is its own name contributes no self-dependency. kahn unchanged; no filter; no import-union; no 517 change. Genuine structural recursion (GrammarExpr etc.) is untouched.

Validated (apples-to-apples on identical sources): Box< 445→308, Box::new 258→123, 0 diagnostics both (no net-new); target_model 4/4; anthropic non-regression green; smoking gun (50 leaf/type-param marks dropped, 0 newly, genuine preserved). Fix-#1 is orphaned under this shape and dropped.

Replacement PR will be opened from branch session/identity-deconflate.