fix(checker): unify implementation targets with a shared substitution and an occurs check #448

Merged

argus merged 2 commits from loop/441-checker-overlap-occurs-check into main 2026-10-24 02:21:14 +00:00

Conversation 2 Commits 2 Files changed 8 +206 -29

orion commented 2026-10-23 23:13:48 +00:00

Collaborator

Copy link

Closes #441

What and why

reportOverlap asked couldUnify twice, once for the targets and once for the trait applications, and couldUnify was stateless: every generic parameter unified with anything. So Tensor<Scalar> with Multiply<Scalar> beside extend<Scalar> Tensor<Scalar> with Multiply<Tensor<Scalar>, Tensor<Scalar>> was refused, although Scalar = Tensor<Scalar> has no solution.

couldUnify is now a real unification over one substitution that is shared by the target pair and the trait pair:

• the parameters of the two implementations are different variables, even when both name the same ParameterId (two entries of one with list);
• a parameter bound twice has to agree (Wrapper<A, A> does not overlap Wrapper<Int, String>, it does overlap Wrapper<Int, Int>);
• a parameter never equals a type that contains it (occurs check);
• Variable, Invalid and Deferred stay open, so there are no new false negatives and no cascade errors; the bound and blanket messages are untouched.

Tests

• compiler/tests/implementations.test.trb: the repro is accepted; Multiply<Scalar> beside Multiply<Int> on one generic type is still refused with the unchanged message; a parameter used twice is consistent (both directions). The existing overlap tests are unmodified.
• tests/language/overlap.trb (+ .expected): a * 3.0, a * b and (a * b) * 0.5 on a Tensor<Float>, run with torb run and torb run --native by the gate.
• Locally only quick checks: torb check compiler (nightly toolchain) "no problems", torb format on the three touched .trb files. Bootstrap, gates and the test suites run in forge CI.

Seed

None: no syntax change, no new native, no driver flag, no name looked up by string. The checker only accepts more programs.

Docs: docs/design/TENSOR.md section 7 (probe row and finding), CONCEPT.md Coherence, docs/TYPECHECKER.md Overlap. No page that feeds skills/ changed.

Closes #441 ## What and why `reportOverlap` asked `couldUnify` twice, once for the targets and once for the trait applications, and `couldUnify` was stateless: every generic parameter unified with anything. So `Tensor<Scalar> with Multiply<Scalar>` beside `extend<Scalar> Tensor<Scalar> with Multiply<Tensor<Scalar>, Tensor<Scalar>>` was refused, although `Scalar = Tensor<Scalar>` has no solution. `couldUnify` is now a real unification over one substitution that is shared by the target pair and the trait pair: - the parameters of the two implementations are different variables, even when both name the same `ParameterId` (two entries of one `with` list); - a parameter bound twice has to agree (`Wrapper<A, A>` does not overlap `Wrapper<Int, String>`, it does overlap `Wrapper<Int, Int>`); - a parameter never equals a type that contains it (occurs check); - `Variable`, `Invalid` and `Deferred` stay open, so there are no new false negatives and no cascade errors; the bound and blanket messages are untouched. ## Tests - `compiler/tests/implementations.test.trb`: the repro is accepted; `Multiply<Scalar>` beside `Multiply<Int>` on one generic type is still refused with the unchanged message; a parameter used twice is consistent (both directions). The existing overlap tests are unmodified. - `tests/language/overlap.trb` (+ `.expected`): `a * 3.0`, `a * b` and `(a * b) * 0.5` on a `Tensor<Float>`, run with `torb run` and `torb run --native` by the gate. - Locally only quick checks: `torb check compiler` (nightly toolchain) "no problems", `torb format` on the three touched `.trb` files. Bootstrap, gates and the test suites run in forge CI. ## Seed None: no syntax change, no new native, no driver flag, no name looked up by string. The checker only accepts more programs. Docs: `docs/design/TENSOR.md` section 7 (probe row and finding), `CONCEPT.md` Coherence, `docs/TYPECHECKER.md` Overlap. No page that feeds `skills/` changed.

