Plan: Quote row semantics — de-isolate, fix scheme quantification, keep rows open where possible

Status: implemented (2026-07-10; deviations noted at the end)
Date: 2026-07-10

Goal

lang/tests/type_check/frame_row_mismatch.blr should not be a type error:

df::show(df::filter(df::filter(df::fromcsv("test.csv"), :( fn (r) => r.a > r.b )),
                        :( fn (r) => r.c > r.d )))

Inference should infer the chained frame as DataFrame<{a: i64, b: i64, c: i64, d: i64}>.

Semantics: Quote<fn R -> bool> means "the quoted code's parameter row contains the
fields it references" (observed fields ++ unknown remainder), instead of today's
"the parameter has exactly this row".

Investigation

Why the test fails today

Verified by instrumenting check_quote_inner (temporary prints, since reverted).

1. filter : DataFrame<'a> -> Quote<'a -> bool> -> DataFrame<'a>
   (stdlib/src/df.blr:10) instantiates 'a to one fresh type unifier ~f shared by the
   frame row, the quoted parameter type, and the returned row.
2. The quote is checked in an isolated TypeInference (check_quote_inner).
   Field access builds row-superset evidence in the inner context:

   TypeEqual(Prod(~r0), ~u)          -- r's row is row var ~r0
   RowCombine({a:~ta}, ~rest1, ~r0)
   RowCombine({b:~tb}, ~rest2, ~r0)
   

   The two combinations share goal ~r0 but are not merged during solving
   (is_unifiable's two-out-of-three rule needs an equatable left or right).
3. close_unbound_rows (quote contexts only) pins ~r0 := {a,b} exactly — the
   remainder vars are discarded. Exact-row semantics.
4. The quote reports closed Quote<Abs(Prod(Closed{a,b}), Bool)>; inner variables die at
   the boundary.
5. Outer call 1: ~f1 := Prod({a,b}). Call 2: ~f2 = ~f1, second quote reports
   Prod({c,d}), unify_row_row's Closed/Closed requires identical field lists →
   RowsNotEqual({c,d} != {a,b}).

Why the isolation exists (history)

• Introduced in 63acc3d: "the quoted code's row evidence and unsolved variables never
  leak into the enclosing item's scheme (an open-row record select would otherwise keep
  main polymorphic and drop it during monomorphization)".
• The drop, end to end (verified in code):
  1. An unsolved body-local unifier survives to item end.
  2. substitute_ty/expr turns it into a fresh rigid var and marks it unbound
     (subst.rs tyvar_for_unifier/rowvar_for_unifier); the unbound sets from the
     typed expr, the wrappers, and the evidence all merge into
     TypeScheme.unbound_tys/unbound_rows (crust/mod.rs:1040-1087) — so a variable
     that appears only in the body ends up quantified in the item's scheme.
  3. The mantle wraps the item type in one TypAbs per scheme quantifier
     (mantle/mod.rs:900 lower_ty_scheme).
  4. monomorph_module partitions items by is_mono_type(typ);
     Type::TypAbs(_) => false (monomorph.rs:279-291) → the item is "poly".
  5. Poly items survive only if some call site recorded an instance for them
     (monomorph.rs:26-55, instances map). main is the entry point: nothing ever
     calls it, so no instance is recorded → unwrap_or_default() → main silently
     disappears from the emitted module (WASM has no generic functions; the entry
     point must be a concrete export).
• The quantifier is vacuous: the row var is not in main's signature
  (() -> i64). The system conflates "unsolved somewhere in the item" with "the item is
  parametric in this variable".
• The same series (0233f2f) added default_body_local_ty_unifiers for the identical
  problem on type unifiers. Isolation, type defaulting, and (later) quote row-closing
  are three parallel stopgaps for one root problem: body-local unsolved unifiers
  quantifying the enclosing item.

Can open rows just be handled, without closing/defaulting?

Yes — for liveness. Rows are phantom in codegen (frame is an i32 handle;
is_mono_type(DataFrame(_)) => true; the row flows into exactly two artifacts):

1. Instance mangling (monomorph_symbol, sexpr of the type arg). An open row has a
   deterministic sexpr ((row N)-ish); the same unsolved var shared by several call
   sites yields the same name → instance dedup still works. filter[(prd (row 5))] is
   a perfectly good mangled name.
2. Emitted code: none. subst_typ with an open row is a no-op on filter's body;
   the host _filter is monomorphic. filter[(row 5)] and filter[{a,b,c,d}] are
   byte-identical in WAT.

