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

orion commented

2026-10-23 16:27:49 +00:00

Collaborator

Context

Found by the scratch probe of the std/tensor design record (#438, step 1 of #82; docs/design/TENSOR.md, "Operators"). A generic type that implements Multiply<Scalar> (its own scalar) and Multiply (itself) is refused as overlapping, although the two cannot be the same instance: Scalar = Tensor<Scalar> has no finite solution.

Reproduction

type Tensor<Scalar: Numeric = Float> with Multiply<Scalar> {
  data: Buffer<Scalar>

  fn multiply(factor: Scalar): Self {
    Tensor(data)
  }
}

extend<Scalar: Numeric> Tensor<Scalar> with Multiply<Tensor<Scalar>, Tensor<Scalar>> {
  fn multiply(other: Tensor<Scalar>): Tensor<Scalar> {
    other
  }
}

torb check: error: `Tensor<Scalar>` already implements `Multiply<Tensor<Scalar>, Tensor<Scalar>>` ... Two implementations of one trait may not overlap: only different target types tell them apart. Declaring the second one on a concrete scalar (extend Tensor<Float64> with Multiply<Float64> beside with Multiply on the generic type) is accepted and a * 3.0 and a * b both run, so the rule can tell them apart there. Probed with the nightly of 2026-10-23.

Goal

The overlap check unifies with an occurs check (a variable never equals a type that contains it), so tensor * scalar and tensor * tensor can be written once for every scalar.

Acceptance criteria

The two implementations above are accepted and a * 3.0 and a * b run in both back ends.
A real overlap (Multiply<Scalar> beside Multiply<Int> on one generic type) is still refused; compiler tests pin both.

Seed

None expected (the checker accepts more programs; nothing in std/ depends on it).

Out of scope

std/tensor slices: they spell the element-wise product of two tensors as scaled(by:) and do not wait for this.

## Context Found by the scratch probe of the `std/tensor` design record (#438, step 1 of #82; `docs/design/TENSOR.md`, "Operators"). A generic type that implements `Multiply<Scalar>` (its own scalar) and `Multiply` (itself) is refused as overlapping, although the two cannot be the same instance: `Scalar = Tensor<Scalar>` has no finite solution. ## Reproduction ```trb type Tensor<Scalar: Numeric = Float> with Multiply<Scalar> { data: Buffer<Scalar> fn multiply(factor: Scalar): Self { Tensor(data) } } extend<Scalar: Numeric> Tensor<Scalar> with Multiply<Tensor<Scalar>, Tensor<Scalar>> { fn multiply(other: Tensor<Scalar>): Tensor<Scalar> { other } } ``` `torb check`: ``error: `Tensor<Scalar>` already implements `Multiply<Tensor<Scalar>, Tensor<Scalar>>` ... Two implementations of one trait may not overlap: only different target types tell them apart``. Declaring the second one on a concrete scalar (`extend Tensor<Float64> with Multiply<Float64>` beside `with Multiply` on the generic type) is accepted and `a * 3.0` and `a * b` both run, so the rule can tell them apart there. Probed with the nightly of 2026-10-23. ## Goal The overlap check unifies with an occurs check (a variable never equals a type that contains it), so `tensor * scalar` and `tensor * tensor` can be written once for every scalar. ## Acceptance criteria - [ ] The two implementations above are accepted and `a * 3.0` and `a * b` run in both back ends. - [ ] A real overlap (`Multiply<Scalar>` beside `Multiply<Int>` on one generic type) is still refused; compiler tests pin both. ## Seed None expected (the checker accepts more programs; nothing in `std/` depends on it). ## Out of scope `std/tensor` slices: they spell the element-wise product of two tensors as `scaled(by:)` and do not wait for this.

orion added the

loop

label

2026-10-23 16:27:49 +00:00

orion referenced this issue

2026-10-23 16:34:11 +00:00

docs(compute): design record for std/tensor on the CPU #442

orion referenced this issue

2026-10-23 16:39:43 +00:00

compute: design record for std/tensor on the CPU (step 1 of #82) #438

orion commented

2026-10-23 22:00:57 +00:00

Author

Collaborator

[loop:torbscript] intake: in scope (author orion, label loop). claim refine by session:loop-torbscript-20261024 until 2026-10-24T00:00Z

orion commented

2026-10-23 22:02:27 +00:00

Author

Collaborator

[loop:torbscript] refine: ready, claim released, next: implement

Definition of ready

Goal / design point: docs/design/TENSOR.md section 7 ("Operators", finding on tensor * tensor) and CONCEPT.md "Coherence" (blanket and overlap rule, "Disjointness is proved by different target heads, or by bounds ..."). It is the false positive filed there as #441; the rule itself ("two implementations of one trait may never overlap") does not change, only the unifier behind it gets exact.
Cause (read in compiler/src/semantics/checker/implementation.trb): reportOverlap calls couldUnify once on the targets and once on the trait applications. couldUnify is stateless: every Parameter unifies with anything. For the repro, targets give Scalar = Scalar and the trait arguments give Scalar = Tensor<Scalar>, which only conflicts when the two answers share one substitution and an occurs check.
Seed: none. No syntax change, no new native, no driver flag, no name looked up by string; the checker only accepts more programs, and nothing in std/ depends on it. The seed refresh stays untouched.
Size: one PR, two Conventional Commits (see below).

Acceptance criteria (replaces the two in the description, same intent, now testable)

couldUnify becomes a real unification: one substitution (parameter -> type) is shared by the target pair and the trait pair of the two implementations, a parameter bound twice must agree, and a parameter never equals a type that contains it (occurs check). Variable, Invalid and Deferred keep being open (no new false negatives, no cascade errors).
The repro of this issue (type Tensor<Scalar: Numeric = Float> with Multiply<Scalar> plus extend<Scalar: Numeric> Tensor<Scalar> with Multiply<Tensor<Scalar>, Tensor<Scalar>>) is accepted by torb check.
A program in tests/language/ (with .expected) builds a Tensor<Float>, runs a * 3.0 and a * b, and passes with torb run and torb run --native (both back ends). If call resolution picks the wrong implementation or lowering fails for the generic pair, fixing that is part of this issue (same PR), not a new one.
Compiler tests in compiler/tests/implementations.test.trb pin: (a) the repro is accepted; (b) a real overlap is still refused with the unchanged message (Multiply<Scalar> beside Multiply<Int> on one generic type); (c) a parameter used twice is consistent (Wrapper<A, A> vs Wrapper<Int, String> do not overlap, Wrapper<A, A> vs Wrapper<Int, Int> do); (d) the two-blanket and bound-disjointness messages are unchanged.
sh tools/gates.sh a green in forge CI (not run locally); the existing overlap tests in implementations.test.trb stay green unmodified.

Commit plan

fix(checker): unify implementation targets with a shared substitution and an occurs check - the unifier, the tests of criterion 4, the tests/language/ program of criterion 3.
docs(design): record that tensor times tensor no longer overlaps scalar times tensor - docs/design/TENSOR.md section 7 (the "refused" probe row and the #441 bullets become "fixed by #441"; the revisit of * between two tensors stays a decision for the first-release numbers, not promised), one sentence in CONCEPT.md Coherence ("... and a parameter never equals a type that contains it"), regenerated skills/ (docs skill).

decided by the loop:

Fix in the unifier, not a special case for the repro. Why: the occurs check is the textbook rule, it makes the check exact for every generic type (tensors, matrices, Wrapper<A, A>), and a pattern-specific exemption would keep the next false positive in place. Technical checker design, so no owner question.
Bounds are not consulted for this (Scalar: Numeric vs Tensor<Scalar>). Why: the occurs check already separates the two and reportBlanketOverlap / the bound-disjointness path stay as they are; mixing the two would widen the change beyond one PR.
tensor * tensor as a language decision stays out. Why: TENSOR.md section 7 deliberately names scaled(by:) and matmul; this issue only removes the checker obstacle, and the std/tensor slices do not wait for it (as the description says).
3.0 * tensor (#440) is not part of this. Related, refined separately: #440

No owner question: none of the contract's categories applies (internal checker design, no published contract broken, since the checker only accepts more).

Tokens: RE worker ~60k (sonnet, refine).

[loop:torbscript] refine: ready, claim released, next: implement **Definition of ready** - **Goal / design point:** `docs/design/TENSOR.md` section 7 ("Operators", finding on `tensor * tensor`) and `CONCEPT.md` "Coherence" (blanket and overlap rule, "Disjointness is proved by different target heads, or by bounds ..."). It is the false positive filed there as #441; the rule itself ("two implementations of one trait may never overlap") does not change, only the unifier behind it gets exact. - **Cause (read in `compiler/src/semantics/checker/implementation.trb`):** `reportOverlap` calls `couldUnify` once on the targets and once on the trait applications. `couldUnify` is stateless: every `Parameter` unifies with anything. For the repro, targets give `Scalar = Scalar` and the trait arguments give `Scalar = Tensor<Scalar>`, which only conflicts when the two answers share one substitution and an occurs check. - **Seed:** none. No syntax change, no new native, no driver flag, no name looked up by string; the checker only accepts more programs, and nothing in `std/` depends on it. The seed refresh stays untouched. - **Size:** one PR, two Conventional Commits (see below). **Acceptance criteria (replaces the two in the description, same intent, now testable)** 1. `couldUnify` becomes a real unification: one substitution (parameter -> type) is shared by the target pair and the trait pair of the two implementations, a parameter bound twice must agree, and a parameter never equals a type that contains it (occurs check). `Variable`, `Invalid` and `Deferred` keep being open (no new false negatives, no cascade errors). 2. The repro of this issue (`type Tensor<Scalar: Numeric = Float> with Multiply<Scalar>` plus `extend<Scalar: Numeric> Tensor<Scalar> with Multiply<Tensor<Scalar>, Tensor<Scalar>>`) is accepted by `torb check`. 3. A program in `tests/language/` (with `.expected`) builds a `Tensor<Float>`, runs `a * 3.0` and `a * b`, and passes with `torb run` and `torb run --native` (both back ends). If call resolution picks the wrong implementation or lowering fails for the generic pair, fixing that is part of this issue (same PR), not a new one. 4. Compiler tests in `compiler/tests/implementations.test.trb` pin: (a) the repro is accepted; (b) a real overlap is still refused with the unchanged message (`Multiply<Scalar>` beside `Multiply<Int>` on one generic type); (c) a parameter used twice is consistent (`Wrapper<A, A>` vs `Wrapper<Int, String>` do not overlap, `Wrapper<A, A>` vs `Wrapper<Int, Int>` do); (d) the two-blanket and bound-disjointness messages are unchanged. 5. `sh tools/gates.sh a` green in forge CI (not run locally); the existing overlap tests in `implementations.test.trb` stay green unmodified. **Commit plan** 1. `fix(checker): unify implementation targets with a shared substitution and an occurs check` - the unifier, the tests of criterion 4, the `tests/language/` program of criterion 3. 2. `docs(design): record that tensor times tensor no longer overlaps scalar times tensor` - `docs/design/TENSOR.md` section 7 (the "refused" probe row and the #441 bullets become "fixed by #441"; the revisit of `*` between two tensors stays a decision for the first-release numbers, not promised), one sentence in `CONCEPT.md` Coherence ("... and a parameter never equals a type that contains it"), regenerated `skills/` (`docs skill`). **decided by the loop:** - *Fix in the unifier, not a special case for the repro.* Why: the occurs check is the textbook rule, it makes the check exact for every generic type (tensors, matrices, `Wrapper<A, A>`), and a pattern-specific exemption would keep the next false positive in place. Technical checker design, so no owner question. - *Bounds are not consulted for this (`Scalar: Numeric` vs `Tensor<Scalar>`).* Why: the occurs check already separates the two and `reportBlanketOverlap` / the bound-disjointness path stay as they are; mixing the two would widen the change beyond one PR. - *`tensor * tensor` as a language decision stays out.* Why: TENSOR.md section 7 deliberately names `scaled(by:)` and `matmul`; this issue only removes the checker obstacle, and the `std/tensor` slices do not wait for it (as the description says). - *`3.0 * tensor` (#440) is not part of this.* Related, refined separately: https://git.torb.dev/torbscript/language/issues/440 No owner question: none of the contract's categories applies (internal checker design, no published contract broken, since the checker only accepts more). Tokens: RE worker ~60k (sonnet, refine).

orion added the

ready

label

2026-10-23 22:02:27 +00:00

orion referenced this issue

2026-10-23 22:02:38 +00:00

checker: scalar * value with a user Multiply on the number type lowers as the builtin product #440

orion commented

2026-10-23 22:55:48 +00:00

Author

Collaborator

[loop:torbscript] claim implement by session:loop-torbscript-20261024 until 2026-10-24T04:30Z

orion referenced this issue from a commit

2026-10-23 23:13:43 +00:00

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

orion referenced this issue from a pull request that will close it,

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

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

orion commented

2026-10-23 23:26:54 +00:00

Author

Collaborator

[loop:torbscript] release implement: the implement worker hit its 30 minute run timeout without a result comment, after opening PR #448 (two commits: checker fix with shared substitution and occurs check, design doc note). Forge CI: bootstrap (linux-x64) green, gates, tier A/B and the remaining jobs still pending. Claim released. next: waiting (CI running on PR #448), then review/fix rounds

[loop:torbscript] release implement: the implement worker hit its 30 minute run timeout without a result comment, after opening PR https://git.torb.dev/torbscript/language/pulls/448 (two commits: checker fix with shared substitution and occurs check, design doc note). Forge CI: bootstrap (linux-x64) green, gates, tier A/B and the remaining jobs still pending. Claim released. next: waiting (CI running on PR #448), then review/fix rounds

orion referenced this issue from a commit

2026-10-24 00:16:42 +00:00

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

orion referenced this issue

2026-10-24 00:34:27 +00:00

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