Compute erased types from new-resolution shape analysis by LPTK · Pull Request #575 · hkust-taco/mlscript

LPTK · 2026-10-15T08:09:21Z

With new resolution (#lang(0.3.x)), unannotated parameters, results, variables and fields now receive runtime representations from the shapes observed flowing into them. Previously these slots remained unknown. For example, a private parameter that only receives Int32 values can use a physical i32 slot on Wasm. Annotations continue to fix representations, and lowering enforces conversions at slot boundaries.

Resolution records source-slot observations in ErasureInputs before completing the compilation unit; erasure reads the completed observations without reopening resolution. Later worksheet blocks cannot widen representations fixed by earlier blocks. Constructor-companion signatures survive cloning and IR symbol refreshes.

Mutable-field inference includes initializers, subsequent assignments and writes permitted through exposed interfaces. Nominal fields exposed to other compilation units require annotations. Record interfaces retain separate read/write bounds, including their variance through aliases and generic arguments. This PR uses the existing whole-record mut {...} syntax and interval type arguments; complete structural subtype checking remains outside its scope.

The remaining Scala diff is 832 changed compiler lines across 14 files, plus 42 changed test lines across two files. The language reference and diff-test goldens describe the resulting inference behavior.

Separate follow-ups:

Retype fused values and prove representation casts #624: deforestation retyping and flow-proved casts (E29–E30), to merge after this PR.
Support per-field mutability and record field bounds #625: per-field mutability and explicit record-field bounds (E33–E34), to merge after this PR.
Propagate partial calls with checked arguments #626: partial-call argument propagation (E20), independently targeting hkmc2.
Preserve constructor behavior and ordered matches during fusion #627: constructor and match safety (E21–E23), independently targeting hkmc2.
Keep fused values compatible with container field storage #628: fusion across container storage (E24), independently targeting hkmc2.

The two dependent PRs use codex/pr575-inference-base, a review-only mirror of this head, to keep their diffs focused. After this PR merges, integrate updated hkmc2 into those branches and retarget their PRs to hkmc2, reconciling squash-merge ancestry if necessary.

Validation: Metals compilation and hkmc2AllTests/test passed on f74e393f5; all golden outputs are committed. Four targeted :fixme blocks retain their assertions for Array/Object fusion matching, optional-field fusion and its dependent worksheet check (#627), and recursive fused result-slot types (#624). Reconcile those markers when the corresponding fixes land.

Important: all the deforestation regressions observed in this PR (removed fusion logs in the diff-tests) are reverted by merging the three PRs: constructor safety (#627); storage (#628); and retyping (#624); which should be reviewed separately and will be merged as follow-ups.

LPTK · 2026-10-15T08:10:57Z

 //│ dead-param-elim > <<< dead-param-elim results <<<
 //│ ——————————————| Optimized IR |——————————————————————————————————————————————————————————————————————
-//│ @private define f⁰ as fun f¹(a) { return a }; return 42
+//│ @private define f⁰ as fun f¹(a) { return (a as! Int⁰) }; return (42 as! Int⁰)


Why are casts now inserted here?

[Astra] These casts became redundant after propagation/inlining, but the simplifier did not reconsider them. Fixed in 1f5390b: it now removes a cast when the rewritten operand is provably below its target, including checked casts whose check is guaranteed to succeed. This example is back to return a and return 42. The full test suite passes.

[Claude] Verified: at b87501d, this file's output is identical to hkmc2 again.

LPTK · 2026-10-15T08:11:03Z

 main1()
 //│ dead-param-elim > >>> dead-param-elim results >>>
 //│ dead-param-elim > apply⁰#0 @ main1⁰.main⁰.apply¹ -> eliminable: {1}
-//│ dead-param-elim > lambda⁰#0 @ main1⁰ -> eliminable: {0}


Why is this optimization lost?

[Astra] Lowering assigned no erased representation to generated lambda functions. That introduced a checked cast around the closure, which made flow analysis treat it as escaping and prevented dead-parameter elimination. Fixed in f853f10 by preserving the generated function calling convention. The unused parameter is eliminated again; the full suite passes.

[Claude] Verified: the parameter is eliminated again, and this file matches hkmc2.

f853f10 has a side effect in the compiled Predef.mjs and Runtime.mjs: closures passed as arguments now stay bound to a temporary. For example, Predef.equals now reads:

lambda$here = lambda$1(Predef, b); return runtime.safeCall(a.every(lambda$here))

where hkmc2 has a.every(lambda$1(Predef, b)).

Erased types do not block inlining here. In the IR, call arguments must be paths (Arg.value: Path), and BlockSimplifier only propagates pure calls into Result positions. On hkmc2, the generated lambda had no representation, so lowering wrapped the argument in a checked cast to Function, the erasure of the function type that the prelude declares for every's parameter. Cast is a Path whose operand is a Result, so the simplifier could substitute the call into it, and JS code generation drops the cast. The optimized IR was a.every((lambda$(P.this, b) as! Function)).

Now that generated lambdas have a function representation, that cast is correctly gone, and nothing can absorb the call. Getting the old output back would take either allowing pure calls as arguments or folding single-use temporaries into arguments in the JS backend. Neither is specific to this PR, so I've listed this as a known limitation in the PR description.

LPTK · 2026-10-15T08:22:44Z

 //│     else
 //│       set tmp = -⁰(n, 1);
-//│       return countdown¹(tmp)
+//│       return countdown¹((tmp as! Int⁰))


Why is a cast now inserted here?

[Astra] Shape inference now gives n the Int representation, while the lowered builtin subtraction still has an unspecified result representation. The cast bridges that physical result to the inferred parameter slot. It is not a cast from Int to Int at the IR level, so the redundant-cast cleanup deliberately preserves it. Giving arithmetic builtins precise result representations would allow this cast to disappear too.

[Claude] Fixed in b87501d, using the workaround @LPTK suggested. Until the builtins are declared as overloaded functions, semantics.BuiltinOperatorResults approximates operator results from the primitive classes of their operands, on the JS target only. Resolution and IR erasure share these rules.

-⁰(n, 1) is now an Int, so the cast is gone and this file matches hkmc2 again. For the same reason, sumPlus in dead-param-elim/todos.mls is back to its baseline output (Nil => return 1), and so are checkArgs and showStackTrace in Runtime.mjs.

LPTK · 2026-10-15T08:23:53Z

 //│   match xss
 //│     Nil⁰ =>
-//│       return 0
+//│       return (len$ls_Nil⁰() as! Object⁰)(eta$0$0, eta$0$1, eta$0$2, eta$0$3, eta$0$4)


Can we avoid this unsightly case?

[Astra] Fixed in 551e4a8. Generated branch functions now retain their two parameter lists, so supplying just the constructor fields produces Function rather than an unknown value. The Object cast disappears and the branch calls inline again. The fix also updates fused parameters, results, captured values, and locals together; regression tests cover monomorphic fusion and field projection. The full suite passes.

[Claude] Verified: no as! Object casts remain in this file, and the branch calls are inlined again.

LPTK · 2026-10-15T08:24:29Z

-//│ return flatten$flatten$worker⁰(tmp4, undefined, undefined, undefined)
+//│ set tmp5 = flatten$flatten⁰((tmp4 as! Object⁰));
+//│ return tmp5(undefined, undefined, undefined, undefined, undefined)


This looks like a concerning regression.

[Astra] Fixed the lost branch inlining in 551e4a8 and the remaining partial-call propagation regression in 3caffd0. Checked arguments are now evaluated at the original partial application site, leaving a pure call prefix that can combine with its later application. The enum/sum example is back to an inlined loop, and flatten/append no longer retain the branch closures shown here. New regressions check argument capture and preservation of Wasm cast failures; the full suite passes.

[Claude] Verified: the call is back to flatten$flatten$worker⁰(tmp4, undefined, undefined, undefined), as on hkmc2. I also checked that the new simplifier rule that hoists checked arguments out of partial applications terminates.

LPTK · 2026-10-15T08:25:44Z

+private fun roundtrip(value) =
+  let saved = value
+  Slot(saved).value
+let input = wasm.i32.const(42)


Why not open wasm.i32 { const } to avoid all these repeated paths?

[Astra] Done in 0629de9. Qualified open bases are currently rejected, so the test uses open wasm { i32 } followed by open i32 { const }, and then plain const(...) throughout. The regenerated erasure test passes.

[Claude] Verified: open wasm.i32 { const } is rejected with "Illegal 'open' statement base.", so the two-step open is the best option for now.

LPTK · 2026-10-15T08:26:24Z

-//│ set tmp1 = Predef⁰.hide⁰(4);
-//│ set tmp2 = +⁰(tmp1, 1);
-//│ return Predef⁰.print⁰(tmp2)
+//│ set x = (tmp as! Int⁰);


Why the new cast?

[Astra] x is now inferred as Int, including its writes. hide remains a separately compiled generic function with an unknown physical result representation, even though resolution propagates the argument shape through it. The cast narrows that result before storing it in x; retaining it preserves the imported function’s calling convention. Casts exposed as redundant by propagation/inlining are now removed in 1f5390b.

[Claude] The mechanism is right. hide is a separately compiled polymorphic function with an unknown physical result, while resolution sees the Int flowing through it. So x is inferred as Int, and each write narrows hide's result with a checked cast. The cast is not needed to preserve hide's calling convention, though: leaving x at the top representation would preserve it too.

The cost shows in this test. Checked casts are effectful, so the dead write set x = hide(3) survives as do (tmp1 as! Int⁰). b87501d removes the cast on the +⁰ result, since builtin results are now approximated, but two kinds of casts remain:

the casts of hide's results;

do (old as! Int⁰) in the finally block of the set … in test below, because the old temporary that lowering introduces has no representation.

The second kind could be fixed by giving such temporaries the representation of the variable they copy. The first needs representations instantiated per call for polymorphic functions. Both are listed as known limitations in the PR description.

[Claude] Update: the old cast is fixed in d710d52. Erasure now infers the representation of the temporary that set … in declares, like a source variable, so the set … in test below is back to its hkmc2 output. (On Wasm, the same untyped temporary made set x = … in an error for an unboxed Int32 variable; newres/wasm/Erasure.mls now covers that.) The casts of hide's results remain.

LPTK · 2026-10-15T08:27:22Z

-//│   (import "repl" "counter" (global $counter (mut (ref null any))))
-//│   (import "repl" "step" (global $step (mut (ref null any))))
-//│   (func $entry (export "entry") (type $entry) (result (ref null any))
-//│     (return
-//│       (call $plus_impl
-//│         (global.get $counter)
-//│         (global.get $step))))
+//│   (import "repl" "counter" (global $counter (mut (ref null i31))))
+//│   (import "repl" "step" (global $step (mut (ref null i31))))
+//│   (func $entry (export "entry") (type $entry) (result (ref null i31))
+//│     (local $tmp (ref null any))
+//│     (block (result (ref null i31))
+//│       (local.set $tmp
+//│         (call $plus_impl
+//│           (global.get $counter)
+//│           (global.get $step)))
+//│       (return
+//│         (ref.cast (ref null i31)
+//│           (local.get $tmp)))))


Why is the generated code longer than it used to be?

[Astra] The worksheet globals and entry result are now inferred as Int (Wasm (ref null i31)), while the imported plus_impl still returns (ref null any). The extra ref.cast is therefore required at that boundary. The extra local is the existing normalization of the call followed by its cast. Previously all three slots were anyref, so no narrowing was necessary.

[Claude] Accurate. The cast is inherent to narrowing counter: once the write to counter is emitted, storing the anyref result of plus_impl into the i31 global needs the same cast.

Related, but it predates this PR: neither this branch nor hkmc2 emits global.set $counter for set counter += step. The block returns 3, but a later block still reads counter = 1. I've proposed fixing that separately.

LPTK · 2026-10-15T08:27:48Z

 //│     (local $receiver (ref null any))
 //│     (return
-//│       (block (result (ref $Child))
+//│       (block (result (ref null $Child))


Why is this now nullable?

[Astra] This is intentional: a source slot of type Child must also accept undefined, whose Wasm representation is a null reference. Hence source parameters/results use (ref null $Child), including this cast of a virtual call's result. Constructor results and the receiver passed to an actual method remain non-null. The undefined parameter/field/result regressions in newres/wasm/Erasure.mls cover the distinction.

[Claude] Accurate, but this has a cost that the reply doesn't mention:

Field reads through class-typed parameters and locals now need a ref.cast (ref $C) first (see getX in wasm/Basics.mls).

wasm/ClassMethods.mls gets a double cast: (ref.cast (ref $A) (ref.cast (ref null $A) …)).

Constructor results are non-null in constructor signatures, but the locals that receive them are nullable ((local $tmp (ref null $Foo))).

@LPTK asked whether, since reading back undefined is undefined behavior, it would make sense to fill such a slot with an uninitialized object of the corresponding class. Yes. This is consistent with the semantics now documented under Runtime Representations in doc/reference.md, and it would let class slots be non-null (ref $C), which removes these casts. A sketch:

Keep one placeholder instance per class that needs one, in an immutable global. Build it with struct.new from the class's type info and from placeholders for its fields: zero for numeric fields, ref.i31 0 for boxed integers, and the placeholder of the field's class for class-typed fields. Abstract classes work the same way, since Wasm does not distinguish them. Function, Array, and Str slots also need placeholder values.

A class whose non-null class-typed fields form a cycle with no abstract class in between, like class Node(next: Node), has no finite placeholder, so its slots could stay nullable. Without undefined, such a class cannot be instantiated anyway.

The alternative is to make a slot nullable only when undefined can reach it. Resolution observes undefined like any other value, and dead-parameter elimination knows which parameters it fills with placeholders. But that requires tracking nullability in erased types, which placeholders avoid. I haven't implemented either; it seems best done in a follow-up.

it would let class slots be non-null (ref $C), which removes these casts. A sketch

Note: This has already been implemented and is sitting in a branch for this PR to be merged first.

Resolution observes undefined like any other value, and dead-parameter elimination knows which parameters it fills with placeholders

Note: this is no longer true sicne the optional param PR (which made undefined, renamed to unsafe.undefined an illegitimate value).

LPTK · 2026-10-15T08:28:30Z

 //│     this.#b = tmp;
-//│     lambda$here = lambda$(this);
-//│     this.f = lambda$here;
+//│     this.f = lambda$(this);


Looks like this is no longer inlined.

[Astra] This test explicitly uses :noInline, and the call was not inlined before either: the old output assigned lambda$(this) to lambda$here and then copied that temporary into this.f. The reviewed output assigned the same call directly to this.f, removing a temporary rather than losing inlining. After the generated-function representation fix in f853f10, this snapshot is back to its original form.

[Claude] Verified: this hunk is back to its hkmc2 form. The file's other differences from hkmc2 are improvements, such as the p = tmp3 copies now being propagated.

@claude @codex but why isn't copy-propagation actually optimizing this in the first place?

Preserve delayed erasure for constructor and placeholder symbols alongside private constructor storage and placeholder source locations. Keep exhaustive loops non-terminating in the ScopedBlocks expectation, and add erasure regressions for private construction, private shadowing, implicit lambdas, and trailing arguments. Regenerate golden outputs. Validated with Metals compilation, ctest, focused diff tests, and hkmc2AllTests/test.

- Type generator calls as iterators: `@generator` functions return an `Iterator`, both in resolution (`listenDefinitionResult`) and in erasure (`callableResult`), instead of the payload of their final step. - Check overrides against the representations of the members they override: unannotated override parameters take the inherited representations, override results must fit the inherited result, and declared parameters must admit the inherited ones (and match them on Wasm, which calls overrides through the signature of the overridden method). - Require type annotations on open members whose parameters are exposed to other compilation units, since subclasses there must implement them with the same representations. Annotate such members in the library and the tests. - WORKAROUND: approximate the results of builtin operators from the primitive classes of their operands (`BuiltinOperatorResults`), in resolution and in IR erasure, until the builtins are declared as overloaded functions. This only applies to the JavaScript target, as the Wasm backend implements operators with dynamically typed intrinsics. - Locate representation-conversion diagnostics (`Lowering.castTo` and `WatBuilder.castConserve`). - Document runtime representations in `doc/reference.md`, including `undefined` as undefined behavior and the rejection of programs whose only problem is a misleading annotation. - Add regression tests for the inference of representations across worksheet blocks, with a :fixme for the Wasm REPL crash when reading a field whose representation is another session class. - Clear `WasmScratch.mls`, moving its unique tests to `BuiltinOperators.mls`, `Casts.mls`, and `ReplImports.mls`. Co-Authored-By: Claude Opus 5.5 <noreply@anthropic.com>

LPTK

[Claude] This is my review of the PR at d41909e, updated with @LPTK's answers. The fixes are in b87501d. A follow-up commit, e5e6126, updates two line numbers in a golden output: comment edits in b87501d shifted them, and CI's no-changes check caught it. hkmc2AllTests/test passes at e5e6126 with no golden-output changes. The PR description now covers the design and the known limitations, and I've replied to the existing threads in place.

These are the findings that the existing threads didn't cover (details inline):

Wasm virtual dispatch could trap at run time (at Erasure.checkOverride): overrides are now checked against the members they override, and exposed open members must be annotated.
Without strict resolution, worksheet blocks fix the representations of public definitions (at newres/loose/ErasureAcrossBlocks.mls): this only affects diff tests, so the new tests record the behavior.
Generators got the representation of their final payload (at Erasure's callable results): fixed.
Builtin operator results had no representation (at BuiltinOperatorResults): they are now approximated, as a marked workaround.
Closure arguments are no longer inlined in Predef.mjs and Runtime.mjs: explained in the dead-param-elim/lambda.mls thread. Erased types are not the cause, and this is now listed as a known limitation.
Every class-typed Wasm slot is nullable: discussed in the wasm/VirtualMethods.mls thread, including placeholder objects for undefined.

Also in b87501d:

Conversion diagnostics have source locations (at Lowering.castTo).
The design decisions are documented (at doc/reference.md).
wasm/WasmScratch.mls is cleared. Its unique tests moved to wasm/BuiltinOperators.mls, wasm/Casts.mls, and wasm/ReplImports.mls, and the duplicates were deleted.

One more note: the merge commit d41909e also contains real changes. codegen/ScopedBlocks.mls now expects an infinite loop instead of an error, and the commit adds erasure tests. The new expectation looks right (a while … else whose branches all repeat never exits), but changes like these are easier to review in their own commit.

LPTK · 2026-10-18T11:47:18Z

+    * fail at run time. Parameters without declared types already take the inherited representations (see
+    * `inheritedParams` in `run`), so only declared ones can fail the parameter checks.
+    */
+  private def checkOverride(td: TermDefinition): Unit =


[Claude] Finding 1. On Wasm, an override is called through the virtual slot of the method that introduced it, but that slot's representations were inferred only from how the introducing method itself is used. Programs that work on hkmc2 trapped with RuntimeError: illegal cast, even within one block and with private classes:

private class P1() with open fun get() = P1() private class C1() extends P1() with override fun get() = "str" private fun read1(p) = p.get() read1(C1())

Since inheritance is open-world, @LPTK asked to check overrides rather than merge their representations into the base. b87501d does the following:

This check requires overrides to satisfy the erased signature of the member they override:

An unannotated override parameter takes the inherited representation (inheritedParams in run).

A declared parameter must admit the inherited representation, and on Wasm match it exactly.

The result must fit the inherited result. overrideResultType coerces a wider result of an unannotated override to the inherited one with checked casts. An unrelated result is reported here.

checkExposedOpenMember (below) requires an open member to annotate its parameters and result when its parameters receive values from the unit's interface. This is detected through the existing unknown propagation (UnknownValueShape.fromPublicInterface).

The tests are in wasm/VirtualMethods.mls (Producer/StrProducer is the program above with public classes, plus Consumer/EchoConsumer, O1/O2, and N1/N2) and in newres/Erasure.mls (JS). The library and the tests now annotate their exposed open members (Iter.mls, ObjectBuffer.mls, Runtime.mls, newres/Overrides.mls, newres/wasm/Super.mls).

LPTK · 2026-10-18T11:47:18Z

@@ -0,0 +1,34 @@
+:.
+
+// Worksheet blocks are compiled one after the other, and the representations erasure infers for a block's


[Claude] Finding 2. Without strictResolution, Elaborator.topLevel does not expose a block's public definitions to unknown callers, and each block's observations are sealed when the block completes. So later blocks must use the representations inferred from an earlier block's own uses:

ident("a") after ident(1) is rejected.

set counter = "hello" after let counter = 1 is rejected too, even under strict resolution, since top-level lets are not exposed to later writes.

Per @LPTK, this only matters for diff tests (compiled files expose their exports), so this file and wasm/ErasureAcrossBlocks.mls record the behavior rather than change it.

The Wasm file also has a :fixme for a crash that this behavior makes more likely. Reading b.v, where the representation of v is another session class, fails with Missing type definition for type index $Foo, because the session module does not import the types that its imported struct types refer to. A declared field type fails the same way.

LPTK · 2026-10-18T11:47:18Z

+    // Resolution gives calls of such functions the same wrapper shapes.
+    val callableResult =
+      if !config.language.useNewResolution then resultType
+      else td.resultWrapperAnnotation match


[Claude] Finding 3. Only @async results were special-cased, so @generator fun gen() = { yield 0; 1 } was lowered as gen(): Int, the representation of its final payload. This would mislead anything that trusts the IR's types. Fixed in b87501d:

TermDefinition.resultWrapperAnnotation covers both annotations. Async generators are not modeled; they are treated as async.

Resolution's listenDefinitionResult publishes an Iterator for generator calls, which resolves the :fixme in newres/GeneratorResults.mls.

Here, the callable returns an Iterator, while returns in the body are still coerced to the payload's representation (bodyResultType).

LPTK · 2026-10-18T11:47:18Z

+
+import hkmc2.utils.*, shorthands.*
+
+/** WORKAROUND: the builtin operators are not declared functions, and several of them are overloaded


[Claude] Finding 4. Builtin operators had no representation, so every write of a builtin result such as n - 1 into an inferred Int slot got a checked cast. Checked casts are effectful, so they blocked dead-code elimination and branch pushing. Examples are dead-param-elim/recursive.mls, sumPlus in dead-param-elim/todos.mls, and the extra name and localsMsg variables in Runtime.mjs. All three are now back to their hkmc2 output.

@LPTK pointed out that the proper fix is overloaded builtins, which is out of scope here. This object is the requested workaround, and it is marked as such here and at its two uses (NewResolver.builtinApplication and ErasedType.builtinOperatorResult). Notes:

Resolution and IR erasure share these rules, so the representation inferred for a slot agrees with the erased type of the application flowing into it.

The rules apply to the JS target only. On Wasm, operators lower to dynamically typed intrinsics (wasm.*_impl), and their results are unknown.

Like InvalML's prelude signatures, the rules assume that Int arithmetic stays within Int, so an overflow to Infinity is not detected. As a result, fun f(x: Int, y: Int): Int = x + y no longer gets a checked cast. codegen/CheckedCasts.mls and codegen/ErasedTypes.mls now use Num operands so that they still test casts.

The casts that remain in opt/DeadAssignmentRemoval.mls have other causes (see that thread).

LPTK · 2026-10-18T11:47:18Z

    */
  def castTo[R <: Result](r: R, expected: Opt[ErasedType], loc: Opt[Loc]): (R | Cast) =
-    r.coerceTo(expected.getOrElse(ErasedType.Unknown), loc)
+    r.coerceTo(expected.getOrElse(ErasedType.Unknown), loc.orElse(r.toLoc))


[Claude] From my review: conflicts in inferred slots were reported without a source location (═══[COMPILATION ERROR] Types 'Int32' and 'Unknown' have no common representation). Fixed in b87501d:

A coercion without a better location now points at the coerced value.

A field synthesized from a constructor parameter points at the field's name (the ValDefn case).

The errors of the Wasm backend's castConserve carry the location of the value being cast.

LPTK · 2026-10-18T11:47:18Z

 still reported. Dynamic values also do not remove the need for an unambiguous
 class or type identity in constructor patterns, class projections, or type references.

+### Runtime Representations


[Claude] As @LPTK asked, the two design decisions from my review are now explicit:

undefined is an unspecified value, and reading it back is undefined behavior. This is documented here, in the literal table above, and in Block.isUndefined.

Programs whose only problem is a misleading annotation are now rejected. This is documented here and in the Erasure class documentation.

This section also covers interface exposure, worksheets, overrides, and the builtin-operator approximation.

LPTK · 2026-10-18T11:47:18Z

+      td.body.foreach(body => listenResult(body)(publish))
+      // Mutable fields admit replacements not represented by initializer flow.
+      // Keep the resolver's unknown-write alternative when choosing their storage.
+      if (td.k is syntax.MutVal) || mutableField then


[Claude] Re @LPTK's question about my remark that mutable fields "stay untyped correctly": I meant that the PR handles them conservatively. Resolution does not observe writes through selections (set o.f = v; assignVariable only tracks variables), so an initializer's shapes do not cover later writes. This line adds an unknown input instead, so mutable fields keep the top representation, including when later blocks write to them.

Agreed that they should be typed from their shapes, and that open-ended mutable fields exposed through the unit's interface should require an annotation. For that, resolution needs to route each field write to the field's host, for every class the receiver can be an instance of, and add an unknown write for fields reachable from the interface. I'd do this as a follow-up.

[Astra] The mutable-field inference described as a follow-up above is now implemented in this PR (8bfe6a3 and 1b878f2), and 081891b fixes the remaining exposure and variance problems.

Exposure now follows values assigned into escaping record fields as well as their initializers, including fields copied through nested mutable spreads and assignments discovered after exposure. It preserves the member scope paths and generic substitutions. Thus an assigned object with an unannotated mutable class field gets the required annotation error, and an assigned callback receives unknown external inputs. The three previously documented exposure failures are now ordinary passing regression tests.

The variance concern was correct: one substituted field type cannot represent both bounds. Structural fields now retain separate input/output types internally, and the syntax { mut f: in S out T } is supported. Inputs are contravariant and outputs covariant; they are interpreted separately before substitution. This also applies through aliases and enclosing negative positions. Omitted inputs are Nothing, omitted outputs are Any, and intersecting record interfaces unions shared field inputs while intersecting their outputs. Writes through both structural and nominal interfaces constrain assigned callbacks against the input bound rather than the read bound.

The regressions cover these cases, recursive fields, generic capture and factory-call isolation, and a control ensuring that exposing an immutable source does not expose writes to its mutable copy. ctest, dtest MutableField, and the full hkmc2AllTests/test pass at 081891b, with all golden outputs committed and pushed. The exposure merge blocker is addressed; the PR description and language reference now describe the implemented behavior.

Follow-up on ordinary mutable fields: before 081891b, the reverse constraint only reached concrete assignable fields; it was skipped when the source was a declared record interface. This was a bug even without wildcard syntax. The new listenFieldInput path makes { mut f: S } <: { mut f: T } propagate both S <: T for reads and T <: S for writes. mut { f: S } uses the same rule. Commit 632d227 adds six direct regressions covering both directions and immutable-destination controls. Removing only that new reverse path makes both write-direction tests fail; with it restored, the full hkmc2AllTests/test suite passes.

These are the resolver's constraints for inference and callback checking, rather than a complete structural subtype checker. New resolution does not diagnose all concrete subtype mismatches, and InvalML does not yet support structural record types. The reference and PR description now state that limitation explicitly.

The internal errors that `newres/Overrides.mls` records cite their location in NewResolver.scala, which moved when comments were added there. Co-Authored-By: Claude Opus 5.5 <noreply@anthropic.com>

A backtracking assignment `set x = v in body` saves `x` in an `old` temporary and restores it in a `finally` block. The temporary had no representation, so saving and restoring it converted from and back to the representation of `x`. This was a checked cast that dead-code elimination must keep (on JS), and an error for an unboxed `Int32` variable (on Wasm). Erasure now treats the temporaries that elaboration declares with `LetDecl` (currently only this one) as slots like source variables, inferring their representations from the values flowing into them. Co-Authored-By: Claude Opus 5.5 <noreply@anthropic.com>

- Route assignments to fields (`set o.f = v`, including compound and temporary assignments) to the fields they assign: resolve the assigned member as selections do, for every class that the receiver can be an instance of (including through projections, wildcard opens, annotated receivers, and captures), and record the assigned values in each field's host (`NewResolver.assignField` and `writeField`). - Infer the erased type of an unannotated mutable field from its initializer and its assignments, replacing the blanket unknown input. Record fields are included: a mutable copy `mut {...r}` assigns the fields of `r`. - Make reads of unannotated mutable fields observe their assignments. A read used to see only the initializer, so a member could be resolved statically in the initializer's class while an instance of another class had been assigned (a silent miscompilation on Wasm). - Interface exposure assigns unknown values to the mutable fields (and mutable record fields) that a compilation unit exposes, and `Erasure.checkExposedMutableField` requires exposed mutable fields to declare their types. Annotate such fields in the library, the apps, and the tests. - Share the projection lookup of `newSel` (`projectedLookup`). - Document mutable fields in Runtime Representations, and add tests, with :fixme regressions for assignments through structural types and for private classes used in later Wasm worksheet blocks. Co-Authored-By: Claude Opus 5.5 <noreply@anthropic.com>

- Record fields can be declared mutable with `mut`, in record literals (`{mut count: 0, label: "x"}`) and record types (`{mut item: T}`). Other fields are immutable, unless their whole record is (`mut {...}`). A record literal with a mutable field is allocated unfrozen; resolution assumes its other fields are never assigned, which type checking will ensure. - Through a record type, the values it describes can be assigned values of the types of its mutable fields: `constrainRecord` assigns such values to the actual values' assignable fields, as `constrainFunction` feeds the declared parameter types to callbacks. Assignments through record types' immutable fields are assumed not to happen, so assignments through record types need not be followed. Record type views carry their mutable fields. - Reads of mutable record fields return their initializer and the values assigned to them, instead of values of unknown shape. - Interface exposure assigns unknown values to the mutable fields of exposed records. - Share the resolution of assignable fields between assignments and record constraints (`assignableTargets`, `listenAssignedValues`). - Update the reference and the tests: the structural-assignment :fixme is resolved, and the record :fixmes now only reflect that resolution is not flow-sensitive. Co-Authored-By: Claude Opus 5.5 <noreply@anthropic.com>

Diagnostics now cite definition headers, and internal-error line numbers shifted. Co-Authored-By: Claude Opus 5.5 <noreply@anthropic.com>

LPTK · 2026-10-19T06:10:39Z

-//│ set tmp1 = Predef⁰.hide⁰(4);
-//│ set tmp2 = +⁰(tmp1, 1);
-//│ return Predef⁰.print⁰(tmp2)
+//│ set x = (tmp as! Int⁰);


[Claude] Update: the old cast is fixed in d710d52. Erasure now infers the representation of the temporary that set … in declares, like a source variable, so the set … in test below is back to its hkmc2 output. (On Wasm, the same untyped temporary made set x = … in an error for an unboxed Int32 variable; newres/wasm/Erasure.mls now covers that.) The casts of hide's results remain.

LPTK · 2026-10-19T11:17:25Z

+      td.body.foreach(body => listenResult(body)(publish))
+      // Mutable fields admit replacements not represented by initializer flow.
+      // Keep the resolver's unknown-write alternative when choosing their storage.
+      if (td.k is syntax.MutVal) || mutableField then


[Astra] The mutable-field inference described as a follow-up above is now implemented in this PR (8bfe6a3 and 1b878f2), and 081891b fixes the remaining exposure and variance problems.

Exposure now follows values assigned into escaping record fields as well as their initializers, including fields copied through nested mutable spreads and assignments discovered after exposure. It preserves the member scope paths and generic substitutions. Thus an assigned object with an unannotated mutable class field gets the required annotation error, and an assigned callback receives unknown external inputs. The three previously documented exposure failures are now ordinary passing regression tests.

The variance concern was correct: one substituted field type cannot represent both bounds. Structural fields now retain separate input/output types internally, and the syntax { mut f: in S out T } is supported. Inputs are contravariant and outputs covariant; they are interpreted separately before substitution. This also applies through aliases and enclosing negative positions. Omitted inputs are Nothing, omitted outputs are Any, and intersecting record interfaces unions shared field inputs while intersecting their outputs. Writes through both structural and nominal interfaces constrain assigned callbacks against the input bound rather than the read bound.

The regressions cover these cases, recursive fields, generic capture and factory-call isolation, and a control ensuring that exposing an immutable source does not expose writes to its mutable copy. ctest, dtest MutableField, and the full hkmc2AllTests/test pass at 081891b, with all golden outputs committed and pushed. The exposure merge blocker is addressed; the PR description and language reference now describe the implemented behavior.

Follow-up on ordinary mutable fields: before 081891b, the reverse constraint only reached concrete assignable fields; it was skipped when the source was a declared record interface. This was a bug even without wildcard syntax. The new listenFieldInput path makes { mut f: S } <: { mut f: T } propagate both S <: T for reads and T <: S for writes. mut { f: S } uses the same rule. Commit 632d227 adds six direct regressions covering both directions and immutable-destination controls. Removing only that new reverse path makes both write-direction tests fail; with it restored, the full hkmc2AllTests/test suite passes.

These are the resolver's constraints for inference and callback checking, rather than a complete structural subtype checker. New resolution does not diagnose all concrete subtype mismatches, and InvalML does not yet support structural record types. The reference and PR description now state that limitation explicitly.

Integrate the lowered parameter-list and member-key APIs with inferred representations, mutable-field bounds, flow cast proofs, and Wasm calls. Coerce dynamically extracted optional/trailing slots and check statically aligned trailing arguments against their destination representations. Keep generator/async body payloads separate from inherited callable result wrappers, and handle literal tests when deforestation fuses through a proved cast. Add regression coverage for both cases. Audit branch-added tests, consolidate overlapping optional and mutable-field cases, and move AI-authored diff files into slop while preserving strict, loose, JS, and Wasm configurations. Record overwritten-field exposure and trailing-parameter override gaps as explicit known-failure regressions. Regenerate and include all affected golden output, adapting older cast fixtures to the new default resolution mode with explicit Any interfaces. Validation: ctest; focused erasure and slop tests; hkmc2AllTests/test (1,128 tests passed).

Respect overwritten record fields and distinguish exposing a frozen spread copy from admitting external writes into its source. Inherit and check rest/trailing parameter representations when overriding layouts correspond. Select fused match arms using ordered subtype tests, specialize default closures by constructor layout, and require proofs that elided construction is harmless and projected fields retain their original argument values. Preserve effectful constructors, superclass effects, qualifiers, and lifted argument layouts. Consolidate regression cases in slop and include regenerated golden outputs. Record incompatible override-layout behavior pending a language policy decision. Remove implicit default overloads from the touched compiler APIs. Validation: ctest (56 tests), hkmc2AllTests/test (1,128 tests), git diff --check.

Resolve the golden-output conflicts and retain OptionalBinding instead of restoring the duplicated OptionalNull suite. Adapt consolidated regression tests to the new strictres configuration, preserving strict and eager resolution for the Wasm mutable-field tests as well. Include regenerated golden outputs for upstream rest-parameter inference and changed diagnostic locations. Validation: ctest (56 tests), sdtest (31 tests), and hkmc2AllTests/test (1,131 tests) all pass.

Derppening

I took a cursory look at the core ErasedType and WASM backend changes , as well as the updated diffs. They all look good to me.

LPTK · 2026-10-30T05:43:25Z

I took a cursory look at the core ErasedType and WASM backend changes , as well as the updated diffs. They all look good to me.

Thanks!

Builtin applications lacked result shapes, while exhaustive splits and loops could contribute spurious normal values. Share operand-dependent builtin result rules between resolution and IR, track ordered branch fallthrough and loop repetition, and avoid lowering unreachable continuations. Keep Wasm builtin results conservative. Extract B02 (E09 and E16) from PR #575. Add focused JS and explicitly typed Wasm regressions, retain narrowing-cast coverage with Num inputs and a fractional SCC result, and include the regenerated goldens and builtin approximation documentation. Validation: Metals compilation, ctest and cwtest, focused diff tests, and hkmc2AllTests/test (1,157 tests). Confirmed the builtin-call and abortive-control-flow regressions fail on the extraction base. Reviewed the complete diff and checked whitespace. Co-authored-by: Codex <codex@openai.com>

Integrate hkust-taco#599 and hkust-taco#600 while preserving inferred erasure and representation-changing deforestation. Reconcile shared function signatures with retyped and refreshed bindings, retain inferred wrapper regressions, and adapt the cast-comment fixtures to inference and cast elimination. Update the extraction plan and include regenerated golden outputs. Validation: Metals hkmc2JVM compilation and hkmc2AllTests/test (1,172 tests).

Use the upstream override layout and representation checks while retaining shape-based erasure. Keep inherited result signatures unchanged, validate only current declarations, and reserve physical Wasm result adaptation for undefined values. Make Iterator a structural protocol so collection implementations satisfy the newly annotated interfaces, and resolve generator results through the same alias. Preserve the upstream optional-call and immutability fixes, carry forward their regressions, and regenerate golden output. Validation: hkmc2AllTests/test passed all 1,200 tests.

Integrate a95f0e1, preserving representationless Nothing, non-null Wasm placeholders, backend-owned calling conventions, and the resolver fixes. Adapt coerceToOr to the Cast smart constructor's Path result, the new record graph-growth regression to field input/output types, and the heterogeneous optional-argument fixture to an explicit Any input. Regenerate affected golden output and update the extraction plan with E17-E18 as the next focused candidate (30 Scala additions, 12 removals). Validation: hkmc2AllTests/test passed all 1,210 tests with an 8 GB heap; Metals hkmc2JVM compilation passed.

Adapt inferred erasure and deforestation to shared argument layouts, split cast nodes, and retained definition symbols. Preserve pattern-local erasure and incoming regression coverage, regenerate goldens, and update the extraction plan. Validation: Metals hkmc2JVM compilation and hkmc2AllTests/test (1,294 tests).

Retain structural Iterator, E27 effect/value separation, and E32 mutable-write exposure. Defer E20–E24, E31, E35, and E36 with ten targeted fixmes that preserve the failing regressions' assertions. Restore the optional-binding fixtures and unused runtime helper, and update the extraction plan and generated outputs. Validation: hkmc2AllTests/test passed all 1,293 tests. The Scala diff against hkmc2 shrinks by 261 changed lines across three fewer files.

Integrate implicit-namespace resolution and tail-resumptive handler improvements through fdddc58 while preserving inferred erasure, constructor signatures, and mutable-field read/write flow. Adapt field bounds to the separated type-argument representation and preserve namespace probes through explicit projections. Keep structural constraint scope paths when descending through tuple, record, and function aliases; this fixes the repeated-scope assertion exposed by erasure observations. Add diff regressions for nested generic results and implicit namespaces in mutable-field assignments. Include refreshed golden outputs and update the extraction plan's upstream snapshot. Validation: hkmc2AllTests/test passed all 1,338 tests.

LPTK · 2026-11-09T08:12:19Z

-//│ define main⁰ as fun main¹(): ? {
-//│   let i: ?, f: ?, s: ?, b: ?, t: ?, r: ?, x: ?, y: ?;
+//│ define main⁰ as fun main¹(): Unit⁰ {
+//│   let i: Int⁰, f: Num⁰, s: Str⁰, b: Bool⁰, t: Array⁰, r: Unknown, x: Int⁰, y: Str⁰;


For a follow-up PR: a record literal should have erased type Object, not Unknown.

LPTK and others added 2 commits October 15, 2026 14:26

WIP

484eafb

Compute runtime erased types from completed resolution shapes

45842c6

LPTK added the slopfest label Oct 15, 2026

LPTK commented Oct 15, 2026

View reviewed changes

LPTK and others added 8 commits October 15, 2026 16:29

WIP

fca467d

Shorten i32 constants in erasure regressions

0629de9

Eliminate casts made redundant by IR simplification

1f5390b

Preserve function representations when lowering lambdas

f853f10

Preserve representations across deforestation rewrites

551e4a8

Preserve checked arguments when propagating partial calls

3caffd0

Fuse constructors through casts proved by flow analysis

35fa0bd

Preserve existing spacing in Wasm regression tests

c6b0f63

LPTK force-pushed the compute-erased-types-from-shapes branch from 149217f to c6b0f63 Compare October 15, 2026 10:15

codex and others added 2 commits October 18, 2026 12:01

LPTK commented Oct 18, 2026

View reviewed changes

claude and others added 9 commits October 18, 2026 19:49

Update golden output for shifted internal-error line numbers

e5e6126

The internal errors that `newres/Overrides.mls` records cite their location in NewResolver.scala, which moved when comments were added there. Co-Authored-By: Claude Opus 5.5 <noreply@anthropic.com>

Merge branch 'hkmc2' into compute-erased-types-from-shapes

eb47bae

Update golden output after rebasing mutable-field work

c0af69c

Diagnostics now cite definition headers, and internal-error line numbers shifted. Co-Authored-By: Claude Opus 5.5 <noreply@anthropic.com>

test: cover values escaping through mutable record assignments

9539de3

Fix mutable-field exposure and preserve read/write variance

081891b

test: verify both mutable record constraint directions

632d227

LPTK commented Oct 19, 2026

View reviewed changes

LPTK marked this pull request as ready for review October 19, 2026 12:10

codex added 3 commits October 23, 2026 00:16

Derppening reviewed Oct 30, 2026

View reviewed changes

LPTK mentioned this pull request Oct 30, 2026

Resolve builtin results and abortive expression flow #598

Merged

codex added 2 commits October 30, 2026 14:08

Merge expression-result extraction from hkmc2

5058fd3

Record async and generator results extraction

d18c25e

This was referenced Oct 30, 2026

Separate async and generator body results from callable wrappers #599

Merged

Preserve callable signatures through IR transformations #600

Merged

This was referenced Oct 30, 2026

Locate representation conversion diagnostics at their source #601

Merged

Preserve override argument bindings and runtime representations #602

Merged

codex added 7 commits November 2, 2026 23:08

Record independently validated PR 575 extraction branches

c51a855

Merge hkmc2 Iterator and effect-flow updates

ae50d88

Merge hkmc2 and separate optimizer and record-syntax follow-ups

f74e393

codex and others added 2 commits November 9, 2026 15:48

Minor

7983b39

LPTK commented Nov 9, 2026

View reviewed changes

Add some IR doc about casts

ec2f9b2

LPTK force-pushed the compute-erased-types-from-shapes branch from 739a53d to 8814a72 Compare November 10, 2026 06:10

Merge branch 'hkmc2' into compute-erased-types-from-shapes

51ee553

LPTK force-pushed the compute-erased-types-from-shapes branch from 8814a72 to 51ee553 Compare November 10, 2026 06:58

		@@ -0,0 +1,34 @@
		:.

		// Worksheet blocks are compiled one after the other, and the representations erasure infers for a block's


		import hkmc2.utils., shorthands.

		/** WORKAROUND: the builtin operators are not declared functions, and several of them are overloaded

Conversation

LPTK commented Oct 15, 2026 • edited Loading Uh oh! There was an error while loading. Please reload this page.

Uh oh!

Uh oh!

Choose a reason for hiding this comment

Uh oh!

LPTK Oct 15, 2026 • edited Loading Uh oh! There was an error while loading. Please reload this page.

Uh oh!

Choose a reason for hiding this comment

Uh oh!

Choose a reason for hiding this comment

Uh oh!

Choose a reason for hiding this comment

Uh oh!

LPTK Oct 15, 2026 • edited Loading Uh oh! There was an error while loading. Please reload this page.

Uh oh!

Choose a reason for hiding this comment

Uh oh!

Choose a reason for hiding this comment

Uh oh!

Choose a reason for hiding this comment

Uh oh!

Choose a reason for hiding this comment

Uh oh!

Choose a reason for hiding this comment

Uh oh!

Choose a reason for hiding this comment

Uh oh!

LPTK Oct 15, 2026 • edited Loading Uh oh! There was an error while loading. Please reload this page.

Uh oh!

Choose a reason for hiding this comment

Uh oh!

Choose a reason for hiding this comment

Uh oh!

Choose a reason for hiding this comment

Uh oh!

LPTK Oct 15, 2026 • edited Loading Uh oh! There was an error while loading. Please reload this page.

Uh oh!

Choose a reason for hiding this comment

Uh oh!

Choose a reason for hiding this comment

Uh oh!

Choose a reason for hiding this comment

Uh oh!

LPTK Oct 15, 2026 • edited Loading Uh oh! There was an error while loading. Please reload this page.

Uh oh!

Choose a reason for hiding this comment

Uh oh!

Choose a reason for hiding this comment

Uh oh!

Choose a reason for hiding this comment

Uh oh!

LPTK Oct 15, 2026 • edited Loading Uh oh! There was an error while loading. Please reload this page.

Uh oh!

Choose a reason for hiding this comment

Uh oh!

Choose a reason for hiding this comment

Uh oh!

Choose a reason for hiding this comment

Uh oh!

Choose a reason for hiding this comment

Uh oh!

Choose a reason for hiding this comment

Uh oh!

Choose a reason for hiding this comment

Uh oh!

Choose a reason for hiding this comment

Uh oh!

Choose a reason for hiding this comment

Uh oh!

Choose a reason for hiding this comment

Uh oh!

Choose a reason for hiding this comment

Uh oh!

Choose a reason for hiding this comment

Uh oh!

LPTK Oct 15, 2026 • edited Loading Uh oh! There was an error while loading. Please reload this page.

Uh oh!

Choose a reason for hiding this comment

Uh oh!

LPTK commented Oct 15, 2026 •

edited

Loading

LPTK Oct 15, 2026 •

edited

Loading

LPTK Oct 15, 2026 •

edited

Loading

LPTK Oct 15, 2026 •

edited

Loading

LPTK Oct 15, 2026 •

edited

Loading

LPTK Oct 15, 2026 •

edited

Loading

LPTK Oct 15, 2026 •

edited

Loading

LPTK Oct 15, 2026 •

edited

Loading

LPTK left a comment •

edited

Loading