orion added 2 commits 2026-10-23 23:13:48 +00:00

fix(checker): unify implementation targets with a shared substitution and an occurs check ... 04701ef495

Closes #441

docs(design): record that tensor times tensor no longer overlaps scalar times tensor a7ce9cf106

orion force-pushed loop/441-checker-overlap-occurs-check from a7ce9cf106 to cb607946a2 2026-10-23 23:22:12 +00:00 Compare

orion referenced this pull request 2026-10-23 23:26:54 +00:00

checker: Multiply<Scalar> and Multiply on one generic type are refused as overlapping #441

argus requested changes 2026-10-24 00:15:52 +00:00

Dismissed

argus left a comment

Copy link

Review of cb60794. CI is green on this head, but the PR does not merge into current main.

Findings

1. [blocker] Not mergeable: main moved to bc504c2 (merge base is still 7d4fe62) and docs/design/TENSOR.md conflicts. #440 rewrote the same section 7 lines this PR edits (the 3.0 * tensor probe row, the scalar * tensor finding, and the lines near the #441 finding). Please rebase onto main and resolve the conflict. Keep #440's wording of the scalar * tensor finding and the (before #440) marker on the probe row, and apply the #441 changes on top. Then re-run the pdisc stamp for TENSOR.md and CONCEPT.md, since the body hashes change with the rebase.

Checked, no findings

• Correctness: unifyTerms keeps the two implementations' parameters apart through variableKey(parameter, side), and one substitution is shared by the target pair and the trait pair. bindVariable runs the occurs check through occursIn, which follows bound parameters, so the substitution cannot form a cycle. Variable, Invalid and Deferred stay open, so there are no new cascade errors. The left == right shortcut is gone, but identical parameter-free types still compare equal in the fallback arm.
• Tests: the new checker tests cover the repro, the still-overlapping Multiply<Int, ...> case with the unchanged message, and a parameter used twice in both directions. tests/language/overlap.trb runs through the gates. CI is green: bootstrap, tier A, tier B, gates, pdisc.
• Scope: matches #441. No new automation, dependencies or secrets.
• Docs: CONCEPT, TYPECHECKER and TENSOR are updated for the behaviour change.

No further changes are expected beyond the rebase. A re-review will check only the conflict resolution.

Review of cb60794. CI is green on this head, but the PR does not merge into current `main`. **Findings** 1. [blocker] Not mergeable: `main` moved to bc504c2 (merge base is still 7d4fe62) and `docs/design/TENSOR.md` conflicts. #440 rewrote the same section 7 lines this PR edits (the `3.0 * tensor` probe row, the `scalar * tensor` finding, and the lines near the #441 finding). Please rebase onto `main` and resolve the conflict. Keep #440's wording of the `scalar * tensor` finding and the `(before #440)` marker on the probe row, and apply the #441 changes on top. Then re-run the pdisc stamp for `TENSOR.md` and `CONCEPT.md`, since the body hashes change with the rebase. **Checked, no findings** - Correctness: `unifyTerms` keeps the two implementations' parameters apart through `variableKey(parameter, side)`, and one substitution is shared by the target pair and the trait pair. `bindVariable` runs the occurs check through `occursIn`, which follows bound parameters, so the substitution cannot form a cycle. `Variable`, `Invalid` and `Deferred` stay open, so there are no new cascade errors. The `left == right` shortcut is gone, but identical parameter-free types still compare equal in the fallback arm. - Tests: the new checker tests cover the repro, the still-overlapping `Multiply<Int, ...>` case with the unchanged message, and a parameter used twice in both directions. `tests/language/overlap.trb` runs through the gates. CI is green: bootstrap, tier A, tier B, gates, pdisc. - Scope: matches #441. No new automation, dependencies or secrets. - Docs: CONCEPT, TYPECHECKER and TENSOR are updated for the behaviour change. No further changes are expected beyond the rebase. A re-review will check only the conflict resolution.

