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

[jfrolich]

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_or → union 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

[pkg-pr-new]

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

[fhammerschmidt]

@codex review

[chatgpt-codex-connector]

💡 Codex Review

Here are some automated review suggestions for this pull request.

Reviewed commit: fb1ed3ac02

ℹ️ About Codex in GitHub

Your team has set up Codex to review pull requests in this repo. Reviews are triggered when you

• Open a pull request for review
• Mark a draft as ready
• Comment "@codex review".

If Codex has suggestions, it will comment; otherwise it will react with 👍.

Codex can also answer questions or update the PR. Try commenting "@codex address that feedback".

[chatgpt-codex-connector]

Require permissive payload before subtracting a variant tag

Do not record the parent tag as definitely matched when a polymorphic-variant arm has a selective payload pattern. With | #A(#B) => ... | ...rest => ..., the first arm does not handle all #A values, but this code always adds (path, "A"), so the later ...rest can be narrowed as if #A were impossible. That can mis-type rest (e.g. rejecting valid #A(#C) flow or allowing code that assumes #A cannot appear). The parent tag should only be subtracted when the payload pattern is permissive.

Useful? React with 👍 / 👎.