De-fork grounding keystone: fix v2 generic type-alias instantiation so FreeMonoid aliases resolve - brief in docs plans dsl-v2-defork-audit section 3b

[gunbai-bot]

De-fork grounding keystone — generic type-alias instantiation for coproduct aliases

Brief: docs/plans/dsl-v2-defork-audit.md §3b (operator ruling), phase 1 — the keystone. Also docs/plans/fold-ergonomics.md Root B #1 / dissolve-on feature:free-monoid-entry-generic-inference. Scope = keystone only; def-unification (phase 2), repoints (phase 3) and 🟡-marker dissolution (phase 4) are later PRs.

The bug

A non-parametric alias whose RHS is an applied generic coproduct — type QualifiedName = FreeMonoid<Symbol> — did not expand to its underlying coproduct, so the FreeMonoid variants (Empty | Cons) were unreachable through the alias name. This forced consumers (qualified_name.dag, catalog.dag fold_list, ParseTable) to hand-roll a parallel coproduct + eq/for_all.

Before (match on an alias-typed value):

type QName = FreeMonoid<Symbol>
fn qname_len(qn: QName) -> Int {
  match qn { Empty => 0  Cons { head: _, tail: t } => 1 + qname_len(qn: t) }
}

error: variant 'Empty' not found in type 'QName'
error: variant 'Cons'  not found in type 'QName'

The same value typed directly as FreeMonoid<Symbol> matched fine — the bug was purely the alias indirection.

After: resolves and runs (qname_len over a 3-element path returns 3; length, field-binding and the Empty variant all work through the alias).

Root cause & fix

In src/v1/04_resolve.dag resolve_node_bounded, a bare alias reference followed one level of .inferred to the un-instantiated applied-generic node (FreeMonoid<Symbol>, NoConnective with type-arg children) but never ran the generic instantiation that the direct-use branch (is_user_generic_use_site) already performs. The fix runs that same instantiation one pass when the alias target is an applied generic.

• Falls out of the existing model — reuses resolve_generic_use_decl + resolve_node_bounded; no special-case patch, no substrate change.
• Gated to Disj (coproduct) decls — principled and found by execution: leaving it ungated instantiated record aliases too (Nat = CommutativeSemiring<Magnitude>), breaking Optional<alias> Present/Absent synthesis (17 dsl errors). Records must stay the bare applied node; the gate is the §5 fail-closed boundary.
• Emitted seed (v1_compiler_infer_resolve.rs) hand-synced to the .dag.

Verification (green by execution)

• CI floor discovery corpus: 694/694 PASS (zero type-resolution regressions tree-wide).
• dsl whole-tree compile --target rust: 0 diagnostics.
• Durable RED-on-revert witness: src/v2/test/claim/algebra/generic_alias_coproduct_instantiation_test.dag — constructs, matches and recurses through type SymbolPath = FreeMonoid<Symbol>; reverting the fix makes it fail to typecheck (a wall, not a passive assertion).
• cargo fmt --all --check clean; cargo clippy -p v1-compiler --all-targets -- -D warnings clean. (The floor's rust_monolith_gate flagged during the run was sccache infra flakiness, not this change.)

🤖 Generated with Claude Code