Skip to content
Merged
Changes from all commits
Commits
File filter

Filter by extension

Filter by extension

Conversations
Failed to load comments.
Loading
Jump to
Jump to file
Failed to load files.
Loading
Diff view
Diff view
Original file line number Diff line number Diff line change
Expand Up @@ -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<U>(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<Item>`. 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<T>(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<A>` 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.",
Expand Down