So an open row as an instance argument is first-class. The only things that actually
break are: (a) the scheme quantification above (main dropped), and (b) informative
types/names — without closing, the final type shows an open row, not {a,b,c,d}, which
fails the stated goal. Both have targeted fixes that avoid blanket closing/defaulting:

• (a) Scheme hygiene: quantify only variables the signature mentions.
• (b) Row closing as computation, not hygiene (see below) — still needed to make the
  inferred type name all four fields, but no longer load-bearing for liveness.

Boundary of "just handle the open row": an open row inside a real record/sum layout
is code-relevant (ABI field order), so is_mono_type(Row::Open) => false must stay for
those. In v1 open rows only occur in the phantom DataFrame-parameter position (source
syntax has no open-row row spelling; lower_row_inner always builds closed rows), so
this never actually fires.

Design

1. De-isolate the quote — crust/infer.rs

• Expr::Quote infer arm: self.infer(env, *inner), wrap in Type::Quote.
• check arm (Expr::Quote, Type::Quote(inner_ty)): self.check(env, *inner, *inner_ty)
  (the pre-63acc3d shape).
• Delete check_quote_inner, translate_ty, translate_row, default_unbound, and the
  lossy error re-emit (which panic!s on any inner error kind other than
  TypeNotEqual — a live bug: RowsNotEqual inside a quote panics the compiler).
• Row evidence (RowCombine) now lives in the outer context directly; filter's 'a
  unifies the frame row with the quoted parameter row ~r0; chained filters accumulate
  combinations on the same goal. No leaking mechanism.

2. Scheme hygiene — the real fix for the main-drop bug class — crust/mod.rs

In type_infer_with_items, after all substitution/merging, intersect the scheme's
quantifier sets with the variables reachable from the signature type (the existing
collect_unifiers reachability walk, extended per §4):

scheme.unbound_tys   = unbound_tys   ∩ reachable(typ)
scheme.unbound_rows  = unbound_rows  ∩ reachable(typ)

• Fixes the bug class at the root: a variable that floats only in the body no longer
  makes the item parametric. Applies to rows and types uniformly.
• evidence filters itself: normalize_mentioned_row_combs only keeps combinations
  that mention scheme-quantified vars, so for main the leftover combinations are
  simply dropped (they are pure evidence, referenced by nothing), and for a generic item
  they become Evidence::RowEquation re-injected at call sites
  (inst.rs:45, mod.rs:1136) — the machinery already built for this.
• default_body_local_ty_unifiers stays (not replaced): an open type var at a
  code-relevant position cannot reach codegen (add-[(t5)] — no such host function,
  unknown representation). Rows don't need an analog, because rows are phantom:
  leftover row vars (e.g. ~rest) live only in combinations/evidence and are either
  dropped (main) or re-instantiated (generic items).

3. Row closing, demoted to type computation — crust/unification.rs, mod.rs

Generalize close_unbound_rows with the same reachability filter (close only pending
goals unbound and unreachable from the signature), run at the existing slot
(mod.rs:1032, before substitution). Its role changes from keeping the item
monomorphic (§2 does that now) to computing the informative concrete row:

• Test flow: the four leaked combinations on ~r0 close it to {a,b,c,d} (merging
  lefts, unifying shared-field types — extract the merge into a helper; a merge
  conflict must surface as TypeError, not be silently swallowed, which the isolated
  code does today via default_unbound); the rest rows close to their diffs;
  ~ta..~td default to Int via the existing pass.
• The goal is met literally: the frame's type in the typed module is
  DataFrame(Prod(Closed{a:i64,b:i64,c:i64,d:i64})), and instances mangle as
  filter[{a,b,c,d}].
• Proof of demotion (regression guard): show(df::fromcsv(p)) (unconstrained row)
  compiles and emits main with fromcsv[(row N)]-style instance names even though
  nothing closes that row — i.e. liveness no longer depends on closing.

4. Reachability helper — crust/infer.rs

