Plan: land ticket 46 with surface row variables (replacing the RowConcat evidence)

1. Branch map

All feature work hangs off the same master (4c3d9ee). The new integrated series is
built on a fresh branch (e.g. df-aggregate-46-rows).

2. P1 review: what it is, compared to the submitted series

The submitted C3 (4f1b953, 443/−208 across 11 files) introduced the RowConcat
evidence mechanism to express "'gr .. 'b is the concat of rows 'gr and 'b":

• Evidence::RowConcat — a new evidence variant whose three type variables stand
  for product rows.
• A definition-site constraint dropped (desugaring would bind interface type
  vars to body-local product rows, collapsing polymorphism).
• At every call site, instantiate / type_check_with_items desugar the
  evidence into TypeEqual ×3 + RowCombine (infer.rs ~392, mod.rs ~1474).
• reify_row_concat_evidence (subst.rs) rewrites bound unifiers back into the
  scheme so the equation survives generalization.
• Mantle: the evidence lowers to an empty dictionary record (no AST node
  references it), with a corresponding empty-record minimum-alignment fix in the
  nucleus.
• Surface: .. as a type-level operator (ConcatType).

P1 (surface row variables) makes all of that machinery unnecessary, because the
crust already has first-class rows:

• Row::Open(RowVar) inside Type::Prod, TypeScheme.unbound_rows (already
  serialized, already iterated by instantiate, which maps Open → Unifier
  with fresh row unifiers and returns wrapper_rowvars).
• Instantiate::evidence already turns Evidence::RowEquation into
  Constraint::RowCombine at call sites (inst.rs:38) — the existing evidence
  type used by quotes and projections.
• substitute_wrapper already re-emits RowEquation evidence through
  generalization (subst.rs:280) — no reification step needed, because rows live
  in the scheme's unbound_rows, not hidden inside type variables.
• The solver (unify_row_comb, partial_row_combs, close_unbound_rows)
  already solves row combinations over open rows and keeps interface-reachable
  goals open.
• The mantle's lower_ty_scheme already builds a kinds vector
  (Type/Row per parameter) and folds Type::ty_fun(kind, …) for each —
  row parameters become TypAbs(Kind::Row).
• The call-site TypApp::Row emission (mantle Application lowering, the
  wrapper.rows fold) already exists — it is dead code today precisely because
  the surface can't produce row-polymorphic items.
• P0 (S1) makes TypAbs(Kind::Row) instantiate per applied row in monomorph
  and beta-reduce in simplify.

The new surface design (explicit conversion, no promotion):

• Row positions: DataFrame<…>, CachedDataFrame<…>, and (new)
  Transpose<…> take a row expression: a row variable 'x, a concat
  'x .. 'y (left-associative), or a row literal { … } (closed fields
  and/or a fragment).
• Row variables are row variables in all contexts. A 'x in a row
  position is a row variable, full stop; there is no kind pre-pass and no
  implicit promotion. Where a type position needs the product of a row
  variable, it is written explicitly as a record type with a fragment:
  {'a} means the product of row 'a (lowers to Prod(Open(r_a))).
• The record row node gains an optional fragment: { a: i64 } (closed,
  today's syntax), {'a} (fragment only), and { a: i64, 'b} (fields plus
  fragment; the mixed form desugars to a fresh row variable plus a
  RowEquation, reusing the .. mechanism). The same node is read as a
  row in row positions and as Prod(row) in type positions.
• .. desugars at lowering to a fresh row variable w plus
  Evidence::RowEquation { left: 'x, right: 'y, goal: w } in the scheme's
  evidence — which lower_typ already returns and which
  item_source.register_with_visibility already puts into the item scheme.
  No new evidence variant, no desugaring at call sites (the existing
  RowEquation path does it), no reification, no empty-dict record.
• 'x in other type positions (function arrows, Quote<…>, []…,
  sums, …) is a type variable exactly as today — unchanged semantics.