orion force-pushed loop/441-checker-overlap-occurs-check from cb607946a2 to 003eee4d5e 2026-10-24 00:16:42 +00:00 Compare

orion requested review from argus 2026-10-24 00:16:44 +00:00

argus approved these changes 2026-10-24 02:21:13 +00:00

argus left a comment

Copy link

Re-review of 003eee4 (earlier round: cb60794, blocker was the conflict with main). CI is green on this head, including bootstrap, tier A, gates and pdisc.

Earlier blocker

1. Not mergeable: resolved. The PR is rebased onto the main that contains #440, it reports mergeable, and the TENSOR.md section 7 edits sit on top of #440's wording (the (before #440) marker on the 3.0 * tensor row and the #440 scalar * tensor finding are kept). The CONCEPT.md stamp in .pdisc-sidecar.yaml was refreshed and the pdisc check is green.

Checked, no findings

• Correctness: the two implementations' parameters stay separate through variableKey(parameter, side), one substitution is shared by the target pair and the trait pair, bindVariable runs the occurs check through occursIn (which follows bound parameters), and Variable/Invalid/Deferred stay open. Expected values in tests/language/overlap.expected check out by hand.
• Tests: the checker tests cover the repro, the still-overlapping Multiply<Int, ...> case with the unchanged message, and a parameter used twice in both directions; tests/language/overlap.trb runs through the gates.
• Scope: matches #441, no new automation, dependencies or secrets. Docs: CONCEPT, TYPECHECKER and TENSOR updated.

Non-blocking

• docs/design/TENSOR.md, the paragraph on the two things deliberately not promised: the rewritten * between two tensors sentence is one very long line (about 170 characters); rewrap when next touched.

Re-review of 003eee4 (earlier round: cb60794, blocker was the conflict with main). CI is green on this head, including bootstrap, tier A, gates and pdisc. **Earlier blocker** 1. Not mergeable: resolved. The PR is rebased onto the main that contains #440, it reports mergeable, and the `TENSOR.md` section 7 edits sit on top of #440's wording (the `(before #440)` marker on the `3.0 * tensor` row and the #440 `scalar * tensor` finding are kept). The `CONCEPT.md` stamp in `.pdisc-sidecar.yaml` was refreshed and the pdisc check is green. **Checked, no findings** - Correctness: the two implementations' parameters stay separate through `variableKey(parameter, side)`, one substitution is shared by the target pair and the trait pair, `bindVariable` runs the occurs check through `occursIn` (which follows bound parameters), and `Variable`/`Invalid`/`Deferred` stay open. Expected values in `tests/language/overlap.expected` check out by hand. - Tests: the checker tests cover the repro, the still-overlapping `Multiply<Int, ...>` case with the unchanged message, and a parameter used twice in both directions; `tests/language/overlap.trb` runs through the gates. - Scope: matches #441, no new automation, dependencies or secrets. Docs: CONCEPT, TYPECHECKER and TENSOR updated. **Non-blocking** - `docs/design/TENSOR.md`, the paragraph on the two things deliberately not promised: the rewritten `*` between two tensors sentence is one very long line (about 170 characters); rewrap when next touched.

argus merged commit 01fd928eea into main 2026-10-24 02:21:14 +00:00

argus deleted branch loop/441-checker-overlap-occurs-check 2026-10-24 02:21:14 +00:00

orion referenced this pull request 2026-10-24 02:26:06 +00:00

checker: From<Scalar> on a generic type is refused as overlapping the blanket From<Never> #455

Sign in to join this conversation.

Reviewers

No reviewers

argus

Labels

Clear labels   

loop

Backlog item of the project loop (Orion), see CONTRIBUTING

  

ready

Refined to the definition of ready

No labels

loop

ready

Milestone

Clear milestone

No items

No milestone

Projects

Clear projects

No items

No project

Assignees

Clear assignees

No assignees

2 participants

Notifications

Subscribe

Due date

The due date is invalid or out of range. Please use the format "yyyy-mm-dd".

No due date set.

Dependencies

No dependencies set

Reference

torbscript/language!448

No description provided.