Extend collect_unifiers/collect_row_unifiers to also collect Row::Unifier /
Row::Open nodes (today only closed-row field types), so "reachable from the signature"
covers row vars through solved type unifiers ('a → Prod(~r0)). Used by §2 and §3.

5. stdlib — no changes.

Tests

1. Type check: rename frame_row_mismatch → frame_row_accumulate; .typ becomes a
   typed module with the frame at DataFrame(Prod(Closed{a,b,c,d})) and empty
   scheme quantifiers for main. missing_field stays negative.
2. Open-row liveness (the new guarantee): an item whose frame row is never closed
   (e.g. df::show(df::fromcsv("test.csv")) — already in the integration set? add
   df_unconstrained.blr if not) must still emit a working main; WAT shows
   fromcsv[(... open row ...)] naming and byte-identical host calls.
3. Generic item: fn f(df: DataFrame<'a>) -> DataFrame<'a> { df::filter(df, :(fn (r) => r.x > r.y)) } — snapshot: row-polymorphic scheme, row-equation evidence
   (intended improvement over today's row-monomorphic {x,y}); verify instance
   mangling at a concrete call site.
4. Integration: df_chain2.blr = the goal expression, run end-to-end; std::df
   instances mangle filter[{a,b,c,d}]; host filter executes. df_filter/df_chain
   stay green.
5. Unit (crust/tests.rs): de-isolated quote infer/check; scheme hygiene (body-only
   unifier → not quantified; signature-reachable → quantified); filtered closing
   (body-local → union; reachable → open); merge-conflict TypeError; inner
   RowsNotEqual surfaces instead of panicking.
6. Gates: workspace cargo test, cargo fmt, cargo clippy --workspace -- -D warnings; snapshot audit — expect: renamed type-check snapshot, generic-item
   snapshot, crust tests whose schemes change (body-local quantifiers disappear —
   review each), instance names in df WAT.

Work items

Ordering note: S2 is independently valuable (root fix for the isolation's original
bug) and de-risks S3: after S2, de-isolating the quote can no longer drop main, so S3
and S4 become orthogonal (S4 only affects the displayed row).

Deviations from the written plan

• Hygiene evidence rule refined by a regression: the first cut dropped all
  evidence over non-signature vars, which broke the wand combinator — its row
  equations name signature rows but introduce derived rows (goal/rest) that are part
  of the item's interface (evidence lowers to an implicit dictionary parameter). Rule
  as landed: keep equations naming ≥1 signature variable; quantify everything the kept
  equations name (wand behavior byte-identical).
• LowerTypes local vars (new mechanism, not in plan): body-local rigid row vars
  in body types (pre-S4 state, and any future open-row position) hit the mantle's
  ICE: Unexpected open row panics. LowerTypes now maps semantic vars absent from
  the scheme env to fresh local mantle type vars starting after the scheme's
  quantifiers, per-var consistently, so shared open rows get consistent instance names.
• df_chain2 uses b > a then c > b, not the goal expression's a > b / c > d
  verbatim: the runtime CSV has no d column (the host would fail to plan the d
  projection). The a/b/c/d accumulation is covered by the type-check test
  frame_row_accumulate; the integration test exercises the same mechanism end-to-end
  (row accumulates {a,b} then {a,b,c}; both filter instances dedup to one export
  mangled with the closed row).
• Merge-conflict diagnostics carry the item's node id (row combinations do not
  store per-field node ids); the conflict is a TypeNotEqual kind. Triggering it
  needs two predicates typing the same field differently, which the v1 node set cannot
  express (field types default to i64), so there is no end-to-end test — the unit
  path is exercised by code inspection only.
• df_unconstrained was not added: the pre-existing df.blr integration test is
  exactly that case (show(fromcsv(p)), no predicates); it stays green and its WAT
  keeps the pre-change fromcsv[(int)]/show[(int)] mangling.

Risks

• Scheme-shape churn: S2 changes TypeScheme quantifier sets for any item with
  body-local unsolved vars; snapshots encoding them change. Each change should be a
  removal of a vacuous quantifier — review for that shape.
• Mangling with open rows: filter[(prd (row N))] names are new territory in
  instance recording/dedup (monomorph.rs) and cross-module instances requests
  (std::df). Deterministic per compilation; verify dedup and the stdlib_guard test.
• Rigid vars in body annotations: unsolved unifiers become rigid RowVar/TypeVar
  in the typed body and flow through mantle lowering; confirm simplify/subst_typ
  treat them as inert terms (they should — they're already how generic params work).
• Merge-conflict diagnostics: two quotes using the same field with conflicting
  types must produce a clean TypeError, not a panic or silent swallow (pre-existing
  weakness; fixed in S4).
• is_mono_type(Row::Open) => false stays: correct for real record layouts; in v1
  open rows only reach phantom positions. If source syntax ever allows open-row
  annotations on record values, this needs revisiting (out of scope).
• Semantic loosening: filter accepts predicates over a subset of the frame's
  fields; the inferred row is an under-approximation of the CSV schema. Document in
  knowledge/design/dataframe-row-types.md (supersedes decision 4 and the
  "Quote row-closing" deviation).