Skip to content

SPATIAL-2b: carried coordinate-frame identity and operational frame refusal - #8156

Merged
briansrls merged 1 commit into
mainfrom
spatial-2b-carried-frame-identity
Aug 12, 2026
Merged

briansrls merged 1 commit into
mainfrom
spatial-2b-carried-frame-identity

Conversation

@gunbai-bot

@gunbai-bot gunbai-bot Bot commented Aug 11, 2026

Copy link
Copy Markdown
Contributor

What this corrects

#8091 merged claiming that a phantom frame parameter made cross-frame subtraction fail to typecheck — "the stronger of the two options, available here rather than merely preferable."

Measured on the production compile-and-run path (no test harness involved) 2026-08-11:

fn frame_violation() -> Int {          // RoomFrame location minus BuildingFrame location
  match displacement_between3(from: room_point(),      // Point3<RoomFrame>
                              to:   building_point())  // Point3<BuildingFrame>

Compiles clean. Returns 9. A plausible number for a question with no answer — the fabricated output DESIGN §5 forbids.

Why the phantom could never have worked

Not a modelling slip. v1.compiler.infer's argument-position judge compares nominal head names; applied type arguments live in Node.children and every name-level comparison discards them. Point3 matched Point3, so the frames were never looked at. A probe matrix isolated the axis — a primitive mismatch fires TypeMismatch:Primitive(String), while wrong type argument, wrong nominal record type, and a record returned as Int all produce zero diagnostics.

A separate compiler PR closes the call boundary. It cannot close the producer side: return-position conformance is a different relation that declines to judge record types at all, blocked on feature:conformance-produced-type-identity. So this stays writable regardless:

fn falsely_reframe(p: Point3<RoomFrame>) -> Point3<BuildingFrame> { p }

A consumer sees only the declared type. It cannot reconstruct an identity the producer erased. Therefore the carried identity is the authority.

The change

  • std.coordinate_frame mints CoordinateFrameIdentity — declaration-owned, never derived from a name or from contents (the HostResourceIdentity precedent; a content-derived key makes two coincidentally-identical frames one frame). Recorded as the corpus's third minted-occurrence carrier, which is evidence the subject-parameterized extraction is due — left as a trigger, not built here.
  • Phantom <F> removed, not demoted. Two authorities for one fact is the §3 violation whichever is right, and the weaker one is the one the compiler cannot enforce end to end.
  • SpatialResult has three arms — ready, arithmetic refusal, frame refusal. One coproduct rather than nested result types: there is one question at the operation boundary and the causes are what differ.
  • The refusal names roles, not expected/observed. In add_vector3(a, b) neither frame is normatively expected — the first operand merely establishes the result's frame, so "expected" would report argument order as a requirement. It carries an operation identity and the relation required.
  • The frame check precedes the arithmetic everywhere, because operands in different frames pose no question to overflow.

Guarantee rung, stated honestly

Frame consistency by checked derivation — not by construction. It is not true that cross-frame programs are unwritable. std.coordinate_frame carries the full account and the dissolve-on: when feature:conformance-produced-type-identity closes, a static projection can be reintroduced above this carrier, and the carried check remains as the serialization / external-input boundary a static guarantee cannot reach.

Evidence (green by execution)

Cross-frame subtraction, addition, subtraction, translation and transform application each refuse and name both frames · same-frame operations still answer (the positive sibling a refusal-only control cannot see) · frame and overflow asserted distinct in both directions · a transform's translation must be in its destination frame.

The decisive one is the lying-producer control: a function handing back a room-frame value under a building-frame annotation cannot rewrite the carried frame, and the next operation refuses.

Mutation-tested — disabling a single frame guard turns the suite red.

Sequencing

Independent of the compiler PR; repairs the current-main operational guarantee on its own. Whichever merges second should merge main and regenerate rather than hand-resolve generated artifacts. SPATIAL-3A resumes after both are in CI.

…efusal

#8091 claimed that a phantom frame parameter made cross-frame subtraction
fail to typecheck, and called that the stronger of the two available
options. Measured on the production compile-and-run path 2026-08-11, that
program compiles clean and returns 9 -- a plausible number for a question
with no answer, which is the fabricated output DESIGN 5 forbids.

The cause is a v1 seed limitation, not a modelling slip: the
argument-position judge compares nominal HEAD NAMES, and applied type
arguments live in the type node's children where every name-level
comparison discards them. Point3 matched Point3, so the frames were never
compared. A separate compiler PR closes the call boundary; it cannot close
the producer side, because return-position conformance declines to judge
record types at all pending feature:conformance-produced-type-identity.

So the carried identity is the authority and the honest claim is frame
consistency BY CHECKED DERIVATION, not by construction:

- std.coordinate_frame mints CoordinateFrameIdentity, declaration-owned and
  never derived from a name or from contents (the HostResourceIdentity
  precedent). Recorded as the third minted-occurrence carrier in the corpus,
  which is evidence the subject-parameterized extraction is due -- left as a
  trigger rather than built here.
- Phantom <F> is removed rather than demoted. Two authorities for one fact
  is the DESIGN 3 violation whichever is right, and the weaker one is the
  one the compiler cannot enforce end to end.
- SpatialResult carries three arms: ready, arithmetic refusal, frame
  refusal. One coproduct rather than nested result types -- there is one
  question at the operation boundary and the causes are what differ.
- The refusal names ROLES, not expected/observed: for a symmetric operation
  neither frame is normatively expected, so an operation identity and the
  required relation replace a report of argument order.
- The frame check precedes the arithmetic everywhere, because operands in
  different frames pose no question to overflow.

Green by execution, with discriminating controls: cross-frame subtraction,
addition, subtraction, translation and transform application each refuse and
name both frames; same-frame operations still answer (the positive sibling a
refusal-only control cannot see); frame and overflow are asserted distinct in
both directions; a transform's translation must be in its destination frame.

The decisive one is the lying-producer control: a function handing back a
room-frame value under a building-frame annotation cannot rewrite the carried
frame, and the next operation refuses. Mutation-tested -- disabling a single
frame guard reds the suite.

Co-Authored-By: Claude Opus 5 (1M context) <noreply@anthropic.com>
@briansrls
briansrls merged commit bd73f49 into main Aug 12, 2026
12 of 15 checks passed
@briansrls
briansrls deleted the spatial-2b-carried-frame-identity branch August 12, 2026 02:04
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