04_resolve: preserve peelable form for non-recursive coproduct-container aliases (Witness arms)

[gunbai-bot]

What

Extend the 04_resolve children==0 lazy-return branch to preserve the peelable form for non-recursive coproduct-container aliases (e.g. Witness<C> = Holds | Violates), exactly as it already does for recursive types.

} else if n.children |> count == 0 {
    let n_target_is_coproduct_container = match n.inferred { Present { value: Resolved { node: target } } =>
        target.connective == NoConnective && target.children |> count > 0
        && is_container_type(name: target.name)
        && resolve_generic_use_decl(env: env, n: target).connective == Disj   _ => false }
    if is_recursive_type_for(env: env, node: n) || n_target_is_coproduct_container {
      NodeResolveResult { resolved: n, diagnostics: [] }   // preserve; do not collapse
    } else { ... unchanged ... }

Why (one concept, two structural inhabitants — §3)

The lazy-return NodeResolveResult { resolved: n } is a single "preserve the peelable form — do not collapse" behavior. It is inhabited by two structural conditions:

1. is_recursive_type_for(n) — a recursive type cannot be eagerly expanded (pre-existing);
2. n_target_is_coproduct_container — a non-recursive alias whose target is a registered container (is_container_type) with a Disj declaration; collapsing it drops the coproduct arms.

A nullary alias to a generic coproduct container whose only recursion is an imported recursive type is correctly un-marked non-recursive once cross-module recursion-marking is fixed (separate lever PR). Before this fix, such an alias was collapsed during resolution → its Holds/Violates arms were dropped → VariantNotFound at match sites (e.g. self_host.dag StageEmissionEquality = Witness<StructurallyEqual>). This change makes the non-recursive case resolve to the same peelable form the recursive case produced — recursion-independence — so existing downstream variant resolution fires regardless of recursion-marking.

Name-free / §3-clean: keys on is_container_type (= map_get(container_type_arity, name).is_present, container-registry membership) AND resolve_generic_use_decl(target).connective == Disj. No literal "Witness"; is_witness_type_name untouched.

Genealogy (why not the broader version)

The first attempt — a blanket || n_is_resolved_alias (any resolved alias lazy) — over-broadened: it forced struct aliases lazy too, breaking generic-lambda field-access element-type unification. 3-way emit control:

state	full-corpus emit
pristine main	835 files, 0 diagnostics
blanket-alias-only on main	6 errors (02_parse p.name/p.expression → field on type 'T')
this fix (narrow) on main	835 files, 0 diagnostics (no-op)

The narrow is_container_type && Disj gate leaves struct aliases (Conj decls) on the unchanged collapse path.

Proof (by execution)

• No-op on main: this fix only — full-corpus emit = 835 files, 0 diagnostics == pristine main.
• Red-on-revert (emit causality): with the cross-module recursive-set lever held (separate PR) and this fix absent → 4× VariantNotFound at self_host.dag:51 (StageEmissionEquality Holds/Violates); with this fix → 0. The toggle is the proof.
• Generic-alias resolution preserved: cargo test -p v1-compiler-tests — generic_alias_field_access_resolves_through_expansion ✓ (the exact path the blanket version broke), list_and_freemonoid_* alias-compat ✓ (10), *coproduct* ✓ (20), real_optional_coproduct_* ✓.

Sequencing

This is the prerequisite. The cross-module recursive-set fix (the lever) that exposes the recursion-masked sites lands as a follow-up PR rebased on this one, carrying a permanent floor witness for the resolution + its red-on-revert.

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

🤖 Generated with Claude Code