• Definition-site enforcement is possible (unlike RowConcat): the equation
  references only interface rows, so it does not collapse polymorphism; the
  solver keeps the goal open (reachable from the signature) and the equation
  re-emerges in the scheme. Checkpoint during S4: confirm the solver handles
  an interface-only RowCombine at the definition site without over-constraining.

Backward compatibility: DataFrame<'a> / CachedDataFrame<'a> switch from a
type variable to a row variable (the position determines the kind); any use
of that name in a type position (e.g. Quote<'a -> bool>) must be written
Quote<{'a} -> bool> — an explicit, reviewable migration in S3 (df.blr and
the df type_check tests). Elsewhere, 'x in type positions is untouched.
The expected observable change is snapshot churn
(DataFrame(Var(TypeVar(0))) → DataFrame(Prod(Open(RowVar(0))))); the 174
integration tests are the behavioral oracle.

3. The new series (replaces the sent 6 commits)

Each commit: full suite green + cargo fmt --check + clippy clean. Built on
df-aggregate-46-rows off master.

What gets deleted (never exists in the new series)

• Evidence::RowConcat and every arm around it (crust enum, sexpr, inst, linearity-adjacent handling).
• The TypeEqual ×3 + RowCombine desugaring at both call sites (infer.rs instantiate, type_check_with_items).
• reify_row_concat_evidence (subst.rs).
• The definition-site-drop behavior (no longer needed — see §2).
• The mantle empty-dictionary special case for RowConcat in lower_ev_ty / item lowering.
• The type-level .. (ConcatType) surface syntax and its air nodes.

What changes shape

• Transpose<'a>: type-variable parameter → row position (S5).
• All DataFrame<'a> / CachedDataFrame<'a> surface signatures: type variable →
  row variable (S3); type-position uses of a frame row are written {'a}
  (S3 migration).
• The record row syntax gains an optional fragment {'a} / { a: i64, 'b} (S3/S4).
• The instance mechanism: N-ary types → N-ary (type|row) args (S6).

4. Risks / checkpoints

1. S3 compatibility — field access inside quotes against Prod(Open(r))
   (vs today's bare unifier that the solver treats as a product). The 174-test
   e2e suite + type_check snapshots are the oracle; expect localized solver or
   snapshot fixes, not redesigns.
2. S3 migration surface — find every type-position use of a frame-row name
   (df.blr, type_check tests) that must become {'a}; the compile errors are
   the checklist.
3. lower_ty_scheme parameter ordering — the kinds/.rev() handling with
   mixed (type, row) parameters; the call-site TypApp application order must
   match the TypAbs order in the scheme. Verify in S3 and again in S6.
4. lower_ty_scheme parameter ordering — the kinds/.rev() handling with
   mixed (type, row) parameters; the call-site TypApp application order must
   match the TypAbs order in the scheme. Verify in S3 and again in S6.
5. Definition-site RowEquation (S4) — confirm the solver keeps an
   interface-only RowCombine partial and re-emits the evidence unchanged
   through substitute_wrapper.
6. LALR conflicts (S3/S4) — 'ident is already a TypeExpr; the row
   expression non-terminal and the record-fragment alternative are separate
   production contexts, but the {…} row literal shared between row and type
   positions and the .. in row positions need the generated parser checked.
7. Entry items (main(d: DataFrame<'a>)) remain broken for both kinds
   (pre-existing nucleus gap, verified empirically); out of scope.
8. Ticket #47 (duplicate wasm export) is orthogonal; row-aware mangling
   makes per-row instances distinct but does not fix the underlying dedup.

5. Process

• Everything stays under ticket 46 (no new ticket): all commits reference
  Ticket: #46.
• The finished series is one git send-email master..HEAD replacing the sent
  6-commit series (note the replacement in the email body and a ticket 46
  comment).
• Delete rework-backup, aggregate-46, df-aggregate-surface once the new
  series is sent; keep df-aggregate-46-clean as the sent-series reference
  until 46 lands.
• Ticket 46 stays in_progress (under review) throughout; status changes only by
  the user.