Implement Typed IR

[Derppening]

No description provided.

[LPTK]

Some possible next immediate steps:

• Update printer to show the erased types at variable and member declaration/definition sites.
• Update Lowering so it generates erased types from parameter type annotations, to be used to annotate the corresponding VarSymbol.
• Make sure we are never overriding an existing erased type in a given symbol by using softAssert, as a sanity check.

A subtlety we should get right: the erasure of annotated class parameter types should successfully propagate to their defining fields. Param has a ``fldSym` which can be used for this.

[LPTK]

It seems many cases like this one should carry over the previous erasedType somehow.

[Derppening]

The current task list (work items created by me, organized by AI):

• Phase A — erasedType on Result (keystone infra) — ✅ committed

  • Enum redesign — PrimitiveType.Array + totalized sym; three-case ErasedType; ErasedType.sym; erasedType_!; Normalization → ObjectRef
  • Infra — Result extends HasErasedType; lazy val erasedType; abstract def on trait; Value's override val removed; this match over Tuple/Record/Instantiate/Value
  • Materialization sweep (Cat 1 + 2 + 3) — all applied, compiles clean, committed
  • Core sites (subTerm, ReflectionInstrumenter.assign, ValDefn.mk); join-point traps left N

• Phase B — printer baseline (was C1) — captures post-A erasedType so later tightening shows as a diff

  • showErasedType toggle in Printer.scala (mirror showPurity, default OFF); render at variable + member declaration/definition sites
  • Commit one curated baseline test file (tuple/instantiate/lit/record/call/select/val-def, ≥1 case through Lifter) with post-A types as-is

• Phase C — Annotation-driven erasedType + invariant guard (was Phase B; lands right after the B baseline)

  • Param-annotation → VarSymbol (Lowering erases param type annotation onto the VarSymbol)
  • Class-param erasure → defining field via Param.fldSym
  • softAssert no-clobber invariant (never override an existing symbol erasedType)

• Phase D — WatBuilder consumes ErasedType (was C2; correctness harness)

  • Drive anyref cast targets from operand erasedType (additive + N-graceful); WASM goldens shift here
  • Optional explicit asserts when a known erasedType contradicts the required use-site type

• Phase E — FuncRef + AnyFuncRef (was Phase D)

  • Add AnyFuncRef coarse constant, then FuncRef(params, result)
  • Fill Lambda → FuncRef

• Phase F — refine residual inference (was Phase E)

  • Call return types (easy win: builtin-op result-type table, survey §6)
  • Select/DynSelect field/member types
  • rest params; Lifter capture symbols; function results
  • revisit resSym/l sites left N in Phase A

[LPTK]

• join-point traps left N

What does that mean?

• C1 — showErasedType toggle in Printer.scala

This should be moved to phase B. In fact, it's the first thing yoiu should do, just so you can actually see what you're doing!

[Derppening]

• join-point traps left N

What does that mean?

erasedType = N, will be left for Phase D.

What does that mean?

• C1 — showErasedType toggle in Printer.scala

This should be moved to phase B. In fact, it's the first thijng yoiu should do, just so you can actually see what you're doing!

Good point, I have updated to task list.

[Derppening]

The core logic is mostly implemented - I will review the entire patchset's changes before marking it as ready.

There are also several issues that needs to be clarified/fixed, namely:

• For the checkCast config, we agreed that it would affect whether the Cast node is pure. But the config primarily controls frontend compilation behavior, correct?
• There are two failing tests due to unreachable type propagation issues. I will fix them in another branch, since they are not relevant to typed IR and is specific to the Wasm backend.
• I am not sure if the Cast(Lit, _) extraction for copy propagation is correct - Would be nice if you can take a look.

[LPTK]

• For the checkCast config, we agreed that it would affect whether the Cast node is pure. But the config primarily controls frontend compilation behavior, correct?

Incorrect.

The actual problem is that I think we have many places that use isPurewithout a Config in scope. We should probably just add a checked flag to Cast that is only true when checkCast is.

• There are two failing tests due to unreachable type propagation issues. I will fix them in another branch, since they are not relevant to typed IR and is specific to the Wasm backend.

No idea what you mena. Is this a WASM thing?

• I am not sure if the Cast(Lit, _) extraction for copy propagation is correct - Would be nice if you can take a look.

Just check who uses this valueAnalysis thing where the cast is dropped (or do you mean somewhere else?). There's no reason to assume that the cast is no longer needed after the value is propagated. You can see that, right?

[Derppening]

The actual problem is that I think we have many places that use isPure without a Config in scope. We should probably just add a checked flag to Cast that is only true when checkCast is.

Just to clarify, does checkCast control what the backend emits? If so, how would it affect (for example) what the WAT backend generates for a checkCast vs non-checkCast` configuration?

