Skip to content

Reject non-primitive string interpolation at the typechecker - #813

Merged
jasisz merged 2 commits into
mainfrom
feat/explicit-stringify-interpolation
Aug 8, 2026
Merged

Reject non-primitive string interpolation at the typechecker#813
jasisz merged 2 commits into
mainfrom
feat/explicit-stringify-interpolation

Conversation

@jasisz

@jasisz jasisz commented Aug 8, 2026

Copy link
Copy Markdown
Owner

Interpolation renders primitives only — Int, Float, Bool, String, exactly the set the __to_str lowering implements on every backend. Any other embed is a type error naming the offending type and asking for a named function returning String; no standard-library renderer is added.

  • Reverts the wasm-gc List<Int> interpolation stringifier: no typechecked program can reach the compound arm any more.
  • That arm now raises a wasm-gc codegen error naming the function and the embed type instead of bailing to a silent unreachable trap stub, so pipelines that skip the typecheck get a diagnostic. The other unsupported-shape bails in the MIR emitter still trap-stub; AVER_WASMGC_REQUIRE_MIR=1 lists them.
  • Migrates the self-hosted evaluator's two Expr diagnostics to a named exprLabel function (self-host regenerated). The rest of the tree already used named render functions.
  • Tests: checker rules for each primitive and each compound shape, no double report on an already-errored embed, a rewritten packed-field red-check plus a three-way differential that keeps the packed-projection coverage through an explicit local render function, and a codegen test that an ungated pipeline gets the loud error.

🤖 Generated with Claude Code

jasisz and others added 2 commits August 8, 2026 21:09
Conversion to String must be named in the source. An interpolated part
now has to be an Int, a Float, a Bool or a String — exactly the set the
__to_str lowering renders on every backend. Any other embed is a type
error that names the offending type and asks for a named function
returning String; no standard-library renderer is offered, because none
exists.

Reverts the wasm-gc List<Int> interpolation stringifier: with the
checker rule in place, no typechecked program can reach the compound
arm of the interpolation emitter. That arm now raises a codegen error
naming the function and the embed type instead of bailing out to a
silent unreachable trap stub, so an internal pipeline that skips the
typecheck gets a diagnostic rather than a module that traps at runtime.
The remaining unsupported-shape bails in the MIR body emitter still
produce a trap stub; AVER_WASMGC_REQUIRE_MIR=1 enumerates them.

Migrates the self-hosted evaluator's two Expr diagnostics onto a named
exprLabel function and regenerates the self-host output. The two wasm-gc
tests that covered the old behaviour are rewritten rather than dropped:
one pins the new type error, the other keeps the three-way packed-field
projection differential by building its string through an explicit local
render function.

Co-Authored-By: Claude Fable 5 <noreply@anthropic.com>
An unresolved type variable was accepted alongside `Type::Invalid` on the
theory that it always follows an earlier diagnostic. It does not. Matching
on a bare `Option.None` with an arm `Option.Some(x) -> "{x}"` binds `x` to
the `T` of an `Option<T>` nothing in the program fixes; the file otherwise
type-checks clean, so the embed passed the interpolation rule and reached
the backends with no renderable type. A bare `[]` subject is the same hole.

A bare `Type::Var` is now its own verdict with its own diagnostic: the type
could not be determined, pin it and convert through a named function
returning String. `Type::Invalid` keeps its acceptance — that one really is
downstream of an error already reported.

The verdict is decided where the embed is inferred rather than in a later
sweep, because there is no later chance to pin it: the checker holds no
ambient substitution (every `subst` map lives and dies inside one
`compatible` / `match_with` call), `Spanned::set_ty` writes a `OnceLock` so
the type read at the rule is the final stamp every backend will see, and
the one top-down channel fires only for the fixed recogniser list, which
never descends into an interpolation part.

Records the argument for the emitter's "typechecked source cannot reach
this arm" claim at the wasm-gc error site, now that the checker's partition
of `Type` has no remainder: the four accepted primitives are exactly the
four the dispatch handles, `Invalid` implies the compile is already gated,
and everything else is rejected by name. Pins the reported line number for
both interpolation diagnostics on a line past the first, since an embed's
own line is 1-based inside the `{...}` fragment and only the outer node's
line is source-accurate.

Co-Authored-By: Claude Fable 5 <noreply@anthropic.com>
@jasisz
jasisz merged commit 27f90dd into main Aug 8, 2026
35 checks passed
@jasisz
jasisz deleted the feat/explicit-stringify-interpolation branch August 8, 2026 21:45
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