You signed in with another tab or window. Reload to refresh your session.You signed out in another tab or window. Reload to refresh your session.You switched accounts on another tab or window. Reload to refresh your session.Dismiss alert
{{ message }}
Repository navigation
Add a lenient type-check entry point and the L4/L5 scoreboards #82
Part of #74 (Phase 1). Without a lenient type-check entry point, L4/L5 cannot be scored the way L2/L3 are.
Do
Add psrs_driver::check_program_types_lenient, alongside check_program_lenient (crates/psrs-driver/src/program/lenient.rs:7) and check_program_kinds_lenient (:15): resolve leniently, then type-check every module that resolved, tolerating the ones that did not.
Then add l4_type_scoreboard_with_annotations and l5_class_scoreboard_with_annotations to crates/psrs-driver/tests/suite.rs, following the existing pattern exactly — read @shouldFailWith, skip FFI-excluded and ErrorParsingModule files, skip files whose annotation mixes in codes outside the milestone's set, count per-code agreement, and print mismatches.
Both must run against the vendored corpus with no purs and no PURESCRIPT_REPO.
Acceptance
PSRS_ORACLE=annotations cargo test -p psrs-driver --test suite -- --ignored --nocapture reports L4 and L5 per-code agreement, and docs/design/D-04-suite-roadmap.md gate rows L4 and L5 carry those numbers instead of "not measured".
Landed in #110, together with #81's errorCode mappings — the two are one change, because a board with no mapped codes measures a compiler that cannot emit any, and a mapping with no board reports nothing.
check_program_types_lenient resolves leniently, then kind-checks and type checks every module that resolved. A module is type checked only if it desugars and kind checks, so a type error is never attributed to a module that failed an earlier stage. It shares resolve_partial with check_program_kinds_lenient instead of duplicating the resolution.
l4_l5_scoreboard_with_annotations measures both gates in one pass, following the existing pattern: read @shouldFailWith, skip FFI-excluded and ErrorParsingModule files, measure a case only when every code it declares belongs to the milestone's set, count per-code agreement, print mismatches. Both run against the vendored corpus with no purs and no PURESCRIPT_REPO.
One addition to the pattern: a case blocked before the type checker is counted as blocked with its reason, not as a disagreement. Without that, a missing library module reads as a type-checker regression, which is exactly the misreading the D-04 gate rows must not invite.
L5 37/74 — OverlappingInstances 8/8, NoInstanceFound 28/36, MissingClassMember 1/2, and 0 for the eight codes that need a check we do not have.
D-04's L4 and L5 rows now carry those numbers instead of "not measured". The decomposition is what is worth reading: 16 of 26 M4 mismatches and 26 of 37 M5 mismatches stop on a library module, so most of what is left in these gates is Phase 3's to unblock, not the type checker's. The rest is #97 (11 cases where we accept a program purs rejects) and #99 (6 Coercible cases where role checking rejects an instance before unification sees it, plus 4 cases with no diagnostic).
Evidence: cargo fmt --all --check; cargo clippy --workspace --all-targets -- -D warnings; PSRS_REQUIRE_WASMTIME=1 cargo test --workspace (987 passed, 0 failed, 0 skipped); CI green on #110.
Activity
biuld commentedon Oct 2, 2026
Landed in #110, together with #81's errorCode mappings — the two are one change, because a board with no mapped codes measures a compiler that cannot emit any, and a mapping with no board reports nothing.
check_program_types_lenientresolves leniently, then kind-checks and type checks every module that resolved. A module is type checked only if it desugars and kind checks, so a type error is never attributed to a module that failed an earlier stage. It sharesresolve_partialwithcheck_program_kinds_lenientinstead of duplicating the resolution.l4_l5_scoreboard_with_annotationsmeasures both gates in one pass, following the existing pattern: read@shouldFailWith, skip FFI-excluded andErrorParsingModulefiles, measure a case only when every code it declares belongs to the milestone's set, count per-code agreement, print mismatches. Both run against the vendored corpus with nopursand noPURESCRIPT_REPO.One addition to the pattern: a case blocked before the type checker is counted as blocked with its reason, not as a disagreement. Without that, a missing library module reads as a type-checker regression, which is exactly the misreading the D-04 gate rows must not invite.
Measured
L4 12/38 —
IntOutOfRange1/1,InfiniteType1/1,TypesDoNotUnify10/32,EscapedSkolem0/2,ExpectedType0/1,AmbiguousTypeVariables0/1.L5 37/74 —
OverlappingInstances8/8,NoInstanceFound28/36,MissingClassMember1/2, and 0 for the eight codes that need a check we do not have.D-04's L4 and L5 rows now carry those numbers instead of "not measured". The decomposition is what is worth reading: 16 of 26 M4 mismatches and 26 of 37 M5 mismatches stop on a library module, so most of what is left in these gates is Phase 3's to unblock, not the type checker's. The rest is #97 (11 cases where we accept a program
pursrejects) and #99 (6Coerciblecases where role checking rejects an instance before unification sees it, plus 4 cases with no diagnostic).Evidence:
cargo fmt --all --check;cargo clippy --workspace --all-targets -- -D warnings;PSRS_REQUIRE_WASMTIME=1 cargo test --workspace(987 passed, 0 failed, 0 skipped); CI green on #110.feat(typecheck): map the official errorCodes and add a lenient type c…