Skip to content

Narrow polymorphic variant row at ...rest catch-all#8382

Open
jfrolich wants to merge 1 commit intorescript-lang:masterfrom
jfrolich:poly-narrowing
Open

Narrow polymorphic variant row at ...rest catch-all#8382
jfrolich wants to merge 1 commit intorescript-lang:masterfrom
jfrolich:poly-narrowing

Conversation

@jfrolich
Copy link
Copy Markdown
Collaborator

Summary

In a switch over a polymorphic variant, | ...rest => (optionally ...rest as r) now binds rest to the residual row — the scrutinee's row at that structural position minus the tags matched by earlier unguarded arms — instead of inheriting the full row.

Before

let fn = (r: result<int, [#Foo | #Bar | #Baz]>) =>
  switch r {
  | Error(#Foo)   => Ok()
  | Error(...rest) => Error(rest)  // rest : [#Foo | #Bar | #Baz]  ← loses narrowing
  | Ok(a)         => Ok(a)
  }

After

// rest : [#Bar | #Baz]  — #Foo is marked absent in the residual
let fn = (r: result<int, [#Foo | #Bar | #Baz]>) =>
  switch r {
  | Error(#Foo)   => Ok()
  | Error(...rest) => handleBarBaz(rest)   // type-checks: rest fits [#Bar | #Baz]
  | Ok(a)         => Ok(a)
  }

Scope

Works for:

  • Closed ([#A | #B | #C]) and open ([> #A | #B], inferred rows, row_fixed) scrutinee rows.
  • Top-level ...rest and nested positions: inside constructors (Error(...rest)), record fields ({inner: ...rest}), tuple elements with permissive siblings ((_, ...rest)), and variants-within-variants (#Outer(...rest)).
  • ...rest as r — the alias also binds to the narrowed type.
  • Or-patterns in earlier arms: | #A | #B => subtracts both tags.
  • Guards on earlier arms suppress subtraction (a guarded arm can fall through).
  • Guards on the ...rest arm itself — it doesn't contribute to the matched set so later arms see the same matched-so-far.

Design

Type-checker-only. No parser changes, no new AST constructors, no new keywords.

  1. Pre-pass in type_cases (annotate_rest_nodes_with_matched_tags) walks each arm's Parsetree.pattern tracking a structural path (constructor / tuple index / record field / variant payload) and, for every Ppat_type + res.patFromVariantSpread node, attaches a new res.polyVariantNarrowMatchedTags attribute whose payload lists the tags matched by earlier unguarded arms at the same path.

  2. extract_matched_at_path collects what each arm unconditionally handles:

    • Ppat_variant (tag, _) → one match at the current path.
    • Ppat_orunion of branches (both branches together cover their tags).
    • Ppat_tuple / Ppat_record → descend into a sub-position only if every other sub-position is permissive (Ppat_any / Ppat_var), avoiding unsound subtraction from conditional patterns like (#A, #B).
  3. build_ppat_or_for_variant_spread gets a new first branch: when expected_ty expands to Tvariant row, rewrite Ppat_type + spread attr to Ppat_var + matched_tags attr and return the narrowed type so the outer Ppat_alias (…, r) handler propagates the narrowed type onto r.

  4. Btype.narrow_row_by_tags (new helper) produces the residual: matched tags become Rabsent; row_fixed and row_closed are inherited; row_name is dropped; row_more is a fresh variable so the residual is isolated from the source.

  5. Ppat_var handler consumes the matched-tags attribute and binds the variable (enter_variable) to the narrowed row. pat_type stays at expected_ty (the full scrutinee row) so per-arm unification in type_cases and parmatch's exhaustiveness checks still see a full catch-all.

Soundness

  • Tag-lifting through tuple/record positions is gated on sibling permissiveness. (#A, _) subtracts #A at position 0 (sibling is _); (#A, #B) subtracts nothing (neither position's match is unconditional). This preserves the invariant that a tag marked absent in the residual is truly unreachable at that path regardless of the sibling positions' runtime values.
  • Guarded earlier arms don't contribute: a #P when g => arm can fall through when g is false, so #P stays reachable in later arms.
  • When the residual is empty (every declared tag is matched on a closed row), parmatch emits the standard Warning 11 ("this match case is unused") — no new plumbing needed.

Tests

Thirteen integration tests in tests/tests/src/poly_variant_narrow_test.res:

Case
Basic single-tag subtraction
Or-pattern subtracts both tags
...rest as r binds both names to the narrowed type
Guarded earlier arms are not subtracted
Nested: Error(...rest)
Open row: inferred scrutinee, residual closes to exactly match a closed consumer
Explicit [> ...] annotation
Record field nesting
Tuple with permissive sibling
Multiple constructors at independent paths (First(...) vs Second(...))
Guard on the ...rest arm itself
Variant-within-variant (#Outer(...rest))
Prenex-quantified row ('a. ([> …] as 'a) => … — exercises row_fixed)

Plus two super_errors fixtures:

  • polyvariant_narrow_wrong_type.res — passing the residual to a function that expects a narrower row produces a clear "doesn't include constructor" error.
  • polyvariant_narrow_unreachable.res — pinning the Warning 11 behavior when every declared tag is already matched.

Files changed

File Change
compiler/ml/typecore.ml Path type + walkers + pre-pass, poly-variant branch in build_ppat_or_for_variant_spread, narrow-aware Ppat_var handler
compiler/ml/variant_type_spread.ml mk_poly_variant_narrow_matched_tags_attr / get_poly_variant_narrow_matched_tags
compiler/ml/btype.ml + .mli narrow_row_by_tags
tests/tests/src/poly_variant_narrow_test.res (+ generated .mjs) 13 integration tests
tests/build_tests/super_errors/fixtures/polyvariant_narrow_*.res (+ .expected) Two regression snapshots
CHANGELOG.md Entry under :rocket: New Feature

Test plan

  • make test — full suite green
  • node scripts/test.js -mocha — all 13 new integration tests pass
  • node ./tests/build_tests/super_errors/input.js — new snapshots match, no unrelated snapshot churn
  • make checkformat — OCaml/ReScript/JS/Rust formatting clean

In a switch over a polymorphic variant, `| ...rest =>` (optionally
`...rest as r`) now binds `rest` to the scrutinee's row at that
structural position minus the tags matched by earlier unguarded arms,
rather than inheriting the full row. Works for closed and open rows,
for top-level scrutinees and nested positions (`Error(...rest)`,
`{field: ...rest}`, tuples with permissive siblings).

Implementation is type-checker-only, no parser changes. A pre-pass in
type_cases walks each arm's pattern, attaches a
res.polyVariantNarrowMatchedTags attribute to each Ppat_type+spread
node carrying the tags matched at the same structural path in earlier
arms. build_ppat_or_for_variant_spread rewrites the node to Ppat_var;
the Ppat_var handler reads the attribute and binds the variable via
the new Btype.narrow_row_by_tags helper, while pat_type stays at the
scrutinee's type so arm-wise unification and exhaustiveness checking
continue to see a full catch-all.

Signed-off-by: Jaap Frolich <jaap@tella.com>

Co-Authored-By: Claude Opus 4.7 (1M context) <noreply@anthropic.com>
@pkg-pr-new
Copy link
Copy Markdown

pkg-pr-new Bot commented Apr 21, 2026

Open in StackBlitz

rescript

npm i https://pkg.pr.new/rescript@8382

@rescript/darwin-arm64

npm i https://pkg.pr.new/@rescript/darwin-arm64@8382

@rescript/darwin-x64

npm i https://pkg.pr.new/@rescript/darwin-x64@8382

@rescript/linux-arm64

npm i https://pkg.pr.new/@rescript/linux-arm64@8382

@rescript/linux-x64

npm i https://pkg.pr.new/@rescript/linux-x64@8382

@rescript/runtime

npm i https://pkg.pr.new/@rescript/runtime@8382

@rescript/win32-x64

npm i https://pkg.pr.new/@rescript/win32-x64@8382

commit: fb1ed3a

Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment

Labels

None yet

Projects

None yet

Development

Successfully merging this pull request may close these issues.

1 participant