Stop fabricating List<Unit> for an empty list with no expected type

[gunbai-bot]

An empty list literal with no expected type answered List<Unit>. It cannot know its element type there, and instead of saying so it substituted a confident wrong answer.

Why it survived

List<Unit> reads as fully resolved. The if-join already carries re-inference for exactly this case — where one branch is under-resolved and the other is not, re-infer the first against the second — and a fabrication that looks resolved switches that repair off.

So the defect did not merely produce a wrong type. It consumed the mechanism that existed to correct it. That is why the RED needs both branches empty, and why the one-typed-branch case is green on main today.

The repair answers a fresh type variable — how "I do not know the element type yet" is already spelled everywhere else in this module (lambda_param, callable_param). One line.

Two arms, by execution

Same witness, same sources, same flags, on main f84c91b774a. The only difference is the fix:

	unpatched	patched
both branches empty (the RED)	false	true
one typed branch (positive control)	true	true

The control holds in both arms, so it discriminates rather than tracking the fix — it says the repair did not buy its green by making the checker blind. Before the witness existed, the same pair was measured directly at the compile boundary: the RED source refused with no field 'label' on type 'Unit', the control compiled clean.

The fixture

fn both_empty(flag: Bool) -> List<String> {     // RED
  let picked = if flag { [] } else { [] }
  picked |> map(r => r.label)
}

fn one_typed(flag: Bool, given: List<Row>) -> List<String> {   // control
  let picked = if flag { [] } else { given }
  picked |> map(r => r.label)
}

Scope

This is not namespace work and needs no qualified reference. It was found while working integration/namespace-cut (#8282, now frozen) and reproduces on main in six lines. It is the first of several defects being extracted from that branch and landed independently, per operator ruling.

The witness declares SubstrateInputsOnly — without a live-tree disposition the floor's fail-closed default declines it and it would never run. Its not-runnable arm returns false rather than a count, so a census that could not be taken cannot read as a clean compile.

The mirror is regenerated, not hand-edited: required-regen over the 135-module closure drifts exactly one file by exactly the one line, and the final green above was measured against that regenerated mirror with zero scratch markers present.

[gunbai-bot]

Returning this to draft. It is approved by two reviewers and it regresses real corpus code — the approvals were right about what they examined and the regression is outside what a diff review can see.

What CI caught

dag/extdeps/render/terminal.dag refuses with no field 'kept' on type 'Unit'. Two arms, same file, same flags, only the fix differing:

	blocking
pristine main	0
with this fix	1

So this is a regression I introduced, not a latent defect the fix surfaced. I want to be precise about that distinction because I would have preferred the second reading.

Reduced to 20 lines

fn f(spans: List<Span>, budget: Int) -> Int {
  let state = fold(spans,
    init: Present { value: { kept: [], remaining: budget } },
    f: (acc, span) => match acc {
      Absent => none
      Present { value: st } =>
        if st.remaining <= 0 { acc } else {
          match w(s: span) {
            Present { value: n } => Present { value: { kept: concat(st.kept, [span]), remaining: st.remaining - n } }
            Absent => none
          }
        }
    }
  )
  match state { Present { value: s } => s.kept |> count  Absent => 0 }
}

The trigger is a nested match inside the fold step whose arms include none. Without that nested match the same shape compiles clean under the fix — I checked both.

Why the fix is incomplete rather than wrong

List<Unit> was wrong but concrete, so st.kept type-checked. A fresh type variable is honest but unresolved, and the join across the step's arms cannot yet close it — it renders as Unit and the field access fails.

So the fabrication was load-bearing for exactly the reason it was worth removing: downstream code depended on getting some concrete answer, and the machinery that should resolve the honest answer does not reach this position. Removing the fabrication is still right; it needs the resolution path to arrive with it, which is more than one line.

The original argument stands and the two-arm receipt stands — the enrolled witness still goes red-then-green. What it did not cover is a fold accumulator whose element type must be closed through a multi-arm step, and no fixture I wrote would have caught that. CI over the real corpus did.

Next

I will either narrow the change to positions where the variable can be closed, or land it together with the resolution path. Not merging it in this state.

Also of note for the program ledger, measured while diagnosing this: defect I (the parser guard) drops out of the extraction queue entirely. qualified_ctor_literal_here does not exist anywhere on main, and main parses a qualified constructor literal in condition position cleanly — verified by execution. Extracting it would add a second implementation of behaviour main already has, with no possible main-red fixture.

— sent from crisp-crab-430