[LPTK]

[Astra] Description originally drafted by Claude Code and updated following review at @LPTK's request.

Summary

With new resolution (#lang(0.3.x)), erasure now infers the runtime representation (erased type) of unannotated slots (parameters, results, let bindings and other variables, and fields) from the shapes that resolution observes flowing into them. Previously only annotations gave slots a representation, and every other slot was unknown. Annotations still fix the representations of their slots.

Lowering converts each value to the representation of the slot it flows into, using the existing coerceTo. A value whose representation is already within the target's needs no cast, a downcast becomes a checked cast, and unrelated representations are a compilation error. On Wasm, the inferred representations select the physical types: an Int32 slot is an unboxed i32, and a slot of class instances is a reference to the class's struct.

The user-facing rules are documented under Runtime Representations in doc/reference.md.

Design

• Observation (resolution). NewResolver.prepareErasure registers one host per erasable source slot in ErasureInputs, in the slot's defining compilation unit. The host collects the shapes flowing into the slot until completeBlock seals it. ErasureDeclarations enumerates the slots that are not reachable through subStatements: split bindings, handler parameters, auxiliary constructor parameters, and synthesized record fields. Observation and assignment share this enumeration, so every delayed slot is prepared before erasure reads it. Resolution stores no erased types on source symbols.
• Assignment (erasure). Erasure maps each observed shape to a value type, and the slot gets the union of these types (inferredType). This includes the temporary that lowering introduces for set … in.
• Mutable fields. Resolution observes field initializers and later writes through selections (set o.f = v), routing each write to the possible receiver fields. Field reads and erasure include these assigned values. An unannotated mutable field can therefore have a precise representation, including an unboxed Wasm representation.
• Mutable record fields. {mut field: value} declares an individually mutable field; mut {...record} also makes its copied fields assignable. Record-field writes participate in resolution. Record fields cannot declare their types, so exposed mutable record fields admit unknown writes and keep the top representation.
• Mutable field interfaces and variance. Structural fields retain separate write and read types. { mut f: in S out T } accepts S on writes and exposes T on reads; omitted inputs are Nothing, and omitted outputs are Any. An ordinary { mut f: A } interprets A separately in the two polarities before substitution, so substituting in S out T preserves both bounds, including inside aliases and negative positions. Thus { mut f: S } <: { mut f: T } contributes both S <: T (reads) and T <: S (writes); mut { f: S } follows the same rule. Shared fields in record intersections union their input types and intersect their output types. Assignments through structural and nominal interfaces constrain callbacks against the write type, independently of the read type.
• Interface exposure. Exposed definitions receive unknown inputs (see InterfaceExposure), so the representations of their unannotated parameters stay general. Mutable class fields reachable through the unit's interface must declare their types (Erasure.checkExposedMutableField), because external writes cannot be inferred from local uses. Exposing a record follows both its field initializers and assigned values, including assignments arriving later and fields copied through nested mutable spreads. The traversal preserves member scope paths and generic substitutions, so assigned objects and callbacks receive the same exposure checks as initializers.
• Overrides. An override shares the representations of the member it overrides. Its unannotated parameters take the inherited representations. Its declared parameters must admit the inherited ones, and on Wasm they must match them exactly, because Wasm calls overrides through the signature of the method that introduced the virtual slot. Its results must fit the inherited result. Mismatches are compilation errors (Erasure.checkOverride).
• Exposed open members. Subclasses in other compilation units must implement an open member with the representations of its erased signature. So an open member whose parameters receive inputs from the unit's interface must annotate its parameter and result types (Erasure.checkExposedOpenMember).
• Wrapped results. Once all of their written parameter lists are applied, @async functions return a Promise and @generator functions an Iterator. Their bodies produce only the payload (Erasure.bodyResultType).
• Builtin operators (WORKAROUND). The builtins are not declared as overloaded functions yet. On the JavaScript target, resolution and IR erasure therefore approximate operator results from the primitive classes of the operands, using the same rules (semantics.BuiltinOperatorResults). For example, Int + Int is an Int, and + with a Str operand is a Str. On Wasm, operators lower to dynamically typed intrinsics, and their results are unknown. This logic should be removed once the builtins are properly overloaded.
• undefined. undefined is an unspecified value of any representation, and reading it back is undefined behavior. A backend may therefore materialize it as any value of the slot's representation: on Wasm, 0 for an i32 slot, or a null reference. The placeholders that dead-parameter elimination passes rely on this.

Optimizer and backend changes

• BlockSimplifier removes casts that propagation and inlining make redundant, including checked casts whose check is guaranteed to succeed. Narrowing casts and their evaluation order are kept. When it propagates a partial application, checked arguments are evaluated at the original site, leaving a pure call prefix.
• Flow analysis proves each cast against all of its incoming producers, so deforestation can fuse constructors through casts. Any unknown or incompatible input invalidates the proof.
• Deforestation recomputes the representations of fused parameters, results, captured values, and locals. Generated branch functions keep their two parameter lists.
• Generated lambdas keep a function representation. The lifter, eta-expansion, polymorphic instantiation, and the symbol refresher preserve the representations of the slots they create.
• Wasm: overrides are compiled with the signature of the method that introduced the virtual slot, bridged by ref.cast. Lowering maps builtin operators to the wasm.*_impl intrinsics, and WatBuilder rejects any remaining builtin calls. Slots of class instances are nullable so that they can hold undefined.

Programs that are now rejected

Because inferred representations are as binding as declared ones, some programs that used to compile, and run on the JavaScript backend, are now rejected. This includes programs whose only problem is a misleading annotation. Fixing these errors uncovered bugs in the compiled test sources:

• The parsing app passed a list where argument: Tree is declared (Tree.App(op, acc :: rhs :: Nil), now Tree.Tuple(...)), and built a Tree.Error with the wrong arguments. These fixes change the app's printed output.
• nofib/fish.mls passed a string as a list (showl(xs, ""), now Nil).
• Two nofib ports used String to mean List[Char]; they now declare type String = List[Char].

Exposed open members, including abstract ones, now have annotations in the library sources (Iter.mls, ObjectBuffer.mls, Runtime.mls). Exposed mutable class fields also require annotations; private fields whose writes are confined to the unit can be inferred.

Known limitations

• Structural subtype checking. New resolution propagates record constraints for type-argument inference and callback checking, including both directions for mutable fields. It does not perform complete structural subtype checks, and InvalML does not yet support record types. Preserving these constraints does not mean every invalid record ascription is diagnosed.
• Separately compiled polymorphic functions such as Predef.hide have unknown physical results. Binding such a result to a narrower inferred slot therefore needs a checked cast, and dead writes of these results survive dead-assignment removal because checked casts are effectful (opt/DeadAssignmentRemoval.mls).
• Closures passed as arguments stay bound to a temporary in the JavaScript output (lambda$here in Predef.mjs and Runtime.mjs). Call arguments must be paths, and the simplifier only propagates pure calls into Result positions. On hkmc2, the call reached the argument only because it was wrapped in a checked cast to Function, and that cast is no longer needed.
• Nullable Wasm class slots admit undefined, but field reads can need extra non-null casts, including redundant nested casts. Non-null placeholders or tracking whether undefined can reach a slot remain optimization follow-ups.
• Builtin operator approximation applies to the JavaScript target only. Like InvalML's prelude signatures, it assumes that Int arithmetic stays within Int: an overflow to Infinity is not detected.
• Worksheets without #lang(strictResolution: true) infer the representations of public definitions from the uses in their own block. Later blocks must use these representations consistently (see newres/loose/ErasureAcrossBlocks.mls). This affects only diff tests: compiled files expose their exports.
• Wasm REPL:
  • Reading a field whose representation is another session class crashes code generation, because the type import is missing (:fixme in wasm/ErasureAcrossBlocks.mls). A declared field type fails the same way, but inference makes such fields more common.
  • Writes to REPL globals are not visible to later blocks. This predates the PR.

Validation

• Local ctest and hkmc2AllTests/test pass at 632d227cb. All updated golden outputs are committed.
• newres/MutableFieldExposure.mls now checks the assigned-object, copied-field, and assigned-callback cases as ordinary regressions, without :breakme markers. It also covers nested spreads, writes discovered after exposure, generic captures, isolation between separate factory calls, and a control ensuring that exposing an immutable source does not expose writes to its mutable copy.
• newres/MutableFieldVariance.mls covers split input/output bounds, positive and negative substitution through aliases, one-sided bounds, structural and nominal callback writes, intersections, whole-record mutability, and recursive fields. The existing bounded recursive-intersection test still passes.
• newres/MutableRecordConstraints.mls separately checks the read and reverse write constraints for both { mut f: S } and mut { f: S }, with immutable-destination controls. Removing the reverse constraint added in 081891b34 makes the two write-direction regressions fail.

[LPTK]

Why are casts now inserted here?

[LPTK]

[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.

[LPTK]

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

[LPTK]

Why is this optimization lost?

[LPTK]

[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.

[LPTK]

[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]

Why is a cast now inserted here?

[LPTK]

[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.

[LPTK]

[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]

Can we avoid this unsightly case?

[LPTK]

[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.

[LPTK]

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

[LPTK]

This looks like a concerning regression.

[LPTK]

[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.

[LPTK]

[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]

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

[LPTK]

[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.

[LPTK]

[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]

Why the new cast?

[LPTK]

[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.

[LPTK]

[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.

[LPTK]

[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]

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

[LPTK]

[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.

[LPTK]

[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]

Why is this now nullable?

[LPTK]

[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.

[LPTK]

[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.

[LPTK]

Looks like this is no longer inlined.

[LPTK]

[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.

[LPTK]

[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.

[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):

1. 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.
2. 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.
3. Generators got the representation of their final payload (at Erasure's callable results): fixed.
4. Builtin operator results had no representation (at BuiltinOperatorResults): they are now approximated, as a marked workaround.
5. 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.
6. 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]

[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]

[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]

[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]

[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:

1. 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.
2. The rules apply to the JS target only. On Wasm, operators lower to dynamically typed intrinsics (wasm.*_impl), and their results are unknown.
3. 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.
4. The casts that remain in opt/DeadAssignmentRemoval.mls have other causes (see that thread).

[LPTK]

[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]

[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]

[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.

[LPTK]

[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.

[LPTK]

[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]

[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.