diff --git a/dag/gunbc/recurring_failure_mode/generic_formal_unjudged_against_a_sibling_bound_argument.dag b/dag/gunbc/recurring_failure_mode/generic_formal_unjudged_against_a_sibling_bound_argument.dag index 7bd38263d1d..a2779b8aed8 100644 --- a/dag/gunbc/recurring_failure_mode/generic_formal_unjudged_against_a_sibling_bound_argument.dag +++ b/dag/gunbc/recurring_failure_mode/generic_formal_unjudged_against_a_sibling_bound_argument.dag @@ -9,6 +9,8 @@ data generic_formal_unjudged_against_a_sibling_bound_argument: RecurringFailureM receipts: [ "INVALID STATE: a direct call to a generic function whose type parameter is already FIXED by one argument admits a later argument of a different concrete type at a formal declared as that same parameter. Measured on main 7af52ea7e2 (entry compile of a scratch probe): `pair(a: U, b: U)` called as `pair(a: Item { .. }, b: other())` with `other() -> Other` is admitted, and so is `list_snoc_item(xs: xs, item: other())` with `xs: List`. Each such argument raises only the advisory DeclaredTypeInhabitanceUndecided with reason UndecidableGenericFormal. The same argument at a CONCRETE formal (`take(b: Item)`) refuses DeclaredTypeNotInhabited in the same run, so refusal is reachable at the position and the admission is a gap, not a limit.", + "GROUND-SCALAR SPECIMEN, measured 2026-10-05 at main ed68b5573b (gunbc run and gunbc compile --entry over fixture modules): `fn pick(a: T, b: T) -> T { a }`; `take_s(s: pick(a: 'x', b: 2))` with `take_s(s: String)` is admitted and returns `x`, and `fn f() -> Int { pick(a: 1, b: 's') }` is admitted and returns 1. Each draws DeclaredTypeInhabitanceUndecided (UndecidableGenericFormal) at BOTH `a` and `b` and nothing else, so the population is the same with kernel scalars as with products. A ground scalar needs no nominal-identity carrier to decide the conflict, so this subset can be refused before the general identity-keyed trigger lands. Filed first as a separate row in gunbc#13348 and folded here on review, because it is this class.", + "HOW IT WAS FOUND: as the incompatible-applications control requested on #12931. A fold seeded with an applied `List` whose step pushes a `B` is admitted. That is NOT a fold defect: the fold's step return is judged against the accumulator (a step returning `[b]` refuses at the list element). The admission is the step's inner call, `list_snoc_item(xs: acc, item: b)`, i.e. this class.", "DISTINGUISHING FACTS. (1) The parameter is bound by a SIBLING argument at the same call; the judged argument's formal still reads as the raw type parameter, because v1.compiler.infer direct_call_argument_inhabitance_diags hands the obligation the substitution basis whenever the formal carries an unbound variable, and declared_type_inhabitance answers UndecidableGenericFormal for any generic formal. (2) NOT a spelling collision: the probe's parameter is spelled U and involves no List, and it is admitted identically. (3) NOT silent: every occurrence is a typed, located, counted advisory inside the declared drop gunbc.rung_drop.direct_call_unbound_carried_generic_compat, whose population is exactly this diagnostic, reason and position.",