Lower the expression ascription e :: T #84

Activity

1. biuld

   added

   enhancementNew feature or requestNew feature or request

   on Oct 1, 2026
2. biuld

   added a parent issue on Oct 1, 2026

   • Phase 2: close frontend surface-lowering coverage #75
3. biuld

   marked this as blocked on Oct 1, 2026

   • Add a compile-and-run runtime scoreboard for the passing suite #93
4. biuld

   unmarked this as blocked on Oct 1, 2026

   • Add a compile-and-run runtime scoreboard for the passing suite #93
5. biuld

   added this to the Phase 2 — Frontend surface lowering milestone on Oct 1, 2026
6. biuld

   added

   gate:L2Blocks module, import, export and name resolution (D-04 L2)Blocks module, import, export and name resolution (D-04 L2)

   area:frontendFrontend: syntax, resolution, kinds, types, classesFrontend: syntax, resolution, kinds, types, classes

   on Oct 1, 2026
7. biuld

   marked this as blocking on Oct 1, 2026

   • Prelude surface: classes, instances, and the value functions #94
8. biuld commented on Oct 2, 2026

   

   biuld

   on Oct 2, 2026

   OwnerAuthor

   More actions

   Landed in #111. The ascription is checked against its written type and leaves no node behind.

   The design

   An ascription is a type-directed check at a known expression, not a coercion, so it elaborates on the spine instead of becoming a wrapper. AST and HIR carry Typed { expression, ty }; the checker elaborates the written type the way it elaborates a signature, checks the expression against it, and returns the expression carrying that type. Typed Core has no Typed node, there is no runtime representation, and there is no side table. The ascription is erased by type checking, which is the only correct answer because e :: T has no runtime effect.

   A written forall is checked with skolems and becomes the result type, so f = (\_ -> 0) :: forall b. b -> Int needs no signature.

   Measured: 28 passing files recovered

   P2 surface lowering drops from 134 to 106 in both the L2 and L6 boards.

   The missing-module count rises from 216 to 244 for the same reason — those files now reach resolution and stop on Effect.Console. Both numbers are recorded together in D-04, because either alone would be misleading: it looks like the library blocker got worse when the frontend blocker got better by more.

   Two more failing cases now reach the type checker, so the denominators moved with the numerators:

   Gate	Before	After
   M4 types	12/38	12/40
   M5 classes	37/74	41/81

   Scope not covered, and why

   A free type variable in an ascription does not work yet — passing/2941.purs alone, in the chain ((\_ -> 0) :: b -> Int) :: forall b. b -> Int. purs resolves the inner b against the outer forall b, which needs the enclosing signature's variables in scope while the body is checked. I tried sharing them and produced a second set of variables that could not unify, so the work stays open with #87 (type wildcards) rather than landing a wrong rule.

   The bare form (e :: T), the unparenthesized e :: T, and a written forall all work.

   Type wildcards did not land

   The issue says wildcards _ land with or immediately after this, since they appear in the same position. They did not: a wildcard is a fresh type variable at a known position, and the resolution above — which purs also applies to wildcards — is the same missing piece. Leaving it to #87 keeps one rule in one place instead of two partial ones.

   Evidence: cargo fmt --all --check; cargo clippy --workspace --all-targets -- -D warnings; PSRS_REQUIRE_WASMTIME=1 cargo test --workspace (992 passed, 0 failed, 0 skipped); CI green on #111.
9. biuld

   closed this as completedon Oct 2, 2026
10. biuld

    added a commit that references this issue on Oct 6, 2026

    feat(frontend): check the expression ascription against its written type

    ...

    29720d2