No idea what you mean. Is this a WASM thing?

Yes, one example can be found in wasm/ControlFlow.mls (with the :fixme directive). The generated optimized IR has this shape:

define sccP_sccQ as fun sccP_sccQ⁰(id: Int⁰, param0: ?): Int⁰ {
  loop loopLabel:
    match id
      0 =>
        set id = 1;
        continue loopLabel
      1 =>
        let scrut: ?, tmp: ?, tmp1: Int⁰;
        set scrut = wasm⁰.le_impl﹖(param0, 0);
        match scrut
          true =>
            return (99 as Int⁰)
          else
            set tmp = wasm⁰.minus_impl﹖(param0, 1);
            set tmp1 = (tmp as Int⁰);
            set param0 = tmp1;
            set id = 0;
            continue loopLabel
        end
      else
        end
    end
  end
};

Note that while the function is typed to return Int, all return paths are via explicit returns in the loop body. The Wasm backend currently naively translates this to WAT, and since the function is declared to return Int (i.e. i31ref) but the body doesn't actually leave anything on the Wasm program stack, the module fails to validate.

The "unreachable type propagation" I was referring to will allow Wasm instructions and control flow structures to be unreachable-typed, so that the backend can add unreachable instructions to satisfy Wasm's requirements.

Just check who uses this valueAnalysis thing where the cast is dropped (or do you mean somewhere else?). There's no reason to assume that the cast is no longer needed after the value is propagated. You can see that, right?

Right, I see. I can fix this first by copy-propagating the entire Cast to its use-sites, but I suspect there will be other Block{Simplifier,Transformer} that also needs to be taught to handle Casts. In fact, the bigger question is whether this kind of propagation even makes sense if we preserve the Cast - Since we will essentially be inlining the cast to wherever the value is used, it means that an additional cast op will be done at each use site.

There was another idea that I was considering - Adding an erasedType field to Value.Lit (which defaults to N), and populating its type in a new or existing BlockTransformer if it has a type annotation (e.g. let v: Int32; set v = (1 as Int32) is transformed into let v: Int32; set v = 1i32, borrowing Rust's syntax). That way, the Lit stays as such in the IR but with the additional type information, and any downstream simplification/transformations can still operate on Lits as they do without having to handle the additional casts, and the casts do not leak into the backend either. Moreover, it makes lowering literals in the Wasm backend simpler, since we can inspect its type and emit the correct instruction rather than relying the on parent Cast node.

Let me know what you think about this.

[LPTK]

Just to clarify, does checkCast control what the backend emits? If so, how would it affect (for example) what the WAT backend generates for a checkCast vs non-checkCast` configuration?

WASM has to have explicit casts, so they will always be "checked" anyway. But perhaps when checkCast is on, we can insert manual checks that produce a better error message that's consistent with the JS version of the check. This is not very important or critical for now, though.

The easiest approach is probably to just have a backend-generic pass that adds these manual checks to the IR when checkCast is on (but ofc only for Casts that have their check flag as true).

The "unreachable type propagation" I was referring to will allow Wasm instructions and control flow structures to be unreachable-typed, so that the backend can add unreachable instructions to satisfy Wasm's requirements.

What is meant by "propagation", here? I'm worried to you start reintroducing some crazy type-inference-like process.

Maybe the simpler approach would be for Lowering to insert Unreachable nodes whenever a unit value is found but something else is expected. (The type system will catch mistakes separately.)

In fact, the bigger question is whether this kind of propagation even makes sense if we preserve the Cast - Since we will essentially be inlining the cast to wherever the value is used, it means that an additional cast op will be done at each use site.

Yeah, I don't think it makes much sense. Let's just (1) not propagated casted values; and (2) later implement an IR pass that removes unnecessary casts. That should be enough.

Of course Value.Lit should have the correct erased type! But why would you need a field for that? You should just have one literal case per literal type (such as Int, Int32, etc.).